7 Explicit estimates
We will try to systematically collect explicit estimates related to the prime number theorem from the literature, and formalize them in a modular fashion. We divide such estimates into four classes:
Zeta function explicit estimates: bounds on the zeta function and its zeroes.
Primary explicit estimates: those that are directly control \(\psi (x)\) and \(M(x)\), usually via information on the zeta function.
Secondary explicit estimates: these are useful general-purpose estimates on functions relating to the primes, such as bounds on the \(n\)-th prime, or estimates for the prime counting function \(\pi (x)\). These are generally derived from primary estimates and elementary arguments.
Tertiary explicit estimates: these are bespoke applications to particular problems in analytic number theory or combinatorics that often require secondary estimates as input.
In this project we will state the best available zeta and primary estimates known in the literature, and try to formalize at least some of them; state the best available secondary estimates known in the literature, as well as various tools from passing from primary to secondary estimates, and formalize these; and then finally formalize some tertiary estimates as applications of the secondary ones.
7.1 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.
For any \(x \geq 1\), one has
(NOTE: this identity is not actually needed in the proof of Mertens’ theorems, but may be worth recording nevertheless.)
We have
For any \(x \geq 1\), one has
Trivial since \(\log n \leq \log x\).
For any \(x \geq 1\), one has
We have
Here we use the monotonicity of \(\log n\) (and its vanishing at \(n=1\)) and the crude bound \(\log x \leq x\). Note: the tools at Mathlib.Analysis.SumIntegralComparisons may be useful.
For any \(x \geq 1\), one has
Follows from the definition of the factorial function. Is not needed for the Mertens theorems, but is a natural fact to have.
For any \(x \geq 1\), one has
We have
We define \(E_{1,\Lambda }(x) := \sum _{d \leq x} \frac{\Lambda (d)}{d} - \log x\).
For any \(x \geq 1\), one has
For any \(x \geq 1\), one has
For any \(x \geq 1\), one has
Immediate from previous two corollaries.
We define \(E_{1,p}(x) := \sum _{p \leq x} \frac{\log p}{p} - \log x\).
For any \(x \geq 1\), one has
Drop all terms in Lemma 7.1.3 arising from prime powers.
For any \(x \geq 1\), one has
Drop all terms in Lemma ?? arising from prime powers.
One has \(E_1 \leq \frac{5 \log 2 + 3}{4}\)
We can bound \(E_1 \leq \sum _{n=2}^\infty \frac{\log n}{n(n-1)} \leq \frac{\log 2}{2} + \frac{3}{2} \sum _{n=3}^\infty \frac{\log n}{n^2}\). Calculus shows that \(\log x / x^2\) is decreasing for \(x \geq 2 {\gt} e^{1/2}\), so we can bound \(\sum _{n=3}^\infty \frac{\log n}{n^2} \leq \int _2^\infty \frac{\log t}{t^2}\ dt = \frac{\log 2+1}{2}\).
For any \(x \geq 1\), one has
and thus
where
Use the triangle inequality and the geometric series formula to estimate in Lemma ?? arising from prime powers.
For any \(x \geq 1\), one has
Immediate from previous two corollaries.
We set \(\gamma := \int _2^\infty \frac{E_{1,\Lambda }(t)}{t \log ^2 t} \, dt + 1 - \log \log 2\).
We define \(E_{2,\Lambda }(x) := \sum _{d \leq x} \frac{\Lambda (d)}{d \log d} - \log \log x - \gamma \).
For any \(x \geq 2\) and any \(f : {\mathbb N} \mapsto {\mathbb R}\), one has
Establish the identity
for \(2 \leq n \leq x\),multiply by \(f(n)\), then sum.
For any \(x \geq 2\), one has
From Lemma 7.1.1 one has
Now substitute the definitions of \(E_{1,\Lambda }\), \(E_{2,\Lambda }\), \(\gamma \) and simplify.
For any \(x \geq 2\), one has
If \(s {\gt} 1\) then \(\log \zeta (s) = - \log (s-1) + \Gamma '(1) + \gamma + (s-1) \int _1^\infty E_{2,\Lambda }(x) x^{-s}\ ds\).
First write
and integrate by parts to write this as
Standard calculations give
and
giving the claim.
\(\gamma \) is the Euler–Mascheroni constant.
Take limits as \(s \to 1\) in the previous asymptotic using known asymptotics for \(\zeta (s)\), and using that \(- \Gamma '(1)\) is the Euler–Mascheroni constant.
For any \(x \geq 2\), one has
Immediate from previous two corollaries.
We define \(M := \int _2^\infty \frac{E_{1,p}(t)}{t \log ^2 t} \, dt + 1 - \log \log 2\).
One has \(M \leq \frac{\log 4 + 4}{\log 2} + 1 - \log \log 2\).
Insert Lemma 7.1.6 into the definition of \(M\) and use the fact that \(\int _2^\infty \frac{dt}{t \log ^2 t} = 1/\log 2\).
One has \(M \geq -\frac{2 + E_1}{\log 2} + 1 - \log \log 2\).
Insert Lemma 7.1.7 into the definition of \(M\) and use the fact that \(\int _2^\infty \frac{dt}{t \log ^2 t} = 1/\log 2\).
For any \(x \geq 2\), one has
From Lemma 7.1.1 one has
Now substitute the definitions of \(E_{1,p}\), \(E_{2,p}\), \(M\) and simplify.
For any \(x \geq 2\), one has
Similar to Lemma 7.1.12.
For any \(x \geq 2\), one has
Immediate from previous two corollaries.
One has \(M = \gamma + \sum _p \log (1-\frac{1}{p}) + \frac{1}{p}\).
The RHS can be Taylor expanded as \(\sum _{j=2}^\infty \sum _p \frac{1}{jp^j}\). Meanwhile, the difference between \(\sum _{n \leq x} \frac{\Lambda (n)}{n \log n}\) and \(\sum _{p \leq x} \frac{1}{p}\) is equal to \(\sum _{j=2}^\infty \sum _{p: p^j \leq x} \frac{1}{j p^j}\). Applying the monotone convergence theorem, Lemma 7.1.13, and Lemma 7.1.9 gives the claim.
We define \(E_3(x) := \sum _{p \leq x} \log (1 - \frac{1}{p}) + \log \log x + \gamma \).
For any \(x \geq 2\), one has
Immediate from definition
For any \(x \geq 2\), one has
Using the Taylor expansion
one can write
One can bound \(\sum _{j \geq 2: p^j {\gt} x} \frac{j}{p^j}\) by \(O(1/p^2)\) when \(p {\gt} \sqrt{x}\) and by \(O(1/x)\) when \(p \leq \sqrt{x}\), so the second error here is \(O(1/\sqrt{x})\), giving the claim.