OAI/Combinatorics/HadwigerCounterexample/GramProbabilities.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Gram Probabilities

  1. abbrev OAI.HadwigerCounterexample.num line 12
  2. def OAI.HadwigerCounterexample.columnInv line 16
  3. theorem OAI.HadwigerCounterexample.outer_act line 20
  4. theorem OAI.HadwigerCounterexample.colSp_outer line 24
  5. theorem OAI.HadwigerCounterexample.shift_pmax line 32
  6. theorem OAI.HadwigerCounterexample.shift_fail line 50
  7. theorem OAI.HadwigerCounterexample.unif_fail line 70
  8. def OAI.HadwigerCounterexample.gramGood line 77
  9. def OAI.HadwigerCounterexample.GramL line 80
  10. theorem OAI.HadwigerCounterexample.gramL_surj line 86
  11. theorem OAI.HadwigerCounterexample.pr_gram_fixed line 93
  12. theorem OAI.HadwigerCounterexample.gram_shift line 104

    Source documentation

    Conditional minus columns: adding columns in the annihilator of P doesn't change the pre-injectivity Gram law.

    theorem gram_shift (P : Mat U I) (G : Mat I J) :
    columnInv (w:=unifOn (fun Q : Mat U J => Pᵀ * Q = G)) (ker (Pᵀ.mulVecLin)) := by
…

    Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.columnInv, OAI.HadwigerCounterexample.unifOn

  13. theorem OAI.HadwigerCounterexample.pr_gram_inj_fixed line 114
  14. theorem OAI.HadwigerCounterexample.gram_norm line 139

    Source documentation

    Uniform lower and upper estimates including the full Gram normalization.

    theorem gram_norm (G : Mat I J) (hsize : num I + num J ≤ num U) :
    let v := (pairW unif unif : Wgt (Mat U I × Mat U J))
…

    Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.unif, OAI.HadwigerCounterexample.Wgt