An elementary pole bound for the logarithmically weighted prime series

Logarithmic intervals and Chebyshev's bound give P(σ)≪deg(Q)/(σ−1). The leading constant is not asserted to be one. The exact integrating factor allows this elementary bound to be used separately from sharp bounds on R.

theorem NairTenenbaum.log_div_rpow_le_log_bin {p : ℕ} (hp : Nat.Prime p) {σ : ℝ} (hσ : 1 < σ) : Real.log ↑p / ↑p ^ σ ≤ Real.log ↑p / ↑p * Real.exp (-(σ - 1)) ^ ⌊Real.log ↑p⌋₊

theorem NairTenenbaum.prime_log_power_sum_le_geometric (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 < σ) : ∑ p ∈ S, Real.log ↑p / ↑p ^ σ ≤ Real.log 4 * Real.exp 2 / (1 - Real.exp (-(σ - 1)))

theorem NairTenenbaum.geometric_exp_inv_le_two_div {u : ℝ} (hu : 0 < u) (hu₁ : u ≤ 1) : (1 - Real.exp (-u))⁻¹ ≤ 2 / u

theorem NairTenenbaum.rootPrimeDirichletSum_le_pole {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {σ : ℝ} (hσ : 1 < σ) (hσ₂ : σ ≤ 2) : rootPrimeDirichletSum Q σ ≤ 2 * ↑Q.natDegree * (Real.log 4 * Real.exp 2) / (σ - 1)

theorem NairTenenbaum.hooleyReducedMomentMajorant_le_pole {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} {q : ℕ} (hq : 2 < q) (htq : t ≤ ↑q) (hσ : 1 < σ) (hσ₂ : σ ≤ 2) : hooleyReducedMomentMajorant Q t q σ ≤ hooleyPrimeErrorConstant Q q ^ (t / ↑q) / (↑q - 1) * (2 * ↑Q.natDegree * (Real.log 4 * Real.exp 2)) ^ (1 - t / ↑q) * (σ - 1) ^ (t / ↑q - 1) * Real.exp ((2 ^ t - 2 ^ (t / ↑q)) / (↑q - 1) * rootPrimePowerSum Q σ)

With the exact integrating factor, an elementary pole bound suffices for the logarithmically weighted prime series. Only R(σ) remains in the exponential factor.