OAI/Combinatorics/KMedianRecovery/Algorithms/GlobalOuter.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.P.matrix line 11
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.P.clients line 12
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.P.facilities line 13
  4. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.P.budget line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.scales line 16
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.scales_computes line 17
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.scales_bits line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.callInput line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.callInput_computes line 23
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.callInput_pack line 30
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.one line 33
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.one_computes line 35
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.calls line 37
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.calls_computes line 39
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.demand line 43
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.demand_computes line 44
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.demands line 45
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.demands_computes line 47
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.budget line 51
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.fallbackInput line 52
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.fallbackInput_computes line 53
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.fallback line 56
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.fallback_computes line 57
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.zeroInput line 58
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.zeroInput_computes line 59
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.zero line 61
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.zero_computes line 62
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.candidates line 63
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.candidates_computes line 65
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.selectInput line 71
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.selectInput_computes line 74
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.select line 81
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.select_computes line 83
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.maskCount line 85
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.maskCount_computes line 86
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.run line 88
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.run_computes line 90
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.start line 98
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.start_subset line 99
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.start_card line 100
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.start_nonempty line 102
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.start_budget line 103
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.fallback_bits line 104
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.zero_bits line 108
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.words line 114
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.calls_bits line 116
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.candidates_bits line 121
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.output line 124
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.select_bits line 126
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.run_bits line 132
  51. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.output_feasible line 138
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.flat_mem line 141
  53. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.demand_bound line 143
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.realCost_eq line 158
  55. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.cost_le_word line 165