Theorems · Theorem · measure theory

MeasureTheory.lintegral_enorm_le_liminf_of_tendsto

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

If G n tends to f a.e. and each ‖G n ·‖ₑ is AEMeasurable, then the lower Lebesgue integral of ‖f ·‖ₑ is at most the liminf of the lower Lebesgue integral of ‖G n ·‖ₑ.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

2 results in Mathlib

Foundations

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