OAI/Analysis/MatrixSigning/Complexity/StorageCost.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KS.W08.AccessCounted line 12
  2. def OAI.KS.W08.AccessCounted.pure line 23
  3. def OAI.KS.W08.AccessCounted.bind line 25
  4. def OAI.KS.W08.AccessCounted.work line 29
  5. def OAI.KS.W08.AccessCounted.add line 31
  6. def OAI.KS.W08.AccessCounted.sub line 32
  7. def OAI.KS.W08.AccessCounted.mul line 33
  8. def OAI.KS.W08.AccessCounted.div line 34
  9. def OAI.KS.W08.AccessCounted.neg line 35
  10. def OAI.KS.W08.AccessCounted.inv line 36
  11. def OAI.KS.W08.AccessCounted.positive line 37
  12. theorem OAI.KS.W08.AccessCounted.add_work line 39
  13. theorem OAI.KS.W08.AccessCounted.sub_work line 40
  14. theorem OAI.KS.W08.AccessCounted.mul_work line 41
  15. theorem OAI.KS.W08.AccessCounted.div_work line 42
  16. theorem OAI.KS.W08.AccessCounted.neg_work line 43
  17. theorem OAI.KS.W08.AccessCounted.inv_work line 44
  18. theorem OAI.KS.W08.AccessCounted.positive_work line 45
  19. def OAI.KS.W08.AccessCounted.erase line 47
  20. abbrev OAI.KS.W08.AccessCounted.toArithmetic line 49
  21. def OAI.KS.W08.AccessCounted.ofArithmetic line 51
  22. theorem OAI.KS.W08.AccessCounted.ofArithmetic_value line 53
  23. theorem OAI.KS.W08.AccessCounted.ofArithmetic_ops line 54
  24. theorem OAI.KS.W08.AccessCounted.ofArithmetic_work line 55
  25. theorem OAI.KS.W08.AccessCounted.erase_ofArithmetic line 56
  26. theorem OAI.KS.W08.AccessCounted.erase_pure line 59
  27. theorem OAI.KS.W08.AccessCounted.erase_bind line 60
  28. theorem OAI.KS.W08.AccessCounted.erase_eq_of_value_ops line 63
  29. theorem OAI.KS.W08.AccessCounted.pure_ops line 69
  30. theorem OAI.KS.W08.AccessCounted.bind_ops line 70
  31. theorem OAI.KS.W08.AccessCounted.pure_work line 73
  32. theorem OAI.KS.W08.AccessCounted.bind_work line 75
  33. theorem OAI.KS.W08.AccessCounted.bind_work_le line 78
  34. def OAI.KS.W08.AccessCounted.readVector line 83
  35. theorem OAI.KS.W08.AccessCounted.readVector_value line 87
  36. theorem OAI.KS.W08.AccessCounted.readVector_ops line 92
  37. theorem OAI.KS.W08.AccessCounted.readVector_work line 95
  38. def OAI.KS.W08.AccessCounted.readMatrix line 98
  39. theorem OAI.KS.W08.AccessCounted.readMatrix_value line 102
  40. theorem OAI.KS.W08.AccessCounted.readMatrix_ops line 105
  41. theorem OAI.KS.W08.AccessCounted.readMatrix_work line 108
  42. def OAI.KS.W08.AccessCounted.traverse line 111
  43. theorem OAI.KS.W08.AccessCounted.traverse_value_get line 117
  44. theorem OAI.KS.W08.AccessCounted.traverse_ops line 122
  45. theorem OAI.KS.W08.AccessCounted.erase_traverse line 127
  46. theorem OAI.KS.W08.AccessCounted.traverse_work line 135
  47. theorem OAI.KS.W08.AccessCounted.traverse_work_le line 142
  48. def OAI.KS.W08.AccessCounted.sumVector line 150
  49. theorem OAI.KS.W08.AccessCounted.sumVector_value line 153
  50. theorem OAI.KS.W08.AccessCounted.sumVector_ops line 156
  51. theorem OAI.KS.W08.AccessCounted.sumVector_work line 159
  52. def OAI.KS.W08.AccessCounted.dot line 162
  53. theorem OAI.KS.W08.AccessCounted.dot_value line 166
  54. theorem OAI.KS.W08.AccessCounted.dot_work line 172
  55. theorem OAI.KS.W08.AccessCounted.dot_ops line 177
  56. theorem OAI.KS.W08.AccessCounted.dot_work_le line 182