Decomposition.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The unit cube extruded by the segment from zero to the all-ones vector. Its decomposition uses the cube and one extrusion cell for every upper facet. The set definitions are literal subsets of a finite real coordinate space.

def OAI.DiagonalZonotope.cube line 21
Source documentation
The actual unit cube in the coordinate space.
```
def cube : Set (ι → ℝ) := {x | ∀ j, 0 ≤ x j ∧ x j ≤ 1}
```
def OAI.DiagonalZonotope.zonotope line 24
Source documentation
The Minkowski sum of the unit cube and the diagonal unit segment.
```
def zonotope : Set (ι → ℝ) :=
…
```
def OAI.DiagonalZonotope.cell line 28
Source documentation
The extrusion of the upper facet normal to coordinate i.
```
def cell (i : ι) : Set (ι → ℝ) :=
…
```
lemma OAI.DiagonalZonotope.cube_subset_zonotope line 31
lemma OAI.DiagonalZonotope.cell_subset_zonotope line 37
theorem OAI.DiagonalZonotope.zonotope_decomposition line 49
Source documentation
Decompose the actual diagonal extrusion by a maximal coordinate.
```
theorem zonotope_decomposition [Fintype ι] :
    (zonotope : Set (ι → ℝ)) = cube ∪ ⋃ i, cell i := by
…
```
Mentions: OAI.DiagonalZonotope.zonotope, OAI.DiagonalZonotope.cube, OAI.DiagonalZonotope.cell
theorem OAI.DiagonalZonotope.cube_inter_cell_subset line 84
Source documentation
The cube and an upper-facet extrusion meet only in that facet's hyperplane.
```
theorem cube_inter_cell_subset (i : ι) :
    (cube : Set (ι → ℝ)) ∩ cell i ⊆ {x | x i = 1} := by
…
```
Mentions: OAI.DiagonalZonotope.cube, OAI.DiagonalZonotope.cell
theorem OAI.DiagonalZonotope.cell_inter_cell_subset line 90
Source documentation
Distinct extrusion cells meet only on a coordinate-equality hyperplane.
```
theorem cell_inter_cell_subset (i j : ι) :
    cell i ∩ cell j ⊆ {x : ι → ℝ | x i = x j} := by
…
```
Mentions: OAI.DiagonalZonotope.cell
def OAI.DiagonalZonotope.extrusionMap line 99
Source documentation
A shear of the cube followed by translation by the ith unit vector.
```
def extrusionMap (i : ι) (s : ι → ℝ) : ι → ℝ :=
…
```
theorem OAI.DiagonalZonotope.cell_eq_image_cube line 103
Source documentation
Each extrusion cell is an actual affine image of the unit cube.
```
theorem cell_eq_image_cube (i : ι) : cell i = extrusionMap i '' cube := by
…
```
Mentions: OAI.DiagonalZonotope.cell, OAI.DiagonalZonotope.extrusionMap, OAI.DiagonalZonotope.cube