Mertens' theorems

DefinitionThe constant in Mertens' first theorem#✓fully proved

With \(p\) ranging over the primes and \(\log\) the natural logarithm, this is the real number

\[M = \lim_{n \to \infty} \Bigl(\sum_{p \le n} \frac{\log p}{p} - \log n\Bigr),\]

the limit taken over natural numbers \(n\).

noncomputable def mertensConstant : ℝ :=
  Filter.limUnder Filter.atTop (fun n : ℕ =>
    (∑ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)),
      Real.log p / (p : ℝ)) - Real.log n)

Used by 2

Used byAxler's explicit Mertens first theorem · Dusart's explicit Mertens first theorem

TheoremDusart's explicit Mertens first theorem#●ready to prove

Let \(p\) range over the primes, let \(\log\) be the natural logarithm, and let \(M = \lim_{n \to \infty} \bigl(\sum_{p \le n} \frac{\log p}{p} - \log n\bigr)\) be the constant in Mertens' first theorem. For every real number \(x \ge 912560\) there is a real number \(E\) with \(|E| \le \frac{0.3}{(\log x)^2}\) such that

\[\sum_{p \le x} \frac{\log p}{p} = \log x + M + E.\]

theorem_wanted dusart_log_prime_sum (x : ℝ) (hx : 912560 ≤ x) :
    ∃ E, ((∑ p ∈ Finset.filter Nat.Prime (Finset.range (⌊x⌋₊ + 1)),
        Real.log p / (p : ℝ))
      = Real.log x + mertensConstant + E
      ∧ |E| ≤ 0.3 / (Real.log x) ^ 2)

Sources

• Pierre Dusart, Explicit estimates of some functions over primes, Ramanujan J. 45(1) (2018), 227–251, https://doi.org/10.1007/s11139-016-9839-4, Theorem 5.7.

Uses 1

Statement usesThe constant in Mertens' first theorem

DefinitionThe Meissel–Mertens constant#✓fully proved

With \(p\) ranging over the primes and \(\log\) the natural logarithm, the Meissel–Mertens constant is the real number

\[B = \lim_{n \to \infty} \Bigl(\sum_{p \le n} \frac{1}{p} - \log \log n\Bigr),\]

the limit taken over natural numbers \(n\). Numerically, \(B \approx 0.2614972128\).

noncomputable def meisselMertensConstant : ℝ :=
  Filter.limUnder Filter.atTop (fun n : ℕ =>
    (∑ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)),
      1 / (p : ℝ)) - Real.log (Real.log n))

Used by 13

Used byAxler's explicit Mertens second theorem · Mertens' second theorem with the Rosser–Schoenfeld error term · Upper bound for twisted prime sums with real coefficients · Dusart's explicit Mertens second theorem · Expansion of the reciprocal logarithm of the semiprime count · Counting primes of semiprime index · Crişan–Erban expansion of the semiprime counting function · Explicit estimate for the reciprocal sum of the semiprimes · Counting semiprimes of prime index · Eventual bound for \(C(k)B(k)\) by an explicit logarithm · Eventual bound for \(C(k)B(k)\) by \(e^\gamma \log\log\) of a primorial quotient · Mertens-type bound for a product over the first primes with one prime omitted · Explicit bound for a product over the first primes with one prime omitted

TheoremDusart's explicit Mertens second theorem#●ready to prove

Let \(p\) range over the primes, let \(\log\) be the natural logarithm, and let \(B = \lim_{n \to \infty} \bigl(\sum_{p \le n} \frac{1}{p} - \log \log n\bigr)\) be the Meissel–Mertens constant. For every real number \(x \ge 2278383\) there is a real number \(E\) with \(|E| \le \frac{0.2}{(\log x)^3}\) such that

\[\sum_{p \le x} \frac{1}{p} = \log \log x + B + E.\]

theorem_wanted dusart_reciprocal_prime_sum (x : ℝ) (hx : 2278383 ≤ x) :
    ∃ E, ((∑ p ∈ Finset.filter Nat.Prime (Finset.range (⌊x⌋₊ + 1)),
        1 / (p : ℝ))
      = Real.log (Real.log x) + meisselMertensConstant + E
      ∧ |E| ≤ 0.2 / (Real.log x) ^ 3)

Sources

• Pierre Dusart, Explicit estimates of some functions over primes, Ramanujan J. 45(1) (2018), 227–251, https://doi.org/10.1007/s11139-016-9839-4, Theorem 5.6.

Uses 1

Statement usesThe Meissel–Mertens constant

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.