Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm

∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} {μ : MeasureTheory.Measure β}
  [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    Filter.Tendsto
      (fun n => ∫⁻ (x : β), ‖(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ)
      Filter.atTop (nhds 0)

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceNormedAddCommGroupOpensMeasurableSpaceTopologicalSpace.SeparableSpace