The universal corner cap and the external-midpoint cost

• cornerCap_volume: a triangle of side σ ≤ 1 containing a point of level 2 (for a unit level form) has volume < σ²/46 at levels ≤ 1. Applied to a corner owner and the level form of its corner cell this is |A_j ∩ H| / A < r²/23 (research proof, Lemma 2.1).
• midpoint_cost_volume: a triangle of side σ ≤ 1 containing a point of level 3/2 has volume ≥ σ²/8 at levels > 1. Applied to a side owner containing an external corner midpoint this is D_i ≥ r²/4 (Lemma 4.1).

The polynomial inequalities

theorem ConwaySoifer.cap_ineq {S p : ℝ} (hS : 1 < S) (hc : S ^ 2 - S * p + p ^ 2 ≤ 1) : 23 * (S - 1) ^ 2 < S * p

23 (S-1)² < S p on the region S² - S p + p² ≤ 1, 1 < S.

theorem ConwaySoifer.mid_ineq {S R : ℝ} (hR : R < 1 / 2) (hS : S ≤ 7 / 6) (hS12 : 1 / 2 < S) : (S - 1 / 2) ^ 2 ≤ 3 / 4 * ((S - R) * S)

(S - 1/2)² ≤ (3/4) (S - R) S when R < 1/2, 1/2 < S ≤ 7/6.

Measure bookkeeping

theorem ConwaySoifer.toReal_le_of_subset {A B : Set Point} (h : A ⊆ B) {x : ℝ} (hx : 0 ≤ x) (hB : MeasureTheory.volume B = ENNReal.ofReal x) : (MeasureTheory.volume A).toReal ≤ x

theorem ConwaySoifer.det_of_volume {a b c : Point} {σ : ℝ} (hσ : 0 < σ) (hvol : MeasureTheory.volume ((convexHull ℝ) {a, b, c}) = ENNReal.ofReal (σ ^ 2 / 2)) : |triangleDet a b c| = σ ^ 2

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

theorem ConwaySoifer.hull_level_ge {a b c : Point} (u : Point) {p : Point} (hp : p ∈ (convexHull ℝ) {a, b, c}) {m : ℝ} (ha : m ≤ cross u a) (hb : m ≤ cross u b) (hc : m ≤ cross u c) : m ≤ cross u p

The level values of a hull point lie between the minimal and maximal vertex levels.

The corner cap for a labelled triangle

theorem ConwaySoifer.cornerCap_aux {σ : ℝ} (hσ : 0 < σ) (hσ1 : σ ≤ 1) (u : Point) (hu : u ≠ 0) {a b c : Point} (hdet : triangleDet a b c ≠ 0) (hvol : MeasureTheory.volume ((convexHull ℝ) {a, b, c}) = ENNReal.ofReal (σ ^ 2 / 2)) (hid : (cross u b - cross u a) ^ 2 - (cross u b - cross u a) * (cross u c - cross u a) + (cross u c - cross u a) ^ 2 = σ ^ 2) (hab : cross u a ≤ cross u b) (hbc : cross u b ≤ cross u c) (hc2 : 2 ≤ cross u c) : (MeasureTheory.volume ((convexHull ℝ) {a, b, c} ∩ {p : Point | cross u p ≤ 1})).toReal < σ ^ 2 / 46

The midpoint cost for a labelled triangle

theorem ConwaySoifer.midpointCost_aux {σ : ℝ} (hσ : 0 < σ) (hσ1 : σ ≤ 1) (u : Point) (hu : u ≠ 0) {a b c : Point} (hdet : triangleDet a b c ≠ 0) (hvol : MeasureTheory.volume ((convexHull ℝ) {a, b, c}) = ENNReal.ofReal (σ ^ 2 / 2)) (hid : (cross u b - cross u a) ^ 2 - (cross u b - cross u a) * (cross u c - cross u a) + (cross u c - cross u a) ^ 2 = σ ^ 2) (hab : cross u a ≤ cross u b) (hbc : cross u b ≤ cross u c) (hc32 : 3 / 2 ≤ cross u c) : σ ^ 2 / 8 ≤ (MeasureTheory.volume ((convexHull ℝ) {a, b, c} ∩ {p : Point | 1 < cross u p})).toReal