Bounded higher-prime-power contributions to the logarithmic main term

theorem NairTenenbaum.sum_inverse_prime_powers_ge_two_le {p : ℝ} (hp : 2 ≤ p) (L : ℕ) : ∑ ν ∈ Finset.Icc 2 L, p⁻¹ ^ ν ≤ 2 / p ^ 2

theorem NairTenenbaum.local_smoothLogRootMain_le {Q : Polynomial ℤ} {p L : ℕ} (hp : Nat.Prime p) {K : ℝ} (hK : 0 ≤ K) (hroot : ∀ (ν : ℕ), 0 < ν → ↑(rootCount Q (p ^ ν)) ≤ K) : ∑ ν ∈ Finset.Icc 1 L, ↑(rootCount Q (p ^ ν)) / ↑p ^ ν ≤ ↑(rootCount Q p) / ↑p + 2 * K / ↑p ^ 2

theorem NairTenenbaum.summable_log_div_nat_sq : Summable fun (n : ℕ) => Real.log ↑n / ↑n ^ 2

noncomputable def NairTenenbaum.primeRootLogSum (Q : Polynomial ℤ) (z : ℝ) : ℝ

The prime sum weighted by root counts and logarithms.

Equations

• NairTenenbaum.primeRootLogSum Q z = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, ↑(NairTenenbaum.rootCount Q p) / ↑p * Real.log ↑p

theorem NairTenenbaum.exists_smoothLogRootMain_le_prime_sum {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (hD : Q.discr ≠ 0) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (z : ℝ) (L : ℕ → ℕ), smoothLogRootMain Q z L ≤ primeRootLogSum Q z + B