The Koopman operator: classical mechanics in Hilbert space

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #47.

Glossary: https://glossary.constraintsurfacedynamics.com/koopman-operator/ Plain-language, CSD-role and formal statements of the Koopman operator, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Koopman (1931) and von Neumann (1932): a measure-preserving flow on phase space acts on L²(μ) by composition, U_t f = f ∘ φ_t, and that action is a unitary group. So Hilbert space, unitarity, superposition and spectral theory are all available in classical mechanics. What is not available is a noncommutative algebra of observables: classical observables multiply pointwise, and the Koopman operator is an algebra homomorphism for that product (koopmanFun_mul). The commutator [x, p] = iℏ is the one thing quantum mechanics adds — which is the sharpest statement of where the two theories part.

• ★ koopmanL2 — the Koopman operator of a measure-preserving map as a linear isometry of L²(μ). Mathlib has the composition as an AddMonoidHom (Lp.compMeasurePreserving) and its isometry, but not the linear packaging, and no Koopman operator;
• ★★ koopmanUnitary — for an invertible measure-preserving map, the unitary: a LinearIsometryEquiv whose inverse is the Koopman operator of the inverse map;
• ★★ koopmanL2_flow — the group law: for a measure-preserving flow, U_{s+t} = U_t ∘ U_s, so t ↦ U_t is a one-parameter unitary group;
• koopmanFun, koopmanFun_mul — on observables the Koopman map is an algebra homomorphism for the pointwise product: the classical side of the contrast;
• ★ hasDerivAt_koopmanFun — the generator on differentiable observables: along a flow line, d/dt (f ∘ φ_t)(x) = Df(φ_t x)[X(φ_t x)]. For a Hamiltonian field that derivative is the Poisson bracket {f, H} — the Liouvillian — which is the corpus's SigmaLayer/ChartBracket.lean (poissonBracket, BracketIsDerivative).

Honest scope

⚠️ The generator is pointwise, on differentiable observables along a given flow line. No statement is made about the generator as an operator on L² — its domain, its self-adjointness, or Stone's theorem for t ↦ U_t. That is the analytic half of Koopman–von Neumann and is not here.

⚠️ The flow is a hypothesis. koopmanL2_flow takes a family φ with the flow property and each φ t measure preserving; that a Hamiltonian flow has those properties is Liouville's theorem, which the corpus proves elsewhere (LF4/ArenaSymplectic.lean, Q29) and this module does not reprove.

⚠️ The contrast is prose, deliberately. koopmanFun_mul records that the classical observable algebra is a commutative algebra carried by composition; no theorem here states a quantum commutator, and none could witness the sentence "the commutator is what quantum mechanics adds". That sentence is positioning, and it is the row's point.

References: B. O. Koopman, Hamiltonian systems and transformations in Hilbert space, PNAS 17 (1931) 315; J. von Neumann, Zur Operatorenmethode in der klassischen Mechanik, Ann. Math. 33 (1932) 587; specs/BACKLOG.md #47; specs/future-work.md.

The Koopman operator on L²

noncomputable def Koopman.koopmanL2 {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (T : α → α) (hT : MeasureTheory.MeasurePreserving T μ μ) : ↥(MeasureTheory.Lp ℂ 2 μ) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

★ The Koopman operator of a measure-preserving map: f ↦ f ∘ T, a linear isometry of L²(μ).

Equations

• Koopman.koopmanL2 T hT = { toFun := ⇑(MeasureTheory.Lp.compMeasurePreserving T hT), map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

theorem Koopman.coeFn_koopmanL2 {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (T : α → α) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp ℂ 2 μ)) : ↑↑((koopmanL2 T hT) g) =ᵐ[μ] ↑↑g ∘ T

noncomputable def Koopman.koopmanUnitary {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (T T' : α → α) (hT : MeasureTheory.MeasurePreserving T μ μ) (hT' : MeasureTheory.MeasurePreserving T' μ μ) (hleft : ∀ (y : α), T' (T y) = y) (hright : ∀ (y : α), T (T' y) = y) : ↥(MeasureTheory.Lp ℂ 2 μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

★★ The Koopman operator of an invertible measure-preserving map is unitary: composition with the inverse map inverts it, and it is an isometry, so it is a LinearIsometryEquiv of L²(μ).

Equations

• One or more equations did not get rendered due to their size.

theorem Koopman.koopmanL2_flow {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {φ : ℝ → α → α} (hφ : ∀ (t : ℝ), MeasureTheory.MeasurePreserving (φ t) μ μ) (hadd : ∀ (s t : ℝ) (y : α), φ (s + t) y = φ s (φ t y)) (s t : ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 μ)) : (koopmanL2 (φ (s + t)) ⋯) g = (koopmanL2 (φ t) ⋯) ((koopmanL2 (φ s) ⋯) g)

★★ The group law: a measure-preserving flow gives a one-parameter group of Koopman unitaries, U_{s+t} = U_t ∘ U_s (composition of observables with the flow reverses the order).

Observables, and the generator

def Koopman.koopmanFun {α : Type u_1} {F : Type u_2} (T : α → α) (f : α → F) : α → F

The Koopman map on observables: f ↦ f ∘ T, for observables valued anywhere.

Equations

• Koopman.koopmanFun T f = f ∘ T

theorem Koopman.koopmanFun_mul {α : Type u_1} {F : Type u_2} [Mul F] (T : α → α) (f g : α → F) : koopmanFun T (f * g) = koopmanFun T f * koopmanFun T g

The Koopman map is an algebra homomorphism for the pointwise product — the classical observable algebra is commutative and the evolution respects it.

theorem Koopman.hasDerivAt_koopmanFun {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : ℝ → E → E} {f : E → F} {x v : E} {t : ℝ} (hφ : HasDerivAt (fun (s : ℝ) => φ s x) v t) (hf : DifferentiableAt ℝ f (φ t x)) : HasDerivAt (fun (s : ℝ) => koopmanFun (φ s) f x) ((fderiv ℝ f (φ t x)) v) t

★ The Koopman generator on differentiable observables (the Liouvillian): along a flow line, d/dt (f ∘ φ_t)(x) = Df(φ_t x)[X(φ_t x)], where X is the flow's velocity field. For a Hamiltonian field that derivative is the Poisson bracket {f, H}.