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
For all x > 2 we have \(E_ψ(x) {\lt} 9.22022(\log x)^{3/2} \exp (-0.8476836 \sqrt{\log x})\).
Proof
TODO.