Sharp logarithmic upper bound for minimal-polynomial prime roots

For an integral primitive generator of a number field, the prime root series is bounded by −log(σ−1)+O(1) as σ decreases to one. The coefficient of the logarithm is one. The finite conductor-prime contribution is explicit.

theorem NairTenenbaum.minpoly_goodPrimeSum_le_log_idealNormDirichlet {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (hgood : ∀ p ∈ S, ¬p ∣ RingOfIntegers.exponent θ) {σ : ℝ} (hσ : 1 < σ) : ∑ p ∈ S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ) ≤ Real.log (idealNormDirichlet K σ) + ↑(minpoly ℤ θ).natDegree ^ 2 * ∑' (n : ℕ), ↑n ^ (-2)

theorem NairTenenbaum.monic_primeRoot_sum_le_degree_mul_card {Q : Polynomial ℤ} (hQ : Q.Monic) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) ≤ ↑Q.natDegree * ↑S.card

theorem NairTenenbaum.minpoly_primeSum_le_log_idealNormDirichlet {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (B : PowerBasis ℚ K) (hB : B.gen = ↑θ) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 < σ) : ∑ p ∈ S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ) ≤ Real.log (idealNormDirichlet K σ) + ↑(minpoly ℤ θ).natDegree ^ 2 * ∑' (n : ℕ), ↑n ^ (-2) + ↑(minpoly ℤ θ).natDegree * ↑(RingOfIntegers.exponent θ).primeFactors.card

theorem NairTenenbaum.exists_minpoly_primeSum_log_bound {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (B : PowerBasis ℚ K) (hB : B.gen = ↑θ) : ∃ (C : ℝ) (b : ℝ), 0 ≤ C ∧ 1 < b ∧ ∀ (σ : ℝ), 1 < σ → σ < b → ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → ∑ p ∈ S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ) ≤ C - Real.log (σ - 1)