Appendix A of BKLNW

Stream: PrimeNumberTheorem+

[Terence Tao]

I've spun off Appendix A of the BKLNW paper to a separate blueprint chapter and Lean file. This appendix combines together several existing results on the zeta function, as well as ways to convert the zeta function to estimates on $\psi$, to actually establish explicit estimates on $\psi$ of the form $|\psi(x) - x| \leq \varepsilon(b) x$ for all $x \geq e^b$, for various $b$, where $\varepsilon$ is a rather complicated piecewise constant function described in a lengthy table in the paper. The various inputs that go into this themselves involve a lot of argument and computation, but the way they are glued together here is actually rather straightforward. So about half of the sublemmas here cannot be proven yet because the precursor material has not yet been formalized, but there are several sublemmas PNT#750 PNT#751 PNT#752 PNT#753 connecting them together that should be fairly easy tasks.

There's only one outstanding task claimed for BKLNW right now, so soon I should be able to refactor the remaining portion of BKLNW (minus this appendix) and reopen the tasks there for claiming.