Abel summation for the reciprocal-prime Dirichlet series

This file packages the general LSeries_eq_mul_integral_of_nonneg theorem for the coefficient sequence which is 1 / p at primes and zero elsewhere. Its partial sums are exactly primeReciprocalSum, so the resulting integral is a direct Abel/Mellin bridge for Mertens' second theorem.

noncomputable def AnalyticNumberTheory.Mertens.primeReciprocalCoeff (n : ℕ) : ℝ

The reciprocal-prime coefficient sequence, extended by zero away from primes.

Equations

• AnalyticNumberTheory.Mertens.primeReciprocalCoeff n = if Nat.Prime n then 1 / ↑n else 0

theorem AnalyticNumberTheory.Mertens.primeReciprocalCoeff_nonneg (n : ℕ) : 0 ≤ primeReciprocalCoeff n

theorem AnalyticNumberTheory.Mertens.primeReciprocalLSeries_eq_primeDirichletSum (s : ℂ) : LSeries (fun (n : ℕ) => ↑(primeReciprocalCoeff n)) s = ∑' (n : ℕ), if Nat.Prime n then ↑n ^ (-(1 + s)) else 0

Expanding the L-series shows explicitly that its exponent is shifted by one: at s = ε this is the prime Dirichlet sum ∑ p, p ^ (-(1 + ε)).

theorem AnalyticNumberTheory.Mertens.sum_Icc_primeReciprocalCoeff (n : ℕ) : ∑ k ∈ Finset.Icc 1 n, primeReciprocalCoeff k = primeReciprocalSum n

The partial sums of primeReciprocalCoeff are the finite reciprocal-prime sums.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_le_succ (n : ℕ) : primeReciprocalSum n ≤ ↑(n + 1)

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_le_one_add_log (n : ℕ) : primeReciprocalSum n ≤ 1 + Real.log ↑n

The reciprocal-prime sum is bounded by the corresponding harmonic sum.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_isBigO_natCast : primeReciprocalSum =O[Filter.atTop] fun (n : ℕ) => ↑n

A coarse unconditional growth bound, sufficient for the half-plane 1 < re s.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_isBigO_rpow {r : ℝ} (hr : 0 < r) : primeReciprocalSum =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r

The reciprocal-prime sum grows more slowly than every positive real power. This elementary estimate extends the Abel bridge to Re(s) > 0.

theorem AnalyticNumberTheory.Mertens.primeReciprocalLSeries_eq_mul_integral {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re) (hO : primeReciprocalSum =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) : LSeries (fun (n : ℕ) => ↑(primeReciprocalCoeff n)) s = s * ∫ (t : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊t⌋₊) * ↑t ^ (-(s + 1))

An Abel/Mellin representation of the reciprocal-prime L-series. The explicit growth hypothesis is deliberately separated from the analytic identity: any subsequent bound for primeReciprocalSum can be inserted here without changing the bridge.

theorem AnalyticNumberTheory.Mertens.primeDirichletSum_eq_mul_integral {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re) (hO : primeReciprocalSum =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) : (∑' (n : ℕ), if Nat.Prime n then ↑n ^ (-(1 + s)) else 0) = s * ∫ (t : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊t⌋₊) * ↑t ^ (-(s + 1))

The Abel/Mellin bridge written directly as a prime Dirichlet sum at exponent 1 + s.

theorem AnalyticNumberTheory.Mertens.primeDirichletSum_eq_mul_integral_of_pos (ε : ℝ) (hε : 0 < ε) : (∑' (n : ℕ), if Nat.Prime n then ↑n ^ (-(1 + ↑ε)) else 0) = ↑ε * ∫ (t : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊t⌋₊) * ↑t ^ (-(↑ε + 1))

The prime Dirichlet Abel formula in the full range needed at the pole: every positive real displacement ε from s = 1.

theorem AnalyticNumberTheory.Mertens.realPrimeDirichletSum_eq_mul_integral_of_pos (ε : ℝ) (hε : 0 < ε) : ↑(∑' (p : Nat.Primes), ↑↑p ^ (-(1 + ε))) = ↑ε * ∫ (t : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊t⌋₊) * ↑t ^ (-(↑ε + 1))

Real prime-indexed form of the positive-displacement Abel formula.

theorem AnalyticNumberTheory.Mertens.primeReciprocalLSeries_eq_mul_integral_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ↑(primeReciprocalCoeff n)) s = s * ∫ (t : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊t⌋₊) * ↑t ^ (-(s + 1))

An unconditional specialization of the Abel/Mellin bridge. Its coarse growth proof only gives 1 < re s; sharper Mertens bounds can instead be supplied to primeReciprocalLSeries_eq_mul_integral to reach every positive real part.