Gaussian measure on the continuous real tempered dual

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.gaussian_characteristic_law

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 every $\sigma\in\mathcal C$ there exists a probability measure $\mu$ on $\Omega=\mathcal S(\mathbb R^n;\mathbb R)'$ , the continuous real dual with its evaluation sigma-algebra, such that every real Schwartz test $\psi$ satisfies

\int_\Omega e^{i\omega(\psi)}\,d\mu(\omega)=\exp\!\left(-\frac12\int_{\mathbb R^n}|\widehat\psi(u)|^2\,d\sigma(u)\right).

This constructs the distribution Gaussian law, including the Dirac law at zero when $\sigma=0$ . No symmetry of $\sigma$ is assumed.

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

/-- §1(d), PDF p.3 (standing assumptions pp.2--6): existence of the distribution
Gaussian law. Includes σ=0, and assumes no reflection symmetry. -/
theorem gaussian_characteristic_law (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ) :
    ∃ μ : Measure (Omega n), CharacteristicLaw σ μ := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 3, §1(d), unnumbered: distribution Gaussian characteristic law

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$ such that, for some natural number $p$ , including possibly $p=0$ ,

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

there exists a probability measure $\mu$ on the space $\Omega_n$ of continuous real-linear functionals on the real-valued Schwartz functions on $\mathbb R^n$ , equipped with the measurable structure generated by all evaluations $\omega\mapsto\omega(\psi)$ . For every real-valued Schwartz function $\psi$ , regarded as complex-valued when taking its Fourier integral, the extended nonnegative quantity

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

is finite, and

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

The exponent uses the real value of the finite energy. Existence, rather than uniqueness, of $\mu$ is asserted.

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