Comparing a root Euler product with its prime sum

The quadratic logarithm error is summable uniformly for σ≥1.

theorem NairTenenbaum.self_le_log_one_add_add_sq {x : ℝ} (hx : 0 ≤ x) : x ≤ Real.log (1 + x) + x ^ 2

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

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

theorem NairTenenbaum.monic_primeRoot_sum_le_log_product {Q : Polynomial ℤ} (hQ : Q.Monic) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) ≤ Real.log (∏ p ∈ S, (1 + ↑(rootCount Q p) * ↑p ^ (-σ))) + ↑Q.natDegree ^ 2 * ∑' (n : ℕ), ↑n ^ (-2)