$\mathcal{S}(\mathbb{R}^n)$ is a complex vector space

Proved

SchwartzSpaceWiki.schwartzSpace_isSubspace

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

fourier-analysisschwartz-space

The Schwartz space $\mathcal{S}(\mathbb{R}^n,\mathbb{C})$ is a complex linear subspace of $C^\infty(\mathbb{R}^n,\mathbb{C})$ : it contains the zero function, and for all $f,g\in\mathcal{S}(\mathbb{R}^n)$ and $c\in\mathbb{C}$ we have $f+g\in\mathcal{S}(\mathbb{R}^n)$ and $cf\in\mathcal{S}(\mathbb{R}^n)$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem schwartzSpace_isSubspace (n : ℕ) :
    (0 : Rn n → ℂ) ∈ schwartzSpace n ∧
    (∀ f ∈ schwartzSpace n, ∀ g ∈ schwartzSpace n, f + g ∈ schwartzSpace n) ∧
    (∀ (c : ℂ), ∀ f ∈ schwartzSpace n, c • 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 "Definition" ("is a subspace of C^∞") and section "Examples", 3rd bullet ("Because the Schwartz space is a vector space")

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 a complex vector space

$\mathcal{S}(\mathbb{R}^n)$ is a complex vector space