The distributional adjoint product is the spectral kernel

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.distributional_adjoint_product

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$ .

Let $\sigma\in\mathcal C$ and let $Q:\mathcal S\to L^2(dx)$ be a continuous complex Hilbert factor of the spectral form (3.6). The spectral pairing defines a continuous complex-linear map $A$ into the continuous anti-dual of $\mathcal S$ , and

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

Here an anti-dual pairs against conjugated test functions; this is the distributional kernel $\widehat\sigma(t-s)$ in the proof's variable order. The final extra $du$ in the printed formula is removed. No real Gaussian assumption enters.

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 5.3, PDF pp.14--15. SOURCE CORRECTION: remove the duplicated final du
from (5.4). Use the proof's spectral pairing/kernel σ-hat(t-s), not pointwise
values of a distribution. The anti-dual pairs against conjugated test functions;
Mathlib inner(Q φ,Q ψ) is the source's first-slot-linear inner(Q ψ,Q φ).
No real Gaussian compatibility is assumed. -/
theorem distributional_adjoint_product (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ)
    (Q : ComplexTest n →L[ℂ] L2 (volume : Measure (SpectralDomain n))) (hQ : HilbertFactor σ Q) :
    ∃ A : ComplexTest n →L[ℂ] AntiDual n,
      (∀ ψ, A ψ = spectralDistribution σ ψ) ∧
      (∀ ψ φ, A ψ φ = spectralPairing σ ψ φ) ∧
      (∀ ψ, A ψ = adjointProduct Q ψ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 14, Theorem 5.3: distributional adjoint product

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}$ , let $\mathcal S_{\mathbb C}(X)$ be its complex-valued Schwartz space, and let $\sigma$ be a regular measure satisfying $\int_X(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly zero. Define

\widehat\psi(u)=\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx, \qquad B_\sigma(\psi,\phi)=\int_X\widehat\psi(u)\,\overline{\widehat\phi(u)}\,d\sigma(u),

using the total complex-valued integral, which is zero when the integrand is not integrable. Let $\mathcal S_{\mathbb C}(X)^\times$ denote the space of continuous conjugate-linear maps from $\mathcal S_{\mathbb C}(X)$ to $\mathbb C$ . Suppose that $Q:\mathcal S_{\mathbb C}(X)\to L^2(X,du;\mathbb C)$ is continuous and complex-linear and satisfies

\langle Q\phi,Q\psi\rangle_{\mathbb C}=B_\sigma(\psi,\phi) \quad\text{for every }\psi,\phi.

For each $\psi$ , define $D_\sigma(\psi)$ to be a chosen member $T$ of $\mathcal S_{\mathbb C}(X)^\times$ satisfying $T(\phi)=B_\sigma(\psi,\phi)$ for every $\phi$ , if such a member exists, and zero otherwise. Then there exists a continuous complex-linear map $A:\mathcal S_{\mathbb C}(X)\to\mathcal S_{\mathbb C}(X)^\times$ such that, for every $\psi,\phi$ ,

A\psi=D_\sigma(\psi),\qquad (A\psi)(\phi)=B_\sigma(\psi,\phi),\qquad A\psi=\bigl(\phi\mapsto\langle Q\phi,Q\psi\rangle_{\mathbb C}\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