OAI/Combinatorics/KMedianRecovery/Encoding/RationalCap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.capped line 11
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.minimum_capped line 12
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.capped_cast line 21
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.rowBits line 30
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.look line 32
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.look_computes line 33
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.offers line 35
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.offers_computes line 38
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.offers_pack line 41
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.cap line 47
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.cap_computes line 49
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.cap_pack line 52
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.weightedRowBits line 63
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.weightedCap line 64
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.weightedCap_computes line 67
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.weightedCap_pack line 70