Theorems · Theorem · measure theory

TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn

∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E}
  [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ᶠ (i : ι) in l, ContinuousOn (F i) (Set.uIcc a b)) →
    TendstoUniformlyOn F f l (Set.uIcc a b) →
      Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFilter.IsCountablyGeneratedMeasureTheory.IsLocallyFiniteMeasure