The winding number of a straight segment

The winding number of the straight segment t ↦ v · t + z₀ about a point not on it is the logarithmic increment (2πi)⁻¹ (log (b - q) - log (a - q)), valid whenever (t : ℂ) ≠ q for t ∈ [a, b].

This extends the segment winding API (Segment/Basic.lean) with the explicit formula for a single straight piece. The formula is a building block for the winding decomposition of HW Proposition 2.2.

Main results

• TauCeti.Contour.windingNumber_segment — the winding number formula for a straight segment, under a slit-plane hypothesis.
• TauCeti.Contour.windingNumber_segment_of_im_ne_zero — specialization when the reference point has nonzero imaginary part.
• TauCeti.Contour.windingNumber_segment_of_ne — the formula under the natural avoidance hypothesis (t : ℂ) ≠ q, covering real reference points on both sides.

References

• L. Ahlfors, Complex Analysis, Chapter 4, §2.1.

theorem TauCeti.Contour.windingNumber_segment {v z₀ q : ℂ} {a b : ℝ} (hv : v ≠ 0) (hslit : ∀ t ∈ Set.uIcc a b, ↑t - q ∈ Complex.slitPlane) : windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * q + z₀) = (2 * ↑Real.pi * Complex.I)⁻¹ * (Complex.log (↑b - q) - Complex.log (↑a - q))

The winding number of a straight segment about a point beside it is the increment of the principal logarithm, valid whenever (t : ℂ) - q lies in the slit plane throughout [a, b]. This covers both the nonreal case (q.im ≠ 0) and real points below the segment (q.re < min a b).

theorem TauCeti.Contour.windingNumber_segment_of_im_ne_zero {v z₀ q : ℂ} {a b : ℝ} (hv : v ≠ 0) (hq : q.im ≠ 0) : windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * q + z₀) = (2 * ↑Real.pi * Complex.I)⁻¹ * (Complex.log (↑b - q) - Complex.log (↑a - q))

The winding number of a straight segment about a nonreal point. Specialization of windingNumber_segment when q.im ≠ 0, which guarantees the slit-plane condition.

theorem TauCeti.Contour.windingNumber_segment_of_ne {v z₀ q : ℂ} {a b : ℝ} (hv : v ≠ 0) (hne : ∀ t ∈ Set.uIcc a b, ↑t ≠ q) : windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * q + z₀) = (2 * ↑Real.pi * Complex.I)⁻¹ * (Complex.log (↑b - q) - Complex.log (↑a - q))

The winding number formula under the natural avoidance hypothesis. The formula (2πi)⁻¹ (log (b - q) - log (a - q)) holds whenever the affine-parametrised reference point avoids the segment, with no restriction to the slit plane. For nonreal q the slit-plane condition is automatic; for real q beyond the far endpoint, both Complex.log terms share the branch offset πi, which cancels in the difference.