LeanPool.Rupert.Cube

Imported Lean Pool material for LeanPool.Rupert.Cube.

def Cube.cube : Fin 8 → ℝ³

Vertices of the cube centered at the origin with side length 2.

Equations

• Cube.cube = ![!₂[1, 1, 1], !₂[1, -1, 1], !₂[-1, -1, 1], !₂[-1, 1, 1], !₂[1, 1, -1], !₂[1, -1, -1], !₂[-1, -1, -1], !₂[-1, 1, -1]]

@[reducible, inline]

noncomputable abbrev Cube.outerRotDenorm : Matrix (Fin 3) (Fin 3) ℝ

Denormalized rotation matrix used for the outer cube shadow.

Equations

• Cube.outerRotDenorm = !![0, -√3, √3; 2, -1, -1; √2, √2, √2]

@[reducible, inline]

noncomputable abbrev Cube.outerRot : Matrix (Fin 3) (Fin 3) ℝ

Normalized rotation matrix used for the outer cube shadow.

Equations

• Cube.outerRot = (1 / √6) • Cube.outerRotDenorm

theorem Cube.two_three_six : √3 * √2 = √6

theorem Cube.outerRot_so3 : outerRot ∈ SO3

def Cube.outerShadow : Set ℝ²

Projection of the rotated cube vertices for the outer shadow.

Equations

• Cube.outerShadow = {x : ℝ² | ∃ (i : Fin 8), projXy ((Matrix.toEuclideanLin Cube.outerRot) (Cube.cube i)) = x}

def Cube.outerShadowDenorm : Set ℝ²

Projection of the denormalized rotated cube vertices for the outer shadow.

Equations

• Cube.outerShadowDenorm = {x : ℝ² | ∃ (i : Fin 8), projXy ((Matrix.toEuclideanLin Cube.outerRotDenorm) (Cube.cube i)) = x}

noncomputable def Cube.outerShadowPointsDenorm : Fin 8 → ℝ²

Denormalized outer-shadow vertices of the cube.

Equations

• Cube.outerShadowPointsDenorm = ![!₂[0, 0], !₂[√3 * 2, 2], !₂[√3 * 2, -2], !₂[0, -4], !₂[-√3 * 2, 2], !₂[0, 4], !₂[0, 0], !₂[-√3 * 2, -2]]

theorem Cube.outerShadow_points_in_shadow (i : Fin 8) : (1 / √6) • outerShadowPointsDenorm i ∈ outerShadow

noncomputable def Cube.rpp : ℝ²

Upper-right point of the rectangle inside the outer shadow convex hull.

Equations

