Caps of a triangle cut by a line

For a triangle conv {a, b, c} and a linear level function g = cross u ·, the part above level ℓ when a, b lie at or below ℓ and c strictly above is contained in the triangle conv {c, X, Y} with X, Y the level-ℓ points of the edges ca, cb; conversely that triangle is contained in the part at or above ℓ when a, b ≤ ℓ ≤ c. Its volume is the product of the two edge fractions times the volume of the whole triangle. A level line has measure zero. These are the tools for the two area lemmas of the research proof (§2.1 and §4.1), proved in CornerCap.lean.

noncomputable def ConwaySoifer.capPoint (u : Point) (ℓ : ℝ) (c a : Point) : Point

The level-ℓ point of the segment from c towards a.

Equations

• ConwaySoifer.capPoint u ℓ c a = c + ((ConwaySoifer.cross u c - ℓ) / (ConwaySoifer.cross u c - ConwaySoifer.cross u a)) • (a - c)

theorem ConwaySoifer.cross_capPoint (u : Point) (ℓ : ℝ) (c a : Point) (h : cross u a < cross u c) : cross u (capPoint u ℓ c a) = ℓ

theorem ConwaySoifer.range_vec3 (a b c : Point) : Set.range ![a, b, c] = {a, b, c}

theorem ConwaySoifer.mem_hull3_iff {a b c : Point} (hdet : triangleDet a b c ≠ 0) (p : Point) : p ∈ (convexHull ℝ) {a, b, c} ↔ 0 ≤ baryFirst a b c p ∧ 0 ≤ barySecond a b c p ∧ baryFirst a b c p + barySecond a b c p ≤ 1

theorem ConwaySoifer.mem_hull3_of_coeffs {a b c : Point} {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t ≤ 1) : (1 - s - t) • a + s • b + t • c ∈ (convexHull ℝ) {a, b, c}

theorem ConwaySoifer.hull3_comm (a b c : Point) : (convexHull ℝ) {a, b, c} = (convexHull ℝ) {b, a, c}

theorem ConwaySoifer.hull3_rotate (a b c : Point) : (convexHull ℝ) {a, b, c} = (convexHull ℝ) {b, c, a}

theorem ConwaySoifer.cross_convex_combo (u a b c : Point) (s t : ℝ) : cross u ((1 - s - t) • a + s • b + t • c) = (1 - s - t) * cross u a + s * cross u b + t * cross u c

theorem ConwaySoifer.triangleDet_eq_cross (a b c : Point) : triangleDet a b c = cross (b - a) (c - a)

theorem ConwaySoifer.triangleDet_rotate (a b c : Point) : triangleDet b c a = triangleDet a b c

theorem ConwaySoifer.triangleDet_swap (a b c : Point) : triangleDet b a c = -triangleDet a b c

theorem ConwaySoifer.cap_subset (u : Point) (ℓ : ℝ) {a b c : Point} (hdet : triangleDet a b c ≠ 0) (ha : cross u a ≤ ℓ) (hb : cross u b ≤ ℓ) (hc : ℓ < cross u c) : (convexHull ℝ) {a, b, c} ∩ {p : Point | ℓ ≤ cross u p} ⊆ (convexHull ℝ) {c, capPoint u ℓ c a, capPoint u ℓ c b}

The cap above level ℓ is contained in the triangle c, X, Y.

theorem ConwaySoifer.cap_supset (u : Point) (ℓ : ℝ) {a b c : Point} (ha : cross u a ≤ ℓ) (hb : cross u b ≤ ℓ) (hc : ℓ < cross u c) : (convexHull ℝ) {c, capPoint u ℓ c a, capPoint u ℓ c b} ⊆ (convexHull ℝ) {a, b, c} ∩ {p : Point | ℓ ≤ cross u p}

The triangle c, X, Y lies in the part at or above level ℓ.

theorem ConwaySoifer.volume_capTriangle (u : Point) (ℓ : ℝ) (a b c : Point) : MeasureTheory.volume ((convexHull ℝ) {c, capPoint u ℓ c a, capPoint u ℓ c b}) = ENNReal.ofReal (|(cross u c - ℓ) / (cross u c - cross u a)| * |(cross u c - ℓ) / (cross u c - cross u b)| * (|triangleDet a b c| / 2))

The volume of the cap triangle.

A level line is a null set

theorem ConwaySoifer.volume_level_line (u : Point) (hu : u ≠ 0) (ℓ : ℝ) : MeasureTheory.volume {p : Point | cross u p = ℓ} = 0

theorem ConwaySoifer.volume_inter_level_line (Q : Set Point) (u : Point) (hu : u ≠ 0) (ℓ : ℝ) : MeasureTheory.volume (Q ∩ {p : Point | cross u p = ℓ}) = 0

Level values on an equilateral triangle

theorem ConwaySoifer.orientation_of_lengths {e d : Point} {σ : ℝ} (hσ : 0 < σ) (he : normSq e = σ ^ 2) (hd : normSq d = σ ^ 2) (hed : normSq (d - e) = σ ^ 2) : d = rot60 e ∨ d = rotNeg60 e

The two chiralities, for arbitrary vectors of equal length forming an equilateral triangle with their difference.

theorem ConwaySoifer.cross_rot60_identity (u e : Point) : cross u e ^ 2 - cross u e * cross u (rot60 e) + cross u (rot60 e) ^ 2 = normSq u * normSq e

theorem ConwaySoifer.cross_rotNeg60_identity (u e : Point) : cross u e ^ 2 - cross u e * cross u (rotNeg60 e) + cross u (rotNeg60 e) ^ 2 = normSq u * normSq e

theorem ConwaySoifer.level_identity (Q : EquilateralTriangle) (hσ : 0 < Q.side) (u : Point) (hu : normSq u = 1) (i j k : Fin 3) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : (cross u (Q.vertices j) - cross u (Q.vertices i)) ^ 2 - (cross u (Q.vertices j) - cross u (Q.vertices i)) * (cross u (Q.vertices k) - cross u (Q.vertices i)) + (cross u (Q.vertices k) - cross u (Q.vertices i)) ^ 2 = Q.side ^ 2

For an equilateral triangle of side σ and a level form of unit length, the differences of the level values of the vertices satisfy x² - x y + y² = σ².

theorem ConwaySoifer.cross_le_max_vertex (Q : EquilateralTriangle) (u : Point) {p : Point} (hp : p ∈ Q.carrier) : ∃ (i : Fin 3), (∀ (j : Fin 3), cross u (Q.vertices j) ≤ cross u (Q.vertices i)) ∧ cross u p ≤ cross u (Q.vertices i)

Every point of the carrier has level at most the maximal vertex level.