OAI/Combinatorics/MatchingCount/Arithmetic/BinaryDivision.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.BinaryDivision.low line 9
  2. def OAI.MatchingFPRAS.BinaryDivision.nextQ line 10
  3. def OAI.MatchingFPRAS.BinaryDivision.nextR line 11
  4. def OAI.MatchingFPRAS.BinaryDivision.run line 14
  5. lemma OAI.MatchingFPRAS.BinaryDivision.value_bits_length line 18
  6. lemma OAI.MatchingFPRAS.BinaryDivision.bits_length_mono line 20
  7. lemma OAI.MatchingFPRAS.BinaryDivision.nextR_length line 22
  8. lemma OAI.MatchingFPRAS.BinaryDivision.nextQ_length line 27
  9. lemma OAI.MatchingFPRAS.BinaryDivision.step_remainder line 29
  10. lemma OAI.MatchingFPRAS.BinaryDivision.step_mass line 38
  11. lemma OAI.MatchingFPRAS.BinaryDivision.value_append line 52
  12. lemma OAI.MatchingFPRAS.BinaryDivision.value_reverse_cons line 56
  13. lemma OAI.MatchingFPRAS.BinaryDivision.run_mass line 61
  14. lemma OAI.MatchingFPRAS.BinaryDivision.run_remainder line 69
  15. lemma OAI.MatchingFPRAS.BinaryDivision.run_lengths line 74
  16. theorem OAI.MatchingFPRAS.BinaryDivision.correct line 86