@[reducible, inline]

noncomputable abbrev Integration.lebesgueIntegralNonneg {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (f : X → ENNReal) (E : Set X) : ENNReal

The Lebesgue integral of a nonnegative ℝ≥0∞-valued function over a set E with respect to a measure μ.

def LebesgueIntegration.integrableOnEReal {X : Type u_1} [MeasurableSpace X] (f : X → EReal) (E : Set X) (μ : MeasureTheory.Measure X := by volume_tac) : Prop

Integrability on E for an EReal-valued function: both the positive and the negative parts have finite Lebesgue integral over E.

@[reducible, inline]

abbrev LebesgueIntegration.integrableOn {X : Type u_1} [MeasurableSpace X] (f : X → ℝ) (E : Set X) (μ : MeasureTheory.Measure X := by volume_tac) : Prop

Integrability on E for a real-valued function, defined via Mathlib's IntegrableOn (Melrose Def 4.1).

@[reducible, inline]

noncomputable abbrev LebesgueIntegration.signedIntegral {X : Type u_1} [MeasurableSpace X] (f : X → ℝ) (E : Set X) (μ : MeasureTheory.Measure X := by volume_tac) : ℝ

The signed Lebesgue integral of a real-valued function over E with respect to μ (Melrose Def 4.4).

@[reducible, inline]

abbrev NormedSpaces.IsBanachSpace (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (V : Type u_2) [NormedAddCommGroup V] [NormedSpace 𝕜 V] : Prop

A 𝕜-normed space V is a Banach space iff it is complete.

theorem NormedSpaces.Lp_isBanachSpace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {p : ENNReal} [Fact (1 ≤ p)] : IsBanachSpace ℝ ↥(MeasureTheory.Lp E p μ)

For 1 ≤ p ≤ ∞, the space L^p(μ; E) valued in a Banach space E is itself a Banach space.

theorem NormedSpaces.minkowski_inequality_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] {p : ENNReal} (hp_one : 1 < p) {f g : α → E} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ) : MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ

Minkowski's inequality in L^p for 1 < p ≤ ∞: the L^p-seminorm satisfies the triangle inequality.

theorem Integration.lintegral_eq_zero_iff_measure_pos_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) {E : Set α} (hE : MeasurableSet E) : ∫⁻ (x : α) in E, f x ∂μ = 0 ↔ μ {x : α | x ∈ E ∧ 0 < f x} = 0

Vanishing of the Lebesgue integral over E is equivalent to the set {x ∈ E | f x > 0} having measure zero.

theorem Integration.rpow_mul_rpow_le_add (a b γ : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ₀ : 0 < γ) (hγ₁ : γ < 1) : a ^ γ * b ^ (1 - γ) ≤ γ * a + (1 - γ) * b

Two-term weighted AM-GM inequality: a^γ b^{1-γ} ≤ γ a + (1-γ) b for nonnegative reals and γ ∈ (0, 1).

theorem Integration.rpow_mul_rpow_lt_add (a b γ : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ₀ : 0 < γ) (hγ₁ : γ < 1) (hab : a ≠ b) : a ^ γ * b ^ (1 - γ) < γ * a + (1 - γ) * b

Strict weighted AM-GM: if a ≠ b, the inequality a^γ b^{1-γ} ≤ γ a + (1-γ) b is strict.

theorem Integration.rpow_mul_rpow_eq_add_iff (a b γ : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ₀ : 0 < γ) (hγ₁ : γ < 1) : a ^ γ * b ^ (1 - γ) = γ * a + (1 - γ) * b ↔ a = b

Equality case in the weighted AM-GM inequality: a^γ b^{1-γ} = γ a + (1-γ) b iff a = b.

theorem Integration.rpow_mul_rpow_le_add_and_eq_iff {a b γ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ₁ : 0 < γ) (hγ₂ : γ < 1) : a ^ γ * b ^ (1 - γ) ≤ γ * a + (1 - γ) * b ∧ (a ^ γ * b ^ (1 - γ) = γ * a + (1 - γ) * b ↔ a = b)

Combined weighted AM-GM: the inequality together with the equality characterisation.

theorem Integration.holder_inequality {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) μ) : |∫ (a : α), f a * g a ∂μ| ≤ (∫ (a : α), |f a| ^ p ∂μ) ^ (1 / p) * (∫ (a : α), |g a| ^ q ∂μ) ^ (1 / q)

Hölder's inequality for conjugate exponents p, q: the integral of f * g is bounded by the product of the L^p and L^q norms.

theorem Integration.fatou_lemma {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) : ∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

Fatou's lemma: for a sequence of nonnegative measurable functions, the integral of the lower limit is at most the lower limit of the integrals.

theorem MonotoneConvergence.monotone_convergence_measurable {α : Type u_1} [MeasurableSpace α] {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) : Measurable fun (x : α) => ⨆ (n : ℕ), f n x

The pointwise supremum of a countable family of measurable functions is measurable.

theorem MonotoneConvergence.monotone_convergence_iSup {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) {E : Set α} : ∫⁻ (x : α) in E, ⨆ (n : ℕ), f n x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α) in E, f n x ∂μ

Monotone convergence (supremum form): the integral commutes with the pointwise supremum for a monotone sequence of measurable functions.

theorem MonotoneConvergence.monotone_convergence_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) {E : Set α} : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α) in E, f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α) in E, ⨆ (n : ℕ), f n x ∂μ))

Monotone convergence (limit form): the integrals of a monotone sequence converge to the integral of the limit.