The convergent infinite weighted prime step

The finite recurrence passes to all primes. The main prime series is kept explicit, so its sharp arithmetic estimate remains a separate task.

noncomputable def NairTenenbaum.rootPrimeDirichletSum (Q : Polynomial ℤ) (σ : ℝ) : ℝ

The prime Dirichlet sum weighted by polynomial root counts.

Equations

• NairTenenbaum.rootPrimeDirichletSum Q σ = ∑' (p : Nat.Primes), NairTenenbaum.rootPrimeLogWeight Q σ ↑p

theorem NairTenenbaum.rootPrimeDirichletSum_nonneg (Q : Polynomial ℤ) (σ : ℝ) : 0 ≤ rootPrimeDirichletSum Q σ

theorem NairTenenbaum.summable_rootPrimeLogWeight {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {σ : ℝ} (hσ : 1 < σ) : Summable fun (p : Nat.Primes) => rootPrimeLogWeight Q σ ↑p

theorem NairTenenbaum.finite_root_weighted_hooleyMoment_rpow_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (S : Finset Nat.Primes) (n : ℕ) {q : ℕ} (hq : 1 < q) {σ θ : ℝ} (hσ : 1 < σ) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : (∑ p ∈ S, if ¬↑p ∣ n then rootPrimeLogWeight Q σ ↑p * hooleyMoment q (↑p * n) ^ θ else 0) ≤ (2 * hooleyMoment q n) ^ θ * rootPrimeDirichletSum Q σ + rootPrimeDirichletSum Q σ ^ (1 - θ) * hooleyPrimeErrorBound Q q n ^ θ

theorem NairTenenbaum.infinite_root_weighted_hooleyMoment_rpow_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (n : ℕ) {q : ℕ} (hq : 1 < q) {σ θ : ℝ} (hσ : 1 < σ) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : (∑' (p : Nat.Primes), if ¬↑p ∣ n then rootPrimeLogWeight Q σ ↑p * hooleyMoment q (↑p * n) ^ θ else 0) ≤ (2 * hooleyMoment q n) ^ θ * rootPrimeDirichletSum Q σ + rootPrimeDirichletSum Q σ ^ (1 - θ) * hooleyPrimeErrorBound Q q n ^ θ