Schwartz functions are dense in spectral L2

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.schwartz_dense

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $n\ge1$ , let $\mathcal S=\mathcal S(\mathbb R^n;\mathbb C)$ have its full Schwartz Fréchet topology, and write $\widehat\psi(u)=\int_{\mathbb R^n}e^{-iu\cdot x}\psi(x)\,dx$ . Let $\mathcal C$ consist of the regular positive Borel measures $\sigma$ for which $\int(1+|u|^2)^{-p}\,d\sigma(u)<\infty$ for some nonnegative integer $p$ .

For every $\sigma\in\mathcal C$ , all $\psi\in\mathcal S$ belong to $L^2(\sigma)$ , and their direct images, without Fourier transformation, are dense:

\overline{\{[\psi]_\sigma:\psi\in\mathcal S\}}^{\,L^2(\sigma)}=L^2(\sigma).

This density statement includes zero measures and finitely supported measures; it requires no infinite-dimensional hypothesis.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P38

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P38

open MeasureTheory Filter

open scoped Topology ComplexConjugate ENNReal

/-- Lemma 3.5, PDF p.10: density of direct Schwartz inclusion, not its Fourier
transform. No infinite-dimensional assumption; zero and atomic measures are included. -/
theorem schwartz_dense (n : ℕ) (hn : 0 < n) (σ : Measure (SpectralDomain n)) (hσ : InC σ) :
    (∀ ψ : ComplexTest n, MemLp (fun x => ψ x) 2 σ) ∧
    DenseRange (fun ψ : ComplexTest n => l2Class σ ψ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 10, Lemma 3.5: Schwartz density

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $n>0$ and every regular measure $\sigma$ on $\mathbb R^n$ such that $\int(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly $0$ , every complex-valued Schwartz function $\psi$ is almost everywhere strongly measurable with respect to $\sigma$ and has finite $L^2(\sigma)$ seminorm, and the map sending $\psi$ to its equivalence class in $L^2(\sigma;\mathbb C)$ has dense range. The defined map assigns the usual $L^2$ class when these membership conditions hold and assigns the zero element otherwise; the first asserted condition ensures that the usual class is used for every Schwartz function here. Density means that every element of $L^2(\sigma;\mathbb C)$ can be approximated arbitrarily closely in $L^2$ norm by such classes.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph