Continuity characterizes the spectral growth class

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.spectral_continuity_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$ .

For a regular positive Borel measure $\sigma$ not initially assumed in $\mathcal C$ , define the nonnegative extended integral $Q_\sigma(\psi)=\int|\widehat\psi|^2\,d\sigma$ . Then

\sigma\in\mathcal C\quad\Longleftrightarrow\quad Q_\sigma(\psi)<\infty\ \text{for every }\psi\in\mathcal S,\quad\text{and }\psi\mapsto Q_\sigma(\psi)\text{ is real-valued and continuous}.

The finiteness clause spells out what it means for the printed map to be a continuous real-valued quadratic form.

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

/-- Proposition 3.3, PDF pp.8--9: finiteness is explicit before continuity of the
real-valued form, so a divergent nonnegative integral cannot become zero. -/
theorem spectral_continuity_iff (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hregular : σ.Regular) :
    InC σ ↔ ((∀ ψ : ComplexTest n, fourierEnergy σ ψ < ⊤) ∧ Continuous (spectralQ σ)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 8, Proposition 3.3: continuity characterizes C

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$ , the existence of a natural number $p$ , possibly $0$ , such that

\int_{\mathbb R^n}(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty

is equivalent to the conjunction of these two conditions: for every complex-valued Schwartz function $\psi$ , the extended nonnegative energy

E_\sigma(\psi)=\int_{\mathbb R^n}|\widehat\psi(u)|^2\,d\sigma(u), \qquad \widehat\psi(u)=\int_{\mathbb R^n}e^{-i\langle u,x\rangle}\psi(x)\,dx,

is finite; and the real-valued function $\psi\mapsto E_\sigma(\psi)^{\mathrm{real}}$ is continuous on the Schwartz space. Here the conversion to a real number takes finite extended nonnegative values to their real values and takes $+\infty$ to $0$ ; the separate finiteness condition on the right excludes that latter case.

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