OAI/NumberTheory/ShortEgyptian/MomentAsymptotics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ShortEgyptian.eventually_log_pow_le line 12
2. theorem OAI.ShortEgyptian.eventually_nested_log_le line 29
3. theorem OAI.ShortEgyptian.log_linear_bound line 44
4. theorem OAI.ShortEgyptian.prime_exp_bound line 55
5. theorem OAI.ShortEgyptian.divisor_moment_numeric line 63
6. theorem OAI.ShortEgyptian.uniform_divisor_moment line 247