Plane family normalized polar lift
ProvedBirkhoffGlobalSection.plane_family_normalized_polar_liftdynamical-systemstopology
A jointly continuous nonvanishing plane-valued family that equals (cos s,sin s) at time zero admits jointly continuous positive radius and angle with angle exactly s at time zero.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_winding_interval_bundle open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option maxHeartbeats 800000 open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.plane_family_normalized_polar_lift :
∀ (v : ℝ × ℝ → Plane)
(hv : Continuous v) (hne : ∀ x, v x ≠ 0)
(hzero : ∀ s, v (0, s) = ![Real.cos s, Real.sin s]),
∃ ρ θ : ℝ × ℝ → ℝ, Continuous ρ ∧ Continuous θ ∧
(∀ x, 0 < ρ x) ∧ (∀ s, θ (0, s) = s) ∧
∀ x, v x = ![ρ x * Real.cos (θ x), ρ x * Real.sin (θ x)] := by sorrySource
Independent extraction of component 2 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.