Winding-weighted Green for polygonal cycles

Every finite polygonal subdivision gives a triangle fan about any chosen center. Actual triangle Green identities sum because the radial path generators cancel. The signed indicator formula for the winding weight identifies this sum with the winding-weighted area integral. Both integrabilities are proved, including for self-intersections, repeated vertices, and degenerate or overlapping fan triangles. The fields are C¹ on the whole plane.

theorem TauCeti.Green.green_polygon_of_subdivision {γ : ℝ → ℂ} {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) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) : IntervalIntegrable (circulationFun P Q γ) MeasureTheory.volume a b ∧ MeasureTheory.Integrable (fun (z : ℂ) => windingWeight γ a b z * curl P Q z) MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, circulationFun P Q γ t = ∫ (z : ℂ), windingWeight γ a b z * curl P Q z

Circulation around a closed raw polygon on a nonuniform subdivision equals its winding-weighted curl integral. Both the boundary integrand and weighted curl are integrable.

theorem TauCeti.Green.green_polygonal {γ : ℝ → ℂ} {a b : ℝ} (hpoly : IsPolygonalOnInterval γ a b) (hclosed : γ a = γ b) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) : IntervalIntegrable (circulationFun P Q γ) MeasureTheory.volume a b ∧ MeasureTheory.Integrable (fun (z : ℂ) => windingWeight γ a b z * curl P Q z) MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, circulationFun P Q γ t = ∫ (z : ℂ), windingWeight γ a b z * curl P Q z

Winding-weighted Green for a closed raw polygonal curve and globally C¹ fields. The boundary integrand and winding-weighted curl are integrable, and their integrals agree.