Elementary weighted prime sums

Chebyshev's bound and partial summation control the logarithmically weighted prime sums required in the smooth-tail estimate. No prime number theorem is used.

noncomputable def NairTenenbaum.primeLogWeight (n : ℕ) : ℝ

The logarithmic weight supported on primes.

Equations

• NairTenenbaum.primeLogWeight n = if Nat.Prime n then Real.log ↑n else 0

noncomputable def NairTenenbaum.primeLogSum (x : ℝ) : ℝ

The partial sum of the prime logarithmic weights.

Equations

• NairTenenbaum.primeLogSum x = ∑ p ∈ Finset.Icc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p / ↑p

theorem NairTenenbaum.primeLogWeight_sum (x : ℝ) : ∑ n ∈ Finset.Icc 0 ⌊x⌋₊, primeLogWeight n = Chebyshev.theta x

theorem NairTenenbaum.primeLogSum_eq {x : ℝ} (hx : 2 ≤ x) : primeLogSum x = Chebyshev.theta x / x + ∫ (t : ℝ) in 2..x, Chebyshev.theta t / t ^ 2

An explicit partial-summation identity.

theorem NairTenenbaum.primeLogSum_le {x : ℝ} (hx : 2 ≤ x) : primeLogSum x ≤ Real.log 4 * (1 + Real.log x)

The weighted prime sum is O(log x) with an elementary explicit bound.

theorem NairTenenbaum.exp_sub_one_le_mul_exp (t : ℝ) : Real.exp t - 1 ≤ t * Real.exp t

theorem NairTenenbaum.prime_rpow_gap_sum_le {x β K : ℝ} (hx : 2 ≤ x) (hβ : 0 ≤ β) (hK : β * Real.log x ≤ K) : ∑ p ∈ Finset.Icc 0 ⌊x⌋₊ with Nat.Prime p, (↑p ^ β - 1) / ↑p ≤ β * Real.exp K * (Real.log 4 * (1 + Real.log x))

First-prime-power increment bound used by the exponential moment.

theorem NairTenenbaum.prime_rpow_gap_sum_uniform {x κ : ℝ} (hx : 2 ≤ x) (hκ : 0 ≤ κ) : ∑ p ∈ Finset.Icc 0 ⌊x⌋₊ with Nat.Prime p, (↑p ^ (κ / Real.log x) - 1) / ↑p ≤ κ * Real.exp κ * Real.log 4 * (1 + (Real.log 2)⁻¹)

Choosing β=κ/log x bounds the prime increments uniformly in the cutoff.