OAI/NumberTheory/ShortEgyptian/ScaleBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.scaleFinDecidableEq line 7
2. lemma OAI.ShortEgyptian.eventually_scaleM_large line 12
3. lemma OAI.ShortEgyptian.eventually_depth_tail line 27
4. structure OAI.ShortEgyptian.ListScale line 51
5. lemma OAI.ShortEgyptian.eventually_ListScale line 60
6. lemma OAI.ShortEgyptian.ListScale.log_one line 72
7. lemma OAI.ShortEgyptian.ListScale.S_pos line 73
8. lemma OAI.ShortEgyptian.ListScale.m_bounds line 74
9. lemma OAI.ShortEgyptian.ListScale.m_pos line 77
10. lemma OAI.ShortEgyptian.ListScale.m_hundred line 80
11. lemma OAI.ShortEgyptian.ListScale.m_fourier line 81
12. lemma OAI.ShortEgyptian.exp_neg_small line 83
13. lemma OAI.ShortEgyptian.ListScale.rho_small line 91
14. lemma OAI.ShortEgyptian.ListScale.terminal_small line 93