OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Primes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.Primes line 30
2. instance OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.prime_nonzero line 32
3. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primes_coprime line 35
4. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primes_two line 44
5. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primes_le line 47
6. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primes_eq_filter line 51
7. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.local_sum_bound line 60
8. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.local_product_bound line 74
9. theorem OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.prime_box_sieve line 89