OAI/Geometry/ProjectionBody/ProductFacets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProjectionCounterexample.firstBlockLinear line 11
  2. def OAI.ProjectionCounterexample.secondBlockLinear line 16
  3. def OAI.ProjectionCounterexample.productFunctional line 22

    Source documentation

    The twenty-two bounding inequalities of the actual Cartesian product.

    def productFunctional : Bool × Option (Fin 10) → E 20 →ₗ[ℝ] ℝ
  | (false, i) => (simplexFunctional 10 i).comp firstBlockLinear
  | (true, i) => (simplexFunctional 10 i).comp secondBlockLinear

    Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.simplexFunctional, OAI.ProjectionCounterexample.firstBlockLinear, OAI.ProjectionCounterexample.secondBlockLinear

  4. def OAI.ProjectionCounterexample.productLevel line 26
  5. theorem OAI.ProjectionCounterexample.productFunctional_first line 28
  6. theorem OAI.ProjectionCounterexample.productFunctional_second line 31
  7. theorem OAI.ProjectionCounterexample.productBody_eq_halfspaceBody line 34
  8. theorem OAI.ProjectionCounterexample.blocks_eq_zero_iff line 47
  9. theorem OAI.ProjectionCounterexample.product_has_positive_slope line 58
  10. theorem OAI.ProjectionCounterexample.product_boundingFace_first line 69
  11. theorem OAI.ProjectionCounterexample.product_boundingFace_second line 78
  12. theorem OAI.ProjectionCounterexample.product_functional_balance line 87
  13. theorem OAI.ProjectionCounterexample.product_absolute_slopes line 91