Ergodicity and the point spectrum of the Gaussian action

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.gaussian_ergodicity_iff_point_spectrum

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$ , let $\mu$ have the real characteristic functional of §1(d), and let $U$ be the full complex $L^2(\mu)$ Koopman group of distribution shifts $\theta_t\omega(\psi)=\omega(\psi(\cdot+t))$ . Then

\text{the shift action is ergodic}\quad\Longleftrightarrow\quad\begin{cases}\text{every nonzero joint eigenvector has frequency }a=0,\\\{f:U(t)f=f\ \forall t\}=\mathbb C\mathbf1.\end{cases}

Frequency $a\in\mathbb R^n$ means $U(t)f=e^{ia\cdot t}f$ for every $t$ . Ergodicity means that every measurable set invariant modulo null sets under all shifts has probability zero or one. The fixed space has complex dimension one, including when $\sigma=0$ .

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 8.3, PDF pp.19--20: in this Gaussian distribution regime, ergodicity
is equivalent to absence of nonzero frequencies together with the one-dimensional
constant fixed space. This is not asserted for arbitrary probability actions. -/
theorem gaussian_ergodicity_iff_point_spectrum (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ)
    (μ : Measure (Omega n)) (hμ : CharacteristicLaw σ μ)
    (U : KoopmanFamily μ) (hU : IsKoopman μ U) :
    TrivialPointSpectrum μ U ↔ ShiftErgodic μ := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 19, Theorem 8.3: ergodicity and point spectrum

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 satisfying $\int_X(1+\|u\|^2)^{-p}\,d\sigma(u)<\infty$ for some natural number $p$ , possibly zero. Let $\Omega$ be the continuous real-linear dual of the real-valued Schwartz space on $X$ , equipped with the sigma-algebra generated by evaluations. Suppose that $\mu$ is a probability measure on $\Omega$ such that, for every real-valued Schwartz function $\psi$ , the extended nonnegative number

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

is finite and $\int_\Omega e^{i\omega(\psi)}\,d\mu(\omega)=e^{-\operatorname{toReal}(F_\sigma(\psi))/2}$ . Define $(S_t\omega)(\psi)=\omega(x\mapsto\psi(x+t))$ . Let $(U_t)_{t\in X}$ be a family of surjective complex-linear isometries of $L^2(\mu;\mathbb C)$ such that each $S_t$ is measurable and preserves $\mu$ , $U_0$ is the identity, $U_{t+s}=U_s\circ U_t$ for all $t,s$ , and $U_tf=f\circ S_t$ almost everywhere for each $t,f$ . Then the following conjunction is equivalent to the stated property of measurable sets: for every $a\in X$ and every nonzero $f\in L^2(\mu;\mathbb C)$ ,

\bigl(\forall t\in X,\ U_tf=e^{i\langle a,t\rangle}f\bigr)\ \Longrightarrow\ a=0,

and, for every $f\in L^2(\mu;\mathbb C)$ ,

\bigl(\forall t\in X,\ U_tf=f\bigr) \quad\Longleftrightarrow\quad \exists c\in\mathbb C,\ f=[\,\omega\mapsto c\,]_\mu.

Here the constant function has its usual $L^2$ class because $\mu$ is a probability measure; the underlying class construction returns zero for a function outside $L^2$ . The equivalent measurable-set property is that every measurable $A\subseteq\Omega$ satisfying, for each $t\in X$ , $S_t\omega\in A$ if and only if $\omega\in A$ for $\mu$ -almost every $\omega$ , has $\mu(A)=0$ or $\mu(A)=1$ . The exceptional null set in this invariance hypothesis may depend on $t$ .

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