OAI/Combinatorics/KMedianRecovery/Recovery/BoundedDecision.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.nword line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rest₁ line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.mword line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rest₂ line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.bound line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rows line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.nword_computes line 22
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rest₁_computes line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.mword_computes line 24
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rest₂_computes line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.bound_computes line 26
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rows_computes line 27
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.projections_pack line 28
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.numAbs line 35
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.numAbs_computes line 36
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.numAbs_encode line 37
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.numAbsOp line 39
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.numAbsOp_computes line 40
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffAbs line 41
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffAbs_computes line 42
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffAbs_row line 47
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffSum line 51
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffSum_computes line 52
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.coeffSum_row line 53
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeight line 56
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeight_computes line 58
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeight_row line 60
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeightOp line 65
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeightOp_computes line 66
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeights line 67
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeights_computes line 68
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.rowHeights_pack line 73
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.heightSum line 77
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.heightSum_computes line 78
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.height line 79
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.height_computes line 80
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.height_pack line 84
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.dataHeight_pad line 88
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.padRow line 92
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.padRow_computes line 94
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.padRow_row line 97
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.padRowOp line 105
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.padRowOp_computes line 106
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.paddedRows line 107
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.paddedRows_computes line 108
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.paddedRows_pack line 113
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.prepared line 117
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.prepared_computes line 119
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.prepared_pack line 122
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.run line 128
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.run_computes line 129
  53. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.run_pack line 130
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBoundedDecision.run_correct line 134
  55. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.entries line 144
  56. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.entries_computes line 145
  57. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.entries_row line 146
  58. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denOp line 150
  59. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denOp_computes line 151
  60. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominators line 152
  61. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominators_computes line 153
  62. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominators_row line 158
  63. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominator line 162
  64. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominator_computes line 163
  65. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.rowD line 165
  66. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.denominator_row line 166
  67. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.rowD_cast line 169
  68. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.rowNumerator_rat line 171
  69. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.scale_coeff line 176
  70. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.scale_bound line 180
  71. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.scalar line 184
  72. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.scalar_computes line 185
  73. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.coeffWords line 186
  74. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.coeffWords_computes line 187
  75. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.coeffWords_row line 193
  76. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.boundWords line 198
  77. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.boundWords_computes line 200
  78. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.boundWords_row line 202
  79. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.run line 207
  80. def OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.run_computes line 208
  81. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClearRow.run_row line 209
  82. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.pack line 218
  83. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.first line 221
  84. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rest₁ line 222
  85. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.second line 223
  86. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rest₂ line 224
  87. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.bound line 225
  88. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rows line 226
  89. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.first_computes line 227
  90. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rest₁_computes line 228
  91. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.second_computes line 229
  92. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rest₂_computes line 230
  93. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.bound_computes line 231
  94. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.rows_computes line 232
  95. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.projections_pack line 233
  96. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.clearOp line 238
  97. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.clearOp_computes line 239
  98. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.clearedRows line 240
  99. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.clearedRows_computes line 241
  100. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.clearedRows_pack line 246
  101. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.prepared line 253
  102. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.prepared_computes line 255
  103. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.prepared_pack line 257
  104. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.run line 261
  105. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.run_computes line 262
  106. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.run_pack line 263
  107. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.run_correct line 266
  108. structure OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.System line 272
  109. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.System.bits line 277
  110. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.System.answer line 278
  111. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalDecision.computation line 279
  112. def OAI.MetricKMedianRecovery.BitMachine.WordList.Count.op line 286
  113. def OAI.MetricKMedianRecovery.BitMachine.WordList.Count.op_computes line 287
  114. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Count.operation_eq line 288
  115. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Count.fold_op line 290
  116. def OAI.MetricKMedianRecovery.BitMachine.WordList.Count.run line 297
  117. def OAI.MetricKMedianRecovery.BitMachine.WordList.Count.run_computes line 298
  118. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Count.run_encode line 301