Continuous Hilbert factorization of the spectral form

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.hilbert_space_factorization

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$ and the complex Hilbert space $L^2(\sigma)$ is infinite dimensional. There exists a continuous complex-linear map $Q:\mathcal S\to L^2(\mathbb R^n,dx)$ such that

\langle Q\psi,Q\varphi\rangle_{\mathrm{source}}=\int\widehat\psi(u)\overline{\widehat\varphi(u)}\,d\sigma(u),\qquad\|Q\psi\|_2^2=\int|\widehat\psi|^2\,d\sigma.

This realizes the spectral form in Lebesgue $L^2$ . The codomain follows the construction and proof, correcting the printed $L^2(\sigma)$ . Mathlib's conjugate-linear-first inner product reverses the displayed slots.

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.4, PDF pp.9--10. SOURCE CORRECTION: the theorem and (3.6) print
L2(σ); (3.7), §1(b), and every norm in the proof use L2(dx), used here.
The explicit infinite-dimensional assumption is retained. -/
theorem hilbert_space_factorization (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) (hinfinite : ¬ FiniteDimensional ℂ (L2 σ)) :
    ∃ Q : ComplexTest n →L[ℂ] L2 (volume : Measure (SpectralDomain n)),
      HilbertFactor σ Q ∧ ∀ ψ : ComplexTest n,
        fourierEnergy σ ψ = ENNReal.ofReal (‖Q ψ‖ ^ 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 9, Theorem 3.4: Hilbert-space factorization

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 additionally that the complex Hilbert space $L^2(\sigma;\mathbb C)$ is not finite-dimensional. Then there exists a continuous complex-linear map $Q$ from the complex-valued Schwartz functions on $\mathbb R^n$ to $L^2(dx;\mathbb C)$ such that, for every pair $\psi,\phi$ of such functions,

\langle Q\phi,Q\psi\rangle_{\mathbb C} =\int_{\mathbb R^n}\widehat\psi(u)\, \overline{\widehat\phi(u)}\,d\sigma(u),

and, for every such $\psi$ ,

\int_{\mathbb R^n}|\widehat\psi(u)|^2\,d\sigma(u) =\operatorname{ofReal}\!\left(\|Q\psi\|_2^2\right).

Here $dx$ is Euclidean volume measure, $\widehat\psi(u)=\int_{\mathbb R^n}e^{-i\langle u,x\rangle}\psi(x)\,dx$ , the energy integral is extended nonnegative, and $\operatorname{ofReal}$ embeds the nonnegative real squared norm into the extended nonnegative reals. The complex pairing integral uses the total Bochner integral, which is $0$ when its integrand is not integrable.

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