Polygonal boundaries and triangle fans

Triangle boundaries are actual three-edge raw curves. Their signed path chains use the two forward edges and the negative of the diagonal, so radial edges cancel in a triangle fan. This convention agrees with traversing the third edge backwards and makes the cancellation a literal chain identity.

noncomputable def TauCeti.Green.triangleCurve (c p q : ℂ) (t : ℝ) : ℂ

The boundary of the triangle with ordered vertices c, p, q, traversed on [0,3].

Equations

• TauCeti.Green.triangleCurve c p q t = if t ≤ 1 then c + t • (p - c) else if t ≤ 2 then p + (t - 1) • (q - p) else q + (t - 2) • (c - q)

theorem TauCeti.Green.triangleCurve_eq_first (c p q : ℂ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : triangleCurve c p q t = c + t • (p - c)

The first edge of the triangle boundary.

theorem TauCeti.Green.triangleCurve_eq_second (c p q : ℂ) {t : ℝ} (ht : t ∈ Set.Icc 1 2) : triangleCurve c p q t = p + (t - 1) • (q - p)

The second edge of the triangle boundary, including its two vertices.

theorem TauCeti.Green.triangleCurve_eq_third (c p q : ℂ) {t : ℝ} (ht : t ∈ Set.Icc 2 3) : triangleCurve c p q t = q + (t - 2) • (c - q)

The third edge of the triangle boundary, including its two vertices.

@[simp]

theorem TauCeti.Green.triangleCurve_zero (c p q : ℂ) : triangleCurve c p q 0 = c

@[simp]

theorem TauCeti.Green.triangleCurve_three (c p q : ℂ) : triangleCurve c p q 3 = c

theorem TauCeti.Green.absolutelyContinuousOnInterval_triangleCurve (c p q : ℂ) : AbsolutelyContinuousOnInterval (triangleCurve c p q) 0 3

Every triangle boundary, including a degenerate one, is absolutely continuous.

theorem TauCeti.Green.image_triangleCurve (c p q : ℂ) : triangleCurve c p q '' Set.Icc 0 3 = segment ℝ c p ∪ segment ℝ p q ∪ segment ℝ q c

The trace of the triangle boundary is exactly its three closed edges.

theorem TauCeti.Green.volume_triangle_edges (c p q : ℂ) : MeasureTheory.volume (segment ℝ c p ∪ segment ℝ p q ∪ segment ℝ q c) = 0

The three triangle edges have planar area zero, without a nondegeneracy assumption.

noncomputable def TauCeti.Green.BoundaryChain.triangle (c p q : ℂ) : BoundaryChain

The signed chain around a triangle: two forward edges and the negative diagonal.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Green.BoundaryChain.triangle_def (c p q : ℂ) : triangle c p q = ofPath (Path.segment c p) + ofPath (Path.segment p q) - ofPath (Path.segment c q)

The path generators of the signed triangle boundary.

@[simp]

theorem TauCeti.Green.BoundaryChain.boundary_triangle (c p q : ℂ) : boundary (triangle c p q) = 0

noncomputable def TauCeti.Green.BoundaryChain.polygon {N : ℕ} (v : Fin (N + 1) → ℂ) : BoundaryChain

The chain of successive segments through a finite vertex sequence.

Equations

• TauCeti.Green.BoundaryChain.polygon v = ∑ i : Fin N, TauCeti.Green.BoundaryChain.ofPath (Path.segment (v i.castSucc) (v i.succ))

theorem TauCeti.Green.BoundaryChain.polygon_def {N : ℕ} (v : Fin (N + 1) → ℂ) : polygon v = ∑ i : Fin N, ofPath (Path.segment (v i.castSucc) (v i.succ))

The path generators of a polygonal chain.

theorem TauCeti.Green.BoundaryChain.boundary_polygon {N : ℕ} (v : Fin (N + 1) → ℂ) : boundary (polygon v) = Finsupp.single (v (Fin.last N)) 1 - Finsupp.single (v 0) 1

The endpoint boundary of the successive-edge chain telescopes.

theorem TauCeti.Green.BoundaryChain.sum_triangle {N : ℕ} (v : Fin (N + 1) → ℂ) (c : ℂ) : ∑ i : Fin N, triangle c (v i.castSucc) (v i.succ) = polygon v + ofPath (Path.segment c (v 0)) - ofPath (Path.segment c (v (Fin.last N)))

A triangle fan differs from the polygonal chain only by its two outer radial segments.

theorem TauCeti.Green.BoundaryChain.sum_triangle_of_closed {N : ℕ} (v : Fin (N + 1) → ℂ) (hv : v (Fin.last N) = v 0) (c : ℂ) : ∑ i : Fin N, triangle c (v i.castSucc) (v i.succ) = polygon v

For a closed vertex sequence, the fan boundary is literally the polygon boundary chain.