Areas in skew coordinates

Point = ℝ × ℝ carries the product Lebesgue measure volume. Because (x, z) denotes the Euclidean point (x, (√3/2) z), the physical area of a set is (√3/2) · volume. Hence a filled equilateral triangle of side s has volume = s ^ 2 / 2 and the unit hexagon has volume = 3.

The area budget is the only place where measure theory enters the proof.

Implementation notes.

• volume on ℝ × ℝ is the product measure volume.prod volume, which is an additive Haar measure; we register that instance for Point explicitly.
• A triangle convexHull {p, q, r} is the image of the standard triangle stdTriangle = {(s, t) | 0 ≤ s, 0 ≤ t, s + t ≤ 1} under the affine map (s, t) ↦ p + s • (q - p) + t • (r - p); the linear part has determinant coordDet (q - p) (r - p) and stdTriangle has volume 1/2 (Fubini).
• The hexagon volume is computed by Fubini in the second coordinate: the horizontal section at height z ∈ [-1, 1] is the interval [-1 + |z|/2, 1 - |z|/2] of length 2 - |z|.

instance ConwaySoifer.SevenTriangles.instIsAddHaarMeasure_volume_point : MeasureTheory.volume.IsAddHaarMeasure

The product Lebesgue measure on skew coordinates is an additive Haar measure.

theorem ConwaySoifer.SevenTriangles.isCompact_carrier (T : EquilateralTriangle) : IsCompact T.carrier

theorem ConwaySoifer.SevenTriangles.isClosed_carrier (T : EquilateralTriangle) : IsClosed T.carrier

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

theorem ConwaySoifer.SevenTriangles.isClosed_unitHexagon : IsClosed unitHexagon

theorem ConwaySoifer.SevenTriangles.measurableSet_unitHexagon : MeasurableSet unitHexagon

The standard triangle and its volume

def ConwaySoifer.SevenTriangles.stdTriangle : Set Point

The standard triangle {(s, t) | 0 ≤ s, 0 ≤ t, s + t ≤ 1}.

Equations

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

theorem ConwaySoifer.SevenTriangles.isClosed_stdTriangle : IsClosed stdTriangle

theorem ConwaySoifer.SevenTriangles.convex_stdTriangle : Convex ℝ stdTriangle

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

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

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

Linear and affine images

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

The linear map (s, t) ↦ s • u + t • v.

Equations

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

theorem ConwaySoifer.SevenTriangles.linMap_apply (u v st : Point) : (linMap u v) st = st.1 • u + st.2 • v

theorem ConwaySoifer.SevenTriangles.det_linMap (u v : Point) : LinearMap.det (linMap u v) = coordDet u v

The determinant of linMap u v is the coordinate determinant coordDet u v.

theorem ConwaySoifer.SevenTriangles.volume_image_linMap (u v : Point) (s : Set Point) : MeasureTheory.volume (⇑(linMap u v) '' s) = ENNReal.ofReal |coordDet u v| * MeasureTheory.volume s

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

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

The affine map (s, t) ↦ p + s • u + t • v.

Equations

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

theorem ConwaySoifer.SevenTriangles.triMap_apply (p u v st : Point) : (triMap p u v) st = p + (linMap u v) st

theorem ConwaySoifer.SevenTriangles.triMap_image (p u v : Point) (s : Set Point) : ⇑(triMap p u v) '' s = (fun (x : Point) => p + x) '' ⇑(linMap u v) '' s

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

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

Area of a (possibly degenerate) triangle given by three vertices, in skew coordinates.

Equilateral triangles

theorem ConwaySoifer.SevenTriangles.sqDist_sub_zero (a b : Point) : sqDist (a - b) (0, 0) = sqDist a b

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

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.abs_coordDet (T : EquilateralTriangle) : |coordDet (T.vertices 1 - T.vertices 0) (T.vertices 2 - T.vertices 0)| = T.side ^ 2

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

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

The unit hexagon

theorem ConwaySoifer.SevenTriangles.unitHexagon_section (z : ℝ) : MeasureTheory.volume ((fun (x : ℝ) => (x, z)) ⁻¹' unitHexagon) = (Set.Icc (-1) 1).indicator (fun (z : ℝ) => ENNReal.ofReal (2 - |z|)) z

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

theorem ConwaySoifer.SevenTriangles.volume_unitHexagon : MeasureTheory.volume unitHexagon = 3

The area budget

theorem ConwaySoifer.SevenTriangles.area_budget (r : ℝ) (T : Configuration) (hs : ∀ (i : Fin 7), (T i).side ≤ r) (hc : CoversUnitHexagon T) : ∑ j : Fin 7, (MeasureTheory.volume ((T j).carrier \ unitHexagon)).toReal ≤ 7 * r ^ 2 / 2 - 3

The area budget: the parts of the seven triangles outside the hexagon cannot exceed the total area surplus 7 r ^ 2 / 2 - 3 (skew units; multiply by √3/2 for physical area).