Weighted prime sums via the prime number theorem

∑_{a < p ≤ b} p log p = b θ(b) - a θ(a) - ∫_a^b θ (Abel summation), and with θ(x) ~ x this gives ∑_{K/d < p ≤ K/c} p log p = K² (1/c² - 1/d²)/2 + o(K²).

noncomputable def Zeta5Irrational.cPrime (k : ℕ) : ℝ

c p = log p for primes, 0 otherwise.

Equations

• Zeta5Irrational.cPrime k = if Nat.Prime k then Real.log ↑k else 0

theorem Zeta5Irrational.theta_eq_sum_cPrime (t : ℝ) : Chebyshev.theta t = ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, cPrime k

noncomputable def Zeta5Irrational.wsum (a b : ℝ) : ℝ

The weighted prime sum ∑_{a < p ≤ b} p log p (as a sum over integers k with ⌊a⌋₊ < k ≤ ⌊b⌋₊).

Equations

• Zeta5Irrational.wsum a b = ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, ↑k * Zeta5Irrational.cPrime k

theorem Zeta5Irrational.wsum_eq {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : wsum a b = b * Chebyshev.theta b - a * Chebyshev.theta a - ∫ (t : ℝ) in Set.Ioc a b, Chebyshev.theta t

Abel summation for the weighted prime sum.

theorem Zeta5Irrational.theta_eventually_close {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (y : ℝ) in Filter.atTop, |Chebyshev.theta y - y| ≤ ε * y

The prime number theorem in ε-form: |θ(y) - y| ≤ ε y for all large y.

theorem Zeta5Irrational.integral_theta_bounds {a b ε : ℝ} (_ha : 0 ≤ a) (hab : a ≤ b) (h : ∀ y ∈ Set.Icc a b, |Chebyshev.theta y - y| ≤ ε * y) : |(∫ (t : ℝ) in Set.Ioc a b, Chebyshev.theta t) - (b ^ 2 - a ^ 2) / 2| ≤ ε * (b ^ 2 - a ^ 2) / 2

∫_a^b θ is close to (b² - a²)/2 when θ is close to the identity on [a, b].

theorem Zeta5Irrational.wsum_close {a b η : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (_hη : 0 ≤ η) (h : ∀ y ∈ Set.Icc a b, |Chebyshev.theta y - y| ≤ η * y) : |wsum a b - (b ^ 2 - a ^ 2) / 2| ≤ 2 * η * b ^ 2

The bound |wsum a b - (b² - a²)/2| ≤ 2 η b² when |θ(y) - y| ≤ η y on [a, b].

theorem Zeta5Irrational.wsum_tendsto {c d : ℝ} (hc : 0 < c) (hcd : c < d) : Filter.Tendsto (fun (K : ℝ) => wsum (K / d) (K / c) / K ^ 2) Filter.atTop (nhds ((1 / c ^ 2 - 1 / d ^ 2) / 2))

∑_{K/d < p ≤ K/c} p log p / K² → (1/c² - 1/d²)/2.