Darboux theorem

In plain terms

Classical mechanics is written on phase space, where the essential structure isn't a notion of distance but a pairing between directions, the one that says which coordinate is conjugate to which and turns an energy function into a flow. The question Darboux's theorem answers is how much freedom that structure has.

The answer is none, locally. Given such a pairing, you can always change coordinates near any point so that it becomes the standard one, position paired with momentum, one pair per degree of freedom. Curvature has no analogue here: two symplectic spaces of the same dimension are indistinguishable in any small neighbourhood, and all the geometry is global. The dimension is even, and that's the only local invariant.

The consequence for mechanics is that canonical coordinates always exist. Whatever the phase space is and however it was built, near any point you can write Hamilton's equations in their familiar form, which is why the textbook treatment loses no generality by starting there.

In CSD

The programme's isolated dynamics is the Hamiltonian flow of the sector's own symplectic structure, so the theorem that says such a structure is locally standard is infrastructure the derivation leans on, and the corpus proves it rather than citing it. The route is Moser's trick, which deforms the form along a path and integrates the resulting vector field, so the chart comes from a flow and its regularity is the regularity of that flow.

Four rows were needed. The first gives the chart in which the form is constant, the second upgrades the chart from continuous to continuously differentiable by a quantitative comparison of two linear flows, the third composes with a symplectic basis to reach the standard form and derives evenness of the dimension, and the fourth proves smooth dependence of a flow on its initial point so that the chart is smooth at every order the form is. On a symplectic manifold the result is a smooth Darboux chart at every point. The generator-layer question that motivated the work is recorded with it.

Mathematically

Darboux.lean gives, by Moser's trick, a chart in which a closed non-degenerate two-form equals its value at the base point; FlowSmooth.lean supplies contDiffOn_flow_of_contDiffOn, the C^n dependence of a flow on the initial point, which is what makes that chart C^k for a C^k form. DarbouxStandardForm.lean composes with a symplectic basis: ContinuousAlternatingMap.toBilinForm is the bilinear form of a two-form, alternating and non-degenerate when the form is; IsAlt.exists_isSymplecticBasis (SymplecticBasis.lean) works over any field; exists_continuousLinearEquiv_eq_standardSymplecticForm_comp is linear Darboux with finrank E = 2n.

exists_openPartialHomeomorph_pullback_standard is Darboux on a ball in standard form, with a C^k chart whose derivative pulls the standard form back to the given one, and IsSymplectic.exists_openPartialHomeomorph_localRep_pullback_standard is the manifold statement at every point, with IsSymplectic.even_finrank the evenness corollary. The linear change of coordinates is smooth; the chart inherits the form's order.

The name

Jean Gaston Darboux proved the theorem in 1882 in Paris, in work on Pfaffian systems, and it became the structural fact that organises symplectic geometry. The modern proof is Jurgen Moser's, from a 1965 paper on volume elements on a manifold, whose trick of deforming a form along a path and integrating the resulting field is now the standard tool.

The absence of local invariants is what makes symplectic topology a global subject, and Mikhail Gromov's non-squeezing theorem of 1985 gave it its first genuinely global rigidity.

Related entries

• Kahler formOn the space of quantum states, distance, area and a quarter-turn coming from the complex numbers lock together, and that lock is what makes the volume of the space nobody's choice.
• 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.
• Moment mapThe Born probabilities are coordinates, and the moment map reads them straight off the geometry of the space of quantum states, with no measurement postulate consulted.
• 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.
• Field arenaTake finitely many field modes, cap the number of quanta each can hold, and the whole toolbox of quantum field theory, propagators, light cones, Wick's theorem and thermal states, reappears as exact theorems on one finite arena.