OAI/Combinatorics/KMedianRecovery/Geometry/LocalSets.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.swapWords line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.swapWords_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.addOne line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.addOne_computes line 15
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.addOne_pack line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.without line 24
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.without_computes line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.diff line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.diff_computes line 28
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.diff_pack line 30
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.size line 39
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.size_computes line 40
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.size_pack line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.insertEach line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.insertEach_computes line 45
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSets.insertEach_pack line 46
  17. def OAI.MetricKMedianRecovery.LocalSearch.widthLists line 55
  18. lemma OAI.MetricKMedianRecovery.LocalSearch.sum_map_constant line 60
  19. lemma OAI.MetricKMedianRecovery.LocalSearch.widthLists_length line 67
  20. lemma OAI.MetricKMedianRecovery.LocalSearch.mem_widthLists line 77
  21. def OAI.MetricKMedianRecovery.LocalSearch.listBest line 106
  22. lemma OAI.MetricKMedianRecovery.LocalSearch.listBest_mem line 111
  23. lemma OAI.MetricKMedianRecovery.LocalSearch.listBest_le line 125
  24. lemma OAI.MetricKMedianRecovery.LocalSearch.listBest_fixed line 146
  25. def OAI.MetricKMedianRecovery.LocalSearch.exchangeList line 155
  26. lemma OAI.MetricKMedianRecovery.LocalSearch.exchangeList_length line 159
  27. lemma OAI.MetricKMedianRecovery.LocalSearch.mem_exchangeList line 165
  28. def OAI.MetricKMedianRecovery.LocalSearch.executableStep line 184
  29. lemma OAI.MetricKMedianRecovery.LocalSearch.executableStep_mem line 187
  30. lemma OAI.MetricKMedianRecovery.LocalSearch.executableStep_min line 195
  31. lemma OAI.MetricKMedianRecovery.LocalSearch.executableStep_mono line 200
  32. lemma OAI.MetricKMedianRecovery.LocalSearch.executableStep_fixed line 203
  33. def OAI.MetricKMedianRecovery.LocalSearch.executableDescent line 211
  34. lemma OAI.MetricKMedianRecovery.LocalSearch.executableDescent_properties line 215
  35. lemma OAI.MetricKMedianRecovery.LocalSearch.executableDescent_fixed line 227
  36. theorem OAI.MetricKMedianRecovery.LocalSearch.executableDescent_min line 233
  37. theorem OAI.MetricKMedianRecovery.LocalSearch.executable_integral_descent line 257
  38. def OAI.MetricKMedianRecovery.LocalSearch.executableAnchor line 275
  39. lemma OAI.MetricKMedianRecovery.LocalSearch.seed_card line 279
  40. lemma OAI.MetricKMedianRecovery.LocalSearch.seed_subset line 284
  41. theorem OAI.MetricKMedianRecovery.LocalSearch.executableAnchor_spec line 288