$x^\alpha e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)$

Proved

SchwartzSpaceWiki.monomial_mul_gaussian_mem

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

fourier-analysisschwartz-space

For every multi-index $\alpha\in\mathbb{N}^n$ and every real number $a>0$ , the function $x\mapsto x^\alpha e^{-a|x|^2}$ belongs to $\mathcal{S}(\mathbb{R}^n)$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem monomial_mul_gaussian_mem (n : ℕ) (α : MultiIndex n) (a : ℝ) (ha : 0 < a) :
    (fun x : Rn n => (monomial α x : ℂ) * Complex.exp (-(a * ‖x‖ ^ 2 : ℝ))) ∈
      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", 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

xαe−a∣x∣2∈S(Rn)x^\alpha e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)xαe−a∣x∣2∈S(Rn)

$x^\alpha e^{-a|x|^2}\in\mathcal{S}(\mathbb{R}^n)$