Normalized plane family angle shift

Proved

BirkhoffGlobalSection.normalized_plane_family_angle_shift

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

dynamical-systemstopology

A normalized positive polar lift of a family periodic in its angular parameter satisfies the corresponding full-turn angle shift under the displayed periodicity hypothesis.

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.normalized_plane_family_angle_shift :
∀ (v : ℝ × ℝ → Plane)
    (ρ θ : ℝ × ℝ → ℝ) (hθ : Continuous θ) (hρ : ∀ x, 0 < ρ x)
    (hθ0 : ∀ s, θ (0, s) = s)
    (hpolar : ∀ x, v x = ![ρ x * Real.cos (θ x), ρ x * Real.sin (θ x)])
    (P : ℝ) (hperiod : ∀ t s, v (t, s + P) = v (t, s)),
    ∀ t s, θ (t, s + P) = θ (t, s) + P := by sorry

Source

Independent extraction of component 4 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.

View graph