The winding number differs by one across a straight segment

Letting the reference point v · (s ± h·i) + z₀ approach an interior point v · s + z₀ of the segment from the two sides as h → 0⁺, the two limits of the index integral differ by exactly 1.

For a closed piecewise-C¹ curve one of whose pieces is a straight segment, if the rest of the curve avoids an interior point p of that piece (hypothesis hp), the non-segment contribution is continuous at p, so the winding number of the whole curve differs by exactly 1 between the two sides of the segment near p: it is one larger on the side to the left of the direction of travel.

Main results

• TauCeti.Contour.tendsto_windingNumber_segment_add_mul_I and TauCeti.Contour.tendsto_windingNumber_segment_sub_mul_I — one-sided limits of the winding number at an interior point, from the left and from the right.
• TauCeti.Contour.tendsto_windingNumber_segment_sub — the difference of the winding numbers tends to 1.
• TauCeti.Contour.exists_forall_windingNumber_eq_add_one_of_eqOn_segment — a closed curve differs by one across a straight piece.

References

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

theorem TauCeti.Contour.tendsto_windingNumber_segment_add_mul_I {v z₀ : ℂ} {a b s : ℝ} (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) : Filter.Tendsto (fun (h : ℝ) => windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * (↑s + ↑h * Complex.I) + z₀)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((2 * ↑Real.pi * Complex.I)⁻¹ * (Complex.log (↑b - ↑s) - (↑(Real.log (s - a)) - ↑Real.pi * Complex.I))))

The winding number of a segment about a point approaching it from the left. For s ∈ (a, b) and h → 0⁺, the winding number about v (s + h i) + z₀ — the side to the left of the direction of travel — tends to (2πi)⁻¹ (log (b - s) - (Real.log (s - a) - πi)).

theorem TauCeti.Contour.tendsto_windingNumber_segment_sub_mul_I {v z₀ : ℂ} {a b s : ℝ} (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) : Filter.Tendsto (fun (h : ℝ) => windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * (↑s - ↑h * Complex.I) + z₀)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((2 * ↑Real.pi * Complex.I)⁻¹ * (Complex.log (↑b - ↑s) - (↑(Real.log (s - a)) + ↑Real.pi * Complex.I))))

The winding number of a segment about a point approaching it from the right. For s ∈ (a, b) and h → 0⁺, the winding number about v (s - h i) + z₀ — the side to the right of the direction of travel — tends to (2πi)⁻¹ (log (b - s) - (Real.log (s - a) + πi)).

theorem TauCeti.Contour.tendsto_windingNumber_segment_sub {v z₀ : ℂ} {a b s : ℝ} (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) : Filter.Tendsto (fun (h : ℝ) => windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * (↑s + ↑h * Complex.I) + z₀) - windingNumber (fun (t : ℝ) => v * ↑t + z₀) a b (v * (↑s - ↑h * Complex.I) + z₀)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

The jump of the winding number across a straight segment is 1. As h → 0⁺, the winding numbers about the two points v (s ± h i) + z₀ on either side of the interior point v s + z₀ differ by a quantity tending to 1: the left side minus the right side.

The jump of a closed curve across a straight piece

theorem TauCeti.Contour.exists_forall_windingNumber_eq_add_one_of_eqOn_segment {v z₀ : ℂ} {a b c s : ℝ} {Γ : ℝ → ℂ} (hΓ : IsPiecewiseC1On Γ a c) (hclosed : Γ a = Γ c) (hbc : b ≤ c) (hseg : Set.EqOn Γ (fun (t : ℝ) => v * ↑t + z₀) (Set.Icc a b)) (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) (hp : v * ↑s + z₀ ∉ Γ '' Set.Icc b c) : ∃ r > 0, ∀ w₁ ∈ Metric.ball (v * ↑s + z₀) r, ∀ w₂ ∈ Metric.ball (v * ↑s + z₀) r, 0 < ((w₁ - (v * ↑s + z₀)) / v).im → ((w₂ - (v * ↑s + z₀)) / v).im < 0 → windingNumber Γ a c w₁ = windingNumber Γ a c w₂ + 1

A closed curve jumps by one across a straight piece. Let Γ be a closed piecewise-C¹ curve on [a, c] which on [a, b] is the straight segment t ↦ v · t + z₀, and let p = v · s + z₀ with s ∈ (a, b) be a point of that segment not visited by the rest of the curve. Then on a small disc about p the winding number takes one value on the side to the left of the direction of travel and the value one less on the side to the right.