OAI/Geometry/ProjectionBody/ProductFacetGraphs.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionCounterexample.firstBlock_productFacetLinear_first line 11
  2. lemma OAI.ProjectionCounterexample.secondBlock_productFacetLinear_first line 17
  3. lemma OAI.ProjectionCounterexample.firstBlock_productFacetLinear_second line 23
  4. lemma OAI.ProjectionCounterexample.secondBlock_productFacetLinear_second line 29
  5. lemma OAI.ProjectionCounterexample.productFacetLinear_first_coordinate line 35
  6. lemma OAI.ProjectionCounterexample.productFacetLinear_second_coordinate line 58
  7. def OAI.ProjectionCounterexample.firstSumGraph line 82

    Source documentation

    Graph coefficient vector for the first block's sum facet.

    def firstSumGraph : E 19 := (@EuclideanSpace.finAddEquivProd ℝ _ 9 10).symm (allOnes 9, 0)

    Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.allOnes

  8. def OAI.ProjectionCounterexample.secondSumGraph line 85

    Source documentation

    Graph coefficient vector for the second block's sum facet.

    def secondSumGraph : E 19 := (@EuclideanSpace.finAddEquivProd ℝ _ 10 9).symm (0, allOnes 9)

    Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.allOnes

  9. lemma OAI.ProjectionCounterexample.inner_firstSumGraph line 87
  10. lemma OAI.ProjectionCounterexample.inner_secondSumGraph line 95
  11. lemma OAI.ProjectionCounterexample.productFacetLinear_first_sum line 103
  12. lemma OAI.ProjectionCounterexample.productFacetLinear_second_sum line 126
  13. lemma OAI.ProjectionCounterexample.blockJoin_first line 149
  14. lemma OAI.ProjectionCounterexample.blockJoin_second line 154
  15. lemma OAI.ProjectionCounterexample.graphNormal_succAbove line 159
  16. lemma OAI.ProjectionCounterexample.firstSumGraph_normal line 163
  17. lemma OAI.ProjectionCounterexample.secondSumGraph_normal line 179
  18. lemma OAI.ProjectionCounterexample.firstSumGraph_normal_inner line 195
  19. lemma OAI.ProjectionCounterexample.secondSumGraph_normal_inner line 202