Theorems · Theorem · measure theory

MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le

∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.WeaklyRegular],
  p ≠ ⊤ →
    ∀ {f : α → E},
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) p μ

Any function in ℒp can be approximated by bounded continuous functions when p < ∞, version in terms of eLpNorm.

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceMeasureTheory.Measure.WeaklyRegular