$C_c^\infty(\mathbb{R}^n)\subseteq\mathcal{S}(\mathbb{R}^n)$

Proved

SchwartzSpaceWiki.contDiff_hasCompactSupport_mem

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

fourier-analysisschwartz-space

Every smooth function $f:\mathbb{R}^n\to\mathbb{C}$ with compact support belongs to $\mathcal{S}(\mathbb{R}^n)$ . Equivalently, the space $C_c^\infty(\mathbb{R}^n)$ of bump functions is contained in $\mathcal{S}(\mathbb{R}^n)$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem contDiff_hasCompactSupport_mem (n : ℕ) (f : Rn n → ℂ)
    (hf : ContDiff ℝ (⊤ : ℕ∞) f) (hsupp : HasCompactSupport f) :
    f ∈ schwartzSpace 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 "Examples of functions in the Schwartz space", 2nd bullet, and section "Relation of Schwartz spaces with other topological vector spaces", 2nd 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

Cc∞(Rn)⊆S(Rn)C_c^\infty(\mathbb{R}^n)\subseteq\mathcal{S}(\mathbb{R}^n)Cc∞​(Rn)⊆S(Rn)

$C_c^\infty(\mathbb{R}^n)\subseteq\mathcal{S}(\mathbb{R}^n)$