The Hamiltonian flow on a compact symplectic manifold preserves the symplectic volume #
TERM-SCOPE(Hamiltonian) TERM-SCOPE(Liouville) — this module uses the restricted senses
of "Hamiltonian" and "Liouville"; specs/TERMS.md records what is backed and what is not.
Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Q29(d′) of
specs/generator-layer-scoping.md, the assembly of Q29(a)–(c′).
The pieces: the global flow integralFlow of a C^1 field on a compact manifold with its group
law (IntegralCurve/GlobalFlow.lean), its joint continuity (IntegralCurve/FlowContinuity.lean),
the differentiable dependence of the local flow on the initial point with the flat Liouville
theorem (Analysis/ODE/FlowDerivative.lean: ContDiffAt.exists_localFlow_form_invariant), the
vanishing of the flat Lie derivative of a symplectic form's local representative along its local
Hamiltonian vector (HamiltonianLieDerivative.lean), and the change-of-variables theorem for the
measure of a top form (TopFormMeasure.lean: topFormMeasure_map_eq). This file assembles them.
chartField_eq_trivializationAt_snd,DifferentialForm.chartField_hamiltonianVectorField— the chart field ofFlowContinuity.leanis the trivialised section, and for the Hamiltonian vector field it is the local Hamiltonian vector on the chart's target;ContinuousAlternatingMap.compContinuousLinearMap_comp, ★DifferentialForm.forall_chart_of_forall_exists_chart— from one chart to two: if around every point some chart carries the differentiability and the pullback identity of a mapgfor a form family, then every pair of charts does (localRep_transitionmoves the pullback across the two chart transitions);- ★
DifferentialForm.exists_nhds_forall_integralFlow_localRep_eq— local invariance: near every point, fort ∈ [0, ε], the chart expression of the Hamiltonian flow is differentiable and pulls the local representative of the symplectic form back to itself. In the chart the flow is the Picard–Lindelöf local flow (isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless), its derivative solves the variational equation, and the flat Liouville theorem applies; integralFlowHomeomorph— the time-tmap as a homeomorphism (inverse: time-t);map_integralFlow_eq_of_forall_Icc— a measure invariant for all small non-negative times is invariant for all times (iterate the group law;φ t ∘ φ (-t) = id);- ★
DifferentialForm.exists_forall_map_integralFlow_topFormMeasure_wedgePow_eq— small-time invariance of the measure of every powerα^k: a finite subcover, the two-chart lemma with the naturalitywedgePow_compContinuousLinearMapof the wedge power under pullback, andtopFormMeasure_map_eq; DifferentialForm.IsSymplectic.hamiltonianFlow— the Hamiltonian flow of a smooth energy on a compact symplectic manifold;- ★★★
DifferentialForm.IsSymplectic.map_hamiltonianFlow_topFormMeasure_wedgePow— Liouville's theorem: the Hamiltonian flow of every smoothHpreserves the measure of every power of the symplectic form, at every time, for every Haar measure on the model, basis and chart cover.
The ℂℙⁿ instance (fsVolume_map_hamiltonianFlow) is in
Instances/ProjectiveSpaceHamiltonianFlow.lean.
The chart field is the trivialised section #
The chart field of FlowContinuity.lean is the second component of the tangent
trivialisation of the section, at the chart preimage.
Two charts from one #
Pullback along a composition is the composition of the pullbacks.
★ From one chart to two. If around every point some chart carries the differentiability
and the pullback identity of g for s, then every pair of charts does: the chart expression in
the pair is the one-chart expression conjugated by two transitions, and localRep_transition
moves the pullback across each.
The chart field of a Hamiltonian vector field, and the local invariance #
The chart field of the Hamiltonian vector field is the local Hamiltonian vector, on the chart's target.
★ Local invariance of the symplectic form under the Hamiltonian flow, in a chart. Near
every y there are an open neighbourhood U of y inside the chart's source and a time ε > 0
such that for p ∈ U and t ∈ [0, ε] the flow keeps p in the chart at y, its chart
expression is differentiable at chartAt E y p, and it pulls the local representative of α
back to itself: in the chart the flow is the Picard–Lindelöf local flow (uniqueness of integral
curves), whose derivative solves the variational equation, and the flat Liouville theorem applies
because the flat Lie derivative of the local representative along the local Hamiltonian vector
vanishes.
The flow as a homeomorphism, and invariance for all times from small times #
The flow at time t as a homeomorphism of M (inverse: the flow at time -t).
Equations
- integralFlowHomeomorph hv t = { toFun := integralFlow hv t, invFun := integralFlow hv (-t), left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
A measure invariant under the flow for all small non-negative times is invariant for all
times: iterate the group law forward, and use φ t ∘ φ (-t) = id backward.
Assembly: the Hamiltonian flow preserves the measure of every power of the form #
The Hamiltonian vector field of a symplectic form, as a C^1 section of the tangent bundle in
the form integralFlow takes.
The Hamiltonian flow of a smooth H on a compact symplectic manifold: the flow of its
Hamiltonian vector field.
Equations
- hβ.hamiltonianFlow hH t x = integralFlow ⋯ t x
Instances For
The Hamiltonian flow at any time is continuous (continuous_integralFlow_point).
★ Small-time invariance of the top-power measure. For a symplectic α and a smooth H,
there is ε₀ > 0 such that for t ∈ [0, ε₀] the Hamiltonian flow at time t preserves the
measure of α^k (any k, any Haar μ, any basis, any chart cover): the local statement at
every point, a finite subcover, the two-chart lemma, and topFormMeasure_map_eq.
★★★ Liouville's theorem on a compact symplectic manifold. The Hamiltonian flow of every
smooth H preserves the measure of every power β^k of the symplectic form, at every time.