Winding numbers of contour cycles off their trace

The generalized winding number of a contour cycle is defined at every point by additive extension from its closed piecewise-C¹ generators. Away from the cycle's trace, every generator is in the classical regime: its principal value is an ordinary integral and its winding number is an integer. This file transfers that classical package to finite formal ℤ-combinations of curves.

The support formula is the bridge between the free-abelian-group definition and the single-curve theory. It gives the ordinary contour-integral formula and integer-valuedness off the trace. It also shows that the cycle winding number is locally constant on the trace complement, vanishes far from the cycle, and hence vanishes on every unbounded connected component of the complement.

Main results

• TauCeti.Contour.Cycle.windingNumber_eq_integral_of_not_mem_trace identifies the winding number off the trace with the normalized ordinary cycle integral of the Cauchy kernel.
• TauCeti.Contour.Cycle.exists_int_windingNumber_of_not_mem_trace proves integer-valuedness off the trace.
• TauCeti.Contour.Cycle.isLocallyConstant_windingNumber proves local constancy on the trace complement.
• TauCeti.Contour.Cycle.windingNumber_eq_zero_of_unbounded_component proves vanishing on every unbounded component of the complement.

References

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

theorem TauCeti.Contour.Cycle.windingNumber_eq_sum_support (C : Cycle) (z : ℂ) : (windingNumber z) C = ∑ γ ∈ FreeAbelianGroup.support C, ↑((FreeAbelianGroup.coeff γ) C) * Contour.windingNumber (Function.extend Subtype.val γ.toFun 0) γ.a γ.b z

The winding number of a cycle is the coefficient-weighted sum of the winding numbers of the curves in its canonical support.

theorem TauCeti.Contour.Cycle.sum_support_smul_eq_integral_add_windingNumber_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) (g w : ℂ → E) (S : Finset ℂ) (C : Cycle) : ∑ γ ∈ FreeAbelianGroup.support C, (FreeAbelianGroup.coeff γ) C • ((∫ (t : ℝ) in γ.a..γ.b, deriv (Function.extend Subtype.val γ.toFun 0) t • g (Function.extend Subtype.val γ.toFun 0 t)) + c • ∑ s ∈ S, Contour.windingNumber (Function.extend Subtype.val γ.toFun 0) γ.a γ.b s • w s) = (integral g) C + c • ∑ s ∈ S, (windingNumber s) C • w s

A per-generator splitting resums to the cycle-level one. Summing, over the generators of a cycle and weighted by their coefficients, an integral of g plus c times a w-weighted sum of that generator's winding numbers gives the cycle integral of g plus c times the w-weighted sum of the cycle's winding numbers.

The scalar c, the integrand g and the weight w are all arbitrary; residue applications take c = 2πi. At S = ∅ both sides collapse to integral g C, and at c = 0 to the same.

theorem TauCeti.Contour.Cycle.windingNumber_eq_integral_of_not_mem_trace (C : Cycle) {z : ℂ} (hz : z ∉ C.trace) : (windingNumber z) C = (2 * ↑Real.pi * Complex.I)⁻¹ * (integral fun (w : ℂ) => (w - z)⁻¹) C

Ordinary-integral formula off the trace. At a point z outside a contour cycle's trace, the generalized winding number is the normalized ordinary cycle integral of the Cauchy kernel w ↦ (w - z)⁻¹. No principal value remains: every generator in the canonical support avoids z.

theorem TauCeti.Contour.Cycle.exists_int_windingNumber_of_not_mem_trace (C : Cycle) {z : ℂ} (hz : z ∉ C.trace) : ∃ (n : ℤ), (windingNumber z) C = ↑n

Integer-valuedness off the trace. The winding number of a contour cycle about a point outside its trace is an integer. Each supported generator has an integer winding number there, and the cycle value is their coefficient-weighted sum.

theorem TauCeti.Contour.Cycle.isLocallyConstant_windingNumber (C : Cycle) : IsLocallyConstant fun (z : { z : ℂ // z ∉ C.trace }) => (windingNumber ↑z) C

Local constancy off the trace. The winding number of a contour cycle, viewed as a function on the complement of its trace, is locally constant. This is the finite-sum extension of local constancy for the closed generator curves.

theorem TauCeti.Contour.Cycle.windingNumber_eq_of_mem_connectedComponentIn {C : Cycle} {z₀ z₁ : ℂ} (hz₁ : z₁ ∈ connectedComponentIn C.traceᶜ z₀) : (windingNumber z₁) C = (windingNumber z₀) C

The winding number of a contour cycle is constant on each connected component of the complement of its trace.

theorem TauCeti.Contour.Cycle.windingNumber_eventually_zero_cocompact (C : Cycle) : ∀ᶠ (z : ℂ) in Filter.cocompact ℂ, z ∉ C.trace ∧ (windingNumber z) C = 0

The winding number of a contour cycle eventually vanishes along the cocompact filter. The same eventual set also lies outside the cycle's trace.

theorem TauCeti.Contour.Cycle.windingNumber_eq_zero_of_unbounded_component {C : Cycle} {z : ℂ} (hcomp : ¬Bornology.IsBounded (connectedComponentIn C.traceᶜ z)) : (windingNumber z) C = 0

Vanishing on an unbounded component. If the connected component of a point in the complement of a contour cycle's trace is unbounded, then the cycle has winding number zero about that point.