Translation invariance characterizes spectral quadratic forms

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.translation_invariant_quadratic_iff

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 $q:\mathcal S\to\mathbb R$ be continuous, nonnegative, satisfy $q(c\psi)=|c|^2q(\psi)$ , and satisfy the parallelogram identity. Then

\left[\exists\sigma\in\mathcal C\;\forall\psi\in\mathcal S,\quad q(\psi)=\int|\widehat\psi|^2\,d\sigma\right]\quad\Longleftrightarrow\quad\left[\forall t\in\mathbb R^n\;\forall\psi\in\mathcal S,\quad q(\psi(\cdot-t))=q(\psi)\right].

This characterizes precisely the continuous positive quadratic forms represented by spectral measures.

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

/-- Lemma 3.2, PDF pp.7--8: all translations t are universally quantified.
The complex quadratic axioms are those explicitly given on p.6. -/
theorem translation_invariant_quadratic_iff (n : ℕ) (hn : 0 < n)
    (q : ComplexTest n → ℝ) (hq : PositiveQuadratic q) (hc : Continuous q) :
    (∃ σ : Measure (SpectralDomain n), InC σ ∧
      ∀ ψ : ComplexTest n, fourierEnergy σ ψ = ENNReal.ofReal (q ψ)) ↔
    (∀ (t : SpectralDomain n) (ψ : ComplexTest n), q (testTranslation t ψ) = q ψ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 7, Lemma 3.2: translation-invariant continuous quadratic forms

Read-back

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

For every natural number $n>0$ and every continuous function $q$ from the complex-valued Schwartz functions on $\mathbb R^n$ to $\mathbb R$ , assume that $q(\psi)\ge0$ for every $\psi$ , that $q(c\psi)=|c|^2q(\psi)$ for every complex number $c$ and every $\psi$ , and that

q(\psi+\phi)+q(\psi-\phi)=2\bigl(q(\psi)+q(\phi)\bigr)

for every $\psi,\phi$ . Then the following are equivalent: there exists a regular measure $\sigma$ on $\mathbb R^n$ with $\int(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly $0$ , such that, for every complex-valued Schwartz function $\psi$ ,

\int_{\mathbb R^n}\left|\widehat\psi(u)\right|^2\,d\sigma(u) =\operatorname{ofReal}(q(\psi));

and $q(x\mapsto\psi(x-t))=q(\psi)$ for every $t\in\mathbb R^n$ and every such $\psi$ . Here $\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}(r)$ is the extended nonnegative value of $\max(r,0)$ , which here equals $q(\psi)$ because of the assumed nonnegativity.

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