Subpolynomial root counts for a fixed irreducible polynomial

The discriminant bound is uniform in prime-power exponents. Multiplicativity then bounds the root count by a fixed exponential in the number of distinct prime factors, and hence by every positive power of the modulus.

theorem NairTenenbaum.exists_rootCount_prime_pow_uniform {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C

theorem NairTenenbaum.rootCount_le_primeFactorPower {Q : Polynomial ℤ} {C : ℕ} (hC : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (n : ℕ) : n ≠ 0 → rootCount Q n ≤ C ^ n.primeFactors.card

theorem NairTenenbaum.exists_rootCount_le_rpow {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {ε : ℝ} (hε : 0 < ε) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (n : ℕ), n ≠ 0 → ↑(rootCount Q n) ≤ B * ↑n ^ ε