Fourier transform onto the full covariance RKHS

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.fourier_onto_covariance_rkhs

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 $\sigma\in\mathcal C$ , there exists a probability law $\mu$ on the continuous real tempered dual satisfying $\int e^{i\omega(\psi)}\,d\mu=\exp(-\frac12\int|\widehat\psi|^2\,d\sigma)$ for every real test. Define $C_\sigma(\psi,\varphi)=\exp(-\frac12\int|\widehat{\psi-\varphi}|^2\,d\sigma)$ . This kernel is positive semidefinite, and the transform

(F_\sigma f)(\psi)=\int_\Omega e^{-i\omega(\psi)}f(\omega)\,d\mu(\omega)

is a complex-linear isometric isomorphism from the full $L^2(\mu)$ onto the complex reproducing kernel Hilbert space $H(C_\sigma)$ , with real Schwartz indices $\psi$ . Constants and every Gaussian chaos are included.

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 6.1, PDF pp.15--17: the full Fourier transform, including constants
and all chaoses, is isometric ONTO the covariance RKHS. Kernel positivity and the
probability law are conclusions; RKHS.OfKernel supplies the separated completion. -/
theorem fourier_onto_covariance_rkhs (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) :
    ∃ μ : Measure (Omega n), CharacteristicLaw σ μ ∧
      ∃ hK : (covarianceKernel σ).PosSemidef,
        letI : Fact (covarianceKernel σ).PosSemidef := ⟨hK⟩
        ∃ E : MeasureTheory.Lp ℂ 2 μ ≃ₗᵢ[ℂ] RKHS.OfKernel (covarianceKernel σ),
          ∀ (f : MeasureTheory.Lp ℂ 2 μ) (ψ : RealTest n),
            (E f) ψ = lawFourier μ f ψ := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 15, Theorem 6.1: Fourier transform onto the covariance RKHS

Read-back

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

For every positive integer $n$ , let $X=\mathbb R^{\operatorname{Fin}n}$ , and let $\sigma$ be a regular measure for which $\int_X(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly zero. Let $\mathcal S_{\mathbb R}(X)$ be the real-valued Schwartz space, and let $\Omega$ be its continuous real-linear dual, equipped with the smallest sigma-algebra making every evaluation $\omega\mapsto\omega(\psi)$ measurable. For $\psi\in\mathcal S_{\mathbb R}(X)$ , regard $\psi$ as complex-valued and define the extended nonnegative quantity

F_\sigma(\psi)=\int_X^{\!\!-} \left|\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx\right|^2\,d\sigma(u).

There exists a probability measure $\mu$ on $\Omega$ such that, for every real-valued Schwartz function $\psi$ , $F_\sigma(\psi)<\infty$ and

\int_\Omega e^{i\omega(\psi)}\,d\mu(\omega) =\exp\!\left(-\frac{\operatorname{toReal}(F_\sigma(\psi))}{2}\right).

Moreover, the operator-valued kernel on $\mathcal S_{\mathbb R}(X)$ given by

K(\psi,\phi) =\exp\!\left(-\frac{\operatorname{toReal}(F_\sigma(\psi-\phi))}{2}\right) \operatorname{id}_{\mathbb C}

is positive semidefinite, and, using this positive semidefiniteness to form its associated reproducing kernel Hilbert space $\mathcal H_K$ , there exists a surjective complex-linear isometry $E:L^2(\Omega,\mu;\mathbb C)\to\mathcal H_K$ satisfying

(Ef)(\psi)=\int_\Omega e^{-i\omega(\psi)}f(\omega)\,d\mu(\omega) \quad\text{for every }f\in L^2(\Omega,\mu;\mathbb C) \text{ and }\psi\in\mathcal S_{\mathbb R}(X).

Here $\operatorname{toReal}$ takes the real value of a finite extended nonnegative number and sends $+\infty$ to zero; the asserted finiteness applies to every argument used in the characteristic identity and kernel.

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