OAI/NumberTheory/Ostmann/Construction/GiantWindowScale.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.giantWindowScale line 12
2. lemma OAI.Ostmann.Construction.log_ceil_exp_le_add_one line 14
3. lemma OAI.Ostmann.Construction.giantWindowScale_ge line 26
4. theorem OAI.Ostmann.Construction.giantWindowScale_bounds line 34
5. lemma OAI.Ostmann.Construction.exp_mul_tendsto line 84
6. theorem OAI.Ostmann.Construction.giantWindowScale_eventually line 88