Polynomial sieves with simultaneous congruence conditions

Conditioning on pairwise coprime polynomial congruences preserves the sifting density at primes coprime to their moduli. The main term keeps the full joint congruence density; the remainder costs its numerator.

theorem NairTenenbaum.exists_conditional_polynomial_sieve_bound {g η : ℝ} (hg : 1 ≤ g) (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → ↑Q.natDegree ≤ g → ∀ (P : ℕ), Squarefree P → (∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) → ∀ (r : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r), (Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j)) → P.Coprime (mass m) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ p ∈ P.primeFactors, ↑p ≤ z) → ↑(conditionalPolynomialSiftedCount Q P R m a b) ≤ (4 * (↑b - ↑a) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i)) * ∏ p ∈ P.primeFactors, (1 - ↑(rootCount Q p) / ↑p) + (K * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i))) * z ^ (4 * g * (1 + η))

The congruence density remains in the main term; its numerator controls the error. The constant is uniform in the congruence polynomials and moduli.