OAI/NumberTheory/PrimeGaps/PrincipalGrowth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LargePrimeGaps.zetaRegular_bounds line 9
2. lemma OAI.LargePrimeGaps.zeta_deriv_eq_regular line 39
3. lemma OAI.LargePrimeGaps.horizontal_growth_lipschitz line 50
4. lemma OAI.LargePrimeGaps.zeta_high_line_bounds line 65
5. lemma OAI.LargePrimeGaps.zeta_high_line_lower_aux line 110
6. lemma OAI.LargePrimeGaps.zeta_high_line_lower line 176
7. lemma OAI.LargePrimeGaps.zeta_high_strip_lower_aux line 197
8. lemma OAI.LargePrimeGaps.zeta_high_strip_lower line 246
9. lemma OAI.LargePrimeGaps.principal_deriv_eq_regular line 275
10. lemma OAI.LargePrimeGaps.principal_deriv_growth line 284
11. lemma OAI.LargePrimeGaps.principal_strip_lower line 302