Prime Number Theorem And ...

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

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

Theorem 49 FKS1 Corollary 1.4
#

For all x > 2 we have \(E_ψ(x) {\lt} 9.22022(\log x)^{3/2} \exp (-0.8476836 \sqrt{\log x})\).

Proof

TODO.