• Cube.rpp = (3 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 1 + (1 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 5

theorem Cube.rpp_in_shadow : rpp ∈ (convexHull ℝ) outerShadow

theorem Cube.rpp_contains_cube : 1 < rpp.ofLp 0 ∧ 1 < rpp.ofLp 1

theorem Cube.rpp_contains_cube2 : -1 < rpp.ofLp 0 ∧ -1 < rpp.ofLp 1

noncomputable def Cube.rpn : ℝ²

Lower-right point of the rectangle inside the outer shadow convex hull.

Equations

• Cube.rpn = (3 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 2 + (1 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 3

theorem Cube.rpn_in_shadow : rpn ∈ (convexHull ℝ) outerShadow

noncomputable def Cube.rnp : ℝ²

Upper-left point of the rectangle inside the outer shadow convex hull.

Equations

• Cube.rnp = (3 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 4 + (1 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 5

theorem Cube.rnp_in_shadow : rnp ∈ (convexHull ℝ) outerShadow

noncomputable def Cube.rnn : ℝ²

Lower-left point of the rectangle inside the outer shadow convex hull.

Equations

• Cube.rnn = (3 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 7 + (1 / 4) • (1 / √6) • Cube.outerShadowPointsDenorm 3

theorem Cube.rnn_in_shadow : rnn ∈ (convexHull ℝ) outerShadow

theorem Cube.rnn_contains_cube : -1 > rnn.ofLp 0 ∧ -1 > rnn.ofLp 1

theorem Cube.rnn_contains_cube2 : rnn.ofLp 0 < 1 ∧ rnn.ofLp 1 < 1

def Cube.extract (v : ℝ²) : ℝ × ℝ

Converts a vector in ℝ² to its coordinate pair.

Equations

• Cube.extract v = (v.ofLp 0, v.ofLp 1)

def Cube.inject (v : ℝ × ℝ) : ℝ²

Converts a coordinate pair into a vector in ℝ².

Equations

• Cube.inject v = !₂[v.1, v.2]

def Cube.openRectangle (xmin xmax ymin ymax : ℝ) : Set ℝ²

Open axis-aligned rectangle in ℝ².

Equations

• Cube.openRectangle xmin xmax ymin ymax = Cube.inject '' Set.Ioo xmin xmax ×ˢ Set.Ioo ymin ymax

def Cube.closedRectangle (xmin xmax ymin ymax : ℝ) : Set ℝ²

Closed axis-aligned rectangle in ℝ².

Equations

• Cube.closedRectangle xmin xmax ymin ymax = Cube.inject '' Set.Icc xmin xmax ×ˢ Set.Icc ymin ymax

def Cube.rectVertices (xmin xmax ymin ymax : ℝ) : Fin 4 → ℝ²

Vertices of an axis-aligned rectangle in ℝ².

Equations

• Cube.rectVertices xmin xmax ymin ymax = ![!₂[xmin, ymin], !₂[xmax, ymin], !₂[xmin, ymax], !₂[xmax, ymax]]

theorem Cube.closedRectangle_is_convex_hull (xmin xmax ymin ymax : ℝ) (xlt : xmin < xmax) (ylt : ymin < ymax) : closedRectangle xmin xmax ymin ymax = (convexHull ℝ) (Set.range (rectVertices xmin xmax ymin ymax))

A closed rectangle is the convex hull of its four vertices.

theorem Cube.vector_ext (v : ℝ²) : !₂[v.ofLp 0, v.ofLp 1] = v

theorem Cube.openRectangle_is_interior (xmin xmax ymin ymax : ℝ) : interior (closedRectangle xmin xmax ymin ymax) = openRectangle xmin xmax ymin ymax

The interior of a closed rectangle is the corresponding open rectangle.

theorem Cube.nontrivial_rectangle0 : rnn.ofLp 0 < rpp.ofLp 0

theorem Cube.nontrivial_rectangle1 : rnn.ofLp 1 < rpp.ofLp 1

def Cube.closedMediant : Set ℝ²

Closed rectangle used as the intermediate shadow contained in the outer hull.

Equations

• Cube.closedMediant = Cube.closedRectangle (Cube.rnn.ofLp 0) (Cube.rpp.ofLp 0) (Cube.rnn.ofLp 1) (Cube.rpp.ofLp 1)

def Cube.openMediant : Set ℝ²

Interior rectangle used as the intermediate shadow contained in the outer hull.

Equations

• Cube.openMediant = Cube.openRectangle (Cube.rnn.ofLp 0) (Cube.rpp.ofLp 0) (Cube.rnn.ofLp 1) (Cube.rpp.ofLp 1)

theorem Cube.rect_fact1 : ![rpp.ofLp 0, rnn.ofLp 1] = rpn.ofLp

theorem Cube.rect_fact2 : ![rnn.ofLp 0, rpp.ofLp 1] = rnp.ofLp

theorem Cube.mediant_sub_hull_outer : Set.range (rectVertices (rnn.ofLp 0) (rpp.ofLp 0) (rnn.ofLp 1) (rpp.ofLp 1)) ⊆ (convexHull ℝ) outerShadow

theorem Cube.mediant_sub_outer : closedMediant ⊆ (convexHull ℝ) outerShadow

theorem Cube.rupert : IsRupert cube