OAI/Analysis/MatrixSigning/Complexity/PolynomialStored.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.Realization.flatten_code_le line 18
  2. instance OAI.CurrentKS.Realization.size_appendList line 25
  3. instance OAI.CurrentKS.Realization.poly_flattenList line 34
  4. instance OAI.CurrentKS.Realization.poly_joinList line 35
  5. instance OAI.CurrentKS.Realization.poly_singleton line 36
  6. instance OAI.CurrentKS.Realization.poly_flatMap line 37
  7. instance OAI.CurrentKS.Realization.poly_filterCtx line 39
  8. instance OAI.CurrentKS.Realization.poly_binarySucc line 42
  9. lemma OAI.CurrentKS.Realization.binaryNat_length_le line 43
  10. instance OAI.CurrentKS.Realization.size_binarySucc line 47
  11. instance OAI.CurrentKS.Realization.poly_natToBinary line 57
  12. lemma OAI.CurrentKS.Realization.psd_raw_poly line 59
  13. instance OAI.CurrentKS.Realization.poly_psdStored line 72
  14. instance OAI.CurrentKS.Realization.poly_natLE line 83
  15. instance OAI.CurrentKS.Realization.poly_natEq line 84
  16. instance OAI.CurrentKS.Realization.poly_matrixEntry line 85
  17. instance OAI.CurrentKS.Realization.poly_matrixTabulate line 86
  18. instance OAI.CurrentKS.Realization.poly_identityEntry line 89
  19. instance OAI.CurrentKS.Realization.poly_identityMatrix line 90
  20. instance OAI.CurrentKS.Realization.poly_transposeMatrix line 91
  21. instance OAI.CurrentKS.Realization.poly_matrixMul line 92
  22. instance OAI.CurrentKS.Realization.poly_fromBlocks line 93
  23. instance OAI.CurrentKS.Realization.poly_tabulateFin line 94
  24. instance OAI.CurrentKS.Realization.poly_familyFirst line 97
  25. instance OAI.CurrentKS.Realization.poly_familyIndex line 98
  26. instance OAI.CurrentKS.Realization.poly_pow line 100
  27. instance OAI.CurrentKS.Realization.poly_min line 104
  28. instance OAI.CurrentKS.Realization.poly_max line 105
  29. instance OAI.CurrentKS.Realization.poly_inv line 106
  30. instance OAI.CurrentKS.Realization.poly_lt line 107
  31. instance OAI.CurrentKS.Realization.poly_eq line 108
  32. instance OAI.CurrentKS.Realization.poly_better line 110
  33. lemma OAI.CurrentKS.Realization.fold_select_code line 111
  34. lemma OAI.CurrentKS.Realization.size_selection line 123
  35. instance OAI.CurrentKS.Realization.size_better line 130
  36. instance OAI.CurrentKS.Realization.poly_selectScored line 132
  37. instance OAI.CurrentKS.Realization.poly_chooseCoordinate line 133