OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoveryDemand.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.completionCounter line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.sampleWord line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.sampleWord_computes line 11
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.completionWord line 13
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.completionWord_computes line 14
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandWord line 15
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandWord_computes line 16
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandBits line 17
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandBits_computes line 18
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.cut line 19
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.cut_computes line 22
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandWord_pack line 27
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demandBits_pack line 43
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.cut_pack line 46
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.demand_polynomial line 50
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Prefix.run line 56
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Prefix.run_computes line 57
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Prefix.run_source line 58
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.output line 77
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.output_feasible line 81
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.output_cost_le_start line 87
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.output_success line 92
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.output_exponential line 112