OAI/NumberTheory/ShortEgyptian/LowerBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ShortEgyptian.unitSum_le_length_div line 7
2. theorem OAI.ShortEgyptian.denominator_bound_aux line 18
3. theorem OAI.ShortEgyptian.denominator_bound line 80
4. theorem OAI.ShortEgyptian.hard_numerator_bound line 97
5. theorem OAI.ShortEgyptian.expansion_length_pos line 116
6. theorem OAI.ShortEgyptian.loglog_le_twice_length line 127
7. theorem OAI.ShortEgyptian.main_lower line 154