Winding numbers of absolutely continuous curves

For an absolutely continuous curve avoiding a point, exponentiating its winding integral gives the endpoint ratio. Consequently the winding number of a closed absolutely continuous curve is an integer.

theorem AbsolutelyContinuousOnInterval.exp_two_pi_I_mul_windingNumber {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) : Complex.exp (2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z) = (γ b - z) / (γ a - z)

The endpoint-ratio identity for an absolutely continuous curve, with either orientation of its parameter interval.

theorem AbsolutelyContinuousOnInterval.exists_int_windingNumber {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hz : z ∉ γ '' Set.uIcc a b) : ∃ (n : ℤ), TauCeti.Contour.windingNumber γ a b z = ↑n

The winding number of a closed absolutely continuous curve is an integer off its trace.