ShiftedSieveError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A polynomial bound for the complete error term of the concrete Selberg sieve.

lemma OAI.TotientAsymptotic.odd_sieve_divisor_weight line 11
lemma OAI.TotientAsymptotic.shiftedPrimeSieve_error_sum line 27
theorem OAI.TotientAsymptotic.shiftedPrimePairs_bound line 70
Source documentation
All arithmetic remainders in the two-linear-form sieve are now eliminated.
```
theorem shiftedPrimePairs_bound (b X z : ℕ) (y : ℝ) (hy : 1 ≤ y) :
    ((shiftedPrimePairs b X z).card:ℝ) ≤
      X/selbergBoundingSum (shiftedPrimeSieve b X z y hy)+2*y^3 :=
…
```
Mentions: OAI.TotientAsymptotic.shiftedPrimePairs, OAI.TotientAsymptotic.shiftedPrimeSieve