OAI/Geometry/ProjectionBody/SimplexFacetCharts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectionCounterexample.allOnes line 12
2. theorem OAI.ProjectionCounterexample.allOnes_apply line 14
3. theorem OAI.ProjectionCounterexample.inner_allOnes line 16
4. def OAI.ProjectionCounterexample.simplexFacetLinear line 20

   Source documentation

   Linear part of each simplex facet chart.

   def simplexFacetLinear (n : ℕ) : Option (Fin (n + 1)) → E n →ₗ[ℝ] E (n + 1)
     | none => graphLinear (Fin.last n) (allOnes n)
     | some i => (insertZero i).toLinearMap

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.graphLinear, OAI.ProjectionCounterexample.allOnes, OAI.ProjectionCounterexample.insertZero

5. def OAI.ProjectionCounterexample.simplexFacetCenter line 24
6. theorem OAI.ProjectionCounterexample.simplexFacetChart_none line 28
7. theorem OAI.ProjectionCounterexample.simplex_facet_eq_affine_image line 36
8. theorem OAI.ProjectionCounterexample.simplex_facet_transverse line 49

   Source documentation

   Every defining hyperplane other than the chart's own hyperplane is transverse. The positive dimension excludes the degenerate segment-endpoint case.

   theorem simplex_facet_transverse {n : ℕ} (hn : 0 < n)
       (i j : Option (Fin (n + 1))) (hij : i ≠ j) :
       (simplexFunctional (n + 1) j).comp (simplexFacetLinear n i) ≠ 0 := by
   …

   Mentions: OAI.ProjectionCounterexample.simplexFunctional, OAI.ProjectionCounterexample.simplexFacetLinear