This follows from the mean value theorem.

Use Taylor’s theorem with remainder and the fact that the second derivative of \(\log (1+t)\) is at most \(1\) for \(t \geq 0\).

Use concavity of log.

The expression can be written as \(\frac{|\log (1-t^2)|}{|\log (1-t)| |\log (1+t)|}\). Now use the previous upper and lower bounds, noting that \(t^2 \leq 1/4\). NOTE: this gives the slightly weaker bound of \(16 \log (4/3) / 3\), but this can suffice for applications. The sharp bound would require showing that the left-hand side is monotone in \(t\), which looks true but not so easy to verify.

This follows from the previous estimate.

Symmetrize the integral and use and some numerical integration.

Upper bound \(\log n\) by \(\int _n^{n+1} \log t\ dt\) for \(n {\lt} x-1\) and by \(\log x\) for \(x-1 {\lt} n \leq x\) to bound

giving the claim.

Drop the \(n=1\) term. Lower bound \(\log n\) by \(\int _{n-1}^{n} \log t\ dt\) for \(2 \leq n {\lt} x\) to bound

giving the claim.

This follows from the identity \(\log n = \sum _{d|n} \Lambda (d)\) and rearranging sums.

This follows from direct computation.

This follows from direct computation.

This follows from direct computation.

This follows from direct computation for \(0 \leq x {\lt} 30\), and then by periodicity for larger \(x\).

Use Lemma 10.2.4 and Lemma 10.2.8.

Use Lemma 10.2.4, Lemma 10.2.8, and Lemma 10.2.6.

Use Lemma 10.2.1, Lemma 10.2.2, the definition of \(a\), and the triangle inequality, also using that \(\log (2)+\log (3)+\log (5)+\log (30) \geq 6\).

Use Lemma 10.2.10 and Proposition 10.2.1.

Use Lemma 10.2.10 and Proposition ??.

Numerical check (the maximum occurs at \(x=19\)). One only needs to check the case when \(x\) is a prime power.

Iterate Lemma 10.2.3 using Sublemma 10.2.1 .

Verified by brute-force: an \(O(N)\) incremental checker confirms \(\psi (N) \leq 1.11 N\) for every integer \(N = 1, \ldots , 11723\) via native_decide. The sparse checkpoint ladder originally described here is not needed. The real-variable case follows by monotonicity of \(\psi \).

Strong induction on \(x\). For \(x \leq 11723\) one can use Sublemma 10.2.2. Otherwise, we can use Proposition 10.2.3 and the triangle inequality.

This follows directly from the definitions of \(\psi \) and \(\theta \).

Follows from Sublemma 10.3.1 and substitution.

Follows from Sublemma 10.3.1 and Sublemma 10.3.2.

Follows from Sublemma 10.3.3 and rearranging the sum.

Follows from Sublemma 10.3.2 and substitution.

Follows from Sublemma 10.3.4 and Sublemma 10.3.5.

Follows from Sublemma 10.3.6 and the fact that \(\theta \) is an increasing function.

Follows from Sublemma 10.3.6 and the fact that \(\theta \) is an increasing function.

Follows from Sublemma 10.3.7 and Sublemma 10.3.2.

Follows from Sublemma 10.3.8 and Sublemma 10.3.2.

Both are equivalent to \(\sum _{x {\lt} p \leq x+h} 1 {\gt} 0\).

Both are equivalent to \(\sum _{x {\lt} p \leq x+h} \log p {\gt} 0\).

Lower bound \(\theta (x+h) - \theta (x)\) using \(\theta (x+h) \geq x+h (1 - E_\theta (x+h))\) and \(\theta (x) \leq x (1 + E_\theta (x))\) and apply Lemma 10.4.2.

Apply Lemma 10.4.3.

Apply Lemma 10.4.4 and Lemma 2.0.2.

If \(p_k\) is the largest prime less than or equal to \(x\), then \(p_{k+1} - p_k {\lt} g \leq h\), hence \(x {\lt} p_{k+1} \leq x+h\), giving the claim.

This in principle follows by establishing an analogue of Theorem 6.0.1, using mediumPNT in place of weakPNT.

Trivial

This follows from the definition of the Stieltjes integral.

Follows from Sublemma 10.5.2 and integration by parts.

Follows from Sublemma 10.5.3 and integration by parts.

Follows from Sublemma 10.5.4 and Definition 10.5.1.

