Personal log

Stream: PrimeNumberTheorem+

[Terence Tao]

Inspired by a similar log I wrote for the equational theories project, I am starting a personal log to document the various things going on in this project, hopefully reducing some of the clutter in this Zulip. Here is the first entry: Day 2

[Terence Tao]

Day 3

[Alastair Irving]

Thanks for the interesting daily updates. Small correction, my first name is Alastair not Alex.

[Terence Tao]

Day 4 Day 5

[Terence Tao]

Day 6 - Day 10

Some of the achievements of the project so far:

• Complete proof of the fact that $\mathrm{LCM}(1,\dots,n)$ is not highly abundant for $n \geq 89693^2$ conditional on a prime number theorem of Dusart (which we are very far from being able to formalize right now).
• Near-complete proof of Erdos problem 392 regarding the factorization of $n!$. Only one unclaimed task left for this, PNT#665; perhaps someone would like to claim it?
• A complete proof of the prime number theorem in arithmetic progressions (and hence also Dirichlet's theorem, although the proof we give here instead uses the version docs#Nat.infinite_setOf_prime_and_eq_mod of this theorem from Mathlib).
• A complete proof of the Costa Pereira inequalities $\psi(x^{1/2})+\psi(x^{1/3}) + \psi(x^{1/7}) \leq \psi(x) - \theta(x) \leq \psi(x^{1/2})+\psi(x^{1/3}) + \psi(x^{1/5})$
• A partial proof of Mertens' second theorem $\sum_{p \leq x} 1/p = \log\log x + B + o(1)$ (several tasks in ROSSER still need to be completed for this, but this is in progress). Mertens' first theorem $\sum_{p \leq x} \log p = \log x + E + o(1)$ should also be at least partially proven soon.
• The various other projects ZETABOUND, MOBIUS, FKS2 are in various stages of completion. Some new projects BKLNW-APP, LOG have just been generated but have not yet had significant progress. BKLNW still needs to be refactored; I hope to do that today.
• The Chebotarev density theorem project will require a domain expert to propose a sensible path to the theorem that we can begin blueprint (PNT#584).
• The Fourier decay estimates PNT#562 PNT#563 are awaiting resolution of how best to formalize integration by parts for BV functions.

[Alex Kontorovich]

This is great, thanks! I've been swamped with the first week of class, but amazing how much progress there's been...

Terence Tao said:

• Complete proof of the fact that $\mathrm{LCM}(1,\dots,n)$ is not highly abundant for $n \geq 89693^2$ conditional on a prime number theorem of Dusart (which we are very far from being able to formalize right now).

Why are we far from Dusart's version?

• Near-complete proof of Erdos problem 392 regarding the factorization of $n!$. Only one unclaimed task left for this, PNT#665; perhaps someone would like to claim it?

sure, I'll take it.

• The Chebotarev density theorem project will require a domain expert to propose a sensible path to the theorem that we can begin blueprint (PNT#584).

I'd like to think about this some more. In my mind, it doesn't need to be split up into lots of subcases if we're doing it "properly", that is, using MediumPNT tools (or stronger) with error terms instead of only limits. It should really go through just like Dirichlet, once we get enough algebraic number theory (which for all I know, we already have by now?). But admittedly I haven't thought about it in a while...

[Terence Tao]

Alex Kontorovich said:

Why are we far from Dusart's version?

Basically because the only thing I have put in the blueprint for now from Dusart's paper are the statements of results, with no proofs. Also, Dusart's work relies on multiple prior references, going all the way back to Rosser and Schoenfeld, which I also haven't formalized other than a small number of lemmas. I have also been informed that there are some minor errors this work, though to my knowledge the final results are essentially correct. It is certainly something I plan to get around to, but am focusing for now on the Fiori-Kadiri-Swidninsky papers.

[Harald Helfgott]

Terence Tao said:

Day 6 - Day 10

Hi @Terence Tao - thank you for keeping this log; it is very helpful.

I just wanted to clarify something in the following passage in your log:

Harald Helfgott is closing in on a possible way to handle integration by parts for bounded variation functions; there is a proof of this by Wheeden and Zygmund that Aristotle looks capable of formalizing, though the proofs are not at Mathlib's level of quality so some intermediate process of creating a proof and then refining it within PNT+ may be needed.

What Aristotle and I were closing in on (and in fact achieved) was a formalization of Fejér's theorem in Wheeden and Zygmund, rather than integration by parts.

I would say that the proofs produced by Aristotle still need to be brought up to Mathlib's level of generality (e.g., we should treat functions from $\mathbb{R}/\mathbb{Z}$ to normed vector spaces, rather than functions from $\mathbb{R}$ to $\mathbb{R}$ with period $2\pi$) and that we hope we will also make the proofs more concise along the way. I will try my hand at it soon, but, given that this is my first project, I would be particularly eager to do it in collaboration with others.

The next step, which I am currently working on, is a proof of Dirichlet-Jordan using Fejér's theorem, also as in Wheeden and Zygmund. Integration by parts (of bounded variation functions) does appear there once, in the proof of Theorem 12.24, a decay estimate very similar to PNT#562, which, as one can see from the discussion above, people are still discussing how to prove.

Funnily enough, Wheeden-Zygmund do this IBP via Riemann-Stieltjes integration, and say so explicitly. I think this is a strong hint that
(a) having issues with Lebesgue-Stieltjes IBP at a relatively early level of library development has always been common, even back when there were no software libraries, only textbooks
(b) there is no shame in using Riemann-Stieltjes as a stopgap measure;
(c) Wheeden-Zygmund are ready to use pre-Lebesgue integrals when doing so is most straightforward.
One is almost tempted to add
(d) Wheeden and Zygmund were Hari Seldon, and made a remark whose import would become fully intelligible once we came to a (minor) crisis they foresaw.

At any rate: Aristotle and I will do our best to formalize the proof of Theorem 12.24 essentially as written in Wheeden-Zygmund, that is, using Riemann-Stieltjes. I don't think Riemann-Stieltjes integration is supported by Mathlib, so we will be implementing it as in wheeden-Zygmund, chapter 2. It ought to be easy to change that to Lebesgue IBP once Mathlib implements Lebesgue IBP. I suspect , though, that there must be a reason why a good book mainly on Lebesgue integration uses Riemann-Stieltjes integration in its last chapter.

After that, given what we have just formalized (Fejér, Hardy's Tauberian theorem), formalizing Dirichler-Jordan should be straightforward.

[Sébastien Gouëzel]

Harald Helfgott said:

The next step, which I am currently working on, is a proof of Dirichlet-Jordan using Fejér's theorem, also as in Wheeden and Zygmund. Integration by parts (of bounded variation functions) does appear there once, in the proof of Theorem 12.24, a decay estimate very similar to PNT#562, which, as one can see from the discussion above, people are still discussing how to prove.

Funnily enough, Wheeden-Zygmund do this IBP via Riemann-Stieltjes integration, and say so explicitly.

I think the reason for that is pretty simple: the theory of vector measures (of which signed measures is a particular case) is rather different from the theory of usual measures because you can not use the order structure. This means that all the theory has to be rebuilt from scratch (extension theorems to get vector measures, integration theory wrt vector measures, and so on). If they wanted to use it in Wheeden-Zygmund, they would first have to build it, and it would take tens and tens of pages. This wouldn't make sense to do that in an elementary book mostly dealing with positive measures and the usual integral.

For Mathlib, I'm done with the construction of the vector measure associated to a bounded variation function, so we are on the right track (see #34055) but it will take time to get it merged because it's a little bit long.

[Harald Helfgott]

Sébastien Gouëzel said:

Harald Helfgott said:

The next step, which I am currently working on, is a proof of Dirichlet-Jordan using Fejér's theorem, also as in Wheeden and Zygmund. Integration by parts (of bounded variation functions) does appear there once, in the proof of Theorem 12.24, a decay estimate very similar to PNT#562, which, as one can see from the discussion above, people are still discussing how to prove.

Funnily enough, Wheeden-Zygmund do this IBP via Riemann-Stieltjes integration, and say so explicitly.

For Mathlib, I'm done with the construction of the vector measure associated to a bounded variation function, so we are on the right track (see #34055) but it will take time to get it merged because it's a little bit long.

I am glad to hear that there is progress!

In the mean time, the reality is that we are blocked from doing analysis even at a very basic level (arguably beneath 'elementary', if Wheeden-Zygmund counts as such) because essentials such as integration by parts are missing. What the past seems to suggest is that we should be pragmatic as (e.g.) Wheeden-Zygmund were pragmatic: do a very lightweight implementation of Riemann-Stieltjes, and use it for results we urgently need and cannot get otherwise.

These results will generally not make reference to the Riemann-Stieltjes theory at the level of statements, so I do not see how there would be an incompatibility. One basic example is the following standard bound, which is currently a roadblock in at least two projects here: if $f$ is a function of bounded variation, then its Fourier transform satisfies

$$\widehat{f}(t) = O(1/|t|),\quad\quad\text{in fact} |\widehat{f}(t)|\leq \frac{|f|_{\textrm{TV}}}{2\pi |t|}.$$

The statement itself does not involve Riemann-Stieltjes integration; RS only appears internally in the proof, which proceeds by integration by parts.

I am currently working on such a lightweight theory (or rather: I am waiting for Aristotle to finish a first draft), based on Appendix A from Montgomery-Vaughan, which follows an earlier treatment by Ingham, and uses the same definitions as Wheeden-Zygmund. I think it will be rather small, particularly after golfing.

My question would be whether we should think of editing it (once golfed) so as to meet Mathlib style, and what that would consist in. If it is a no-go for Mathlib, then we need not invest the effort -- but in that case we should think of how we communicate to other communities the existence of this theory, which removes a major early roadblock in analysis.

[Alex Kontorovich]

FYI Erdos 392 is now done, see PNT#784. It ended up not being so small (~700 lines) due to some off-by-one bugs, requiring global changes. I added some more comments to the PR; let me know if you'd like me to record them here as well, in case it's easier to find them in zulip...

[Alex Kontorovich]

FYI, I used Claude and GPT against each other at various points, but both were going around in circles (in different ways!), so I had to get into the proof myself. In the end the proof is something like 1/3 human, 1/3 Claude, 1/3 GPT. So I "labeled" it AI + Claude + GPT. But maybe the AI label is meant for when AI does it completely autonomously? Should I remove that label?

[Terence Tao]

I think the labels are fine as long as you give the more detailed explanation in the PRs. Since this closes off the entire Erdos 392 subproject I think we don't need to discuss the details in zulip. Anyway, thanks for the heroic effort in pushing this one to the finish line!

[David Michael Roberts]

Formatting issue in day 32: "verification of the odd Goldbach conjecture by Ramare and Saouter in 2003: they claimed to verify the conjecture up to" is followed by a number that is (...)\times 10^17 where only the 1 is in superscript and not the 7