Plane curve polar lift
ProvedBirkhoffGlobalSection.plane_curve_polar_liftdynamical-systemstopology
Every continuous nonvanishing real plane curve admits continuous positive radius and continuous real angle functions on the whole real line.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_angular_lift_bundle 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_curve_polar_lift :
∀ (v : ℝ → Plane) (hv : Continuous v)
(hne : ∀ t, v t ≠ 0),
∃ ρ θ : ℝ → ℝ, Continuous ρ ∧ Continuous θ ∧
(∀ t, 0 < ρ t) ∧ ∀ t, v t = ![ρ t * Real.cos (θ t), ρ t * Real.sin (θ t)] := by sorrySource
Independent extraction of component 2 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.