OAI/Combinatorics/KMedianRecovery/Recovery/LeftNum.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.extractPrefix_pairBits line 8
  2. lemma OAI.MetricKMedianRecovery.BitMachine.discardPrefix_pairBits line 9
  3. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.sign_encode line 10
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.numerator_encode line 13
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.denominator_encode line 14
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.decode_pair line 15
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leftNum line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rightNum line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leftDen line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rightDen line 22
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leftNum_computes line 23
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rightNum_computes line 24
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leftDen_computes line 25
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rightDen_computes line 26
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawMul line 28
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawAdd line 31
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawMul_computes line 36
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawAdd_computes line 38
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.addWords line 47
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.mulWords line 48
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.addWords_computes line 49
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.mulWords_computes line 50
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.addWords_pair line 52
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.mulWords_pair line 61
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.addition line 67
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.multiplication line 70
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leWords line 74
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leWords_computes line 77
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.leWords_pair line 83
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.lessEqual line 86
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.negWords line 90
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.negWords_computes line 92
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.negWords_encode line 94
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.negation line 97
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.signed_sign line 100
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawInv line 107
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.invWords line 110
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.rawInv_computes line 111
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.invWords_computes line 118
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.invWords_encode line 119
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.inverse line 129