OAI/Combinatorics/KMedianRecovery/Geometry/LocalCandidates.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.flatMapWith_map line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.widths line 23
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.widths_computes line 27
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.widths_pack line 34
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.sameSize line 46
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.sameSize_computes line 47
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.sameSize_pack line 49
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.removed line 52
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.removed_computes line 54
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.removed_pack line 58
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.raw line 62
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.raw_computes line 64
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.raw_pack line 67
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.run line 72
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.run_computes line 74
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCandidates.run_pack line 76
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.entry line 86
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.entry_computes line 88
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.entry_pack line 91
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.near line 95
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.near_computes line 97
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.pack line 102
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.connection line 104
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.near_pack line 106
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.run line 113
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.run_computes line 115
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.cost line 120
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.run_pack line 121
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.rank line 128
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.rank_computes line 129
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalCost.rank_pack line 130