OAI/Geometry/ProjectionBody/SimplexFacets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectionCounterexample.coordinateFunctional line 13

   Source documentation

   Coordinate linear functional on the Euclidean space.

   def coordinateFunctional {d : ℕ} (i : Fin d) : E d →ₗ[ℝ] ℝ where
   …

   Mentions: OAI.ProjectionCounterexample.E

2. theorem OAI.ProjectionCounterexample.coordinateFunctional_apply line 18
3. def OAI.ProjectionCounterexample.simplexFunctional line 22

   Source documentation

   Outward defining functionals: the sum facet, then the coordinate facets.

   def simplexFunctional (d : ℕ) : Option (Fin d) → E d →ₗ[ℝ] ℝ
     | none => ∑ i, coordinateFunctional i
     | some i => -coordinateFunctional i

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.coordinateFunctional

4. def OAI.ProjectionCounterexample.simplexLevel line 26
5. theorem OAI.ProjectionCounterexample.simplexFunctional_none line 30
6. theorem OAI.ProjectionCounterexample.simplexFunctional_some line 34
7. theorem OAI.ProjectionCounterexample.simplex_eq_halfspaceBody line 37
8. theorem OAI.ProjectionCounterexample.simplex_has_positive_slope line 55

   Source documentation

   Every nonzero direction has a visible defining facet of the simplex.

   theorem simplex_has_positive_slope {d : ℕ} {u : E d} (hu : u ≠ 0) :
       ∃ i, 0 < simplexFunctional d i u := by
   …

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.simplexFunctional

9. theorem OAI.ProjectionCounterexample.simplex_functional_balance line 73
10. theorem OAI.ProjectionCounterexample.simplex_absolute_slopes line 77
11. theorem OAI.ProjectionCounterexample.simplex_boundingFace_coordinate line 81
12. theorem OAI.ProjectionCounterexample.simplex_boundingFace_sum line 87