The logarithmic sieve-product bound for irreducible polynomials

theorem NairTenenbaum.sieveProduct_le_exp_neg_primeRootSum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (x : ℝ) : sieveProduct Q x ≤ Real.exp (-primeRootReciprocalSum Q x)

theorem NairTenenbaum.exists_irreducible_sieveProduct_log_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (x₀ : ℝ) (C : ℝ), 1 < x₀ ∧ 0 < C ∧ ∀ (x : ℝ), x₀ < x → sieveProduct Q x ≤ C / Real.log x