Plane curve polar bound iff

Proved

BirkhoffGlobalSection.plane_curve_polar_bound_iff

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemstopology

For a continuous nonvanishing plane curve, a universal bound on increments of every continuous positive polar angle is equivalent to the corresponding bound for one continuous positive polar lift.

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_bound_iff :
∀ (v : ℝ → Plane) (hv : Continuous v)
    (hne : ∀ t, v t ≠ 0) (T L : ℝ),
    (∀ θ : ℝ → ℝ, Continuous θ →
      (∀ t, ∃ r : ℝ, 0 < r ∧ v t = ![r * Real.cos (θ t), r * Real.sin (θ t)]) →
      L < θ T - θ 0) ↔
    ∃ ρ θ : ℝ → ℝ, Continuous ρ ∧ Continuous θ ∧ (∀ t, 0 < ρ t) ∧
      (∀ t, v t = ![ρ t * Real.cos (θ t), ρ t * Real.sin (θ t)]) ∧ L < θ T - θ 0 := by sorry

Source

Independent extraction of component 8 of the Proved theorem BirkhoffGlobalSection.contact_angular_lift_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_angular_lift_bundle.lean. Exact original component retained.

View graph