OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoveryAll.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.integral_recovery line 11
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.R.run line 77
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.R.budget line 78
  4. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.R.pack line 79
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.pack line 82
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.src line 84
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.src_computes line 85
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchorInput line 86
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchorInput_computes line 88
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchor line 94
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchor_computes line 95
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.recoveryParams line 96
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.recoveryParams_computes line 98
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.bare line 104
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.bare_computes line 105
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.counter line 106
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.demand line 107
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.demand_computes line 108
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.cutRaw line 110
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.cutRaw_computes line 112
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.callInput line 114
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.callInput_computes line 116
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.call line 118
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.call_computes line 119
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.ranks line 121
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.ranks_computes line 122
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.calls line 124
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.calls_computes line 126
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.start line 129
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.start_computes line 130
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.runInput line 131
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.runInput_computes line 134
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.run line 140
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.run_computes line 141
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.demands line 143
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.demands_computes line 144
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.budget line 147
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchorInput_pack line 148
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.anchor_pack line 152
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.ranks_pack line 155
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.words line 160
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.calls_pack line 163
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralDispatch.start_pack line 168