Koopman operator

In plain terms

Quantum mechanics is often introduced by its apparatus: states are vectors in a Hilbert space, a space with a notion of length and angle, and time evolution is unitary, meaning it preserves those lengths and angles. It's natural to read that apparatus as the signature of quantum physics, and it isn't.

Koopman and von Neumann showed that classical mechanics carries the same apparatus. Instead of following a classical system's trajectory, follow the functions on its phase space, the observables. A flow that preserves phase-space volume acts on those functions by composition, and that action preserves the natural notion of length among them, so it is unitary, and the flow's group structure becomes a one-parameter group of unitary operators. Superposition of observables, spectra, eigenvalues and the rest of the toolkit all apply, which is why this picture is now standard in work on complex classical systems.

What classical mechanics doesn't have is a noncommutative algebra of observables. Classical observables multiply pointwise, in either order, and composition with the flow respects that product. The commutation relation between position and momentum is the thing quantum mechanics adds, and the Koopman picture is the cleanest way to see that it's the only thing.

In CSD

The programme claims that the quantum formalism is recoverable from a single trajectory on a constraint surface, so it matters exactly which parts of that formalism are evidence of anything. The corpus proves the Koopman construction to settle one such question: a Hilbert space with a unitary group on it is available to a classical flow, so its presence in the programme's derivation isn't smuggling quantum mechanics in.

Three statements carry that. Composition with a measure-preserving map is a linear isometry of the square-integrable functions, an invertible map gives a genuine unitary whose inverse is composition with the inverse map, and a flow gives the group law, so time evolution is a one-parameter unitary group. On differentiable observables the generator is computed along a flow line, and for a Hamiltonian flow that derivative is the Poisson bracket with the energy, which is the Liouville operator, consuming the corpus's own bracket-is-a-derivation result. The honest boundary is that the generator is pointwise, with nothing claimed about its domain, its self-adjointness, or Stone's theorem for the group, and that the flow's measure-preserving property is a hypothesis here, supplied elsewhere by Liouville's theorem.

Mathematically

koopmanL2 T hT is composition with a measure-preserving T as a linear isometry of L2 of the measure, built on Mathlib's Lp.compMeasurePreserving with the scalar multiplication transported through QuasiMeasurePreserving.ae_eq_comp; coeFn_koopmanL2 is its pointwise description almost everywhere. koopmanUnitary packages an invertible measure-preserving map as a LinearIsometryEquiv whose inverse is the Koopman operator of the inverse map. koopmanL2_flow is the group law U_(s + t) = U_t composed with U_s, the order reversing because observables compose with the flow.

koopmanFun is the same map on observables valued anywhere, and koopmanFun_mul is the algebra homomorphism property for the pointwise product, true by definition, which is the classical side of the contrast. hasDerivAt_koopmanFun differentiates along a flow line, giving the derivative of f composed with the flow as the derivative of f applied to the velocity field, and hasDerivAt_koopmanFun_poissonBracket (SigmaLayer/ChartBracket.lean) identifies that with the Poisson bracket for a Hamiltonian field. No Stone's theorem, no unbounded operator theory.

The name

Bernard Koopman published the construction in 1931 at Harvard, and John von Neumann followed a year later with the operator method in classical mechanics, using it to prove the mean ergodic theorem. The pair of papers founded ergodic theory as a branch of operator theory, and George Birkhoff's pointwise ergodic theorem arrived in the same season.

The picture has had a second life in applied mathematics, where Koopman operators are the basis of data-driven methods for nonlinear systems, since a nonlinear flow becomes a linear operator at the price of working in infinitely many dimensions.

Related entries

• Liouville measureA deterministic substrate needs a notion of volume that its own motion can't distort, and on CSD's sector that volume is forced and it's the Born measure.
• Poisson bracketThe Poisson bracket is the one rule that tells classical mechanics how fast any quantity changes, and the quantum commutator obeys exactly the same algebra, so that shared grammar is what lets a deterministic flow present itself in quantum form.
• Stone's theoremAsk only that time evolution never jumps, and differentiability, a generator and the Hamiltonian all follow for free.
• Hilbert spaceHilbert space is the stage on which quantum mechanics is usually performed, and CSD's claim is that it's scenery, the shadow cast by the physical object and not the object itself.
• Nelson stochastic mechanicsNelson derived the Schrodinger equation from a diffusion, so the same continuity equation that lets Bohm read a velocity off the wavefunction lets Nelson read a drift with noise against it, and the Born density solves both.