OAI/Combinatorics/KMedianRecovery/Recovery/Cf.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.cf line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.cf_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.contextPrice line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.contextPrice_computes line 17
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.contextPrice_pack line 24
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.pack line 30
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.midpoint line 34
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.midpoint_computes line 36
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.query line 38
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.query_computes line 40
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.query_pack line 42
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.countAt line 48
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.countAt_computes line 49
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.run line 50
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.run_computes line 53
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPriceRefine.run_pack line 59