Hamiltonian linearization symplectic
ProvedBirkhoffGlobalSection.hamiltonian_linearization_symplecticdifferential-geometryreal-analysis
The derivative of a smooth Hamiltonian vector field is infinitesimally symplectic: its two contributions to the derivative of a symplectic pairing sum to zero.
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_symplectic :
∀ (F : Phase → ℝ) (y v w : Phase)
(hF : ContDiffAt ℝ ∞ F y),
phaseSymplecticForm (fderiv ℝ (hamiltonianVectorField F) y v) w +
phaseSymplecticForm v (fderiv ℝ (hamiltonianVectorField F) y w) = 0 := by sorrySource
Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.