OAI/Combinatorics/KMedianRecovery/Recovery/Pack8.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.nword line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₁ line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₂ line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₃ line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.pword line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.sword line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.radius line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rows line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.nword_computes line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₁_computes line 24
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₂_computes line 25
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rest₃_computes line 26
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.pword_computes line 27
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.sword_computes line 28
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.radius_computes line 29
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.rows_computes line 30
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.projections_pack line 31
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.twice line 39
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.twice_computes line 40
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.blocks line 41
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.blocks_computes line 44
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.budgetWord line 47
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.budgetWord_computes line 48
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.budgetWord_pack line 49
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.dimBits line 59
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.dimBits_computes line 60
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.dimBits_pack line 61
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.powerWords line 63
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.powerWords_computes line 64
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.cubeWords line 66
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.cubeWords_computes line 67
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.gridWords line 71
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.gridWords_computes line 72
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.gridWords_pack line 76
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.radiusSquare line 84
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.radiusSquare_computes line 85
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.shapeWords line 87
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.shapeWords_computes line 89
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.shapeWords_pack line 93
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.centerWords line 101
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.centerWords_computes line 102
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.centerWords_pack line 104
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.advanceInput line 108
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.advanceInput_computes line 110
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.advanceInput_pack line 112
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.prepared line 116
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.prepared_computes line 117
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.prepared_pack line 119
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.iterated line 123
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.iterated_computes line 124
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.iterated_pack line 125
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.result line 129
  54. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.result_computes line 131
  55. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.run line 136
  56. def OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.run_computes line 137
  57. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryWeakSolve.run_pack line 138