Hamiltonian symplectic differential
ProvedBirkhoffGlobalSection.hamiltonian_symplectic_differentialdifferential-geometryreal-analysis
The symplectic pairing of a Hamiltonian vector field with a phase vector equals the Hamiltonian differential applied to that vector.
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_symplectic_differential :
∀ (F : Phase → ℝ) (y v : Phase),
phaseSymplecticForm (hamiltonianVectorField F y) v = fderiv ℝ F y v := by sorrySource
Independent extraction of component 2 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.