FacetCoordinates.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ProjectionCounterexample.insertZero line 12
Source documentation
The coordinate isometry inserting a zero in slot i.
```
def insertZero {n : ℕ} (i : Fin (n + 1)) : E n →ₗᵢ[ℝ] E (n + 1) where
…
```
Mentions: OAI.ProjectionCounterexample.E
theorem OAI.ProjectionCounterexample.insertZero_same line 26
theorem OAI.ProjectionCounterexample.insertZero_succAbove line 29
theorem OAI.ProjectionCounterexample.sum_insertZero line 32
theorem OAI.ProjectionCounterexample.coordinate_facet_eq_image line 38
Source documentation
A coordinate facet is an actual isometric image of the lower-dimensional simplex.
```
theorem coordinate_facet_eq_image {n : ℕ} (i : Fin (n + 1)) :
    {x ∈ simplex (n + 1) | x i = 0} = insertZero i '' simplex n := by
…
```
Mentions: OAI.ProjectionCounterexample.simplex, OAI.ProjectionCounterexample.insertZero
def OAI.ProjectionCounterexample.sumFacetMap line 62
Source documentation
The affine chart on the facet whose coordinate sum is one.
```
def sumFacetMap (n : ℕ) (x : E n) : E (n + 1) :=
…
```
Mentions: OAI.ProjectionCounterexample.E
theorem OAI.ProjectionCounterexample.sumFacetMap_castSucc line 65
theorem OAI.ProjectionCounterexample.sumFacetMap_last line 68
theorem OAI.ProjectionCounterexample.sum_sumFacetMap line 71
theorem OAI.ProjectionCounterexample.sum_facet_eq_image line 77
Source documentation
The non-coordinate facet is an actual affine image of the lower-dimensional simplex.
```
theorem sum_facet_eq_image (n : ℕ) :
    {x ∈ simplex (n + 1) | ∑ j, x j = 1} = sumFacetMap n '' simplex n := by
…
```
Mentions: OAI.ProjectionCounterexample.simplex, OAI.ProjectionCounterexample.sumFacetMap