The separated spectral completion and the specified factor

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.spectral_completion_isometry

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 a complex Hilbert isometric isomorphism $W:L^2(\sigma)\to L^2(dx)$ . Let $H_\sigma$ be the separated completion of $\mathcal S$ for the seminorm $(\int|\widehat\psi|^2\,d\sigma)^{1/2}$ , concretely the closure of its Fourier image in $L^2(\sigma)$ . There exists an isometric isomorphism $E:H_\sigma\to L^2(dx)$ with

E[\psi]=W[\widehat\psi]_\sigma\qquad(\psi\in\mathcal S).

Thus the identification is the extension of the constructed $Q$ , rather than equality of types or an arbitrary Hilbert-space isomorphism.

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

/-- Corollary 3.6, PDF pp.10--11: the separated spectral completion is isometrically
onto L2(dx), by the specific extension of Q=W composed with Fourier inclusion. -/
theorem spectral_completion_isometry (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) (hinfinite : ¬ FiniteDimensional ℂ (L2 σ))
    (W : L2 σ ≃ₗᵢ[ℂ] L2 (volume : Measure (SpectralDomain n))) :
    (∀ ψ : ComplexTest n, MemLp (paperFourier ψ) 2 σ) ∧
    ∃ E : spectralCompletion σ ≃ₗᵢ[ℂ] L2 (volume : Measure (SpectralDomain n)),
      ∀ ψ : ComplexTest n, E (spectralVector σ ψ) = factorFromW W ψ := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 10, Corollary 3.6: completion via Qσ

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$ satisfying $\int(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly $0$ , assume that $L^2(\sigma;\mathbb C)$ is not finite-dimensional, and let $W:L^2(\sigma;\mathbb C)\to L^2(dx;\mathbb C)$ be any bijective complex-linear isometry, where $dx$ is Euclidean volume measure. For a complex-valued Schwartz function $\psi$ , put

\widehat\psi(u)=\int_{\mathbb R^n}e^{-i\langle u,x\rangle}\psi(x)\,dx,

and let $F_\sigma(\psi)$ be its $L^2(\sigma)$ class if $\widehat\psi$ is almost everywhere strongly measurable and has finite $L^2(\sigma)$ seminorm, and the zero element otherwise. Let $H_\sigma$ be the closure in $L^2(\sigma;\mathbb C)$ of the complex-linear span of all $F_\sigma(\psi)$ . Then every $\widehat\psi$ satisfies those $L^2$ membership conditions, and there exists a bijective complex-linear isometry $E:H_\sigma\to L^2(dx;\mathbb C)$ such that, for every complex-valued Schwartz function $\psi$ ,

E\bigl(F_\sigma(\psi)\text{ regarded as an element of }H_\sigma\bigr) =W\bigl(F_\sigma(\psi)\bigr).

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