A uniform subpolynomial lower bound for the sifting product

theorem NairTenenbaum.sieveFactor_inv_le_prime {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) : (1 - ↑(rootCount Q p) / ↑p)⁻¹ ≤ ↑p

theorem NairTenenbaum.sieveFactor_inv_le_exp {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g p : ℕ} (hg : Q.natDegree ≤ g) (hp : Nat.Prime p) (hlarge : 2 * g ≤ p) : (1 - ↑(rootCount Q p) / ↑p)⁻¹ ≤ Real.exp (2 * ↑g / ↑p)

theorem NairTenenbaum.exists_sieveProduct_inv_le_rpow (g : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Q.natDegree ≤ g → ∀ (z : ℝ), 2 ≤ z → (sieveProduct Q z)⁻¹ ≤ C * z ^ δ

Uniformly in the polynomial coefficients, the inverse sifting product is smaller than every positive power of its cutoff, up to a degree-dependent constant.