OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralAll.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.Dsp.pack line 11
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.Dsp.run line 12
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.Dsp.budget line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.src line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.src_computes line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.less line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.less_computes line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplusInput line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplusInput_computes line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplus line 27
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplus_computes line 28
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplusCalls line 30
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplusCalls_computes line 33
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.candidates line 37
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.candidates_computes line 39
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.runInput line 41
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.runInput_computes line 43
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.run line 48
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.run_computes line 50
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplusInput_pack line 52
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.surplus_pack line 57
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.words line 61
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.candidates_pack line 65
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.output line 70
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.run_output line 73
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.output_feasible line 80
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.cost_le_start line 91
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.cost_le_dispatch line 97
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralAll.cost_le_surplus line 108