The sharp prime-root logarithmic bound for irreducible polynomials

For every integer polynomial irreducible over the rationals, Σ_p ρ_Q(p)/p^σ ≤ −log(σ−1)+O_Q(1) near σ=1. Both convergence and the bound are proved from the Dedekind zeta residue.

theorem NairTenenbaum.primeRootPowerWeight_le_one (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) {σ : ℝ} (hσ : 1 ≤ σ) : ↑(rootCount Q p) * ↑p ^ (-σ) ≤ 1

theorem NairTenenbaum.primeRootSum_le_integralNormalization_add {Q : Polynomial ℤ} (hdeg : 1 ≤ Q.natDegree) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) ≤ ∑ p ∈ S, ↑(rootCount Q.integralNormalization p) * ↑p ^ (-σ) + ↑Q.leadingCoeff.natAbs.primeFactors.card

theorem NairTenenbaum.exists_irreducible_primeSum_log_bound {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (C : ℝ) (b : ℝ), 0 ≤ C ∧ 1 < b ∧ ∀ (σ : ℝ), 1 < σ → σ < b → ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) ≤ C - Real.log (σ - 1)

theorem NairTenenbaum.exists_irreducible_rootPrimePowerSum_log_bound {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (C : ℝ) (b : ℝ), 0 ≤ C ∧ 1 < b ∧ ∀ (σ : ℝ), 1 < σ → σ < b → (Summable fun (p : Nat.Primes) => ↑(rootCount Q ↑p) * ↑↑p ^ (-σ)) ∧ rootPrimePowerSum Q σ ≤ C - Real.log (σ - 1)