Hadamard factorization - PR ideas

Stream: PrimeNumberTheorem+

[Matteo Cipollina]

As anticipated here we have completed a formalization of the Hadamard factorization theorem (here) and of its application to the riemannZeta (here). Since the Hadamard factorization is supposed to play a key role in the formalization of the third path to PNT in PNT+ we thought it may be of interest that we have now refactored it to be more Mathlib/PNT+ idiomatic and self-contained, and we would be glad to PR it to PNT+.
We have tried to follow closely the main proof step and statement given by Terence Tao here (and we hav tried to leverage PNT+ and StrongPNT API as much as we could, though certainly a deeper integration could be achieved) to ensure the API could match the expectations in PNT+.
We haven’t directly PR’d the code to the main repository yet, since the very recent official contribution guidelines formally require contribution on open issues or tasks, but we are happy to proceed as you deem it fit, including connecting the code to the blueprint and doing additional refactor or golfing of the lengthier proofs, as well as helping porting idiomatically the parts of StrongPNT used.
However we have PR’d it to this fork of PNT+, ready to be upstreamed to main if, as and when deemed appropriate by @Alex Kontorovich and @Terence Tao .
In this refactor we have removed the ZeroData structure (useful but not mathlib idiomatic) so that the final theorem takes intrinsic hypotheses on an entire function f, e.g. EntireOfFiniteOrder ρ f, and do not require a user-supplied ZeroData. The proof now internally obtains an enumeration of zeros (or an appropriate divisor) and then applies canonical product API developed in the WeierstarssFactor, CanonicalProduct, Divisor, LogSingularity, CartanBound, ExpPoly and the main files.

There are prerequisites that we aim to submit to Mathlib soon and that we have temporarily added them to the Mathlib folder. They also include 2 files from Carleson that we have used to avoid reduplicating API for Annuli and which seem to be meant to be upstreamed to Mathlib at some point.
Upstreaming the application of this refactored version of Hadamard factorization to the zeta function would require an additional set of prerequisites involving the Gamma function and Stirling bounds that we have also added in the Mathlib folder, to which we would need to add some extracts from StrongPNT.Complex; as they would be too much to swallow in one cycle the zeta corollaries are probably better suited for a subsequent cycle of PRs.

[Terence Tao]

This looks great! Definitely this factorization will be useful later in the explicit PNT project. I haven't been as involved with StrongPNT, so I'll let Alex speak to how it would fit in there, but assuming it is compatible, I for one would be happy to have it PR'ed.

[Alex Kontorovich]

Indeed this is great! Since we already have Borel-Caratheodory, we no longer "need" Hadamard, but of course it would be good to have in general, and I'd be very happy if you decided to upstream it to PNT+. (I suppose even better, as long as you're upstreaming, would be to upstream to Mathlib, so that PNT+ gets it automatically at the next bump. But maybe it's a big file and not Mathlib-ready, in which case, we'd be happy to help host it!)