Follows from Sublemma 10.5.3 applied to \(f(t) = 1\).

Follows from Sublemma 10.5.3 applied to \(f(t) = 1/t\).

Follows from Sublemma 10.5.3 applied to \(f(t) = 1/t\). One can also use this identity to demonstrate convergence of the limit defining \(B\).

Follows from Sublemma 10.5.3 applied to \(f(t) = \log t / t\). Convergence will need Theorem 10.5.1.

This follows from Theorem 10.6.3.

Follows immediately from the given hypothesis \(\theta (x) \leq \psi (x)\), splitting into the cases \(x ≥ x_1\) and \(x {\lt} x_1\).

From Theorem 10.3.1 we have \(\psi (x) - \theta (x) ≤ \psi (x^{1/2}) + \psi (x^{1/3}) + \psi (x^{1/5})\). Now apply the hypothesis on \(\psi (x)\) and Theorem 10.5.3.

Combine Lemmas 10.8.1 with \(b = \log X_1\) for the upper bound, and and 10.8.2 with \(b = \log X_0\) for the lower bound.

We combine together Theorem 10.8.1 and Theorem 10.8.3 with \(X_1 = 10^{19}\).

Bound each \(\theta (x^{1/k})\) term by \((1 + \alpha )x^{1/k}\) in Sublemma 10.3.1.

Clear.

Clear.

We have

Define \(s(k, n) := 2^{\frac{n+1}{k}}(2^{\frac{1}{3} - \frac{1}{k}} - 1)\). Note that \(s(k, n)\) is monotone increasing in \(n\) for each fixed \(k \geq 4\). By numerical computation (using the trick \(x \le 2 ^{p / q} \iff x ^q \le 2 ^p\) to verify decimal lower bounds \(x\)), \(\sum _{k=4}^{n} s(k, n) \ge \sum _{k=4}^{9} s(k, 9) {\gt} 2.12 {\gt} 2\). Thus \(u_{n+1} - u_n {\lt} 0\).

This follows from Sublemmas 10.8.4 and 10.8.5.

Follows from Sublemmas 10.8.3 and 10.8.6.

Follows since \(f(x)\) decreases on \([2^{\lfloor \frac{\log x_0}{\log 2} \rfloor }, 2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1})\).

Combines previous sublemmas.

Combines previous sublemmas.

We apply Proposition 10.8.1 with \(x_0 = e^b\) where we observe that \(x_0 = e^b \geq e^7 {\gt} 2^9\).

Note that in the paper, the inequality in Proposition 4 is strict, but the argument can only show nonstrict inequalities. If \(e^b \leq x \leq x_1^2\), then \(x^{1/2} \leq x_1\), and thus

On the other hand, if \(x^{1/2} {\gt} x_1 = e^{\log x_1}\), then we have by (2.7)

since \(\log x_1 \geq 7\). The last two inequalities for \(\theta (x^{1/2})\) combine to establish (2.8).

Note that in the paper, the inequality in Proposition 4 is strict, but the argument can only show nonstrict inequalities. As in the above subcase, we have for \(x \geq e^b\)

since \(x^{1/2} {\gt} e^{b/2} {\gt} x_1 \geq e^7\).

We have \(\psi (x) - \theta (x) = \theta (x^{1/2}) + \sum _{k=3}^{\lfloor \frac{\log x}{\log 2} \rfloor } \theta (x^{1/k})\). For any \(b \geq 7\), setting \(x_0 = e^b\) in Proposition 4, we bound \(\sum _{k=3}^{\lfloor \frac{\log x}{\log 2} \rfloor } \theta (x^{1/k})\) by \(\eta x^{1/3}\) as defined in (2.3). We bound \(\theta (x^{1/2})\) with Proposition ?? by taking either \(a_1 = 1 + \varepsilon (\log x_1)\) for \(b \leq 2\log x_1\) or \(a_1 = 1 + \varepsilon (b/2)\) for \(b {\gt} 2\log x_1\).

This is Theorem 5 applied to the default inputs in Definition 10.8.2.

