Convex model inverse variational differential
ProvedBirkhoffGlobalSection.convex_model_inverse_variational_differentialconvex-geometryreal-analysis
The inverse radial chart satisfies the displayed differentiated field relation on energy-tangent boundary vectors.
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_reverse_radial_variation_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_inverse_variational_differential :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (y w : Phase) (hy : y ∈ frontier M.body)
(hw : fderiv ℝ M.modelHamiltonian y w = 0),
let X : Phase → Phase := fun z =>
(phaseRadialContact z (hamiltonianVectorField M.modelHamiltonian z))⁻¹ •
hamiltonianVectorField M.modelHamiltonian z
fderiv ℝ (fderiv ℝ radialNormalize) y (X y) w +
fderiv ℝ radialNormalize y (fderiv ℝ X y w) =
fderiv ℝ (convexModelSphereReebField M) (radialNormalize y)
(fderiv ℝ radialNormalize y w) := by sorrySource
Independent extraction of component 9 of the Proved theorem BirkhoffGlobalSection.reverse_radial_variation_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_reverse_radial_variation_bundle.lean. Exact original component retained.