The winding number vanishes far from a bounded closed curve

For a closed curve γ continuous on the compact interval Set.uIcc a b (so its image is bounded), differentiable off a countable set, with interval-integrable derivative, the generalized winding number fun w ↦ windingNumber γ a b w vanishes for every w sufficiently far from the origin: windingNumber_eventually_zero_cocompact states this as an eventual property along the cocompact filter, together with the fact that such w lie off the curve. This is the input to the Liouville step of Dixon's proof of the homology form of Cauchy's theorem (roadmap homologyCauchyTheorem): the Dixon function agrees with dixonH2 wherever the winding number is zero.

Main results

• TauCeti.Contour.windingNumber_eventually_zero_cocompact — off the curve, the winding number is eventually 0 along cocompact ℂ.

Provenance

Adapted from winding_eventually_zero_cocompact_of_lipschitz in NullHomologous.lean of the AINTLIB LeanModularForms development. The raw-function port replaces the Lipschitz derivative bound with the L¹ norm ∫ ‖deriv γ‖, so continuity on the compact interval (which bounds the image) and interval-integrability of the derivative suffice — no Lipschitz hypothesis.

theorem TauCeti.Contour.windingNumber_eventually_zero_cocompact {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} (hclosed : γ a = γ b) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) : ∀ᶠ (w : ℂ) in Filter.cocompact ℂ, (∀ t ∈ Set.uIcc a b, γ t ≠ w) ∧ windingNumber γ a b w = 0

The winding number is eventually zero far from a bounded closed curve. For a closed curve γ (γ a = γ b) continuous on Set.uIcc a b, differentiable off a countable set P, with interval-integrable derivative, every point w far enough from the origin lies off the curve and has winding number 0; equivalently, fun w ↦ (γ avoids w) ∧ windingNumber γ a b w = 0 holds eventually along cocompact ℂ. The bounded image (continuity on the compact interval) and the integer-valuedness of the winding number for a closed curve force the small far-field value to be exactly 0.