Winding bounds for a straight segment

The winding real part of an oriented segment at a point strictly to its left lies between zero and one half. Positivity follows from the imaginary part of the reciprocal kernel; the logarithm formula bounds the argument increment by π. Affine reparametrization preserves the index and reversal negates it away from the segment.

theorem TauCeti.Contour.windingNumber_segment_re_mem_Ioo {p q z : ℂ} (hleft : 0 < ((z - p) / (q - p)).im) : (windingNumber (fun (t : ℝ) => p + t • (q - p)) 0 1 z).re ∈ Set.Ioo 0 (1 / 2)

A point strictly left of a directed segment has winding real part between zero and one half.

theorem TauCeti.Contour.windingNumber_segment_interval {p q z : ℂ} {a b : ℝ} (hab : a < b) (hz : z ∉ segment ℝ p q) : windingNumber (fun (t : ℝ) => p + ((t - a) / (b - a)) • (q - p)) a b z = windingNumber (fun (t : ℝ) => p + t • (q - p)) 0 1 z

An increasing affine parametrization preserves the winding number of a straight segment.

theorem TauCeti.Contour.windingNumber_segment_swap {p q z : ℂ} (hz : z ∉ segment ℝ p q) : windingNumber (fun (t : ℝ) => q + t • (p - q)) 0 1 z = -windingNumber (fun (t : ℝ) => p + t • (q - p)) 0 1 z

Reversing a straight segment negates its winding number away from that segment.