Prime number theorem in AP

Stream: PrimeNumberTheorem+

[Terence Tao]

Now that we have the issues framework up and running, we can start filling in some gaps in the older portions of the project. One natural target is the prime number theorem in arithmetic progressions, which we are close to being able to derive via the Wiener-Ikehara method: I have opened up PNT#541 PNT#542 PNT#543 PNT #592 to finish this off. It is conceivable that some of the proofs here are too long for a single formalization task, and may need to be broken up into subtasks; if you are interested in formalizing a portion of one of these tasks and need help breaking up the theorem into more manageable pieces, let me know and I can try to work on this. (EDIT: I just learned that one can assign a "size" to each task. I am therefore classifying these tasks as "medium", but potentially splittable into "small" tasks.)

There are also a few loose ends in Consequences.Lean; I have added PNT#540 to finish off one of these. The ones involving the Chebotarev density theorem are much further away from completion (at some point I actually need to find a proof of this theorem that I understand), so I will focus on these more achievable goals for now.

[Steven Rossi]

Def interested in doing some of the tasks, haven't looked at the current goals to see if they need to be broken up but if more are added i'll claim some

[Alastair Irving]

Is PNT#541 really needed, we already have the Chebyshev condition for primes so also for primes in AP by monotonicity (we don't care about the constant).

[Terence Tao]

Strictly speaking it isn't needed for the current application for the reason you indicate, but it could be potentially useful to not have to verify the Chebyshev condition for future applications, such as the Chebotarev density theorem (though I still don't have a good enough understanding of how one should prove that theorem to tell for sure).

[Terence Tao]

Added PNT #561 PNT#562 PNT#563 PNT#564 to formalize an alternate version of the decay bounds on the Fourier transform that use fewer differentiability hypotheses than the ones already formalized. (This is not strictly needed for the WeakPNT, but are closer to the "canonical" versions of these lemmas.)

[(Tom de Groot) Tomodovodoo]

I've formalized the WeakPNT-AP-prelim using ChatGPT 5.2 xhigh and Aristotle once more, I'd like to claim #542 to issue a PR to it, but currently it is already claimed. Can I claim it to file my PR and resolve the issue?

[Maksym Radziwill]

Tomodovodoo said:

I've formalized the WeakPNT-AP-prelim using ChatGPT 5.2 xhigh and Aristotle once more, I'd like to claim #542 to issue a PR to it, but currently it is already claimed. Can I claim it to file my PR and resolve the issue?

@Tomodovodoo please go ahead and upload it you can claim it

[(Tom de Groot) Tomodovodoo]

#541 is also finished based on my newer PR; Since it's part of @Alex Nguyen 's PR and I am not a maintainer of the repo, I will need to wait until they have accepted it before it can be merged into main.

In any case, Corollary2.3.2 (auto-cheby) is now solved in Lean as well.

Edit: #733 now has the complete PR ready to be merged now