Hamiltonian linearization pairing

Proved

BirkhoffGlobalSection.hamiltonian_linearization_pairing

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryreal-analysis

For a smooth Hamiltonian, pairing its linearized Hamiltonian vector field with a vector equals the Hessian evaluated on the corresponding two vectors.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble

import Theorems.Thm_BirkhoffGlobalSection_variational_symplecticity_bundle
open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.hamiltonian_linearization_pairing :
∀ (F : Phase → ℝ) (y v w : Phase)
    (hF : ContDiffAt ℝ ∞ F y),
    phaseSymplecticForm (fderiv ℝ (hamiltonianVectorField F) y v) w =
      fderiv ℝ (fderiv ℝ F) y v w := by sorry

Source

Independent extraction of component 3 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.

View graph