Theorems · Theorem · measure theory

MeasureTheory.integrable_of_tendsto

∀ {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  (∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (f x))) →
    (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) μ) →
      Filter.liminf (fun n => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop ≠ ⊤ → MeasureTheory.Integrable f μ

If G n tends to f a.e., each G n is AEStronglyMeasurable and the liminf of the lower Lebesgue integral of ‖G n ·‖ₑ is finite, then f is Lebesgue integrable.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

2 results in Mathlib

Foundations

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