Theorems · Theorem · measure theory

MeasureTheory.tendsto_of_integral_tendsto_of_monotone

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    MeasureTheory.Integrable F μ →
      Filter.Tendsto (fun i => ∫ (a : α), f i a ∂μ) Filter.atTop (nhds (∫ (a : α), F a ∂μ)) →
        (∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) →
          (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i 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.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

3 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound