Sphere reeb variation contact conserved
ProvedBirkhoffGlobalSection.sphere_reeb_variation_contact_conserveddifferential-geometryreal-analysis
For supplied sphere Reeb trajectories and variational solutions, the weighted contact value of the variation is conserved when the weight is smooth and positive.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_variation_preservation_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.sphere_reeb_variation_contact_conserved :
∀ (f : Phase → ℝ) (q v : ℝ → Phase)
(hf : ∀ u ∈ unitThreeSphere, ContDiffAt ℝ ∞ f u ∧ 0 < f u)
(hqS : ∀ t, q t ∈ unitThreeSphere)
(hq : ∀ t, HasDerivAt q (sphereReebExtension f (q t)) t)
(hv : ∀ t, HasDerivAt v (fderiv ℝ (sphereReebExtension f) (q t) (v t)) t)
(h0 : q 0 0 * v 0 0 + q 0 1 * v 0 1 + q 0 2 * v 0 2 + q 0 3 * v 0 3 = 0),
∀ t, f (q t) * phaseRadialContact (q t) (v t) =
f (q 0) * phaseRadialContact (q 0) (v 0) := by sorrySource
Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.contact_variation_preservation_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_variation_preservation_bundle.lean. Exact original component retained.