Theorems · Theorem · measure theory

MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le

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

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

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceMeasureTheory.Measure.WeaklyRegular