The winding number on the unbounded component

For a closed curve γ, the winding number is constant on every connected component of the complement of the curve. If such a component is unbounded, it contains a point outside the compact set on which the far-field vanishing theorem gives no information. At that point the winding number is zero, and componentwise constancy transports the value back to every point of the component.

This proves the final part of the classical off-curve winding package in Layer 0 of the contour integration roadmap: the winding number is zero on the unbounded component.

Main results

• TauCeti.Contour.windingNumber_eq_zero_of_unbounded_component — the winding number vanishes on every unbounded component of the curve complement.
• TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_zero_of_unbounded_component — the direct piecewise-C¹ form.
• TauCeti.Contour.IsPiecewiseC1On.isNullHomologous_of_filledHull_subset — every closed curve in a set without holes, one whose complement has no bounded connected component, is null-homologous there.

References

• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Section 2.

theorem TauCeti.Contour.windingNumber_eq_zero_of_unbounded_component {γ : ℝ → ℂ} {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 : ℂ} (hcomp : ¬Bornology.IsBounded (connectedComponentIn (γ '' Set.uIcc a b)ᶜ w)) : windingNumber γ a b w = 0

The winding number vanishes on every unbounded component of the curve complement. For a closed curve with the usual off-curve regularity, if the connected component of w in ℂ \ γ '' [[a, b]] is unbounded, then the winding number about w is zero. Unboundedness also ensures that w lies outside the curve.

Indeed, far-field vanishing holds outside some compact set. An unbounded component cannot be contained in that compact set, so it contains a far-field point with winding number zero; the winding number is constant on the component.

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

Piecewise-C¹ form of vanishing on the unbounded component. If the component of w in the complement of a closed piecewise-C¹ curve is unbounded, its winding number about w is zero. The finite breakpoint set supplies all raw regularity hypotheses of windingNumber_eq_zero_of_unbounded_component.

theorem TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_zero_of_ray {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) {w v : ℂ} (hv : v ≠ 0) (hray : ∀ (c : ℝ), 0 ≤ c → w + ↑c * v ∉ γ '' Set.uIcc a b) : windingNumber γ a b w = 0

The winding number vanishes at a point joined to infinity by a ray off the curve. If the ray c ↦ w + c · v (0 ≤ c, v ≠ 0) misses the closed curve, then w lies in an unbounded component of the complement and the winding number about w is zero.

This is the form callers can actually discharge: exhibiting one escape ray is elementary, whereas IsPiecewiseC1On.windingNumber_eq_zero_of_unbounded_component asks for the component itself. Any point outside a bounded region the curve encloses -- outside a disc containing the curve, or on the far side of a line the curve does not cross -- has such a ray.

theorem TauCeti.Contour.IsPiecewiseC1On.isNullHomologous_of_filledHull_subset {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (hγU : Set.MapsTo γ (Set.uIcc a b) U) (hU : filledHull U ⊆ U) : IsNullHomologous γ a b U

A closed curve in a set without holes is null-homologous there. If filledHull U ⊆ U, that is, if every connected component of ℂ \ U is unbounded, then every closed piecewise-C¹ curve in U has winding number zero about every point outside U. For open U, the hypothesis is the plane form of the connectedness of the complement of U in the Riemann sphere.