Lᵖ functions on a locally compact space

Let μ be a regular measure on a weakly locally compact R₁ space X with its Borel σ-algebra, for instance a Haar measure on a locally compact group. This file proves that compactly supported continuous functions are dense in Lᵖ(X, μ) for p < ∞.

Mathlib's MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le assumes NormalSpace X in addition to R1Space X and WeaklyLocallyCompactSpace X, and Mathlib provides no NormalSpace instance for locally compact groups. Here normality is not needed: the indicator function of a measurable set t of finite measure is approximated directly. Choose a compact closed K ⊆ t and an open U ⊇ t with μ (U \ K) small, and apply Urysohn's lemma for the compact set K inside the open set U, which holds in every locally compact regular space. Mathlib's MeasureTheory.MemLp.induction_dense extends the approximation from indicator functions to all of Lᵖ.

Main results

• MeasureTheory.exists_hasCompactSupport_eLpNorm_sub_indicator_le: a constant multiple of the indicator function of a measurable set of finite measure is approximated in Lᵖ by compactly supported continuous functions.
• MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le_of_locallyCompactSpace: every Lᵖ function, p < ∞, is approximated in Lᵖ by compactly supported continuous functions.
• MeasureTheory.Lp.dense_setOf_continuous_hasCompactSupport: the classes of compactly supported continuous functions are dense in Lᵖ, p < ∞.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw–Hill (1987), Theorem 3.14.

theorem MeasureTheory.exists_hasCompactSupport_eLpNorm_sub_indicator_le {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {p : ENNReal} [BorelSpace X] [μ.Regular] (hp : p ≠ ⊤) (c : E) {t : Set X} (ht : MeasurableSet t) (htμ : μ t < ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (g : X → E), eLpNorm (g - t.indicator fun (x : X) => c) p μ ≤ ε ∧ Continuous g ∧ HasCompactSupport g

In a weakly locally compact R₁ space, the indicator function of a measurable set of finite measure with constant value c is approximated in Lᵖ, p < ∞, by compactly supported continuous functions.

theorem MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le_of_locallyCompactSpace {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {p : ENNReal} [BorelSpace X] [μ.Regular] (hp : p ≠ ⊤) {f : X → E} (hf : MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (g : X → E), HasCompactSupport g ∧ eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ

Density of compactly supported continuous functions in Lᵖ for a regular measure on a weakly locally compact R₁ space, p < ∞. Unlike MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le, no normality of the space is assumed.

theorem MeasureTheory.Lp.dense_setOf_continuous_hasCompactSupport {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {p : ENNReal} [BorelSpace X] [μ.Regular] [Fact (1 ≤ p)] (hp : p ≠ ⊤) : Dense {u : ↥(Lp E p μ) | ∃ (f : X → E), Continuous f ∧ HasCompactSupport f ∧ ↑↑u =ᵐ[μ] f}

Density of compactly supported continuous functions in Lᵖ for a regular measure on a weakly locally compact R₁ space, p < ∞: the classes of compactly supported continuous functions are dense in Lp E p μ.