OAI/NumberTheory/ShortEgyptian/RandomBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ShortEgyptian.random_lengths line 13
2. lemma OAI.ShortEgyptian.random_fresh_bound line 55
3. lemma OAI.ShortEgyptian.random_atom_bound line 82
4. lemma OAI.ShortEgyptian.random_gcd_exponent line 107
5. lemma OAI.ShortEgyptian.random_error_sum line 123
6. lemma OAI.ShortEgyptian.random_hit_bound line 141
7. lemma OAI.ShortEgyptian.random_outside_moment line 157
8. lemma OAI.ShortEgyptian.random_reduced_scale line 174
9. lemma OAI.ShortEgyptian.random_pair_scalar line 184