TripleSieveError.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.triple_sieve_divisor_weight line 11
lemma OAI.TotientAsymptotic.triplePrimeSieve_error_sum line 26
theorem OAI.TotientAsymptotic.triplePrimeTuples_bound line 69
Source documentation
All arithmetic remainders in the three-linear-form sieve are now eliminated.
```
theorem triplePrimeTuples_bound (a b X z : ℕ) (y : ℝ) (hy : 1 ≤ y) :
    ((triplePrimeTuples a b X z).card:ℝ) ≤
      X/selbergBoundingSum (triplePrimeSieve a b X z y hy)+2*y^3 :=
…
```
Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.triplePrimeTuples, OAI.TotientAsymptotic.triplePrimeSieve