Hamiltonian gradient radius positive
ProvedBirkhoffGlobalSection.hamiltonian_gradient_radius_positivedifferential-geometryreal-analysis
A positive radial Hamiltonian derivative forces the Hamiltonian gradient's squared radius to be positive.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_transverse_contact_frame_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_gradient_radius_positive :
∀ (F : Phase → ℝ) (y : Phase)
(hp : 0 < phaseRadialContact y (hamiltonianVectorField F y)),
0 < zNormSq (TangentialHessian.grad F y) + wNormSq (TangentialHessian.grad F y) := by sorrySource
Independent extraction of component 7 of the Proved theorem BirkhoffGlobalSection.transverse_contact_frame_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_transverse_contact_frame_bundle.lean. Exact original component retained.