OAI/Combinatorics/KMedianRecovery/Geometry/LocalBest.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.choose line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.choose_computes line 12
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.choose_pack line 17
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.listBest_fold line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.pack line 28
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.run line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.run_computes line 32
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalBest.run_pack line 35
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.pack line 59
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.rank line 61
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.rank_computes line 63
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.rank_pack line 71
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.selected line 76
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.selected_computes line 79
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.selected_pack line 82
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.step line 91
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.step_computes line 92
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.step_pack line 98
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.iterate_pack line 103
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.capPoly line 115
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.capacity line 116
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.iterationInput line 117
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.iterationInput_computes line 119
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.run line 121
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.run_computes line 123
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.length_bound line 125
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.run_pack line 143