Green's theorem for degenerate triangles

Collinear triangle edges are interval integrals of one common line coefficient. Their circulations telescope for every continuous field. The degenerate convex hull has zero area, so this completes the oriented triangle formula, including repeated vertices and edges.

theorem TauCeti.Green.curveIntegral_triangle_eq_zero_of_det_eq_zero {c p q : ℂ} (hdet : triangleDet c p q = 0) {P Q : ℂ → ℝ} (hP : ContinuousOn P ((convexHull ℝ) {c, p, q})) (hQ : ContinuousOn Q ((convexHull ℝ) {c, p, q})) : curveIntegral (oneForm P Q) (Path.segment c p) + curveIntegral (oneForm P Q) (Path.segment p q) - curveIntegral (oneForm P Q) (Path.segment c q) = 0

Every continuous field has zero circulation around a degenerate ordered triangle. This includes arbitrary backtracking and repeated vertices.

theorem TauCeti.Green.green_triangle_of_det_eq_zero {c p q : ℂ} (hdet : triangleDet c p q = 0) {P Q : ℂ → ℝ} (hP : ContinuousOn P ((convexHull ℝ) {c, p, q})) (hQ : ContinuousOn Q ((convexHull ℝ) {c, p, q})) : MeasureTheory.IntegrableOn (curl P Q) ((convexHull ℝ) {c, p, q}) MeasureTheory.volume ∧ curveIntegral (oneForm P Q) (Path.segment c p) + curveIntegral (oneForm P Q) (Path.segment p q) - curveIntegral (oneForm P Q) (Path.segment c q) = 0 ∧ ∫ (z : ℂ) in (convexHull ℝ) {c, p, q}, curl P Q z = 0

Degenerate triangle Green for continuous fields: both the actual circulation and every area integral vanish. Area integrability follows from the null convex hull.

theorem TauCeti.Green.green_triangle (c p q : ℂ) {U : Set ℂ} (hU : IsOpen U) (hTU : (convexHull ℝ) {c, p, q} ⊆ U) {P Q : ℂ → ℝ} (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) : MeasureTheory.IntegrableOn (curl P Q) ((convexHull ℝ) {c, p, q}) MeasureTheory.volume ∧ curveIntegral (oneForm P Q) (Path.segment c p) + curveIntegral (oneForm P Q) (Path.segment p q) - curveIntegral (oneForm P Q) (Path.segment c q) = (triangleDet c p q).sign * ∫ (z : ℂ) in (convexHull ℝ) {c, p, q}, curl P Q z

Green's theorem for every ordered triangle and fields that are C¹ on an open neighborhood, including collinear and repeated vertices. The determinant sign agrees with the triangle's winding orientation.