Mertens' theorems
In this section we give explicit versions of Mertens' theorems:
- Mertens' first theorem (von Mangoldt form): \(\sum_{n \leq x} \frac{\Lambda(n)}{n} = \log x + O(1)\).
- Mertens' first theorem (prime form): \(\sum_{p \leq x} \frac{\log p}{p} = \log x + O(1)\).
- Mertens' second theorem (von Mangoldt form): \(\sum_{n \leq x} \frac{\Lambda(n)}{n \log n} = \log \log x + \gamma + O(1/\log x)\).
- Mertens' second theorem (prime form): \(\sum_{p \leq x} \frac{1}{p} = \log \log x + M + O(1/\log x)\), where \(M\) is the Meissel-Mertens constant.
- Mertens' third theorem: \(\prod_{p \leq x} (1 - \frac{1}{p}) = e^{-\gamma}/\log x + O(1/\log^2 x)\).
We aim to upstreaming these results to Mathlib. In particular, the arguments here should be self-contained and written for efficiency, coherency, and clarity. As such, extensive use of AI tools is strongly discouraged in this section.
The arguments here are drawn from Leo Goldmakher's “A quick proof of Mertens' theorem” from https://web.williams.edu/Mathematics/lg5/mertens.pdf
The unfinished formalization of Mertens' theorems by Arend Mellendijk in https://github.com/FLDutchmann/Analytic/blob/main/Analytic/Mertens.lean may also be relevant here.
Partial sum of logarithm… to Integral form for second error…
- Partial sum of logarithm identity
- Partial sum of logarithm upper bound
- Partial sum of logarithm lower bound
- Partial sum of logarithm as logarithm of factorial
- Partial sum of logarithm as sum of \(\Lambda(d)/d\)
- The remainder term in Mertens first theorem (von Mangoldt form)
- Partial sum of \(\Lambda(d)/d\) lower bound
- Partial sum of \(\Lambda(d)/d\) upper bound
- Mertens' first theorem (von Mangoldt form)
- The remainder term in Mertens first theorem (prime form)
- Prime error for Mertens first theorem bounded by von Mangoldt error
- Partial sum of \(\frac{\log p}{p}\) upper bound
- \(E_1\) summable
- Upper bound on \(E_1\)
- Partial sum of \(\frac{\log p}{p}\) lower bound
- Error term in Mertens' first theorem bounded (prime form)
- Alternate Formula for Euler-Mascheroni constant
- The remainder term in Mertens second theorem (von Mangoldt form)
- Integral identity involving inverse log weight
- Integral form for second error (von Mangoldt form)
Bound for second Mertens error… to Mertens' third theorem error…
- Bound for second Mertens error (von Mangoldt form)
- Dirichlet series for \(\log \zeta(s)\)
- Integration by parts identity for \(\log \zeta(s)\)
- First integral identity
- Second integral identity
- An identity for \(\log \zeta(s)\)
- limiting behavior of log zeta
- Compatibility with Mathlib Euler-Mascheroni constant
- Mertens' second theorem (weak von Mangoldt form)
- The Meissel-Mertens constant
- Upper bound for \(M\)
- Lower bound for \(M\)
- Integral form for second error (prime form)
- Bound for second error (prime form)
- Mertens' second theorem (weak prime form)
- Formula for Meissel-Mertens constant
- The remainder term in Mertens third theorem
- Mertens' third theorem error term
- Mertens' third theorem error bound
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.