OAI/Combinatorics/KMedianRecovery/Encoding/OptionEncode.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.optionEncode line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.context line 17
  3. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.item line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.accum line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.context_computes line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.item_computes line 21
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.accum_computes line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.operation line 24
  9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.operation_computes line 26
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Find.operation_pack line 35
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Find.fold_result line 40
  12. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.run line 53
  13. def OAI.MetricKMedianRecovery.BitMachine.WordList.Find.run_computes line 56
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Find.optionEncode_bound line 61
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Find.run_encode line 69
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.encode line 91
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.rowsEncode line 92
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.bound line 93
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.coeff line 94
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.bound_computes line 95
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.coeff_computes line 96
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.dotInput line 97
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.dotInput_computes line 98
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.dot line 99
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.dot_computes line 100
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.good line 101
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.good_computes line 102
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.bad line 105
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.bad_computes line 106
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRow.bad_pack line 112
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRow.find_map line 119
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.run line 127
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryRow.run_computes line 128
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRow.run_pack line 129
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.stateEncode line 138
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.pack line 139
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.dim line 141
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rest line 142
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.precision line 143
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rest₂ line 144
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rows line 145
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.stored line 146
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.shape line 147
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.center line 148
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.dim_computes line 149
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.precision_computes line 150
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rest₂_computes line 151
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rows_computes line 152
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.stored_computes line 153
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.shape_computes line 154
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.center_computes line 155
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.dim_pack line 156
  53. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.precision_pack line 158
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.rows_pack line 160
  55. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.stored_pack line 162
  56. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.shape_pack line 164
  57. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.center_pack line 166
  58. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.found line 168
  59. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.found_computes line 169
  60. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.found_pack line 170
  61. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.direction line 173
  62. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.direction_computes line 174
  63. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.direction_pack line 176
  64. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.normWords line 181
  65. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.normWords_computes line 183
  66. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.zeroDirection line 185
  67. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.zeroDirection_computes line 186
  68. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.normWords_pack line 189
  69. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.zeroDirection_pack line 194
  70. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.cutInput line 204
  71. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.cutInput_computes line 206
  72. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.cutInput_pack line 208
  73. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.updated line 211
  74. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.updated_computes line 213
  75. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.nextState line 218
  76. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.nextState_computes line 220
  77. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.nextState_pack line 225
  78. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.run line 238
  79. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.run_computes line 240
  80. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.run_pack line 242
  81. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidAdvance.iterate_pack line 246