Things to work on

Stream: PrimeNumberTheorem+

[Alastair Irving]

It looks like we're getting very close with medium PNT. I was just wondering if there's anything which would be particularly helpful for me to work on? I'm keen not to duplicate work. If all the outstanding tasks are being dealt with then I can continue to try and tidy/simplify the code.

Maybe some further API changes are required in places like I2bound because we need to know the bound on $\zeta'/\zeta$ not just that it's holomorphic so maybe we need to pass that in as a hypothesis for now.

A couple of more significant tidies I was thinking about:

• Directly use the Mellin transform definition from Mathlib rather than having our own and proving they're equal.
• We could have a structure which captures our smooth function requirements (supported in $[1/2,2]$, cont diff, mass one and non-negative). That might save a lot of typing of those 4 hypotheses.

[Alex Kontorovich]

Thanks Alastair; indeed, there was a big push over the last two weeks at the Simons workshop. (We've been organizing things off of the main PNT+ thread, so the newcomers at the workshop could work without getting scooped by the pro's... I'm giving them one more week or so to wrap up their work, and then will report here the progress and anything that remains.)
As far as next steps, indeed, as soon as MediumPNT is done, I'd like to propose that we pause progress and try to go back to the beginning, refactor/clean everything up, and try to break it into lots of small pieces to go into Mathlib.