A sharp lower bound for the prime-root Dirichlet series

theorem NairTenenbaum.summable_monic_rootPrimePower {Q : Polynomial ℤ} (hQ : Q.Monic) {σ : ℝ} (hσ : 1 < σ) : Summable fun (p : Nat.Primes) => ↑(rootCount Q ↑p) * ↑↑p ^ (-σ)

theorem NairTenenbaum.exists_minpoly_rootPrimePowerSum_lower_bound {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (hD : RingOfIntegers.exponent θ ≠ 0) : ∃ (C : ℝ) (b : ℝ), 1 < b ∧ ∀ (σ : ℝ), 1 < σ → σ < b → -Real.log (σ - 1) - C ≤ rootPrimePowerSum (minpoly ℤ θ) σ