Dominated convergence theorem

Lebesgue's dominated convergence theorem states that the limit and Lebesgue integral of a sequence of (almost everywhere) measurable functions can be swapped if the functions are pointwise dominated by a fixed function. This file provides a few variants of the result.

theorem MeasureTheory.limsup_lintegral_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} (g : α → ENNReal) (hf_meas : ∀ (n : ℕ), Measurable (f n)) (h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g) (h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) : Filter.limsup (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤ ∫⁻ (a : α), Filter.limsup (fun (n : ℕ) => f n a) Filter.atTop ∂μ

theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), Measurable (F n)) (h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for nonnegative Measurable functions.

theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ) (h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for nonnegative AEMeasurable functions.

theorem MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {ι : Type u_2} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => F n a) l (nhds (f a))) : Filter.Tendsto (fun (n : ι) => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for filters with a countable basis.

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound. Auxiliary version assuming moreover that the functions in the sequence are ae measurable.

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : Measure α} (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound.

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_antitone {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If an antitone sequence of functions has a lower bound and the sequence of integrals of these functions tends to the integral of the lower bound, then the sequence of functions converges almost everywhere to the lower bound.