OAI/Combinatorics/KMedianRecovery/Recovery/Pack7.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.pack line 16
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.dummy line 17
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.dummy_computes line 18
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.dummy_replicate line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.indices line 22
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.indices_computes line 23
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.indices_replicate line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.ctx line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.row line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.col line 29
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.ctx_computes line 30
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.row_computes line 31
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.col_computes line 32
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.entryWords line 34
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.entryWords_computes line 38
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.entryWords_pack line 44
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.rowInput line 54
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.rowInput_computes line 56
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.rowWords line 58
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.rowWords_computes line 59
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.rowWords_pack line 61
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.runInput line 68
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.runInput_computes line 69
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.run line 71
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.run_computes line 72
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.run_pack line 73
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.zeroVector line 79
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.zeroVector_computes line 80
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidInitial.zeroVector_replicate line 82
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.pack line 90
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.pack_length line 93
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.advance_pack_length line 97
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.coeff_length line 102
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.input_bounds line 113
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.shapePoly line 131
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.vectorPoly line 132
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.quadPoly line 133
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.incrementPoly line 134
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.centerPoly line 135
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.storagePoly line 136
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.shapePoly_eval line 138
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.incrementPoly_eval line 141
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.centerPoly_eval line 145
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.storagePoly_eval line 148
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.shape_mono line 152
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.increment_mono line 156
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.vector_encode_height line 160
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.iterate_length_bound line 170
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.boundCounter line 204
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.prepared line 205
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.prepared_computes line 207
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.run line 209
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.run_computes line 210
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidIteration.run_pack line 212