OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoverySelection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.FiniteTape.run_of_repeat line 8
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.output line 27
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.run_output line 30
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.output_feasible line 35
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.cost_le_start line 41
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.cost_le_designated line 45
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atDemand line 59
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atDemand_computes line 60
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.demandWords line 62
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.demandWords_computes line 65
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.budget line 68
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.demandWords_pack line 70
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.budget_bound line 78
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.all_counts_budget line 91
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.polynomial_recovery line 102