Monotone convergence theorem and addition of Lebesgue integrals

The monotone convergence theorem (aka Beppo Levi lemma) states that the Lebesgue integral and supremum can be swapped for a pointwise monotone sequence of functions. This file first proves several variants of this theorem, then uses it to show that the Lebesgue integral is additive (assuming one of the functions is at least AEMeasurable) and respects multiplication by a constant.

theorem MeasureTheory.lintegral_iSup {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem, version with Measurable functions.

theorem MeasureTheory.lintegral_iSup' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem, version with AEMeasurable functions.

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))

Monotone convergence theorem expressed with limits.

theorem MeasureTheory.lintegral_iSup_ae {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Weaker version of the monotone convergence theorem.

theorem MeasureTheory.lintegral_iSup_directed_of_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (b : β), Measurable (f b)) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≤ x2) f) : ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence theorem for a supremum over a directed family and indexed by a countable type.

theorem MeasureTheory.lintegral_iSup_directed {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (b : β), AEMeasurable (f b) μ) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≤ x2) f) : ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence theorem for a supremum over a directed family and indexed by a countable type.

theorem MeasureTheory.lintegral_liminf_le' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), AEMeasurable (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, version with AEMeasurable functions.

theorem MeasureTheory.lintegral_liminf_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (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, version with Measurable functions.

theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (SimpleFunc.eapprox f n).lintegral μ

theorem MeasureTheory.lintegral_eapprox_le_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (n : ℕ) : (SimpleFunc.eapprox f n).lintegral μ ≤ ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.measure_support_eapprox_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf_meas : Measurable f) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (n : ℕ) : μ (Function.support ⇑(SimpleFunc.eapprox f n)) < ⊤

theorem MeasureTheory.le_lintegral_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f g : α → ENNReal) : ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ

The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral of their sum. The other inequality needs one of these functions to be (a.e.-)measurable.

theorem MeasureTheory.lintegral_add_aux {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

@[simp]

theorem MeasureTheory.lintegral_add_left {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (g : α → ENNReal) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that f is integrable, see also MeasureTheory.lintegral_add_right and primed versions of these lemmas.

theorem MeasureTheory.lintegral_add_left' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (g : α → ENNReal) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_add_right' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : α → ENNReal) {g : α → ENNReal} (hg : AEMeasurable g μ) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

@[simp]

theorem MeasureTheory.lintegral_add_right {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : α → ENNReal) {g : α → ENNReal} (hg : Measurable g) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that g is integrable, see also MeasureTheory.lintegral_add_left and primed versions of these lemmas.

theorem MeasureTheory.lintegral_finset_sum' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} (s : Finset β) {f : β → α → ENNReal} (hf : ∀ b ∈ s, AEMeasurable (f b) μ) : ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

theorem MeasureTheory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} (s : Finset β) {f : β → α → ENNReal} (hf : ∀ b ∈ s, Measurable (f b)) : ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

theorem MeasureTheory.lintegral_tsum {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (i : β), AEMeasurable (f i) μ) : ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ

@[simp]

theorem MeasureTheory.lintegral_const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_const_mul'' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_const_mul_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) (f : α → ENNReal) : r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ

theorem MeasureTheory.lintegral_const_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) (f : α → ENNReal) (hr : r ≠ ⊤) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_mul_const'' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_mul_const_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) (f : α → ENNReal) : (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ

theorem MeasureTheory.lintegral_mul_const' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (r : ENNReal) (f : α → ENNReal) (hr : r ≠ ⊤) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_lintegral_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_3} [MeasurableSpace β] {ν : Measure β} {f : α → ENNReal} {g : β → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

theorem MeasureTheory.lintegral_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_trim_ae {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : AEMeasurable f (μ.trim hm)) : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