Prove2Me

The winding interval is invariant under reparametrization of [0,1][0,1]

Proved
HryniewiczCriterion.windingInterval_reparam

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

hamiltonian-dynamicssymplectic-geometry

Let φ:R→M2(R)\varphi:\mathbb{R}\to M_2(\mathbb{R}) be any matrix path, and let ψ,χ:[0,1]→[0,1]\psi,\chi:[0,1]\to[0,1] be continuous with ψ(0)=χ(0)=0\psi(0)=\chi(0)=0, ψ(1)=χ(1)=1\psi(1)=\chi(1)=1 and ψ∘χ=id\psi\circ\chi=\mathrm{id} on [0,1][0,1]. Then the winding interval of Hryniewicz §2.1.1 does not change under reparametrization: I(φ∘ψ)=I(φ)I(\varphi\circ\psi)=I(\varphi).

Proof idea: an angle lift θ\theta of φ\varphi gives the angle lift θ∘ψ\theta\circ\psi of φ∘ψ\varphi\circ\psi, with the same endpoint values. Applying this to χ\chi gives the reverse inclusion.

Preamble
import Definitions.Def_HryniewiczCriterion_GraphAngle

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.windingInterval_reparam (φ : ℝ → Matrix (Fin 2) (Fin 2) ℝ) (ψ χ : ℝ → ℝ)
    (hψc : ContinuousOn ψ (Set.Icc 0 1)) (hψm : Set.MapsTo ψ (Set.Icc 0 1) (Set.Icc 0 1))
    (hψ0 : ψ 0 = 0) (hψ1 : ψ 1 = 1)
    (hχc : ContinuousOn χ (Set.Icc 0 1)) (hχm : Set.MapsTo χ (Set.Icc 0 1) (Set.Icc 0 1))
    (hχ0 : χ 0 = 0) (hχ1 : χ 1 = 1) (hψχ : ∀ t ∈ Set.Icc (0 : ℝ) 1, ψ (χ t) = t) :
    windingInterval (fun t => φ (ψ t)) = windingInterval φ := by sorry
Source
Hryniewicz, https://arxiv.org/html/1105.2077v5, Section 2.1.1, equations (4)–(5) (definition of the winding interval I(φ)); invariance under orientation-preserving reparametrization, used for time changes of periodic orbits as in Hofer–Wysocki–Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), https://doi.org/10.2307/120994, (3.31)–(3.32), p. 219.

View graph