The standard triangular division

The right triangle with vertices 0, 1, and I is simultaneously a vertical and a horizontal graph cell. Its actual convex hull is identified with the graph region, and its finite directional divisions compare geometrically with the three straight edges.

noncomputable def TauCeti.Green.standardTriangle : Set ℂ

The standard closed positively oriented triangle.

Equations

• TauCeti.Green.standardTriangle = (convexHull ℝ) {0, 1, Complex.I}

theorem TauCeti.Green.standardTriangle_def : standardTriangle = (convexHull ℝ) {0, 1, Complex.I}

The triangle is the actual convex hull of its three vertices.

@[simp]

theorem TauCeti.Green.mem_standardTriangle {z : ℂ} : z ∈ standardTriangle ↔ 0 ≤ z.re ∧ 0 ≤ z.im ∧ z.re + z.im ≤ 1

Barycentric coordinates give the three half-plane inequalities of the standard triangle.

theorem TauCeti.Green.standardTriangle_eq_verticalRegion : standardTriangle = verticalRegion 0 1 (fun (x : ℝ) => 0) fun (x : ℝ) => 1 - x

The standard triangle is exactly its vertical graph cell, including the boundary.

theorem TauCeti.Green.standardTriangle_eq_horizontalRegion : standardTriangle = horizontalRegion 0 1 (fun (x : ℝ) => 0) fun (y : ℝ) => 1 - y

The same triangle has an independent horizontal graph-cell description.

def TauCeti.Green.GraphCell.standardTriangleCell : GraphCell

The continuous affine graphs presenting the standard triangle in either direction.

Equations

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

@[simp]

theorem TauCeti.Green.GraphCell.standardTriangleCell_a : standardTriangleCell.a = 0

@[simp]

theorem TauCeti.Green.GraphCell.standardTriangleCell_b : standardTriangleCell.b = 1

@[simp]

theorem TauCeti.Green.GraphCell.standardTriangleCell_lowerFun {x : ℝ} (hx : x ∈ Set.Icc 0 1) : standardTriangleCell.lowerFun x = 0

@[simp]

theorem TauCeti.Green.GraphCell.standardTriangleCell_upperFun {x : ℝ} (hx : x ∈ Set.Icc 0 1) : standardTriangleCell.upperFun x = 1 - x

@[simp]

theorem TauCeti.Green.GraphCell.region_standardTriangleCell (d : Coordinate) : standardTriangleCell.region d = standardTriangle

Both coordinate directions of the cell cover exactly the genuine triangle.

theorem TauCeti.Green.isCompact_standardTriangle : IsCompact standardTriangle

The standard triangle is compact.

def TauCeti.Green.Division.standardTriangleDivision (d : Coordinate) : Division d standardTriangle

Independent singleton divisions of the standard triangle in either coordinate direction.

Equations

• TauCeti.Green.Division.standardTriangleDivision d = { cells := {TauCeti.Green.GraphCell.standardTriangleCell}, covers := ⋯, aedisjoint := ⋯ }

@[simp]

theorem TauCeti.Green.Division.standardTriangleDivision_cells (d : Coordinate) : (standardTriangleDivision d).cells = {GraphCell.standardTriangleCell}

@[simp]

theorem TauCeti.Green.Division.boundary_standardTriangleDivision (d : Coordinate) : (standardTriangleDivision d).boundary = GraphCell.standardTriangleCell.boundary d

The triangle division has the actual four-edge cell boundary.

theorem TauCeti.Green.Division.standardTriangle_null_im (U : Set ℂ) : BoundaryChain.NullChain Coordinate.im U ((standardTriangleDivision Coordinate.im).boundary - BoundaryChain.triangle 0 1 Complex.I)

The type-II cell differs from the three-edge cycle only by a collapsed constant edge.

theorem TauCeti.Green.Division.standardTriangle_null_re {U : Set ℂ} (hU : standardTriangle ⊆ U) : BoundaryChain.NullChain Coordinate.re U ((standardTriangleDivision Coordinate.re).boundary - BoundaryChain.triangle 0 1 Complex.I)

The type-I cell compares with the same three-edge cycle by reversing the diagonal and removing a collapsed edge. The graph used for reversal is contained in the triangle.