Documentation

AnalyticNumberTheory.Mertens.PrimeAbel

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.

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

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

Equations
Instances For
    source
    theorem AnalyticNumberTheory.Mertens.primeReciprocalCoeff_nonneg (n : ℕ) :
    0 ≤ primeReciprocalCoeff n
    source
    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 + ε)).

    source
    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.

    source
    theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_le_succ (n : ℕ) :
    primeReciprocalSum n ≤ ↑(n + 1)
    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.