$P(x)e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)$ and polynomials embed

Proved

SchwartzSpaceWiki.polynomial_mul_gaussian_mem

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

fourier-analysisschwartz-space

Fix a real number $a>0$ . For every polynomial $P\in\mathbb{C}[x_1,\dots,x_n]$ , the function $x\mapsto P(x)\,e^{-a|x|^2}$ belongs to $\mathcal{S}(\mathbb{R}^n)$ . Moreover, the map $P\mapsto P(x)e^{-a|x|^2}$ from polynomials to functions is injective, so it embeds the polynomials into $\mathcal{S}(\mathbb{R}^n)$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem polynomial_mul_gaussian_mem (n : ℕ) (a : ℝ) (ha : 0 < a) :
    (∀ P : MvPolynomial (Fin n) ℂ,
      (fun x : Rn n => MvPolynomial.eval (fun i => (x i : ℂ)) P *
        Complex.exp (-(a * ‖x‖ ^ 2 : ℝ))) ∈ schwartzSpace n) ∧
    Function.Injective (fun (P : MvPolynomial (Fin n) ℂ) (x : Rn n) =>
      MvPolynomial.eval (fun i => (x i : ℂ)) P * Complex.exp (-(a * ‖x‖ ^ 2 : ℝ))) := 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", 3rd 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

P(x)e−a∣x∣2∈S(Rn)P(x)e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)P(x)e−a∣x∣2∈S(Rn) and polynomials embed

$P(x)e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)$ and polynomials embed