Theorems · Theorem · measure theory

MeasureTheory.limsup_lintegral_le

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

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpace