Winding-number jump across a regular point of an absolutely continuous curve

If an absolutely continuous curve γ on [a, b] (a < b) is differentiable at an interior parameter t₀ ∈ (a, b) with nonzero derivative v ≠ 0 and visits γ t₀ nowhere else on [a, b], then the difference of winding numbers across the normal line at γ t₀, windingNumber γ a b (γ t₀ + h • (I * v)) - windingNumber γ a b (γ t₀ - h • (I * v)), tends to 1 as h → 0⁺. When γ is closed (γ a = γ b), integer-valuedness of the off-trace winding number upgrades this limit to exact equality = + 1 for all sufficiently small h > 0.

Unlike TauCeti.Contour.exists_forall_windingNumber_eq_add_one_of_eqOn_segment, the curve need not contain a straight segment: near t₀ the Fréchet derivative confines both γ and a three-piece polygonal tangent replacement to the complement of each normal ray γ t₀ ± (0, ∞) • (I * v), which is star-shaped about γ t₀. Star-convex homotopy invariance replaces the local arc of γ by that polygonal replacement, reducing the jump to tendsto_windingNumber_segment_sub.

Main results

• AbsolutelyContinuousOnInterval.tendsto_windingNumber_add_I_mul_sub: the normal-crossing difference of winding numbers tends to 1 as h → 0⁺.
• AbsolutelyContinuousOnInterval.eventually_windingNumber_add_I_mul_eq_add_one_of_forall_eq: for a closed absolutely continuous curve visiting γ t₀ only at t₀, the winding number on the left normal ray eventually exceeds that on the right normal ray by 1.
• AbsolutelyContinuousOnInterval.eventually_windingNumber_add_I_mul_eq_add_one: specialization to simple closed absolutely continuous curves (InjOn γ (Ico a b)).

References

• L. Ahlfors, Complex Analysis, Chapter 4, §2.
• R. B. Burckel, An Introduction to Classical Complex Analysis, Vol. 1, Chapter IV.

theorem AbsolutelyContinuousOnInterval.tendsto_windingNumber_add_I_mul_sub {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) (huniq : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) : (∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ + h • (Complex.I * v) ∉ γ '' Set.uIcc a b ∧ γ t₀ - h • (Complex.I * v) ∉ γ '' Set.uIcc a b) ∧ Filter.Tendsto (fun (h : ℝ) => TauCeti.Contour.windingNumber γ a b (γ t₀ + h • (Complex.I * v)) - TauCeti.Contour.windingNumber γ a b (γ t₀ - h • (Complex.I * v))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Normal-crossing jump of the winding number at a regular interior point. Let γ be an absolutely continuous curve on [a, b] (a < b) that is differentiable at t₀ ∈ (a, b) with nonzero derivative v ≠ 0 and visits γ t₀ nowhere else on [a, b]. Then the winding-number difference between γ t₀ + h • (I * v) (to the left of v) and γ t₀ - h • (I * v) (to the right of v) tends to 1 as h → 0⁺, and both normal test points eventually lie off the trace.

theorem AbsolutelyContinuousOnInterval.eventually_windingNumber_add_I_mul_eq_add_one_of_forall_eq {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) (huniq : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ + h • (Complex.I * v) ∉ γ '' Set.uIcc a b ∧ γ t₀ - h • (Complex.I * v) ∉ γ '' Set.uIcc a b ∧ TauCeti.Contour.windingNumber γ a b (γ t₀ + h • (Complex.I * v)) = TauCeti.Contour.windingNumber γ a b (γ t₀ - h • (Complex.I * v)) + 1

Exact +1 winding-number jump across a regular interior point of a closed AC curve. If γ is closed on [a, b] (a < b), differentiable at t₀ ∈ (a, b) with v ≠ 0, and visits γ t₀ only at t₀, then for all sufficiently small h > 0, both γ t₀ ± h • (I * v) miss the trace and windingNumber γ a b (γ t₀ + h • (I * v)) = windingNumber γ a b (γ t₀ - h • (I * v)) + 1.

theorem AbsolutelyContinuousOnInterval.eventually_windingNumber_add_I_mul_eq_add_one {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ + h • (Complex.I * v) ∉ γ '' Set.uIcc a b ∧ γ t₀ - h • (Complex.I * v) ∉ γ '' Set.uIcc a b ∧ TauCeti.Contour.windingNumber γ a b (γ t₀ + h • (Complex.I * v)) = TauCeti.Contour.windingNumber γ a b (γ t₀ - h • (Complex.I * v)) + 1

Exact +1 winding-number jump across a regular interior point of a simple closed AC curve. For a simple closed absolutely continuous curve (InjOn γ (Ico a b) and γ a = γ b), at any interior point t₀ ∈ (a, b) where HasDerivAt γ v t₀ with v ≠ 0, the winding number at γ t₀ + h • (I * v) eventually equals that at γ t₀ - h • (I * v) plus 1.