OAI/Geometry/ProjectionVolume/ProductPolytope.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.cartesianBody_eq_preimage line 16
  2. def OAI.Paper092.productLiftLeft line 19
  3. def OAI.Paper092.productLiftRight line 22
  4. theorem OAI.Paper092.split_productLiftLeft line 25
  5. theorem OAI.Paper092.split_productLiftRight line 29
  6. theorem OAI.Paper092.inner_productLiftLeft line 33
  7. theorem OAI.Paper092.inner_productLiftRight line 38
  8. theorem OAI.Paper092.productLiftLeft_norm line 43
  9. theorem OAI.Paper092.productLiftRight_norm line 49
  10. theorem OAI.Paper092.cartesianBody_isCompact line 55
  11. theorem OAI.Paper092.cartesianBody_convex line 60
  12. theorem OAI.Paper092.cartesianBody_interior_nonempty line 65
  13. theorem OAI.Paper092.HPolytope.body_interior_nonempty line 77
  14. theorem OAI.Paper092.HPolytope.volume_pos line 89
  15. def OAI.Paper092.HPolytope.productNormal line 94
  16. def OAI.Paper092.HPolytope.productOffset line 98
  17. theorem OAI.Paper092.HPolytope.product_halfspaces_eq line 101
  18. def OAI.Paper092.HPolytope.product line 109
  19. theorem OAI.Paper092.HPolytope.product_body line 164
  20. theorem OAI.Paper092.HPolytope.product_face_inl line 167
  21. theorem OAI.Paper092.HPolytope.product_face_inr line 175