Theorems · Theorem · measure theory

MeasureTheory.tendsto_lintegral_of_dominated_convergence

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

Dominated convergence theorem for nonnegative Measurable functions.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpace