Theorems · Theorem · measure theory

MeasureTheory.lintegral_liminf_le

• 1000+ list: Fatou–Lebesgue theorem

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal}
  {u : Filter ι} [u.IsCountablyGenerated],
  (∀ (i : ι), Measurable (f i)) →
    ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u

Fatou's lemma, version with Measurable functions.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Add

Cited by

3 results in Mathlib

Foundations

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

Assumes

Filter.IsCountablyGenerated