7 Primary explicit estimates
7.1 Definitions
In this section we define the basic types of primary 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) - 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
We say that one has a classical zero-free region with parameter \(R\) if \(zeta(s)\) has no zeroes in the region \(Re(s) \geq 1 - 1 / R * \log |\Im s|\) for \(\Im (s) {\gt} 3\).
7.2 The estimates of Fiori, Kadiri, and Swidinsky
In this section we establish the primary results of Fiori, Kadiri, and Swidinsky.
7.3 Summary of results
In this section we summarize the primary results known in the literature, and (if their proof has already been formalized) provide a proof.
Key references:
FKS1: Fiori–Kadiri–Swidninsky arXiv:2204.02588
FKS2: Fiori–Kadiri–Swidninsky arXiv:2206.12557
MT: M. J. Mossinghoff and T. S. Trudgian, Nonnegative trigonometric polynomials and a zero-free region for the Riemann zeta-function, J. Number Theory. 157 (2015), 329–349.
MTY: M. J. Mossinghoff, T. S. Trudgian, and A. Yang, Nonnegative trigonometric polynomials and a zero-free region for the Riemann zeta-function, arXiv:2212.06867.
One has a classical zero-free region with \(R = 5.5666305\).
One has a classical zero-free region with \(R = 5.558691\).
For all x > 2 we have \(E_ψ(x) \leq 121.096 (\log x/R)^{3/2} \exp (-2 \sqrt{\log x/R})\) with \(R = 5.5666305\).
For all x > 2 we have \(E_ψ(x) \leq 9.22022(\log x)^{3/2} \exp (-0.8476836 \sqrt{\log x})\).
TODO.