8 Secondary explicit estimates
8.1 Definitions
In this section we define the basic types of secondary estimates we will work with in the project. Key references:
FKS1: Fiori–Kadiri–Swidninsky arXiv:2204.02588
FKS2: Fiori–Kadiri–Swidninsky arXiv:2206.12557
\(E_π(x) = |π(x) - Li(x)| / Li(x)\)
\(E_θ(x) = |θ(x) - x| / x\)
We say that \(E_θ\) satisfies a classical bound with parameters \(A, B, C, R, x_0\) if for all \(x \geq x_0\) we have
Similarly for \(E_π\).
8.2 The arguments of Rosser and Schoenfeld
In this section we formalize the arguments of Rosser and Schoenfeld that can convert primary estimates to secondary estimates, with an emphasis on parameter flexibility.
8.3 Summary of results
In this section we summarize the secondary results known in the literature (or obtained from this project), and (if their proof has already been formalized) provide a proof that reduces them to primary results, as well as implications of primary results to secondary results with appropriate choices of parameters.
Key references:
Dusart: https://piyanit.nl/wp-content/uploads/2020/10/art_10.1007_s11139-016-9839-4.pdf
FKS1: Fiori–Kadiri–Swidninsky arXiv:2204.02588
FKS2: Fiori–Kadiri–Swidninsky arXiv:2206.12557
PT: D. J. Platt and T. S. Trudgian, The error term in the prime number theorem, Math. Comp. 90 (2021), no. 328, 871–881.
JY: D. R. Johnston, A. Yang, Some explicit estimates for the error term in the prime number theorem, arXiv:2204.01980.
One has
for all \(x \geq \exp (2000)\).
One has
for all \(x \geq 2\).
One has
for all \(x \geq 2\).
TODO: input other results from JY
One has
for all \(x \geq 2\).
One has
for all \(x \geq 2\).
There exists a constant \(X_0\) (one may take \(X_0 = 89693\)) with the following property: for every real \(x \ge X_0\), there exists a prime \(p\) with
TODO: input other results from Dusart