Theorems · Theorem · measure theory

MeasureTheory.MemLp.exists_hasCompactSupport_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] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ},
  0 < p →
    ∀ {f : α → E},
      MeasureTheory.MemLp f (ENNReal.ofReal p) μ →
        ∀ {ε : ℝ},
          0 < ε →
            ∃ g,
              HasCompactSupport g ∧
                ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g (ENNReal.ofReal p) μ

In a locally compact space, any function in ℒp can be approximated by compactly supported 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

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceR1SpaceWeaklyLocallyCompactSpaceMeasureTheory.Measure.Regular