MediumPNT is Done!

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

The last of the PRs from the Simons workshop arrived a few days ago, and now...
image.png
image.png

Congrats to all!!!

I think I would recommend that the next step be to pause forward progress and try to get as much as we can into Mathlib. This is a really big job, requiring that we go back through the various files (of which there are very many, with many varied degrees of code quality...), decide which things to clean, where to make better API (or even perhaps write some tactics -- for example, it'd be great if there were a filter version of bound?), etc etc.

Anyway, thanks all for your very hard work on this; it was truly a big team effort, and great fun to collaborate with everyone!

[Ruben Van de Velde]

Re: upstreaming - there's 6 files under Mathlib/ that have no PNT+ dependencies, and 11 outside Mathlib/. Not sure if the plan is to do those too. (According to the output of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/356)

[Alex Kontorovich]

Thanks! I merged your PR; I'm not sure exactly what it will do, but of course it'd be great to have an upstreaming blackboard... Let's see how it works

[Ruben Van de Velde]

Looks like there's a missing piece still - I'll look later, but for now there's https://alexkontorovich.github.io/PrimeNumberTheoremAnd/_includes/ready_to_upstream.md

[Alastair Irving]

As an initial simplification we could update the integral bounds in MediumPNT to use the conjugation symmetry where possible. This is already done for I8 but not 6, 7 and 9. That should make the file significantly shorter and hopefully less slow to compile. I'm happy to do this unless someone else has already started.

[Alex Kontorovich]

Sure, that'd be great; thanks Alastair!

[Floris van Doorn]

Very nice!
One small thing I spotted: mediumPNT seems to be missing a \lean command (the link to Lean is missing)

[Alex Kontorovich]

oops thanks!