$\mathcal{S}(\mathbb{R}^n)$ is dense in $L^p(\mathbb{R}^n)$ , $1\le p<\infty$

Proved

SchwartzSpaceWiki.dense_in_Lp

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisschwartz-space

Let $1\le p<\infty$ . Then $\mathcal{S}(\mathbb{R}^n)\subseteq L^p(\mathbb{R}^n)$ (every Schwartz function is $p$ -integrable for Lebesgue measure), and $\mathcal{S}(\mathbb{R}^n)$ is dense in $L^p(\mathbb{R}^n)$ : for every $g\in L^p(\mathbb{R}^n)$ and every $\varepsilon>0$ there is $f\in\mathcal{S}(\mathbb{R}^n)$ with $\|g-f\|_{L^p}<\varepsilon$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem dense_in_Lp (n : ℕ) (p : ENNReal) (hp1 : 1 ≤ p) (hptop : p ≠ ⊤) :
    (∀ f ∈ schwartzSpace n, MemLp f p (volume : Measure (Rn n))) ∧
    (∀ g : Rn n → ℂ, MemLp g p (volume : Measure (Rn n)) →
      ∀ ε : ENNReal, 0 < ε →
        ∃ f ∈ schwartzSpace n, eLpNorm (g - f) p (volume : Measure (Rn n)) < ε) := by sorry

end SchwartzSpaceWiki

Source

Wikipedia, "Schwartz space", revision oldid=1360762580 (https://en.wikipedia.org/w/index.php?title=Schwartz_space&oldid=1360762580), section "Relation of Schwartz spaces with other topological vector spaces", 1st bullet

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

S(Rn)\mathcal{S}(\mathbb{R}^n)S(Rn) is dense in Lp(Rn)L^p(\mathbb{R}^n)Lp(Rn), 1≤p<∞1\le p<\infty1≤p<∞

$\mathcal{S}(\mathbb{R}^n)$ is dense in $L^p(\mathbb{R}^n)$ , $1\le p<\infty$