OAI/Combinatorics/KMedianRecovery/Recovery/LengthCandidates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.freeOp line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.freeOp_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.paidOp line 23
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.paidOp_computes line 24
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.frees line 34
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.frees_computes line 35
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.paids line 37
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.paids_computes line 38
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.candidates line 40
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.candidates_computes line 41
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLength.frees_pack line 42
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLength.paids_pack line 48
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLength.candidates_pack line 56
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.view line 60
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.view_computes line 61
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLength.view_pack line 63