Dense range of the constructed Hilbert factor

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.factor_range_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$ .

Suppose $\sigma\in\mathcal C$ , $L^2(\sigma)$ is infinite dimensional, and fix an isometric isomorphism $W:L^2(\sigma)\to L^2(dx)$ . Assume that, for every compact $K\subset\mathbb R^n$ , the complex linear span of $u\mapsto e^{it\cdot u}$ , $t\in\mathbb R^n$ , is dense in $L^2(K,\sigma)$ . Define $Q\psi=W[\widehat\psi]_\sigma$ . Then

\overline{Q(\mathcal S)}^{\,L^2(dx)}=L^2(dx).

The source's extra local-totality assumption is retained even though Schwartz density and Fourier inversion also imply this conclusion.

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

/-- Theorem 3.7, PDF p.11: dense range of the constructed factor, retaining
local totality of the exponential span and the fixed unitary W from (3.7). -/
theorem factor_range_dense (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) (hinfinite : ¬ FiniteDimensional ℂ (L2 σ))
    (W : L2 σ ≃ₗᵢ[ℂ] L2 (volume : Measure (SpectralDomain n)))
    (htotal : LocallyTotalExponentials σ) :
    DenseRange (factorFromW W) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 11, Theorem 3.7: density of the factor range

Read-back

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

For every positive integer $n$ , put $X=\mathbb R^{\operatorname{Fin}n}$ with its Euclidean structure, and let $\mathcal S_{\mathbb C}(X)$ be the space of complex-valued Schwartz functions on $X$ . Let $\sigma$ be a regular measure on $X$ such that, for some natural number $p$ , including possibly $p=0$ ,

\int_X (1+\|u\|^2)^{-p}\,d\sigma(u)<\infty.

Assume that $L^2(\sigma;\mathbb C)$ is not finite-dimensional over $\mathbb C$ , and let $W:L^2(\sigma;\mathbb C)\to L^2(X,du;\mathbb C)$ be a surjective complex-linear isometry, where $du$ is Euclidean volume. For any measure $\nu$ and complex-valued function $g$ , write $[g]_\nu$ for its $L^2(\nu)$ class when $g$ belongs to $L^2(\nu)$ , and for the zero vector otherwise. Assume that for every compact set $K\subseteq X$ , including the empty set, the complex-linear span of

\left\{\left[u\mapsto e^{i\langle t,u\rangle}\right]_{\sigma|_K}:t\in X\right\}

is dense in $L^2(\sigma|_K;\mathbb C)$ . Define $\widehat\psi(u)=\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx$ . Then the set

\left\{W([\widehat\psi]_\sigma):\psi\in\mathcal S_{\mathbb C}(X)\right\}

is dense in $L^2(X,du;\mathbb C)$ .

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