restarting progress

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

Hi all,

With the start of the new semester, let’s get back to work on PNT! (My apologies for the long delay. Over the summer, @Vláďa Sedláček and I have been quietly finishing off almost all of the theorems in ZetaBounds, and now things are ready to go for PNT with a strong error term.) I'll send a list of tasks for that in the next few days, but we can get started already with discussing the following issues:

1. We should bump to the most recent mathlib (not entirely trivial, but shouldn’t be too hard?) Done by @Kim Morrison and @Ruben Van de Velde
2. Clean up existing code. There’s an awful lot there, generated by different people, and soon it will get so big (if it’s not already) that it will become rather unwieldy, with lots of repetition, extraneous lemmas, etc. Maybe someone wants to volunteer to work on this?
3. Related: Break off small PRs for mathlib. I don’t know if there’s a better or worse time to start doing this, but perhaps someone can already start to take this on.

As always, please announce your intension to work on some aspect here before you start, so that effort isn’t wasted or duplicated.

While I get things ready on my end, we can continue with corollaries of PNT, namely:

4. Prime counting function asymptotic to logarithmic integral Follows from the Chebyshev function bound, summation by parts, and some "easy" asymptotic manipulations. (Note that @Terence Tao recently proved chebyshev-asymptotic, that $\sum_{p \leq x} \log p \sim x$.) Claimed by @Ruben Van de Velde
5. Prime counting function asymptotic to x/log x Follows from the previous bound and some more "easy" asymptotic manipulations.
6. Asymptotic for n^th prime Should be a simple matter of "inverting" the previous result.
7. Bound for gaps between primes Follows from the previous bound and more "easy" asymptotic manipulations.
8. Primes in short intervals An equivalent form of the previous bound.

More soon!

[Rémy Degenne]

Regarding point 3 about PRing to Mathlib: the best moment to do it is asap! The longer you wait and accumulate lemmas in your repository and the more likely it is that your main results will never make it to Mathlib.

[Kim Morrison]

(I just opened the repository to take a look, and noticed that you have very large files, and this significantly impacts the build time. A useful chore might just be splitting Wiener into smaller files.)

[Kim Morrison]

I created https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/186 to do the initial bump to v4.8.0 v4.9.0 v4.10.0 of Lean and Mathlib.

[Kim Morrison]

However I see that your CI is set up so that it doesn't actually run until a maintainer approves the CI run. That's ... not super helpful, and hopefully you can fix that. I'm not an expert on leanblueprint, but I would hope that someone who is can help update your CI so that it runs out of the box.

[Kim Morrison]

One problem I encountered as the behaviour of simp changing: a reminder to use simp only whenever possible, as it makes simp more robust to Lean or Mathlib changing the simp set.

[Terence Tao]

Kim Morrison said:

One problem I encountered as the behaviour of simp changing: a reminder to use simp only whenever possible, as it makes simp more robust to Lean or Mathlib changing the simp set.

This is broader than PNT+, but I wonder if it is worth implementing a linter in Lean to pick up the use of simp in a proof and suggest a switch to simp only.

[Vincent Beffara]

Yeah Wiener is huge in the main branch with quite a few lemmas that are not actually used anywhere. I started separating out more generic things about bounds on Fourier transforms and such, some might still be in a branch I will have a look as soon as I am on a computer.

[Vincent Beffara]

Great to know that the project is alive!

[Johan Commelin]

@Terence Tao Yes, there is a linter that will flag uses of simp that are not "terminal". More precisely, tactics have been classified as "rigid" or "flexible", and simp is flexible, whereas simp only is rigid. A flexible tactic should not have rigid tactics after it.
But there were some issues with the linter, so I'm not sure it is active right now.

[Kim Morrison]

I got as far as bumping to v4.10.0, but will stop there. Hopefully someone can do the next step to v4.11.0, and then master. The next step involves quite a few fixes, from the looks of lake build.

[Damiano Testa]

The "flexible" linter should be in Mathlib, but is off by default. It flags potential maintenance concerns, as Johan mentioned, but sadly not always replacing simp by simp only is a good choice. This is the reason that it is not active by default.

[Damiano Testa]

However, you can turn it on and see what might cause problems during a bump.

[Ruben Van de Velde]

I'm taking a look at updating further

[Ruben Van de Velde]

https://github.com/Ruben-VandeVelde/PrimeNumberTheoremAnd/pull/new/v4.8.0 - hoping someone else will look at the AdditiveCombination failure

[Ruben Van de Velde]

Lunch now

[Ruben Van de Velde]

Pushed some more; now just stuck on additive combination. I also opened https://github.com/MichaelStollBayreuth/EulerProducts/pull/2 (cc @Michael Stoll )

[Mauricio Collares]

