OAI/Combinatorics/KMedianRecovery/Recovery/Pack.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digits line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divisor line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.quotient line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.remainder line 18
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.decode_pack line 20
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digits_pack line 26
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divisor_pack line 28
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.quotient_pack line 30
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.remainder_pack line 32
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.length_pack line 35
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digits_computes line 40
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divisor_computes line 42
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.quotient_computes line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.remainder_computes line 46
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.pack_computes line 49
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.doubled line 55
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.nextBit line 56
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.reduced line 57
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.step line 60
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.doubled_computes line 64
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.nextBit_computes line 66
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.reduced_computes line 69
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.step_computes line 73
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.normalize_length line 81
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.subtract_length line 83
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.reduced_length line 88
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.mass line 99
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.next line 102
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rank line 104
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divisor_next line 106
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.mass_next line 113
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.length_next line 126
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rank_next line 135
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.projection_bounds line 148
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rank_bound line 158
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.iterate_bounds line 163
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.stop line 186
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.loop_computes line 194