Winding numbers of absolutely continuous curves on unbounded components

A closed absolutely continuous curve has winding number zero sufficiently far from its trace. Local constancy then gives vanishing on every unbounded connected component of the complement.

theorem AbsolutelyContinuousOnInterval.windingNumber_eventually_zero_cocompact {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) : ∀ᶠ (z : ℂ) in Filter.cocompact ℂ, z ∉ γ '' Set.uIcc a b ∧ TauCeti.Contour.windingNumber γ a b z = 0

The winding number of a closed absolutely continuous curve is zero sufficiently far from the origin, and such points lie off its trace.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_zero_of_unbounded_component {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) {z : ℂ} (hz : ¬Bornology.IsBounded (connectedComponentIn (γ '' Set.uIcc a b)ᶜ z)) : TauCeti.Contour.windingNumber γ a b z = 0

The winding number of a closed absolutely continuous curve vanishes on every unbounded component of the complement of its trace.