Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm

∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s],
  p ≠ ⊤ →
    ∀ {μ : MeasureTheory.Measure β},
      (∀ᵐ (x : β) ∂μ, f x ∈ closure s) →
        MeasureTheory.eLpNorm (fun x => f x - y₀) p μ < ⊤ →
          Filter.Tendsto (fun n => MeasureTheory.eLpNorm (⇑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) - f) p μ)
            Filter.atTop (nhds 0)

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceNormedAddCommGroupOpensMeasurableSpaceTopologicalSpace.SeparableSpace