The generalized winding number of a straight segment through the point

A straight segment traversed symmetrically through its reference point contributes nothing to the generalized winding number about that point. The mechanism is oddness: for the real inclusion γ t = t on [-R, R], the index integrand γ' t / (γ t - 0) = 1 / t is odd, so every ε-truncated integral over the symmetric interval vanishes identically — not merely in the limit — and the principal value is 0 with no limiting argument at all. The general segment γ t = v · t + z₀ about z₀ then follows by transporting along the affine change of coordinates of Winding/Number/Affine.lean; the degenerate direction v = 0 (the constant curve at z₀) is included, since there every positive-radius truncation is identically zero.

This is the on-curve counterpart of the arc computations in Winding/Number/Circle.lean, which compute the winding of an arc about its centre, a point off the curve. Together they supply the two pieces of an indented contour: a diameter through the singularity contributes 0, and the semicircular arc about it contributes ½ (windingNumber_at_i) — the windingNumber = 1/2 input of the Hungerbühler–Wasem half-residue theorem hasCauchyPV_half_residue.

Main results

• TauCeti.Contour.hasCauchyPVAt_inv_sub_segment, TauCeti.Contour.cauchyPVExistsAt_inv_sub_segment and TauCeti.Contour.windingNumber_eq_zero_segment — an arbitrary straight segment v · t + z₀ traversed symmetrically through z₀ has index principal value and winding number 0 about z₀. The real-axis case through the origin is the private base case from which the general one is transported.

References

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

theorem TauCeti.Contour.hasCauchyPVAt_inv_sub_segment (v z₀ : ℂ) (R : ℝ) : HasCauchyPVAt (fun (t : ℝ) => v * ↑t + z₀) (-R) R (fun (z : ℂ) => (z - z₀)⁻¹) z₀ 0

A straight segment through its reference point has vanishing index principal value. The segment γ t = v · t + z₀ traversed over the symmetric interval [-R, R] passes through z₀ at t = 0, and the principal value of ∫_γ dz / (z - z₀) along it is 0. For v ≠ 0 this is the real-axis case transported by the affine change of coordinates; for v = 0 the curve is constant at z₀, so every positive-radius truncation is identically zero.

theorem TauCeti.Contour.cauchyPVExistsAt_inv_sub_segment (v z₀ : ℂ) (R : ℝ) : CauchyPVExistsAt (fun (t : ℝ) => v * ↑t + z₀) (-R) R (fun (z : ℂ) => (z - z₀)⁻¹) z₀

Existence form of hasCauchyPVAt_inv_sub_segment, matching the existence-form API of the adjacent scaling and affine coordinate changes.

@[simp]

theorem TauCeti.Contour.windingNumber_eq_zero_segment (v z₀ : ℂ) (R : ℝ) : windingNumber (fun (t : ℝ) => v * ↑t + z₀) (-R) R z₀ = 0

The winding number of a straight segment through its reference point vanishes.