Theorems · Theorem · measure theory

intervalIntegral.tendsto_integral_filter_of_dominated_convergence

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E} (bound : ℝ → ℝ),
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → ‖F n x‖ ≤ bound x) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) →
          Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))

Lebesgue dominated convergence theorem for filters with a countable basis

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFilter.IsCountablyGenerated