Off-trace continuity of winding numbers for absolutely continuous curves

For an absolutely continuous curve, windingNumber γ a b is continuous at every point off its trace γ '' uIcc a b. In particular, along symmetric linear perturbations z ± h • u about an avoided point z, the difference of winding numbers tends to 0 as h → 0.

theorem AbsolutelyContinuousOnInterval.continuousAt_windingNumber {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) : ContinuousAt (TauCeti.Contour.windingNumber γ a b) z

The winding number of an absolutely continuous curve is continuous at every point off its trace, in either orientation of the parameter interval.

theorem AbsolutelyContinuousOnInterval.tendsto_windingNumber_add_smul_sub {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) (u : ℂ) : Filter.Tendsto (fun (h : ℝ) => TauCeti.Contour.windingNumber γ a b (z + h • u) - TauCeti.Contour.windingNumber γ a b (z - h • u)) (nhds 0) (nhds 0)

At a point z off the trace of an absolutely continuous curve, the difference of its winding numbers at symmetric perturbations z ± h • u tends to 0 as h → 0.