OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrimitiveTwoLower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primitive_two_lower line 28
2. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.source_local_sum line 49
3. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.coarse_source_tail line 71
4. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.primes_card line 92
5. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.source_boundary_numerator line 100
6. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.eventually_boundary_margin line 144
7. lemma OAI.OrdinaryCorrelations.SourcePrimeBoxSieve.source_boundary_small line 165