Hamiltonian contact frame reconstruction
ProvedBirkhoffGlobalSection.hamiltonian_contact_frame_reconstructiondifferential-geometryreal-analysis
A vector in the Hamiltonian energy and radial-contact kernels is reconstructed from the two contact-frame vectors and its displayed coordinate coefficients.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_frame_basis_bundle open BirkhoffGlobalSection Set Filter SignType open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.hamiltonian_contact_frame_reconstruction :
∀ (F : Phase → ℝ) (y v : Phase)
(hp : 0 < phaseRadialContact y (hamiltonianVectorField F y))
(hv : fderiv ℝ F y v = 0) (hα : phaseRadialContact y v = 0),
let g := TangentialHessian.grad F y
let n := zNormSq g + wNormSq g
let c := transverseFrameCoordinates g v
v = (c 0 / n) • hamiltonianContactFrame F y 0 +
(c 1 / n) • hamiltonianContactFrame F y 1 := by sorrySource
Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.contact_frame_basis_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_frame_basis_bundle.lean. Exact original component retained.