Hamiltonian vector fields on a manifold #

TERM-SCOPE(Hamiltonian) TERM-SCOPE(Kahler) — this module uses the restricted senses of "Hamiltonian" and "Kahler"; the source repository's terms register records what is backed and what is not.

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold, where at the pin the words "Hamiltonian", "moment map" and "Poisson" do not occur).

The defining equation of a Hamiltonian vector field, ι_X ω = dH, at manifold level, the pointwise facts that follow from it by alternation and linearity alone, its existence and uniqueness from non-degeneracy, its smoothness, its integral curves, the passage to the closed 1-form d(ι_X ω) = 0, and the almost Kähler and Kähler predicates.

DifferentialForm.interiorProduct ω X — the interior product ι_X ω, x ↦ (ω x).curryLeft (X x), a 1-form family (interiorProduct_apply);
DifferentialForm.IsHamiltonianVectorField ω X H — ω x (X x, v) = dH_x v at every point, with dH_x = mfderiv 𝓘(ℝ, E) 𝓘(ℝ, ℝ) H x; a Prop demanding the equation, nothing else;
DifferentialForm.IsLocallyHamiltonian ω X — d (ι_X ω) = 0, the closedness of the 1-form family;
for h : IsHamiltonianVectorField ω X H: h.interiorProduct_eq (ι_X ω = dH as families), ★ h.mfderiv_apply_self (dH (X) = 0: the energy is infinitesimally conserved along its own field, by alternation), h.eq_of_nondegenerate and ★ h.unique_of_isSymplectic (the Hamiltonian vector field of H is unique where ω is non-degenerate, in particular for a symplectic form), h.add, h.smul (linearity in H), IsHamiltonianVectorField.const (the zero field is Hamiltonian for a constant), and h.mfderiv_eq (two Hamiltonians of one field have the same derivative — the input to uniqueness up to a constant, brick G8);
h.interiorProduct_eq_mextDeriv_zeroFormFamily (ι_X ω = dH with dH the exterior derivative of the 0-form H, ExteriorDerivative.lean) and ★ h.isLocallyHamiltonian — Hamiltonian implies locally Hamiltonian (G11): d(ι_X ω) = d(dH) = 0 for a C^∞ energy, by d ∘ d = 0;
G2, existence. flatAt α x : E →ₗ[ℝ] Module.Dual ℝ E (the flat map v ↦ α x (v, ·)), flatAt_injective (non-degeneracy at x is its injectivity), flatEquiv (hence bijective, E finite-dimensional: Subspace.dual_finrank_eq), hamiltonianVectorAt α x hnd L (the unique v with α x (v, ·) = L, ★ apply_hamiltonianVectorAt, eq_hamiltonianVectorAt), and ★★ hamiltonianVectorField α hnd H = fun x => (ω♭ₓ)⁻¹ (dH_x) with ★★ hamiltonianVectorField_isHamiltonianVectorField (existence) and h.eq_hamiltonianVectorField (uniqueness: every Hamiltonian vector field of H is it); IsSymplectic.hamiltonianVectorField and its two theorems specialise to a symplectic form;
G3, smoothness. flatVec (G2's construction on the model), flatCLE / coe_flatCLE / inverse_curryLeft_apply (where ξ is non-degenerate curryLeft ξ is a continuous linear equivalence and the flat-level Hamiltonian vector is ContinuousLinearMap.inverse of it), localHamiltonianVector (the field read in a chart), localRep_nondegenerate, ★★ trivializationAt_hamiltonianVectorField_snd (the tangent trivialisation of X_H is the local Hamiltonian vector — uniqueness at the flat level), ★★ contDiffAt_localHamiltonianVector (smooth, by contDiffAt_map_inverse), and ★★★ contMDiff_hamiltonianVectorField — the Hamiltonian vector field of a C^∞ energy for a C^∞ non-degenerate 2-form is a C^∞ section of the tangent bundle; bundled as hamiltonianVectorFieldSection, and IsSymplectic.contMDiff_hamiltonianVectorField;
Q29(a), global flows. ★★ IsSymplectic.exists_isMIntegralCurve_hamiltonianVectorField — on a compact manifold the Hamiltonian vector field of a C^∞ energy has a global integral curve through every point, so its flow integralFlow (IntegralCurve/GlobalFlow.lean) exists with the group law (joint continuity in (t, x) is proved separately, in IntegralCurve/FlowContinuity.lean, which this module does not import);
G4, integral curves. ★ h.hasDerivAt_comp_of_isMIntegralCurve and ★★ h.comp_eq_of_isMIntegralCurve — energy conservation: H is constant along every integral curve of a Hamiltonian vector field of H, by dH (X) = 0 and the mean value theorem; ★★ exists_isMIntegralCurveAt_hamiltonianVectorField (local existence, Picard–Lindelöf on the C^1 section of G3) and ★★ isMIntegralCurve_hamiltonianVectorField_eq (uniqueness of global integral curves on a Hausdorff manifold); the three IsSymplectic. forms specialise;
G7, almost Kähler. apply_swap (antisymmetry of a 2-form family), the predicate IsAlmostKahler β J — a symplectic form with a compatible almost complex structure: J² = -1, J-invariance, and taming β (J v, v) > 0 — with its metric h.metric x u v = β x (J u, v), ★ metric_comm, ★ metric_self_pos, metric_J_J (Hermitian), and apply_eq_metric (β = g (·, J ·)). Its inhabitant on ℂℙⁿ is fsForm_isAlmostKahler (Instances/ProjectiveSpaceFubiniStudySymplectic.lean);
G19, analytic. ofOmega (a C^ω 2-form read as C^∞), ★★ contDiffAt_omega_localHamiltonianVector and ★★★ contMDiff_omega_hamiltonianVectorField — the Hamiltonian vector field of a C^ω energy for a C^ω non-degenerate 2-form is a C^ω section: G3 at ω, on an analytic manifold (contDiffAt_localRep at ω for the local representative);
G14a, Kähler. IsKahler β J J₀ — almost Kähler, and J is the model's complex structure J₀ through the tangent trivialisation of every chart (J_symmL), i.e. integrable in the atlas sense; ★ IsKahler.apply_eq (J y = J₀ in y's chart), ★ IsKahler.fderiv_chart_transition_comm (every chart transition is holomorphic: its derivative commutes with J₀), IsKahler.J₀_J₀. Its inhabitant on ℂℙⁿ is ★★★ fsForm_isKahler (same module as G7's);
G15, J as a section. ★★ IsKahler.contMDiff_hom_section — the complex structure of a Kähler structure, given by continuous linear maps, is a C^∞ section of Hom(TM, TM): in every chart it is the constant J₀. On ℂℙⁿ: fsJL, ★★ contMDiff_fsJL;
G14b, the tensor sense. nijenhuis J V W — the Nijenhuis tensor [JV, JW] − J[JV, W] − J[V, JW] − [V, W] with Mathlib's VectorField.mlieBracket — and ★★★ IsKahler.nijenhuis_eq_zero: on a Kähler manifold it vanishes on vector fields differentiable at the point (every bracket is the flat bracket of the chart pullbacks, J reads as the constant J₀ there, and the flat expression for a constant J₀ with J₀² = -1 is zero). The easy direction of Newlander–Nirenberg; the converse is not stated. On ℂℙⁿ: ★★ nijenhuis_fsJ_eq_zero.

Honest scope #

⚠️ Predicates on families, not on smooth sections. X is any Π x, TangentSpace 𝓘 x and ω any family; the predicates neither assert nor need smoothness. Smoothness is a separate theorem (G3) about the constructed field, under C^∞ hypotheses on ω and H.

⚠️ IsLocallyHamiltonian is stated on families. It applies mextDerivFamily to ι_X α, which is meaningful when that family is smooth — and for hamiltonianVectorField of a C^∞ energy it now is (G3) — and junk otherwise, exactly as fderiv of a non-differentiable function is junk.

⚠️ Kähler in the atlas sense, with the tensor sense derived. IsKahler β J J₀ is IsAlmostKahler plus integrability by the atlas: J is the model's J₀ through every chart's tangent trivialisation, which makes every chart transition holomorphic (IsKahler.fderiv_chart_transition_comm). That is the textbook definition. The tensor formulation follows: the Nijenhuis tensor vanishes (IsKahler.nijenhuis_eq_zero, G14b). The converse — N_J = 0 implies a holomorphic atlas, the Newlander–Nirenberg theorem — is not stated. J as a smooth section of the endomorphism bundle is G15, IsKahler.contMDiff_hom_section, stated for a J supplied as continuous linear maps (the predicate's J is a family of functions), and nijenhuis takes the family.

⚠️ The global flow exists on a compact manifold (Q29(a), 2026-09-11) — IsSymplectic.exists_isMIntegralCurve_hamiltonianVectorField and integralFlow with integralFlow_add (IntegralCurve/GlobalFlow.lean; Mathlib has no flows of vector fields on manifolds, MATHLIB-ABSENT(IsMIntegralCurve.flow)). Not stated: joint continuity of the flow in (t, x) (Q29(a′)), and that the time-t maps preserve the symplectic volume .

⚠️ The converse of G11 is false and not stated. A locally Hamiltonian field need not be Hamiltonian: ι_X ω closed but not exact is exactly the flux obstruction, and H¹ decides it. Nothing here touches that.

⚠️ No inhabitant on ℂℙⁿ here. The moment-map equation for the torus action is brick G6.

Provenance and references. The generator-layer plan (G1, G2, G3, G4, G7, G8, G11, G14a, G14b, G15, G19); Mathlib/Geometry/Manifold/VectorField/LieBracket.lean (mlieBracket, mlieBracketWithin_apply); Geometry/Manifold/SymplecticForm.lean (IsSymplectic); Geometry/Manifold/ExteriorDerivative.lean (mextDerivFamily, zeroFormFamily, toFlat_mextDerivFamily_zeroFormFamily, mextDeriv_mextDeriv); Analysis/InnerProductSpace/HamiltonianVectorField.lean (the linear duality this lifts); RecordLayer/CellLawForced.lean (IsPhaseHamiltonian, the linear moment-map equation); Mathlib/Analysis/Normed/Module/Alternating/Curry.lean; Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean (exists_isMIntegralCurveAt_of_contMDiffAt, isMIntegralCurve_eq_of_contMDiff); the terms register (Hamiltonian); the completed-work ledger.

Hamiltonian vector fields on a manifold #

Honest scope #

The interior product #

Linearity of a 2-form family in its first slot, through curryLeft #

The defining equation #

Existence: the Hamiltonian vector field of H from non-degeneracy (G2) #

Locally Hamiltonian fields, and uniqueness for a symplectic form #

Hamiltonian implies locally Hamiltonian (G11) #

The Hamiltonian vector field of a symplectic form (G2) #

Smoothness: the Hamiltonian vector field is a C^∞ section (G3) #

Integral curves: existence, uniqueness, and energy conservation (G4) #

Almost Kähler structures: a symplectic form with a compatible J (G7) #

Kähler structures: J is the complex structure of a holomorphic atlas (G14a) #

The Nijenhuis tensor, and its vanishing on a Kähler manifold (G14b) #

Linearity of a 2-form family in its first slot, through `curryLeft` #

Existence: the Hamiltonian vector field of `H` from non-degeneracy (G2) #

Smoothness: the Hamiltonian vector field is a `C^∞` section (G3) #

Almost Kähler structures: a symplectic form with a compatible `J` (G7) #

Kähler structures: `J` is the complex structure of a holomorphic atlas (G14a) #