Winding numbers of loops are invariant under a shift of the parameter

Proved

FiniteEnergyPlane.hasLoopWind_comp_add

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

topologywinding-numbers

Let $f:\mathbb{R}\to\mathbb{C}\setminus\{0\}$ be a continuous $1$ -periodic loop with winding number $k\in\mathbb{Z}$ , and let $d\in\mathbb{R}$ . Then the shifted loop $t\mapsto f(t+d)$ also has winding number $k$ .

This lets a winding number be read off a reparametrized loop, for example when an asymptotic description of a curve end involves a constant phase shift.

Formalization Note "Winding number $k$ " is HasLoopWind f k: $f$ is continuous, $1$ -periodic and never $0$ , and some continuous $\theta$ with $f(t)=|f(t)|e^{i\theta(t)}$ has $\theta(1)-\theta(0)=2\pi k$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

/-- The winding number of a loop in `ℂ \ {0}` is unchanged by a shift `t ↦ t + d` of its
parameter. -/
theorem hasLoopWind_comp_add {f : ℝ → ℂ} {k : ℤ} (hf : HasLoopWind f k) (d : ℝ) :
    HasLoopWind (fun t => f (t + d)) k := by
  sorry

end FiniteEnergyPlane

Source

Standard fact on winding numbers of loops in

\mathbb{C}\setminus\{0\}

; used in U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2.4

View graph