I have a cargo-culted version of https://github.com/leanprover-community/mathlib4/pull/15599. Opened https://github.com/Ruben-VandeVelde/PrimeNumberTheoremAnd/pull/1, but a review would be good.

[Ruben Van de Velde]

Finishing a few last changes

[Alex Kontorovich]

Kim Morrison said:

However I see that your CI is set up so that it doesn't actually run until a maintainer approves the CI run. That's ... not super helpful, and hopefully you can fix that. I'm not an expert on leanblueprint, but I would hope that someone who is can help update your CI so that it runs out of the box.

I think that's only for first-time contributions, and after that CI runs automatically. (Just a safety feature, right?)

[Alex Kontorovich]

Mauricio Collares said:

I have a cargo-culted version of https://github.com/leanprover-community/mathlib4/pull/15599. Opened https://github.com/Ruben-VandeVelde/PrimeNumberTheoremAnd/pull/1, but a review would be good.

Sorry I don't see the pull request?...

[Ruben Van de Velde]

Incoming

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/187

[Alex Kontorovich]

Whoops! Something happened... The CI on @Kim Morrison's PR passed, but then when I merged it in, now it's not compiling... D'oh! @Ian Jauslin to the rescue?...

[Vincent Beffara]

Looks like only docgen is failing, it should probably be bumped in the lakefile to a version that matches lean 4.11?

[Ruben Van de Velde]

Ah, that's annoying. I can take a look later

[Mauricio Collares]

Ruben Van de Velde said:

Ah, that's annoying. I can take a look later

I sent a PR to your fork to update doc-gen4

[Ruben Van de Velde]

Ah sorry, I made the change myself as well

[Mauricio Collares]

Even better!

[Mauricio Collares]

@Alex Kontorovich I think merging Ruben's PR will automatically fix CI checks on main.

[Alex Kontorovich]

Great thanks! Just merged, so fingers crossed...

[Alex Kontorovich]

Towards Task 3 (breaking off PRs for Mathlib), I could use some advice on how to organize this. (Or better yet, a volunteer to spearhead it?) Thanks!

[Ruben Van de Velde]

It looks like there's a number of files under PrimeNumberTheoremAnd/Mathlib/ that could easily be submitted. My suggestion to people who want to help is to pick one theorem or group of closely related theorems, do a quick check if there's obvious generalizations possible, put #find_home! foo after it and then make a PR to mathlib to add the results to that file. (Probably you want to mention here what you're looking at)

[Ruben Van de Velde]

I opened #16803 for PrimeNumberTheoremAnd/Mathlib/Topology/UniformSpace/UniformConvergence.lean

[Ruben Van de Velde]

Alex Kontorovich said:

4. Prime counting function asymptotic to logarithmic integral Follows from the Chebyshev function bound, summation by parts, and some "easy" asymptotic manipulations. (Note that Terence Tao recently proved chebyshev-asymptotic, that $\sum_{p \leq x} \log p \sim x$.)

Btw, I'm working on (the first line of) this

[Alex Kontorovich]

Hi @Ruben Van de Velde, it looks like pi_asymp is done, but the PR is still a "draft"? Do you want me to merge it? Thanks!

[Ruben Van de Velde]

I wanted to clean it up a bit first, but haven't had energy for it yet. If you're okay with merging, go ahead

[David Loeffler]

HI guys,

I'm an "interested bystander" on this project; I've been following progress, but haven't had a chance to contribute directly to PNT+ myself. Two thoughts I wanted to share with you:
(1) The above probably makes me a natural reviewer for Mathlib PR's upstreaming bits of this project. Don't hesitate to ping me for reviews.
(2) Analytic continuation of Dirichlet character L-functions is now in mathlib. The proof of $L(\chi, 1) \ne 0$ is not, but is certainly feasible. How much extra work, in addition to what PNT+ is currently doing, would be needed to get from $L(\chi, 1) \ne 0$ to counting primes in arithmetic progressions?

Best wishes, David

[Ruben Van de Velde]

Hi David, see https://github.com/leanprover-community/mathlib4/pull/17394 :)

[Terence Tao]

It should not be too difficult to get from $L(1,\chi) \neq 0$ to Dirichlet's theorem. It is "just" a matter of formalizing https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/sect0002.html#a0000000010 , and then adapting many of the results slowly being formalized in https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/sect0004.html to progressions. Once the non-vanishing theorem is online I can try to refactor the blueprint to smooth out the process (in particular breaking up the proof of Theorem 2 into more digestible pieces, right now it is much more a human readable proof than a human formalizable one).

[Vincent Beffara]

The Wiener-Ikehara theorem was rather painful to formalize, but probably not for deep reasons, mostly because integral and sum manipulations is not something that Lean is well adapted to at the moment. Hopefully the automatic Chebyshev bound will be easier...

