Tidying ZetaBounds

Stream: PrimeNumberTheorem+

[Alastair Irving]

There are several unused results in ZetaBounds.lean and also some significant differences between what the blueprint says we're using and what we're actually doing:

• LogDerivBndUniform, LogDerivZetaBndUniform' and LogDerivZetaBndAlt are all unused despite what the blueprint says. All our bounds actually come from LogDerivZetaBndUnif in MediumPNT.lean which isn't currently in the blueprint.
• ZetaInvBnd' and LogDerivZetaBnd' are strictly stronger than the versions without primes. We could drop the unprimed versions.

Are we happy to drop these unused results? If so do we want to update the blueprint to try and keep it in sync with the Lean files or has it passed its usefulness now we've proved MediumPNT and are wanting to upstream things to Mathlib. We could also consider moving BndUnif and its dependencies into ZetaBounds rather than MediumPNT>

[Alex Kontorovich]

Ideally the blueprint would indeed represent the formal proof (the interweaved LaTeX/Lean setup was supposed to make this easy to execute, but I didn't make a fuss when PRs added lemmas -- not just API -- that could use a blueprint node...). I think it'd be good to move unused theorems to, say, a ZetaBoundsUnused.lean file, so they're not being recorded in the blueprint. This will surely require updating some \uses{} tags as well. If you'd like to do this tidying, that would be fantastic, thank you!