The winding number of an oriented triangle

The triangle winding number is positive or negative on the interior according to the ordered orientation and vanishes outside the convex hull, including for degenerate triangles away from their edges. These signed certificates supply the triangle indicators in finite fan identities.

theorem TauCeti.Green.windingNumber_triangleCurve_eq_sum {c p q z : ℂ} (hz : z ∉ segment ℝ c p ∪ segment ℝ p q ∪ segment ℝ q c) : Contour.windingNumber (triangleCurve c p q) 0 3 z = Contour.windingNumber (fun (t : ℝ) => c + t • (p - c)) 0 1 z + Contour.windingNumber (fun (t : ℝ) => p + t • (q - p)) 0 1 z + Contour.windingNumber (fun (t : ℝ) => q + t • (c - q)) 0 1 z

Away from the three edges, the triangle winding number is the sum of the edge windings.

theorem TauCeti.Green.windingNumber_triangleCurve_eq_one {c p q z : ℂ} (hdet : 0 < triangleDet c p q) (hz : z ∈ interior ((convexHull ℝ) {c, p, q})) : Contour.windingNumber (triangleCurve c p q) 0 3 z = 1

A positively oriented triangle winds once around every point in its interior.

theorem TauCeti.Green.windingNumber_triangleCurve_swap {c p q z : ℂ} (hz : z ∉ segment ℝ c p ∪ segment ℝ p q ∪ segment ℝ q c) : Contour.windingNumber (triangleCurve c p q) 0 3 z = -Contour.windingNumber (triangleCurve c q p) 0 3 z

Reversing the ordered vertices negates the actual triangle winding number off its edges.

theorem TauCeti.Green.windingNumber_triangleCurve_eq_neg_one {c p q z : ℂ} (hdet : triangleDet c p q < 0) (hz : z ∈ interior ((convexHull ℝ) {c, p, q})) : Contour.windingNumber (triangleCurve c p q) 0 3 z = -1

A negatively oriented triangle winds negatively once around every interior point.

theorem TauCeti.Green.windingNumber_triangleCurve_eq_zero_of_notMem_convexHull {c p q z : ℂ} (hz : z ∉ (convexHull ℝ) {c, p, q}) : Contour.windingNumber (triangleCurve c p q) 0 3 z = 0

The winding number of a triangle vanishes outside its convex hull.

theorem TauCeti.Green.windingWeight_triangleCurve_ae_eq (c p q : ℂ) : windingWeight (triangleCurve c p q) 0 3 =ᵐ[MeasureTheory.volume] fun (z : ℂ) => (triangleDet c p q).sign * (interior ((convexHull ℝ) {c, p, q})).indicator (fun (x : ℂ) => 1) z

Almost everywhere, a triangle's actual winding weight is its orientation times the indicator of its interior. Degenerate triangles contribute zero.

theorem TauCeti.Green.windingNumber_triangleCurve_eq_zero_of_degenerate {c p q z : ℂ} (hdet : triangleDet c p q = 0) (hz : z ∉ segment ℝ c p ∪ segment ℝ p q ∪ segment ℝ q c) : Contour.windingNumber (triangleCurve c p q) 0 3 z = 0

A degenerate triangle has winding number zero at every point off its three edges.