Prove2Me

Homotopy invariance of the winding number of a family of loops in C∖{0}\mathbb{C}\setminus\{0\}

Proved
FiniteEnergyPlane.hasLoopWind_of_continuousOn_family

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

pseudoholomorphic-curvestopologywinding-numbers

Let a≤ba\le b and let F:[a,b]×R→CF:[a,b]\times\mathbb{R}\to\mathbb{C} be continuous, such that for every λ∈[a,b]\lambda\in[a,b] the loop Fλ=F(λ,⋅)F_\lambda=F(\lambda,\cdot) is 11-periodic and never vanishes. If FaF_a has winding number k∈Zk\in\mathbb{Z}, then FλF_\lambda has winding number kk for every λ∈[a,b]\lambda\in[a,b].

This is the homotopy invariance of the winding number of loops in C∖{0}\mathbb{C}\setminus\{0\}, in the form used to compare windings of a function along circles of different radii or centres.

Formalization Note FF is F : ℝ → ℝ → ℂ; joint continuity is ContinuousOn (fun p => F p.1 p.2) (Set.Icc a b ×ˢ Set.univ). "Winding number kk" is HasLoopWind (F λ) k (a continuous 11-periodic nowhere-zero loop with a continuous argument θ\theta, θ(1)−θ(0)=2πk\theta(1)-\theta(0)=2\pi k). The case b<ab<a is vacuous.

Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
namespace FiniteEnergyPlane

/-- Homotopy invariance of the winding number. Let `F : ℝ → ℝ → ℂ` be jointly continuous on
`[a, b] × ℝ`, and for each `λ ∈ [a, b]` let `F λ` be a `1`-periodic loop in `ℂ \ {0}`. If `F a`
has winding number `k`, then every loop `F λ`, `λ ∈ [a, b]`, has winding number `k`. -/
theorem hasLoopWind_of_continuousOn_family {a b : ℝ} (F : ℝ → ℝ → ℂ)
    (hF : ContinuousOn (fun p : ℝ × ℝ => F p.1 p.2) (Set.Icc a b ×ˢ Set.univ))
    (hper : ∀ l ∈ Set.Icc a b, Function.Periodic (F l) 1)
    (h0 : ∀ l ∈ Set.Icc a b, ∀ t, F l t ≠ 0) {k : ℤ} (hk : HasLoopWind (F a) k) :
    ∀ l ∈ Set.Icc a b, HasLoopWind (F l) k := by
  sorry

end FiniteEnergyPlane
Source
Standard (degree theory of loops in C∗\mathbb{C}^*); used in U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Lemma 2.15

View graph