Winding weights of polygonal triangle fans

The actual winding number of a raw polygonal curve is the sum of the windings of its finite straight edges. Adding the two radial edges of each triangle leaves this sum unchanged for a closed polygon. Triangle edges have planar area zero, so this gives the almost-everywhere signed indicator identity, with no hypothesis bounding the winding number.

theorem TauCeti.Green.windingNumber_eq_sum_polygon_segments {γ : ℝ → ℂ} {a b : ℝ} {N : ℕ} {s : Fin (N + 1) → ℝ} (hs : StrictMono s) (ha : s 0 = a) (hb : s (Fin.last N) = b) (hsegments : ∀ (i : Fin N), ∀ t ∈ Set.Icc (s i.castSucc) (s i.succ), γ t = γ (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (γ (s i.succ) - γ (s i.castSucc))) {z : ℂ} (hz : z ∉ γ '' Set.uIcc a b) : Contour.windingNumber γ a b z = ∑ i : Fin N, Contour.windingNumber (fun (t : ℝ) => γ (s i.castSucc) + t • (γ (s i.succ) - γ (s i.castSucc))) 0 1 z

The winding number of an absolutely continuous raw polygonal curve is the sum of its successive straight-edge winding numbers, on its given nonuniform subdivision.

theorem TauCeti.Green.windingNumber_eq_sum_triangleCurve {γ : ℝ → ℂ} {a b : ℝ} {N : ℕ} {s : Fin (N + 1) → ℝ} (hs : StrictMono s) (ha : s 0 = a) (hb : s (Fin.last N) = b) (hsegments : ∀ (i : Fin N), ∀ t ∈ Set.Icc (s i.castSucc) (s i.succ), γ t = γ (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (γ (s i.succ) - γ (s i.castSucc))) (hclosed : γ a = γ b) (c : ℂ) {z : ℂ} (hz : z ∉ γ '' Set.uIcc a b) (hzi : ∀ (i : Fin N), z ∉ segment ℝ c (γ (s i.castSucc)) ∪ segment ℝ (γ (s i.castSucc)) (γ (s i.succ)) ∪ segment ℝ (γ (s i.succ)) c) : Contour.windingNumber γ a b z = ∑ i : Fin N, Contour.windingNumber (triangleCurve c (γ (s i.castSucc)) (γ (s i.succ))) 0 3 z

Away from the polygon trace and all fan edges, the actual complex winding number of a closed raw polygon is the sum of the actual triangle winding numbers.

theorem TauCeti.Green.windingWeight_eq_sum_triangleCurve {γ : ℝ → ℂ} {a b : ℝ} {N : ℕ} {s : Fin (N + 1) → ℝ} (hs : StrictMono s) (ha : s 0 = a) (hb : s (Fin.last N) = b) (hsegments : ∀ (i : Fin N), ∀ t ∈ Set.Icc (s i.castSucc) (s i.succ), γ t = γ (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (γ (s i.succ) - γ (s i.castSucc))) (hclosed : γ a = γ b) (c : ℂ) : windingWeight γ a b =ᵐ[MeasureTheory.volume] fun (z : ℂ) => ∑ i : Fin N, windingWeight (triangleCurve c (γ (s i.castSucc)) (γ (s i.succ))) 0 3 z

For a closed raw polygon, the actual winding weight is almost everywhere the sum of the actual winding weights of the triangles in any fan.

theorem TauCeti.Green.windingWeight_eq_triangle_fan {γ : ℝ → ℂ} {a b : ℝ} {N : ℕ} {s : Fin (N + 1) → ℝ} (hs : StrictMono s) (ha : s 0 = a) (hb : s (Fin.last N) = b) (hsegments : ∀ (i : Fin N), ∀ t ∈ Set.Icc (s i.castSucc) (s i.succ), γ t = γ (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (γ (s i.succ) - γ (s i.castSucc))) (hclosed : γ a = γ b) (c : ℂ) : windingWeight γ a b =ᵐ[MeasureTheory.volume] fun (z : ℂ) => ∑ i : Fin N, (triangleDet c (γ (s i.castSucc)) (γ (s i.succ))).sign * (interior ((convexHull ℝ) {c, γ (s i.castSucc), γ (s i.succ)})).indicator (fun (x : ℂ) => 1) z

The winding weight of a closed raw polygon is almost everywhere the signed indicator sum of the interiors of its fan triangles, including degenerate and overlapping triangles.