Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm

∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E},
  p ≠ ⊤ →
    ∀ {μ : MeasureTheory.Measure β} (fmeas : Measurable f)
      [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})],
      MeasureTheory.eLpNorm f p μ < ⊤ →
        Filter.Tendsto
          (fun n =>
            MeasureTheory.eLpNorm (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ)
          Filter.atTop (nhds 0)

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceNormedAddCommGroupBorelSpaceTopologicalSpace.SeparableSpace