A lower bound for the truncated prime-root reciprocal sum

noncomputable def NairTenenbaum.primeRootReciprocalSum (Q : Polynomial ℤ) (x : ℝ) : ℝ

The reciprocal-prime sum weighted by polynomial root counts.

Equations

• NairTenenbaum.primeRootReciprocalSum Q x = ∑ p ∈ Finset.range (⌊x⌋₊ + 1) with Nat.Prime p, ↑(NairTenenbaum.rootCount Q p) / ↑p

theorem NairTenenbaum.primeRootPowerWeight_le_logWeight_div {Q : Polynomial ℤ} {p : ℕ} (_hp : Nat.Prime p) {x σ : ℝ} (hx : 1 < x) (hpx : x ≤ ↑p) : ↑(rootCount Q p) * ↑p ^ (-σ) ≤ rootPrimeLogWeight Q σ p / Real.log x

theorem NairTenenbaum.finite_primeRootPowerSum_le_reciprocal_add_tail {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {x σ : ℝ} (hx : 1 < x) (hσ : 1 < σ) : ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) ≤ primeRootReciprocalSum Q x + rootPrimeDirichletSum Q σ / Real.log x

theorem NairTenenbaum.rootPrimePowerSum_le_reciprocal_add_tail {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {x σ : ℝ} (hx : 1 < x) (hσ : 1 < σ) : rootPrimePowerSum Q σ ≤ primeRootReciprocalSum Q x + rootPrimeDirichletSum Q σ / Real.log x

theorem NairTenenbaum.exists_primeRootReciprocalSum_lower_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (C : ℝ) (x₀ : ℝ), 1 < x₀ ∧ ∀ (x : ℝ), x₀ < x → Real.log (Real.log x) - C ≤ primeRootReciprocalSum Q x