ProductFacetCharts.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Explicit nineteen-dimensional affine charts on the twenty-two product facets.

def OAI.ProjectionCounterexample.productFacetDomain line 14

Source documentation

The product-simplex parameter domain for a facet in the selected block.

def productFacetDomain : Bool → Set (E 19)
  | false => (@EuclideanSpace.finAddEquivProd ℝ _ 9 10) ⁻¹'
      (simplex 9 ×ˢ simplex 10)
  | true => (@EuclideanSpace.finAddEquivProd ℝ _ 10 9) ⁻¹'
      (simplex 10 ×ˢ simplex 9)

/-- Linear part of the affine product facet chart. -/

Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.simplex

def OAI.ProjectionCounterexample.productFacetLinear line 21

Source documentation

Linear part of the affine product facet chart.

def productFacetLinear : Bool × Option (Fin 10) → E 19 →ₗ[ℝ] E 20
  | (false, i) => (@EuclideanSpace.finAddEquivProd ℝ _ 10 10).symm.toLinearMap.comp
      (((simplexFacetLinear 9 i).prodMap (LinearMap.id : E 10 →ₗ[ℝ] E 10)).comp
        (@EuclideanSpace.finAddEquivProd ℝ _ 9 10).toLinearMap)
  | (true, i) => (@EuclideanSpace.finAddEquivProd ℝ _ 10 10).symm.toLinearMap.comp
      (((LinearMap.id : E 10 →ₗ[ℝ] E 10).prodMap (simplexFacetLinear 9 i)).comp
        (@EuclideanSpace.finAddEquivProd ℝ _ 10 9).toLinearMap)

Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.simplexFacetLinear

def OAI.ProjectionCounterexample.productFacetCenter line 29
lemma OAI.ProjectionCounterexample.firstBlock_finAdd line 33
lemma OAI.ProjectionCounterexample.secondBlock_finAdd line 36
lemma OAI.ProjectionCounterexample.productFacetChart_first line 39
lemma OAI.ProjectionCounterexample.productFacetChart_second line 48
theorem OAI.ProjectionCounterexample.product_facet_eq_affine_image line 58
Source documentation
Each product facet is exactly the image of the appropriate product simplex.
```
theorem product_facet_eq_affine_image (i : Bool × Option (Fin 10)) :
    boundingFace productFunctional productLevel i =
      (fun x => productFacetCenter i + productFacetLinear i x) '' productFacetDomain i.1 := by
…
```
Mentions: OAI.ProjectionCounterexample.boundingFace, OAI.ProjectionCounterexample.productFunctional, OAI.ProjectionCounterexample.productLevel, OAI.ProjectionCounterexample.productFacetCenter, OAI.ProjectionCounterexample.productFacetLinear, OAI.ProjectionCounterexample.productFacetDomain
lemma OAI.ProjectionCounterexample.productFacetLinear_first_first line 114
lemma OAI.ProjectionCounterexample.productFacetLinear_first_second line 120
lemma OAI.ProjectionCounterexample.productFacetLinear_second_first line 126
lemma OAI.ProjectionCounterexample.productFacetLinear_second_second line 132
lemma OAI.ProjectionCounterexample.simplexFunctional_ten_ne_zero line 138
theorem OAI.ProjectionCounterexample.product_facet_transverse line 150
Source documentation
Every other defining hyperplane cuts a product facet chart transversely.
```
theorem product_facet_transverse (i j : Bool × Option (Fin 10)) (hij : i ≠ j) :
    (productFunctional j).comp (productFacetLinear i) ≠ 0 := by
…
```
Mentions: OAI.ProjectionCounterexample.productFunctional, OAI.ProjectionCounterexample.productFacetLinear