OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogScales.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.IteratedLogScales.loglog line 11
2. def OAI.Erdos970.NumberTheoryLean.IteratedLogScales.rescale line 13
3. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.loglog_pos line 15
4. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.loglog_tendsto line 22
5. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.eventual_loglog_bounds line 26
6. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.eventual_rescale_lower line 41
7. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.rescale_tendsto line 60
8. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogScales.eventual_loglog_le_logW line 65