OAI/Combinatorics/ThinTrees/Signing/GramRealization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Gram realization.

  1. abbrev OAI.CurrentKS.Realization.GramLift line 16
  2. abbrev OAI.CurrentKS.Realization.gramLiftCode line 17
  3. abbrev OAI.CurrentKS.Realization.gramChild line 18
  4. abbrev OAI.CurrentKS.Realization.gramParent line 19
  5. def OAI.CurrentKS.Realization.firstColumn line 21
  6. instance OAI.CurrentKS.Realization.poly_firstColumn line 24
  7. lemma OAI.CurrentKS.Realization.firstColumn_data line 26
  8. def OAI.CurrentKS.Realization.gramLiftData line 33
  9. def OAI.CurrentKS.Realization.gramLift line 38
  10. instance OAI.CurrentKS.Realization.poly_gramLift line 48
  11. lemma OAI.CurrentKS.Realization.gramLift_data line 52
  12. lemma OAI.CurrentKS.Realization.gram_fold_correct line 63
  13. def OAI.CurrentKS.Realization.gramColumnsProgram line 74
  14. lemma OAI.CurrentKS.Realization.gram_take_history line 79
  15. lemma OAI.CurrentKS.Realization.SchurDesc.gram_wire line 100
  16. lemma OAI.CurrentKS.Realization.runsPoly_gramColumns line 125
  17. def OAI.CurrentKS.Realization.transposeRectData line 155
  18. def OAI.CurrentKS.Realization.transposeRect line 158
  19. instance OAI.CurrentKS.Realization.poly_transposeRect line 166
  20. lemma OAI.CurrentKS.Realization.transposeRect_data line 170
  21. lemma OAI.CurrentKS.Realization.gramColumns_transpose line 179
  22. def OAI.CurrentKS.Realization.gramMatrixProgram line 191
  23. lemma OAI.CurrentKS.Realization.runsPoly_gramMatrix line 195
  24. def OAI.CurrentKS.Realization.whiteningProgram line 203
  25. lemma OAI.CurrentKS.Realization.runsPoly_whitening line 207