Dirichlet's theorem on arithmetic progressions?

Stream: Is there code for X?

[Manuel Candales]

Is the Dirichlet's theorem on arithmetic progressions already implemented, or any of the special cases (like the infinitude of primes of the form 4k+1, 4k-1, etc)?
I didn't find this after doing a google site search or after looking through nat.prime and through the list of 100 theorems.

[Kevin Buzzard]

This is a nontrivial theorem; the standard proof involves a bunch of complex analysis and we have essentially no complex analysis. The special cases such as 4k+1, 4k-1 are easily accessible; we have enough about cyclotomic polynomials to do 1 mod N and indeed this might also be done.

[Manuel Candales]

I'll like to implement those, if you don't mind. How should I call them (still don't fully get the naming convention), and where should I place them? in nat.prime?

[Bhavik Mehta]

https://leanprover-community.github.io/mathlib_docs/number_theory/primes_congruent_one.html Here's the case for 1 mod N

[Riccardo Brasca]

As a special case we have docs#nat.exists_prime_ge_modeq_one for primes congruent to 1 mod N

[Manuel Candales]

ah, nice!

[Kevin Buzzard]

If you do 4k-1 you can also do 6k-1, this is the other elementary one. In general you can prove there's infinitely many primes not in a proper subgroup of $(\Z/N\Z)^\times$ by elementary methods but you only get a concrete equality when this group has order 2

[Bhavik Mehta]

There are a couple more special cases which should be doable without the heavy complex analysis, eg in https://kconrad.math.uconn.edu/blurbs/ugradnumthy/squaresandinfmanyprimes.pdf

[Johan Commelin]

Manuel Candales said:

How should I call them (still don't fully get the naming convention)?

Don't worry about that. Once you have a statement in Lean, you can post it here, and then more experienced users will be able to explain to you how to deduce the Lean name from the statement.

[Kevin Buzzard]

Yeah if you allow quadratic reciprocity (which we have in mathlib) then you can get a little further. There are very elementary methods (which don't use Z/pZ^* cyclic) for classifying when -1 and -3 are squares mod p which is why you don't even need QR for the cases I originally mentioned

[Mario Carneiro]

I would be remiss to not mention the proof of dirichlet's theorem in the form "every arithmetic progression contains infintely many primes" done in lean by translation from metamath. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336

[Mario Carneiro]

It's not in mathlib, though, because it has a dependency on the metamath library

[Dima Pasechnik]

Is there any progress on this - perhaps more complex analysis tools were implemented since April? A student of mine is thinking about this topic as a 4th year project (for a CS students).

[Johan Commelin]

There's ongoing work on getting complex analysis off the ground. I think Yury more or less has Cauchy's theorem?

[Yury G. Kudryashov]

I'm waiting for a review of #9496. Unfortunately, I don't know how to help @Sebastien Gouezel with the review.

[Yury G. Kudryashov]

(it is >4K lines)

[Yaël Dillies]

Wrong topic?

[Yaël Dillies]

Oh no, nevermind :sweat_smile:

[Yaël Dillies]

The obvious thing to make it easier to digest is to split it. Are you planning on doing that? I have a few comments on the finset lemmas.

[Yury G. Kudryashov]

I don't see any finset lemmas in this PR. Currently it has <100 LOC outside of analysis.box_integral and lots of code in this directory. I'm not sure that it makes sense to merge some files in this directory before others but if Sebastien will greenlight a part of the PR, then I'll move it to a new PR and merge to master.

[Yaël Dillies]

Oh sorry, just set. But nevermind because docs#set.pairwise_disjoint is too specialized.

[Patrick Massot]

I thought Sébastien was handling it. I'll try to help.

[Yury G. Kudryashov]

Sébastien already reviewed a large part of the PR. I was not trying to complain. I just wanted to say that there is a lot of code to review here, so one shouldn't expect this PR to be merged very quickly.