Winding numbers add under products of loops

Proved

FiniteEnergyPlane.hasLoopWind_mul

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

complex-analysissymplectic-geometrytopologywinding-numbers

Let $f,g:\mathbb{R}\to\mathbb{C}$ be continuous $1$ -periodic nowhere-zero loops with winding numbers $k$ and $m$ . Then the pointwise product $t\mapsto f(t)g(t)$ has winding number $k+m$ .

Additivity of the winding number under multiplication, for comparing windings of loops in $\mathbb{C}\setminus\{0\}$ .

Formalization Note Hypotheses and conclusion are HasLoopWind f k, HasLoopWind g m and HasLoopWind (fun t => f t * g t) (k + m) from FiniteEnergyPlane_Winding.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

/-- Winding numbers add under pointwise multiplication of loops in `ℂ \ {0}`. -/
theorem hasLoopWind_mul {f g : ℝ → ℂ} {k m : ℤ} (hf : HasLoopWind f k)
    (hg : HasLoopWind g m) : HasLoopWind (fun t => f t * g t) (k + m) := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory (2026 notes), arXiv:1612.01009, Section 3.7 (winding numbers of loops in C minus 0); standard.

View graph