OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/AllPrimeInterval.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryPrimeSupply.all_prime_interval line 23
2. lemma OAI.OrdinaryPrimeSupply.loglog_two_pow_ratio line 33
3. lemma OAI.OrdinaryPrimeSupply.exp_one_le_two_pow line 43
4. theorem OAI.OrdinaryPrimeSupply.dyadic_prime_mass_bound line 53