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.
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.
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
\[ x {\lt} p \le x\Bigl(1 + \frac{1}{\log ^3 x}\Bigr). \]