[Michael Stoll]

I had some ideas as to how to show that $L(1,\chi) \ne 0$ (including for nontrivial quadratic $\chi$), once we have the analytic continuation of $L(s,\chi)$. This could be a project for my stay in Zurich (Oct 13-19) with @David Loeffler .

[Michael Stoll]

Ruben Van de Velde said:

Hi David, see https://github.com/leanprover-community/mathlib4/pull/17394 :)

@Ruben Van de Velde Can you ping me when you PR material from EulerProducts to Mathlib?

[Ruben Van de Velde]

Sure thing

[Michael Stoll]

The non-vanishing of $L(1, \chi)$ has by now been formalized in joint work with @Chris Birkbeck and @David Loeffler; see DirichletNonvanishing, which contains a bueprint. The code has also been upstreamed to EulerProducts.

[Terence Tao]

Ah! Time to get started on Dirichlet's theorem then. I can try later today to break up the large proof of PNT in AP in https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/sect0002.html#a0000000010 into smaller pieces that might be more suitable for formalization.

[Terence Tao]

See https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/196 . (Do we have an abbreviation for PNT PR's?) WeakPNT_AP is now split into three proof_wanted statements, which in principle can be proven independently, though I imagine that it would be logical to prove them in order.

[Kim Morrison]

I created a linkifier: PNT#196

[Michael Stoll]

I'd like to mention that I'm working on the orthogonality relations for DIrichlet characters (which are needed for Lemma 9 (Character decomposition) in the blueprint.

[Terence Tao]

Would you have the statements of the results you will be proving? Perhaps we can just take those statements as a sorry for now in order to prove Lemma 9.

[Michael Stoll]

I'm still fiddling around with this, but I should have something concrete soon.

[Michael Stoll]

I now have a complete proof of the orthogonality relation in the form

variable {R : Type*} [CommRing R] [IsDomain R] [HasAllRootsOfUnity R] {n : ℕ} [NeZero n]

theorem sum_char_inv_mul_char_eq {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
    ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then n.totient else 0 := by

(where HasAllRootsOfUnity is a type class recording that primitive nth roots of unity exist in the domain R for all n).

This is in the Orthogonality.lean file in EulerProducts.

I think I will next try to generalize what I did earlier on the logarithmic derivative of the Riemann zeta function to approach Lemma 9.

[Terence Tao]

OK, so I guess you are officially "claiming" Lemma 9 then? Hopefully once you have the Dirichlet series for the log derivative of L functions, putting everything together should just be some mucking about with the Mathlib support for infinite series.

[Michael Stoll]

Terence Tao said:

OK, so I guess you are officially "claiming" Lemma 9 then?

Yes. I already proved the properties of $-\zeta'/\zeta$ that are necessary to apply Wiener-Ikehara, and I think it should not be hard to generalize this to Dirichlet L-functions (now that we have their analytic continuation, thanks to @David Loeffler).

[Terence Tao]

Great! By the way, feel free to change the spelling of the Lean statement I wrote for Lemma 9. I basically wrote the first thing that passed the Lean compiler and looked right, but it might not be the most appropriate spelling, either to prove, or to apply.

[Michael Stoll]

I now have completed the proofs of Lemma 9, Proposition 2 and Theorem 2 (which is a version of Dirichlet's Theorem) from Section 2 of the blueprint (using the WIT stub defined in EulerProducts); this is in EulerProducts.PNT.

I'll work on polishing this next (but will be considerbly slower next week, working on a non-Lean project while visiting Basel). Once I'm done with it, we can discuss how to best integrate it with PNT+.

[Terence Tao]

That's great! We are now really close to formalizing the infinitude of primes in primitive residue classes (missing theorem 48 in https://leanprover-community.github.io/100-missing.html). I'll add some content to the "elementary corollaries" portion of the blueprint to get to there from Theorem 2 (this is all "obvious" and "routine", but needs some very slightly tricky manipulation with asymptotic error terms etc.; fortunately we already did this for the vanilla prime number theorem, so hopefully it won't be too challenging to adapt to progressions).

[Terence Tao]

Minor comment: I like how one can take advantage of the "junk definition" 0⁻¹ = 0 to simplify (starRingEnd ℂ) (χ a) to (χ a)⁻¹ in your formalization. This goes against my mathematical training, but certainly makes sense from a Lean standpoint!

[Michael Stoll]

I'm assuming IsUnit a, so everything is mathematically correct (and the spelling χ a⁻¹ with a : ZMod q seems to be the most convenient one to work with; no need for starRingEnd).

[Michael Stoll]

The only little thing I stumbled over was that IsUnit a → IsUnit a⁻¹ does not seem to be a one-liner for a : ZMod q...