Density of smooth compactly supported functions in Lp

In this file, we prove that Lp functions can be approximated by smooth compactly supported functions for p < ∞.

This result is recorded in MeasureTheory.MemLp.exist_sub_eLpNorm_le.

theorem HasCompactSupport.exist_eLpNorm_sub_le_of_continuous {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] (μ : MeasureTheory.Measure E := by volume_tac) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal} {ε : ℝ} (hε : 0 < ε) {f : E → F} (h₁ : HasCompactSupport f) (h₂ : Continuous f) : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

For every continuous compactly supported function f there exists a smooth compactly supported function g such that f - g is arbitrary small in the Lp-norm for p < ∞.

theorem MeasureTheory.MemLp.exist_eLpNorm_sub_le {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] {μ : Measure E} [IsFiniteMeasureOnCompacts μ] {p : ENNReal} (hp : p ≠ ⊤) (hp₂ : 1 ≤ p) {f : E → F} (hf : MemLp f p μ) {ε : ℝ} (hε : 0 < ε) : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Every Lp function can be approximated by a smooth compactly supported function provided that p < ∞.

theorem MeasureTheory.Lp.dense_hasCompactSupport_contDiff {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] {μ : Measure E} [IsFiniteMeasureOnCompacts μ] {p : ENNReal} (hp : p ≠ ⊤) [hp₂ : Fact (1 ≤ p)] : Dense {f : ↥(Lp F p μ) | ∃ (g : E → F), ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g}