We denote \(g(x) = (\log x)^{c_2 + k} \exp (-c_3 (\log x)^{\frac{1}{2}})\). By ??, \(|\theta (x) - x| {\lt} \frac{c_1 g(x) x}{(\log x)^k}\) for all \(x \geq c_4\). It suffices to bound \(g\): by calculus, \(g(x)\) decreases when \(x \geq \frac{4(c_2 + k)^2}{c_3^2}\). Therefore \(|\theta (x) - x| \leq \frac{c_1 g(e^b) x}{(\log x)^k}\). Note that \(c_1 g(e^b) = \mathcal{A}_k(b)\) and the condition on \(b\) follows from the conditions \(e^b \geq c_4\) and \(e^b \geq \frac{4(c_2 + k)^2}{c_3^2}\).

We write \(\theta (x) - x = \psi (x) - x + \theta (x) - \psi (x)\), apply the triangle inequality, and invoke Corollary 10.8.3 to obtain

The function in brackets decreases for \(x \geq e^{x_0}\) with \(x_0 \geq 1000\) (assuming reasonable hypotheses on \(A,B,C,R\)) and thus we obtain the desired bound with \(A'\) as above.

This follows from straightforward differentiation.

Clear from previous sublemma.

We apply Lemma 10.9.2. There are no roots when \(b {\lt} -\frac{c^2}{16a}\), and the derivative is always negative in this case.

We apply Lemma 10.9.2. If \(a {\gt} 0\), there are two real roots only if \(\frac{c^2}{4} + 4ab \geq 0\) or equivalently \(b \geq -\frac{c^2}{16a}\), and the derivative is negative for \(u {\gt} \frac{\frac{c}{2} + \sqrt{\frac{c^2}{4} + 4ab}}{2a}\).

We apply Lemma 10.9.2. If \(a = 0\), it is negative when \(u {\lt} \frac{-2b}{c}\). Note: this lemma is mistyped as \(\sqrt{\log x} {\gt} -2b/c\) in [ 15 ] .

This follows from Lemma 10.9.1 applied with \(a=1\), \(b=1-B\) and \(c=C/\sqrt{R}\).

The Dawson function satisfies the differential equation \(F'(x) + 2xF(x) = 1\) from which it follows that the second derivative satisfies \(F''(x) = −2F(x) − 2x(−2xF(x) + 1)\), so that at every critical point (where we have \(F(x) = \frac{1}{2x}\)) we have \(F''(x) = −\frac{1}{x}\). It follows that every positive critical value gives a local maximum, hence there is a unique such critical value and the function decreases after it. Numerically one may verify this is near 0.9241 see https://oeis.org/ A133841.

The proof of Corollary 10.8.4 essentially proves the proposition, but requires that \(x_0 \geq e^{1000}\) to conclude that the function

is decreasing. By Lemma 10.9.1, since \(B {\gt} C^2/8R\), the function is actually decreasing for all \(x\).

By Corollary 9.3.23, with \(R = 5.5666305\), and using the admissible asymptotic bound for \(E_\psi (x)\) with \(A_\psi = 121.096\), \(B = 3/2\), \(C = 2\), for all \(x \geq x_0 = e^{30}\), we can obtain \(\nu _{asymp}(x_0) \leq 6.3376 \cdot 10^{-7}\), from which one can conclude an admissible asymptotic bound for \(E_\theta (x)\) with \(A_\theta = 121.0961\), \(B = 3/2\), \(C = 2\), for all \(x \geq x_0 = e^{30}\). Additionally, the minimum value of \(\varepsilon _{\theta ,asymp}(x)\) for \(2 \leq x \leq e^{30}\) is roughly \(2.6271\ldots \) at \(x=2\). The results found in [ 2 , Table 13 and 14 ] give \(E_\theta (x) \leq 1 {\lt} \varepsilon _{\theta ,asymp}(2) \leq \varepsilon _{\theta ,asymp}(x)\) for all \(2 \leq x \leq e^{30}\).

From [ 14 , Table 6 ] we have \(\nu _{asymp}(x_0) \leq 10^{-200}\). Thus, one easily verifies that the rounding up involved in forming [ 14 , Table 6 ] exceeds the rounding up also needed to apply this step. Consequently we may use values from \(A_\theta \) taken from [ 14 , Table 6 ] directly but this does, in contrast to Corollary 10.9.2, require the assumption \(x {\gt} x_0\), as per that table.

This follows from Sublemma 10.5.6.

This follows from applying the triangle inequality to Sublemma 10.9.3.

NOTE: in order for the proof to work, some lower bounds on \(x_0\) were added to make various limits of integration non-negative.

Since \(\varepsilon _{\theta ,\mathrm{asymp}}(t)\) provides an admissible bound on \(\theta (t)\) for all \(t \geq x_0\), we have

We perform the substitution \(u = \sqrt{\log (t)}\) and note that \(u^{2B-3} \leq m(x_0, x)\) as defined in (21). Thus the above is bounded above by

Then, by completing the square \(u^2 - \frac{Cu}{\sqrt{R}} = \left( u - \frac{C}{2\sqrt{R}} \right)^2 - \frac{C^2}{4R}\) and doing the substitution \(v = u - \frac{C}{2\sqrt{R}}\), the above becomes

Now we have

Combining the above completes the proof.

The starting point is Sublemma 10.9.4. The assumption (\(\varepsilon _{\theta ,\mathrm{asymp}}(x)\) provides an admissible bound on \(\theta (x)\) for all \(x \geq x_0\)) to bound \(\frac{\theta (x) - x}{\log (x)}\) and Lemma 10.9.4 to bound \(\int _{x_0}^{x} \frac{\theta (t) - t}{t (\log (t))^2} dt\). We obtain

We recall that \(x \geq x_1 \geq x_0\). Note that, by Corollary 10.9.1,

is decreasing for all \(x\). Thus,

In addition, we have the simplification

by Definition 2.0.8 and by \(m(x_0,x) = (\log (x))^{(2B - 3)/2}\), since \(B \geq 3/2\). Finally, since \(\sqrt{\log (x_1)} - \frac{C}{2\sqrt{R}} {\gt} 1\), the Dawson function decreases for all \(x \geq x_1\):

We conclude by combining the above:

from which we deduce the announced bound.

The upper bound is immediate since \(\theta (x) \leq \psi (x)\) for all \(x\). For the lower bound, we have

By Theorem 10.3.1, we have

We use [ 4 , Theorem 2 ] , that for \(0 {\lt} x {\lt} 11\), \(\psi (x) {\lt} x\), and that \(\varepsilon _{\psi ,num}(10^{19}) {\lt} 2 \cdot 10^{-8}\). In particular when \(2 {\lt} x {\lt} 10^{38}\),

when \(10^{38} \leq x {\lt} 10^{54}\),

when \(10^{54} \leq x {\lt} 10^{95}\),

and finally when \(x \geq 10^{95}\),

The result follows by combining the worst coefficients from all cases and dividing by \(x\).

We split the integral at each \(e^{b_i}\) and apply the bound

Thus,

We conclude by using the identity: for all \(2 \leq a {\lt} b\),

Differentiate

to see that the difference is strictly increasing. Evaluating at \(x = 6.58\) and applying the mean value theorem gives the announced result.

This follows from Lemma 10.9.6 and the mean value theorem.

This is obtained by combining Sublemma ?? with the admissibility of \(\varepsilon _{\theta ,num}\) and Lemma 10.9.5.

Call the left-hand side \(f(x)\). We have

Using integration by parts, its derivative can be written as

From which we see that \(f'(x_1) = \frac{1}{\log x_1} {\gt} 0\), and that \(f'(x)\) is eventually negative. Thus there exists a critical point for \(f(x)\) to the right of \(x_1\). Moreover, by bounding \(\int _{x_1}^x \frac{6}{\log ^4 t} dt {\lt} 6 \frac{x - x_1}{\log ^4 x_1}\), one finds that \(f'(x_1 \log x_1) {\gt} 0\) if \(x_1 {\gt} e\). Now we write \(f'(x) = \frac{f_1(x)}{x^2}\) with

Its derivative is \(f_1'(x) = -\frac{1}{x} \int _{x_1}^x \frac{1}{\log ^2 t} dt\), which is negative for \(x {\gt} x_1\). Thus \(f_1(x)\) decreases and vanishes at most once, giving \(f(x)\) at most one critical point, \(x_m {\gt} x_1\), which is then the maximum of \(f(x)\). In other words, \(x_m\) satisfies \(f_1(x_m) = 0\), i.e. \(\mathrm{Li}(x_m) - \mathrm{Li}(x_1) + \frac{x_1}{\log x_1} = -\frac{x_m}{1 - \log x_m}\), which shows that \(f(x)\) attains its maximum at \(x = x_m\), where

Now, because \(x_m {\gt} x_1 \log x_1\) we obtain the bound

which gives the announced result.

Let \(f(x)\) be as in the previous sublemma. Notice that by assumption \(x_1 \leq x \leq x_2 \leq x_1 \log x_1 {\lt} x_m\), so that

This follows from the definitions of \(\mu _{num,1}\) and \(\mu _{num,2}\).

This follows by combining the three substeps.

This follows directly from Theorem 10.9.2 by taking the supremum over all partitions ending at infinity.

This follows by applying Theorem 10.9.1 with Proposition 10.9.1. The hypothesis \(B {\gt} C^2/8R\) is not present in original source.

We fix \(R = 1\), \(x_0 = 2\), \(x_1 = e^{100}\), \(A_\theta = 9.2211\), \(B = 1.5\) and \(C = 0.8476\). By Corollary 10.9.2, these are admissible for all \(x \geq 2\), so we can apply Theorem 10.9.1 and calculate that

This implies that \(A_\pi = 121.103\) is admissible for all \(x \geq e^{20000}\).

As in the proof of [ 14 , Lemmas 5.2 and 5.3 ] one may verify that the numerical results obtainable from Theorem 10.9.2, using Corollary 10.9.3, may be interpolated as a step function to give a bound on \(E_\pi (x)\) of the shape \(\varepsilon _{\pi ,asymp}(x)\). In this way we obtain that \(A_\pi = 121.107\) is admissible for \(x {\gt} 2\). Note that the subdivisions we use are essentially the same as used in [ 14 , Lemmas 5.2 and 5.3 ] . In Table 5 we give a sampling of the relevant values, more of the values of \(\varepsilon _{\pi ,num}(x_1)\) can be found in Table 4. Far more detailed versions of these tables will be posted online in https://arxiv.org/src/2206.12557v1/anc/PrimeCountingTables.pdf.

The bounds of the form \(\varepsilon _{\pi , asymp}(x)\) come from selecting a value \(A\) for which Corollary ?? provides a better bound at \(x = e^{7500}\) and from verifying that the bound in Corollary ?? decreases faster beyond this point. This final verification proceeds by looking at the derivative of the ratio as in Lemma ??. To verify these still hold for smaller \(x\), we proceed as below. To verify the results for any \(x\) in \(\log (10^{19}) {\lt} \log (x) {\lt} 100000\), one simply proceeds as in [ 14 , Lemmas 5.2, 5.3 ] and interpolates the numerical results of Theorem 10.9.2. For instance, we use the values in Table 4 as a step function and verifies that it provides a tighter bound than we are claiming. Note that our verification uses a more refined collection of values than those provided in Table 4 or the tables posted online in https://arxiv.org/src/2206.12557v1/anc/PrimeCountingTables.pdf. To verify results for \(x {\lt} 10^{19}\), one compares against the results from Theorem 10.6.1, or one checks directly for particularly small \(x\).

Same as in Corollary ??.

We numerically verify that the inequality holds by showing that, for \(1 \leq n \leq 25\) and all \(x \in [p_n, p_{n+1}]\),

For \(x\) satisfying \(p_{25} = 97 \leq x \leq 10^{19}\), we use Theorems 10.6.5, 10.6.6 and verify

For \(x {\gt} 10^{19}\), we use Theorem ?? as well as values for \(\varepsilon _{\pi ,num}(x)\) found in Table 4 to conclude

Direct computation.

Verified by computer. Unlikely to be formalizable in Lean with current technology, except for the small values of the table.

Brute force verification.

Verified by computer. Unlikely to be formalizable in Lean with current technology, except for the small values of the table.

If not, then there would be an entry in Table 8 with \(g {\gt} 1476\), which can be verified not to be the case.

Direct computation.

Verified by computer. Unlikely to be formalizable in Lean with current technology, except for the small values of the table.

Brute force verification.

Verified by computer. Unlikely to be formalizable in Lean with current technology, except for the small values of the table.

If not, then there would be an entry in Table 8 with \(P {\gt} 3278018069102480227\), which can be verified not to be the case.

Use Lemma 10.4.3 and Theorem 10.12.2.

Use Lemma 10.4.6 and Proposition 10.11.2.

This is a computer computation, likely not formalizable within Lean.

Combine the three substeps.

Unfortunately, Proposition 10.12.4 only covers the range \(x \geq \exp (5000)\). According to the author, the complete verification of this corollary requires several additional unpublished computations to cover the intermediate range, so this corollary will require significant effort to formalize.

This follows trivially (and wastefully) from the work of Dusart [ or the authors [ 23 , Cor. 2 ] . It should also follow from the results of [ 15 ] .