Prove2Me

Scaled hamiltonian linearization symplectic

Proved
BirkhoffGlobalSection.scaled_hamiltonian_linearization_symplectic

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

differential-geometryreal-analysis

The linearization of a differentiably scaled smooth Hamiltonian field is infinitesimally symplectic on vectors in the Hamiltonian differential kernel.

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.scaled_hamiltonian_linearization_symplectic :
∀ (F b : Phase → ℝ) (y v w : Phase)
    (hF : ContDiffAt ℝ ∞ F y) (hb : DifferentiableAt ℝ b y)
    (hv : fderiv ℝ F y v = 0) (hw : fderiv ℝ F y w = 0),
    phaseSymplecticForm (fderiv ℝ (fun x => b x • hamiltonianVectorField F x) y v) w +
      phaseSymplecticForm v (fderiv ℝ (fun x => b x • hamiltonianVectorField F x) y w) = 0 := by sorry
Source
Independent extraction of component 5 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.

View graph