OAI/Geometry/ProjectionVolume/ProductFacetAreas.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Paper092.splitEuclideanProductL2 line 15
  2. theorem OAI.Paper092.splitEuclideanProductL2_apply line 21
  3. def OAI.Paper092.euclideanProductMap line 24
  4. theorem OAI.Paper092.euclideanProductMap_apply line 30
  5. theorem OAI.Paper092.splitEuclideanProduct_inner line 35
  6. theorem OAI.Paper092.euclideanProductMap_inner line 41
  7. def OAI.Paper092.productOrthonormalBasis line 49
  8. theorem OAI.Paper092.split_productOrthonormalBasis_inl line 54
  9. theorem OAI.Paper092.split_productOrthonormalBasis_inr line 63
  10. theorem OAI.Paper092.euclideanProductMap_normDet line 72
  11. theorem OAI.Paper092.euclideanProductMap_image line 92
  12. theorem OAI.Paper092.euclideanProductMap_image_area line 111
  13. theorem OAI.Paper092.splitEuclideanProduct_preimage_vadd line 122
  14. theorem OAI.Paper092.simplexFacet_diagonal_eq_vadd line 143
  15. theorem OAI.Paper092.simplexProduct_coordinate_facet_area_left line 155
  16. theorem OAI.Paper092.simplexProduct_coordinate_facet_area_right line 168
  17. theorem OAI.Paper092.simplexProduct_diagonal_facet_area_left line 181
  18. theorem OAI.Paper092.simplexProduct_diagonal_facet_area_right line 199