OAI/Combinatorics/KMedianRecovery/Recovery/Pack2.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.pack line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.first line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.second line 13
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.first_pack line 14
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.second_pack line 16
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.length_pack line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.firstRem line 23
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.secondRem line 24
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.step line 27
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.first_computes line 32
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.second_computes line 33
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.pack_computes line 34
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.mod_computes line 38
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.firstRem_computes line 45
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.secondRem_computes line 46
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.step_computes line 51
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.modulus_twice_lt line 62
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.size_drop_of_twice_lt line 71
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.second_mod_size_drop line 80
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.measure line 87
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.rank line 88
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.Good line 89
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.next line 91
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.measure_pack line 93
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.rank_true line 96
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.rank_false line 97
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.step_bounds line 99
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcd_step line 117
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.step_good line 131
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.next_bounds line 138
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcd_next line 150
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.good_next line 157
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.iterate_bounds line 163
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.measure_bound line 177
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.rank_bound line 187
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.stop line 191
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.loop_computes line 199
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.loop_correct line 212
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcdWords line 226
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcdWords_computes line 230
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcdWords_pair line 238
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryGCD.gcd line 241