The winding integral for absolutely continuous curves

Off the compact trace of an absolutely continuous curve, the existing generalized winding number is its ordinary winding integral, and the winding integrand is interval integrable.

These results extend the contour index API beyond piecewise C¹ curves.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_inv_sub_mul_deriv {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) : IntervalIntegrable (fun (t : ℝ) => (γ t - z)⁻¹ * deriv γ t) MeasureTheory.volume a b

The off-curve winding integrand of an absolutely continuous curve is interval integrable.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_integral {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) : TauCeti.Contour.windingNumber γ a b z = (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (t : ℝ) in a..b, (γ t - z)⁻¹ * deriv γ t

The existing winding number agrees with the ordinary winding integral for an absolutely continuous curve away from its trace, in either orientation of the parameter interval.