The sharp weighted prime-root upper bound

The quantitative ideal count supplies the Mertens estimate for the ideal von Mangoldt function. Eventual root/ideal agreement gives the bound for each irreducible polynomial, with leading coefficient one.

theorem NairTenenbaum.exists_irreducible_rational_primeRootLogSum_bound {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : ℝ), 1 ≤ x → primeRootLogSum Q x ≤ Real.log x + B

theorem NairTenenbaum.exists_irreducible_primeRootLogSum_bound {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : ℝ), 1 ≤ x → primeRootLogSum Q x ≤ Real.log x + B