Lebesgue area in triangular coordinates. Physical area is sqrt(3)/2 times this measure, so dividing physical area by sqrt(3)/4 amounts to multiplying volume.toReal by two. The standard-simplex integration and affine image argument are adapted from SevenTriangles/Geometry/Area.lean, pinned commit b17ca52a395519f43fc15f83fb49a5dd69996225. The ten-owner budget explicitly keeps the corner triangles' contributions inside H.

instance ConwaySoifer.instIsAddHaarMeasure_volume_point : MeasureTheory.volume.IsAddHaarMeasure

theorem ConwaySoifer.EquilateralTriangle.measurableSet_carrier (T : EquilateralTriangle) : MeasurableSet T.carrier

theorem ConwaySoifer.isClosed_hexagon : IsClosed hexagon

theorem ConwaySoifer.measurableSet_hexagon : MeasurableSet hexagon

def ConwaySoifer.stdTriangle : Set Point

The filled standard simplex with nonnegative coordinates summing to at most one.

Equations

• ConwaySoifer.stdTriangle = {st : ConwaySoifer.Point | 0 ≤ st.1 ∧ 0 ≤ st.2 ∧ st.1 + st.2 ≤ 1}

theorem ConwaySoifer.isClosed_stdTriangle : IsClosed stdTriangle

theorem ConwaySoifer.convex_stdTriangle : Convex ℝ stdTriangle

theorem ConwaySoifer.stdTriangle_eq_convexHull : stdTriangle = (convexHull ℝ) {(0, 0), (1, 0), (0, 1)}

theorem ConwaySoifer.stdTriangle_section (x : ℝ) : MeasureTheory.volume (Prod.mk x ⁻¹' stdTriangle) = (Set.Icc 0 1).indicator (fun (x : ℝ) => ENNReal.ofReal (1 - x)) x

theorem ConwaySoifer.volume_stdTriangle : MeasureTheory.volume stdTriangle = ENNReal.ofReal (1 / 2)

def ConwaySoifer.areaLinMap (u v : Point) : Point →ₗ[ℝ] Point

The linear map with specified edge vectors as its columns.

Equations

• ConwaySoifer.areaLinMap u v = (LinearMap.fst ℝ ℝ ℝ).smulRight u + (LinearMap.snd ℝ ℝ ℝ).smulRight v

theorem ConwaySoifer.areaLinMap_apply (u v st : Point) : (areaLinMap u v) st = st.1 • u + st.2 • v

theorem ConwaySoifer.det_areaLinMap (u v : Point) : LinearMap.det (areaLinMap u v) = cross u v

theorem ConwaySoifer.volume_image_areaLinMap (u v : Point) (s : Set Point) : MeasureTheory.volume (⇑(areaLinMap u v) '' s) = ENNReal.ofReal |cross u v| * MeasureTheory.volume s

theorem ConwaySoifer.volume_image_add_left (p : Point) (s : Set Point) : MeasureTheory.volume ((fun (x : Point) => p + x) '' s) = MeasureTheory.volume s

def ConwaySoifer.areaTriMap (p u v : Point) : Point →ᵃ[ℝ] Point

The affine map from the standard simplex to a triangle with specified base and edges.

Equations

• ConwaySoifer.areaTriMap p u v = { toFun := fun (st : ConwaySoifer.Point) => p + (ConwaySoifer.areaLinMap u v) st, linear := ConwaySoifer.areaLinMap u v, map_vadd' := ⋯ }

theorem ConwaySoifer.areaTriMap_apply (p u v st : Point) : (areaTriMap p u v) st = p + (areaLinMap u v) st

theorem ConwaySoifer.areaTriMap_image (p u v : Point) (s : Set Point) : ⇑(areaTriMap p u v) '' s = (fun (x : Point) => p + x) '' ⇑(areaLinMap u v) '' s

theorem ConwaySoifer.convexHull_triple_eq_image (p q r : Point) : (convexHull ℝ) {p, q, r} = ⇑(areaTriMap p (q - p) (r - p)) '' stdTriangle

theorem ConwaySoifer.volume_triangle (p q r : Point) : MeasureTheory.volume ((convexHull ℝ) {p, q, r}) = ENNReal.ofReal (|cross (q - p) (r - p)| / 2)

theorem ConwaySoifer.EquilateralTriangle.range_vertices (T : EquilateralTriangle) : Set.range T.vertices = {T.vertices 0, T.vertices 1, T.vertices 2}

theorem ConwaySoifer.EquilateralTriangle.abs_det (T : EquilateralTriangle) : |cross (T.vertices 1 - T.vertices 0) (T.vertices 2 - T.vertices 0)| = T.side ^ 2

theorem ConwaySoifer.EquilateralTriangle.volume_carrier (T : EquilateralTriangle) : MeasureTheory.volume T.carrier = ENNReal.ofReal (T.side ^ 2 / 2)

theorem ConwaySoifer.EquilateralTriangle.volume_carrier_lt_top (T : EquilateralTriangle) : MeasureTheory.volume T.carrier < ⊤

theorem ConwaySoifer.hexagon_section (b : ℝ) : MeasureTheory.volume ((fun (a : ℝ) => (a, b)) ⁻¹' hexagon) = (Set.Icc (-1) 1).indicator (fun (b : ℝ) => ENNReal.ofReal (2 - |b|)) b

theorem ConwaySoifer.integral_two_sub_abs : ∫ (z : ℝ) in -1..1, 2 - |z| = 3

theorem ConwaySoifer.volume_hexagon : MeasureTheory.volume hexagon = 3

theorem ConwaySoifer.sum_ten_decompose (f : Fin 10 → ℝ) : ∑ i : Fin 10, f i = f 0 + ∑ i : Fin 6, f (sideIndex i) + ∑ j : Fin 3, f (cornerIndex j)

noncomputable def ConwaySoifer.AnchoredCover.outside {r : ℝ} (C : AnchoredCover r) (i : Fin 6) : ℝ

Twice the area of a side owner outside the central hexagon.

Equations

• C.outside i = 2 * (MeasureTheory.volume ((C.sideOwner i).carrier \ ConwaySoifer.hexagon)).toReal

noncomputable def ConwaySoifer.AnchoredCover.cornerHelp {r : ℝ} (C : AnchoredCover r) (j : Fin 3) : ℝ

Twice the area of a corner owner inside the central hexagon.

Equations

• C.cornerHelp j = 2 * (MeasureTheory.volume ((C.cornerOwner j).carrier ∩ ConwaySoifer.hexagon)).toReal

theorem ConwaySoifer.AnchoredCover.area_budget {r : ℝ} (C : AnchoredCover r) : ∑ i : Fin 6, C.outside i ≤ 7 * r ^ 2 - 6 + ∑ j : Fin 3, C.cornerHelp j

This inequality follows from actual Lebesgue measure of the full cover. The corner contribution is retained; no non-overlap assumption is made.