Adjoining the prime argument to the sieve polynomial

The proof of Theorem 3 sieves both Q(t) and t. Adjoining X adds exactly one root at primes not dividing Q(0). It can introduce fixed prime divisors; the degree bound confines those new obstructions to small primes.

theorem NairTenenbaum.residueRootSet_mul_X (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : have this := ⋯; residueRootSet (Q * Polynomial.X) p = insert 0 (residueRootSet Q p)

theorem NairTenenbaum.rootCount_mul_X_prime (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : rootCount (Q * Polynomial.X) p = rootCount Q p + if p ∣ (Polynomial.eval 0 Q).natAbs then 0 else 1

The additional residue class is new precisely away from Q(0).

theorem NairTenenbaum.rootCount_mul_X_prime_le_degree_add_one {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) : rootCount (Q * Polynomial.X) p ≤ Q.natDegree + 1

theorem NairTenenbaum.rootCount_mul_X_prime_lt {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) (hlarge : Q.natDegree + 1 < p) : rootCount (Q * Polynomial.X) p < p

No new fixed divisor occurs above the enlarged degree.

theorem NairTenenbaum.adjoining_X_can_introduce_fixed_prime : NoFixedPrimeDivisor (Polynomial.X + Polynomial.C 1) ∧ Polynomial.eval 0 (Polynomial.X + Polynomial.C 1) ≠ 0 ∧ ¬NoFixedPrimeDivisor ((Polynomial.X + Polynomial.C 1) * Polynomial.X)

The obstruction to applying Theorem 1 directly to the enlarged family is real, even for a linear polynomial with constant term one.

theorem NairTenenbaum.sieveFactor_mul_X_le (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : 1 - ↑(rootCount (Q * Polynomial.X) p) / ↑p ≤ (1 - ↑(rootCount Q p) / ↑p) * if p ∣ (Polynomial.eval 0 Q).natAbs then 1 else 1 - 1 / ↑p

Local comparison responsible for the additional prime-sieving factor.

theorem NairTenenbaum.progressionSieveProduct_mul_X_le (Q : Polynomial ℤ) (n : ℕ) (x : ℝ) : progressionSieveProduct (Q * Polynomial.X) n x ≤ progressionSieveProduct Q n x * progressionSieveProduct Polynomial.X (n * (Polynomial.eval 0 Q).natAbs) x

The same comparison with an arbitrary set of modulus primes omitted. This is useful when the modulus contains the small fixed-prime obstructions.