Continuity of the generalized winding number in the point

For a curve γ continuous on the interval with endpoints a, b whose index integrand (γ · - w₀)⁻¹ * deriv γ at an avoided point w₀ is interval-integrable, the generalized winding number fun w ↦ windingNumber γ a b w is continuous at w₀ (continuousAt_windingNumber_of_avoidance). Combined with integer-valuedness for closed curves (exists_int_windingNumber_of_closed), this yields that the winding number is locally constant on the complement of the curve — a step toward the homology form of Cauchy's theorem.

Main results

• TauCeti.Contour.continuousAt_windingNumber_of_avoidance — the generalized winding number is continuous in the point, off the curve, on an arbitrary oriented interval.

Provenance

Adapted from generalizedWindingNumber_continuousAt_of_avoids in GeneralizedWindingNumber.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on [a, b].

theorem TauCeti.Contour.continuousAt_windingNumber_of_avoidance {γ : ℝ → ℂ} {w₀ : ℂ} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w₀) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w₀)⁻¹ * deriv γ t) MeasureTheory.volume a b) : ContinuousAt (fun (w : ℂ) => windingNumber γ a b w) w₀

The generalized winding number is continuous in the point, off the curve. If γ is continuous on Set.uIcc a b, avoids w₀ there, and the index integrand (γ · - w₀)⁻¹ * deriv γ at w₀ is interval-integrable, then fun w ↦ windingNumber γ a b w is continuous at w₀, on an arbitrary oriented interval. The stated hypothesis matches windingNumber_eq_integral_of_avoidance and exists_int_windingNumber_of_closed.