OAI/Geometry/ProjectionBody/ProductBrightness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.product_projected_facet_volume line 12
2. theorem OAI.ProjectionCounterexample.product_projected_facet_measurable line 24
3. theorem OAI.ProjectionCounterexample.product_projected_facet_intersection_null line 33
4. theorem OAI.ProjectionCounterexample.product_projectionVolume line 48

   Source documentation

   Actual orthogonal projection volume of the twenty-dimensional product body.

   theorem product_projectionVolume {u : E 20} (hu : ‖u‖ = 1) :
       projectionVolume productBody u =
         (((∑ i, |firstBlock u i|) + |∑ i, firstBlock u i|) +
           ((∑ i, |secondBlock u i|) + |∑ i, secondBlock u i|)) /
         (2 * ((Nat.factorial 9 : ℝ) * Nat.factorial 10)) := by
   …

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.ProjectionCounterexample.productBody, OAI.ProjectionCounterexample.firstBlock, OAI.ProjectionCounterexample.secondBlock