OAI/Geometry/ProjectionBody/SimplexBrightness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.volume_simplex line 16
2. theorem OAI.ProjectionCounterexample.simplexFacetProjection_normDet line 21
3. theorem OAI.ProjectionCounterexample.simplex_projected_facet_volume line 40
4. theorem OAI.ProjectionCounterexample.simplex_projected_facet_measurable line 51
5. theorem OAI.ProjectionCounterexample.simplex_projected_facet_intersection_null line 60
6. theorem OAI.ProjectionCounterexample.simplex_projectionVolume line 76

   Source documentation

   Actual orthogonal projection volume of the convex-hull standard simplex.

   theorem simplex_projectionVolume {n : ℕ} (hn : 0 < n)
       {u : E (n + 1)} (hu : ‖u‖ = 1) :
       projectionVolume (simplex (n + 1)) u =
         ((∑ i, |u i|) + |∑ i, u i|) / (2 * (n.factorial : ℝ)) := by
   …

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.ProjectionCounterexample.simplex