Convex model smooth sphere reeb pushforward
ProvedBirkhoffGlobalSection.convex_model_smooth_sphere_reeb_pushforwardconvex-geometryreal-analysis
The smooth sphere Reeb field for the convex model inverse-gauge weight pushes forward to its contact-normalized Hamiltonian vector field.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained. This is a conditional result for the defined convex regularization model, not a global-section or index-existence theorem.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_smooth_sphere_reeb_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.convex_model_smooth_sphere_reeb_pushforward :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (u : Phase) (hu : u ∈ unitThreeSphere),
let f : Phase → ℝ := fun x => ((gauge M.body x)⁻¹)^2
let R : Phase → Phase := sphereReebExtension f
let G : Phase → Phase := fun x => (gauge M.body x)⁻¹ • x
let y := G u
ContDiffAt ℝ ∞ R u ∧
fderiv ℝ G u (R u) =
(phaseRadialContact y (hamiltonianVectorField M.modelHamiltonian y))⁻¹ •
hamiltonianVectorField M.modelHamiltonian y := by sorrySource
Independent extraction of component 6 of the Proved theorem BirkhoffGlobalSection.smooth_sphere_reeb_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_smooth_sphere_reeb_bundle.lean. Exact original component retained.