theorem SchwartzDensity.schwartz_dense_Lp (n : ℕ) {p : ENNReal} (hp : p ≠ ⊤) [Fact (1 ≤ p)] : DenseRange ⇑(SchwartzMap.toLpCLM ℝ ℂ p MeasureTheory.volume)

Density of Schwartz functions in L^p: for 1 ≤ p < ∞, the canonical continuous linear inclusion SchwartzMap.toLpCLM of 𝓢(ℝⁿ, ℂ) into Lᵖ(ℝⁿ, ℂ) has dense range.