Theorems · Theorem · measure theory

MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset

∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [CompleteSpace E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {f : α → E}
  (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    ∀ (s : Set E) [inst_5 : TopologicalSpace.SeparableSpace ↑s] (hs : Set.range f ∪ {0} ⊆ s),
      Filter.Tendsto (fun n => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n))
        Filter.atTop (nhds (∫ (x : α), f x ∂μ))

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpaceBorelSpaceTopologicalSpace.SeparableSpace