Distribution shifts induce a Koopman unitary group

Open

QAlgorithms.Papers.Independent.Intakethird100.P38.distribution_koopman_action

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 $\mu$ be a probability law on the continuous real tempered dual with the characteristic functional in §1(d). Define the distribution shift by $(\theta_t\omega)(\psi)=\omega(\psi(\cdot+t))$ . Then every $\theta_t$ preserves $\mu$ , and there exists a group of complex unitaries $U(t)$ on the full $L^2(\mu)$ such that

U(0)=I,\qquad U(t+s)=U(t)U(s),\qquad (U(t)f)(\omega)=f(\theta_t\omega)\quad\mu\text{-almost everywhere}.

This defines the action through tests and almost-everywhere classes; it never assigns a point value to a tempered distribution.

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

/-- §8, equation (8.4), PDF pp.18--19: the distribution shifts preserve the law and
induce a group of unitaries on full L2. Pullback equalities are almost everywhere.
This assertion does not use the false general Lemma 8.1 as a hypothesis. -/
theorem distribution_koopman_action (n : ℕ) (hn : 0 < n)
    (σ : Measure (SpectralDomain n)) (hσ : InC σ)
    (μ : Measure (Omega n)) (hμ : CharacteristicLaw σ μ) :
    ∃ U : KoopmanFamily μ, IsKoopman μ U := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P38

end

Source

Stochastic processes induced by singular operators, arXiv:1109.5273v1, PDF p. 19, §8, unnumbered (8.4): distribution shift representation

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

F_\sigma(\psi):= \int_X^{\!\!-}\left|\int_X e^{-i\langle u,x\rangle}\psi(x)\,dx\right|^2\,d\sigma(u) <\infty, \qquad \int_\Omega e^{i\omega(\psi)}\,d\mu(\omega) =e^{-\operatorname{toReal}(F_\sigma(\psi))/2}.

For $t\in X$ , define $S_t:\Omega\to\Omega$ by $(S_t\omega)(\psi)=\omega(x\mapsto\psi(x+t))$ . Then there exists a family $(U_t)_{t\in X}$ of surjective complex-linear isometries of $L^2(\Omega,\mu;\mathbb C)$ such that every $S_t$ is measurable and preserves $\mu$ , $U_0$ is the identity,

U_{t+s}=U_s\circ U_t\quad\text{for every }t,s\in X,

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

(U_tf)(\omega)=f(S_t\omega) \quad\text{for }\mu\text{-almost every }\omega.

The almost-everywhere equality is asserted separately for each $t$ and $f$ .

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