OAI/NumberTheory/PrimeGaps/RieszBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LargePrimeGaps.logRiesz line 9
2. lemma OAI.LargePrimeGaps.near_line_denominator line 11
3. lemma OAI.LargePrimeGaps.logRiesz_local line 45
4. lemma OAI.LargePrimeGaps.logRiesz_iteratedDeriv_bound line 86
5. lemma OAI.LargePrimeGaps.logRiesz_power_bound line 96
6. lemma OAI.LargePrimeGaps.near_strip_geometry line 118
7. lemma OAI.LargePrimeGaps.nonprincipal_logRiesz_bound line 136