OAI/Combinatorics/KMedianRecovery/Encoding/LengthEncode.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rowEncode_injective line 7
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.planBits line 20
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.ctxBits line 23
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.cf line 26
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.pf line 27
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.cf_computes line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.pf_computes line 29
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.isFree line 30
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.isFree_computes line 31
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.source line 33
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.source_computes line 35
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.target line 37
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.target_computes line 39
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.rootIn line 42
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.rootIn_computes line 43
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.freeOut line 45
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.freeOut_computes line 46
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.row line 48
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.row_computes line 49
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.sameRow line 51
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.sameRow_computes line 52
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.extra line 54
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.extra_computes line 55
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.accepts line 61
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryLength.accepts_computes line 63
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLength.accepts_pack line 66