Convex model contact coordinates of combination
ProvedBirkhoffGlobalSection.convex_model_contact_coordinates_of_combinationconvex-geometryreal-analysis
The contact coordinates of a linear combination of the two normalized convex model frame vectors are precisely its two coefficients.
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_contact_frame_angle_disk_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_contact_coordinates_of_combination :
∀ {μ c : ℝ}
(M : ConvexRegularizationModel μ c) (u : Phase) (hu : u ∈ unitThreeSphere) (a b : ℝ),
convexModelContactCoordinates M u (a • convexModelSymplecticContactFrame M u 0 +
b • convexModelSymplecticContactFrame M u 1) = ![a, b] := by sorrySource
Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.contact_frame_angle_disk_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_frame_angle_disk_bundle.lean. Exact original component retained.