OAI/NumberTheory/SingleFold/HeightGrowth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SingleFold.GrowthEstimate.sequence_strict line 11
2. lemma OAI.SingleFold.GrowthEstimate.sequence_unbounded line 28
3. lemma OAI.SingleFold.GrowthEstimate.bracket_unique line 41
4. lemma OAI.SingleFold.GrowthEstimate.bracket_log line 66
5. lemma OAI.SingleFold.GrowthEstimate.output_upper line 84
6. lemma OAI.SingleFold.GrowthEstimate.output_lower line 99
7. lemma OAI.SingleFold.GrowthEstimate.output_upper_log line 126
8. theorem OAI.SingleFold.GrowthEstimate.eventual_output line 143
9. lemma OAI.SingleFold.HeightWindow.index_separation line 181
10. lemma OAI.SingleFold.HeightWindow.separated_window line 191
11. lemma OAI.SingleFold.HeightWindow.multiplicative_window line 214
12. theorem OAI.SingleFold.HeightWindow.square_window line 233