The winding number as an ordinary path integral

For an absolutely continuous path, the existing raw winding number is the normalized ordinary curve integral of the Cauchy kernel, away from the path's trace.

theorem AbsolutelyContinuousOnInterval.curveIntegrable_inv_sub_smul_id {x y w : ℂ} {p : Path x y} (hp : AbsolutelyContinuousOnInterval (⇑p.extend) 0 1) (havoid : ∀ (t : ↑(Set.Icc 0 1)), p t ≠ w) : CurveIntegrable (fun (z : ℂ) => (z - w)⁻¹ • ContinuousLinearMap.id ℂ ℂ) p

The ordinary Cauchy-kernel 1-form is curve integrable along an absolutely continuous path that avoids its pole.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_two_pi_I_inv_mul_curveIntegral {x y w : ℂ} {p : Path x y} (hp : AbsolutelyContinuousOnInterval (⇑p.extend) 0 1) (havoid : ∀ (t : ↑(Set.Icc 0 1)), p t ≠ w) : TauCeti.Contour.windingNumber (⇑p.extend) 0 1 w = (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ᶜ (z : ℂ) in p, (z - w)⁻¹ • ContinuousLinearMap.id ℂ ℂ

The winding number of an absolutely continuous path avoiding a point is its normalized ordinary curve integral of the Cauchy kernel.

theorem AbsolutelyContinuousOnInterval.windingNumber_path_symm {x y w : ℂ} {p : Path x y} (hp : AbsolutelyContinuousOnInterval (⇑p.extend) 0 1) (havoid : ∀ (t : ↑(Set.Icc 0 1)), p t ≠ w) : TauCeti.Contour.windingNumber (⇑p.symm.extend) 0 1 w = -TauCeti.Contour.windingNumber (⇑p.extend) 0 1 w

Reversing an absolutely continuous path negates its actual winding number off the trace.

theorem AbsolutelyContinuousOnInterval.windingNumber_path_trans {x y z w : ℂ} {p : Path x y} {q : Path y z} (hp : AbsolutelyContinuousOnInterval (⇑p.extend) 0 1) (hq : AbsolutelyContinuousOnInterval (⇑q.extend) 0 1) (hpavoid : ∀ (t : ↑(Set.Icc 0 1)), p t ≠ w) (hqavoid : ∀ (t : ↑(Set.Icc 0 1)), q t ≠ w) : TauCeti.Contour.windingNumber (⇑(p.trans q).extend) 0 1 w = TauCeti.Contour.windingNumber (⇑p.extend) 0 1 w + TauCeti.Contour.windingNumber (⇑q.extend) 0 1 w

Concatenating absolutely continuous paths adds their actual winding numbers away from both traces.