Wiener-Ikehara source

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Hi humans,

I was wondering - are you following a text in particular for the Wiener-Ikehara proof?

Part of the reason that I'm asking is the following peculiar situation -
I needed a known Lemma for my own non-formal work. I couldn't find it quite in the form I needed it in the literature, so I had to state and prove it myself (it takes no more than a paragraph). Funnily enough, it turns out to be exactly what you call Lemma 1 (first_fourier).

So, you see: either this is in the literature in this form - or I would like to be able to refer to this project in a citation. In fact this is an inclusive 'or'.

(There are of course related statements in the literature, but the exact conditions are often not right for what I need.)

[David Loeffler]

I'd argue that a citation to the PNT+ project GitHub page would be at least as authoritative as a citation to a traditional journal article – some would say considerably more so!

[Harald Helfgott]

Sure, but is there a convention to follow? What would the appropriate BibTeX entry look like?

At any rate, does the LaTeX writeup here follow (or is it inspired by) a particular non-formal version of the Wiener-Ikehara proof in print?

[Johan Commelin]

I expect that @Terence Tao, @Alex Kontorovich and @Vincent Beffara will be able to give details about the sources of the Wiener-Ikehara formalization.

[Alex Kontorovich]

I looked back at first_fourier, and it's literally just opening the definitions and interchanging orders; I'm not sure what kind of reference you might be looking for that? The exact conditions (as you can see in the formal version) are that $n\mapsto f(n)/n^\sigma$ is summable for all $\sigma>1$, and that $\psi$ is continuous and integrable. Great question about how one references a github repository - I have no idea, but I'm sure lots of others have done this..?

[Harald Helfgott]

Obviously I know that; as I said, I stated and proved it myself (because I needed it and was trivial). It's just that I was annoyed about how I couldn't find it in that form in the literature; people keep making superfluous assumptions that are undesirable to me, such as that $\psi$ is compactly supported.

So, what version in the literature was your starting point?

[Rémy Degenne]

Github has CITATION files: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-citation-files .
I have never used them myself, but it looks like they exist for the purpose of indicating a way of citing the repository.

[Alex Kontorovich]

Harald Helfgott said:

Obviously I know that; as I said, I stated and proved it myself (because I needed it and was trivial). It's just that I was annoyed about how I couldn't find it in that form in the literature; people keep making superfluous assumptions that are undesirable to me, such as that $\psi$ is compactly supported.

So, what version in the literature was your starting point?

Yes, I agree; there are a lot of superfluous assumptions in the literature, and a nice feature of formalization is to force them out into the open. I don't think we're following a particular source in the literature, just improvising an approach. Certainly that's the case for the complex-analytic part, where we're following my own course notes. @Terence Tao, did you look at a reference when you wrote first_fourier?

[Harald Helfgott]

Speaking of superfluous assumptions, do you actually need $\psi$ to be continuous?

[Harald Helfgott]

For switching the order of the integral and the sum, dominated convergence would seem to work fine without a continuity assumption, no?

[Alex Kontorovich]

Heh, yeah, there may still remain some superfluous assumptions! The nice thing about Lean is you can comment out the assumption, see exactly where the proof breaks, and try to fix it...

[Harald Helfgott]

I take I should download a copy rather than vandalize the code.

[Alex Kontorovich]

You can also play with it online in Gitpod (or codespaces) if you don't want to download it; we have a link from the main repo.

[Terence Tao]

I think when I wrote the blueprint, I had located a copy of the statement of Wiener-Ikehara, but not a good source for the proof. It was faster for me to just work out a proof on my own than to hunt through the literature. As for first_fourier, I had written similar formulae in my analytic number theory lecture notes (see Proposition 7 of these notes), and many years previously I explicitly gave myself the task of rewriting some of the standard proofs of the prime number theorem in Fourier-analytic language, so I was probably drawing unconsciously from these past sources.

[Harald Helfgott]

Right, I had looked at your notes, and was a bit annoyed that you required $g$ (which corresponds to $\psi$) to be compactly supported.

[Harald Helfgott]

(in Proposition 7)

[Harald Helfgott]

TL;DR first_fourier (minus the continuity assumption, which I think is unnecessary) seems to me the obvious way to start, so it's funny I can't find in print - but admittedly I haven't tried very hard.

[Harald Helfgott]

And I thought you guys would know.

[Harald Helfgott]

@Terence Tao , I can't get your .dvi. Can you post the right link or set the permissions correctly?

[Harald Helfgott]

Ah, got it, never mind.

[llllvvuu]

Golfed the continuity assumption: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/243

[llllvvuu]

actually I'm not sure Measurable is needed either EDIT: ok that would probably be more than a one-liner OK it is a one-liner

[Terence Tao]

Nice! It's great how formalization can definitively settle these issues without having to need an expert to weigh on with their opinion. Presumably in second_fourier one can similarly relax continuity to integrability (+ AE measurability, I guess, if that is not part of the Lean definition of integrability). For the next few results after that, one could potentially relax the smoothness and compact support hypotheses on $\psi$ to the weaker assertion that $\psi$ and $\hat \psi$ are both integrable, though this might start requiring more than one-line alterations, and I am not sure how useful it would be.

[Harald Helfgott]

In Lemma 3 (and hence Lemma 4 and the following), requiring $\psi$ to be $C^2$ is too much. All you need is that $\psi$ be absolutely continuous and that $\psi'$ be of bounded variation; then the conclusion of Lemma 3 still holds (and you can express $C$ as a multiple of the total variation of $\psi'$). This is actually useful in other contexts. The proof should be the same but of course 'absolutely continuous' and 'bounded variation' must have been defined (have they?).

[Harald Helfgott]

It's an alternative to requiring that $\psi$ and $\widehat{\psi}$ be integrable. Matter of taste.

[Harald Helfgott]

I'm a bit confused though. I thought integrability implies measurability. Did I learn everything from the wrong book?

[Terence Tao]

In Mathlib, the definition of MeasureTheory.Integrable requires only AEStronglyMeasurable, which is slightly weaker than Measurable in a second countable space. I'm not sure as to the history of why Mathlib contributors chose these particular definitions, but I trust they had their reasons (there are certainly many other situations where the act of formalization revealed subtleties in the most natural choice of definitions that deviated from what one would find from textbooks intended for humans).

[Rémy Degenne]

@Sébastien Gouëzel wrote an explanation of our integral/integrable definition on page 7 of https://perso.univ-rennes1.fr/sebastien.gouezel/articles/change_variables.pdf

[Rémy Degenne]

It might have been before the introduction of strong measurability though. At least it explains the "a.e." part.

[Terence Tao]

strong measurability is discussed on page 8

[Sébastien Gouëzel]

strong measurability is needed when you define spectral projections of operators: these are typically integrals taking values in spaces of operators which are not second-countable, so you have to be careful.

[Terence Tao]

@Harald Helfgott By the way I don't see why absolute continuity of $\psi$ is relevant. Integrability, C^1, and bounded variation of the derivative should suffice. (You are welcome, by the way, to submit a pull request with a modified version of the lemma and its proof, to assist in the possible formalization of that modification.)

[Sébastien Gouëzel]

absolute continuity is weaker than C^1, right?

[Harald Helfgott]

On a compact interval, absolute continuity is weaker than $C^1$, right

[Harald Helfgott]

Absolute continuity is equivalent to "obeys the fundamental theorem of calculus". I don't know how to show that bounded variation of the derivative is enough without that.

[Terence Tao]

There is a technical issue in that absolute continuity only ensures that the derivative is defined almost everywhere rather than everywhere. Mathlib's definition of BoundedVariationOn requires a total function. This is likely a solvable problem, though.

[Harald Helfgott]

I mean, without absolute continuity, we could have copies of the devil's staircase added to our function anywhere the devil wants to without changing $f'$ outside a set of measure $0$.

[Terence Tao]

I think Mathlib sets the derivative by default to the junk value of 0 at points of non-differentiability. This may already be enough to solve the issue

[Harald Helfgott]

A problem worth solving, certainly. There are lots of functions that are only piecewise C^1 and that are very nice and useful (in fact some of them are optimal solutions relevant in number theory).

[Terence Tao]

Well, feel free to propose a precise replacement for Lemma 3, either as a pull request or as some LaTeX code here.

[Harald Helfgott]

(Not meaning to impose, just wondering whether people want Lemmas to be as widely useful as is possible without introducing complications.) OK - how do I access the existing LaTeX code?

[Terence Tao]

It starts at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Wiener.lean#L326 (in this project the LaTeX and Lean are integrated into a single file, but the LaTeX is in comments and so changing the LaTeX does not affect the compilation of the Lean). You would use git to clone a copy of the repository, make local edits, commit to a new branch, and submit that branch as a pull request (I may have the terminology slightly off, but this is basically the workflow).

[Terence Tao]

The Mathlib style is generally to state lemmas in their "natural" level of generality, which tends to be close to the "maximal" level of generality though it isn't quite the same thing. Maybe someone more involved with Mathlib can explain the philosophy better.

[Terence Tao]

Given that we would like to have at least one proof of PNT in Mathlib, it makes sense to work on refactoring the lemmas already in the project to be more conforming to Mathlib style now, even before we begin the Mathlib upstreaming in earnest.

[Terence Tao]

As you can see, the Lean code for the proof is somewhat non-trivial, so ideally one would only want to make changes that really do make minimal impact on the proof.

[Harald Helfgott]

OK, thanks. Well, since I am a newbie, let me take your invitation to post some LaTeX code here. I would say something like this:
\begin{lemma}[Decay bounds]\label{decay}\lean{decay_bounds}\leanok
(a) If $\psi:\R \to \C$ is integrable, then $|\hat \psi(u)|\leq |\psi|_1$ for all $u\in \R$.
(b) If $\psi:\R \to \C$ is of bounded variation, $|\hat \psi(u)|\leq \frac{|\psi|_{\textrm{TV}}}{2\pi |u|}$ for all $u\in \R$ with $u\ne 0$.
(c) If $\psi:\R \to \C$ is absolutely continuous and $\psi'$ is of bounded variation, then $|\hat \psi(u)|\leq \frac{|\psi'|_{\textrm{TV}}}{(2\pi |u|)^2}$ for all $u\in \R$ with $u\ne 0$.
\end{lemma}

[Harald Helfgott]

Not sure whether this fits in with the Mathlib style, either in the sense of fitting well enough or in the sense of fitting better than what you have right now. It's motivated by "why say just that a constant exists if the constant is nice, meaningful and pops out of the proof effortlessly", which seems to me to actually fit reasonably well with what you just said, but what do I know.

[Terence Tao]

One may need $\psi$ to be integrable as a running hypothesis for (a), (b), and (c), in order to use the classical definition of the Fourier transform $\hat \psi$. (The distributional Fourier transform would be available without this hypothesis, but I don't think Mathlib's support for distributional Fourier analysis is all that advanced right now.)

[Harald Helfgott]

That seems fair.

[Harald Helfgott]

BTW I'm assuming here that mathlib defines the Fourier transform like a normal person, with a factor of $e(- x t) = e^{- 2\pi i x t}$ in the integrand and no $\pi$s or $2$s floating elsewhere.

[Terence Tao]

I have to teach now but will look at how to integrate this into the Lean file a bit later. Probably it will be best to break things up into several small lemmas, one for each part (a), (b), (c), rather than have a single lemma with a complex conclusion.

[Harald Helfgott]

I agree. In the real world, I'd consider turning (c) or even (b) and (c) into their own thing for arbitrary order (if $\psi, \psi', \psi'',\dotsc,\psi^{(k-2)}$ are absolutely continuous and $\psi^{(k-1)}$ is of bounded variation...) but I do not know whether iteration would introduce complications in the Lean code.

[Terence Tao]

Added lemmas at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/244 as a first step to formalizing the alternate route to the decay bound.

[Harald Helfgott]

Not sure I agree with [Decay bound, alternate form]\label{decay-alt} as stated - we have a bound $|f|_1$ and a bound $|f'|_{TV}/(2\pi u)^2$, but a bound $\max( \|\psi\|_1, \| \psi' \|_{TV} / (2\pi)^2) / (1+|u|^2)$ does not follow. What does follow (easily) is a bound $C/(1+|u|^2)$ for some $C$ (which can be described explicitly, but we may not want to). This seems best: for explicit work, you'd use the bounds $|f|_1$ and $|f'|_{TV}/(2\pi u)^2,$ whereas for non-explicit work, you may choose to use either those bounds or the bound $C/(1+|u|^2)$ people have been using, depending on what you find most convenient.

[Terence Tao]

I think changing "max" to "plus" should fix the issue.

[Harald Helfgott]

Right, by (a+b)/(c+d) >= min(a/c,b/d).

[Sébastien Gouëzel]

I don't think we have absolute continuous functions in mathlib for now. It's not that it's particularly difficult, just that nobody has needed it strong enough to implement it. In general, people are motivated by the applications: they want to prove a theorem, and along the way they need absolute continuity of functions for some proof, so they will implement it. It just hasn't happened yet.

[Harald Helfgott]

They are a useful thing to have. They give the right level of generality for many statements (and if I understand correctly that's a mathlib standard): on a compact interval, they are exactly the functions for which FTC holds.

[Harald Helfgott]

Actually, I don't know whether there's a handy name for functions on $\mathbb{R}$ for which FTC holds. (I suppose it depends on whether one just wants $f(y) - f(x) = \int_x^y f'(t) dt$ or also $f(x) = \lim_{t\to -\infty} f(t) + \int_{-\infty}^x f'(t) dt$.)

[Harald Helfgott]

Is absolute continuity still equivalent to the latter, stronger sense?

[Sébastien Gouëzel]

Sure. It's just that nobody has needed them yet badly enough. For instance, FTC is stated assuming that the function is differentiable everywhere, and its derivative is integrable (which is a nontrivial version, but orthogonal to the question of absolute continuity)

[Harald Helfgott]

That leaves out a lot of useful functions.

[David Loeffler]

Harald Helfgott said:

That leaves out a lot of useful functions.

What kind of functions are "useful"? One of the things I've learned from my own formalization projects is that there can be a bit of a communication gulf between experts in a given area per se, and people working in other areas where those results are used, about which cases of a given theorem are "the interesting ones" and hence which directions of generalisation should be pursued. So I think it's really valuable knowledge that this particular version of FTC (allowing absolutely-continuous functions) has applications in analytic number theory.

(One example of this kind of "mis-match" that comes to mind is Cauchy's integral formula. The version in Mathlib has extremely weak hypotheses on the function, e.g. allowing countably many points of non-differentiability, but requires the contour to be a rectangle or circle. For the applications I have in mind, I'd happily live with far more restrictive hypotheses on the integrand if it would allow us to handle general piecewise C^1 paths.)

[Harald Helfgott]

Continuous, piecewise $C^1$ functions, for instance. Those are useful not just in analytic number theory - often the optimal function with support on $[-1,1]$ in a variational problem is continuous but not differentiable at $-1$ or $1$. You can try to be less general (do piecewise $C^1$ functions - but is that really simpler than absolutely continuous functions?) or more general (distributions - but that, while certainly useful, might open cans of invertebrates). But AC functions seem to be a happy medium, in part because (at least on intervals) they are exactly those for which FTC is true.

[Harald Helfgott]

That's relevant even to Tauberian proofs of PNT (I'll explain in a bit).

[Harald Helfgott]

Now that I think of it, I'm pretty sure I've seen Terry use the quadratic decay Lemma in one of his papers for a function that is only piecewise differentiable.

[Kevin Buzzard]

(double $$ for LaTeX here, for some reason; single $ does nothing and double $$ does not put the maths on a new line. You can edit previous posts to make them more legible if you like)

[Harald Helfgott]

General question: how do we cite a lemma or proposition in the current version of the proof? Reason: at the beginning of a paper I am coauthoring, I am using (and proving) a simple lemma very close to Lemma 1 (first_fourier) here. In fact, now that I've pointed that a condition that used to be present in Lemma 1 here was unnecessary, and that it has been removed, Lemma 1 here and the little lemma in my paper have become essentially identical. I'd like to be able to cite the project in some fashion. (Curiously, I haven't been able to find a form of the lemma that comes as close to what I had.)

[Harald Helfgott]

(I just explained things that everybody in this thread already knows - I thought I'd be able to post my message more broadly, but I've apparently failed.)

[Johan Commelin]

I imagine you could have a link to a specific commit + file + line number on github.

[Harald Helfgott]

OK. But what would the BibTeX entry even look like?

[Johan Commelin]

Isn't there an @online bibtex type, where you give the name of the repo, and a link to github?

[Johan Commelin]

Concerning authors: that's a question for @Alex Kontorovich and @Terence Tao, I suppose.

[Johan Commelin]

But I could also imagine just linking to the repo in a footnote, without a bibtex entry... :shrug:

[Terence Tao]

There is also the URL at https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/sect0002.html#first_fourier , though this is not frozen in time in contrasto the github commit.

I don't think we've discussed authorship yet for the project (it's not clear whether there will be a traditionally published product from this project), so for now I guess it is just the "Prime Number Theorem And..." project, with no authors listed. (But this is a discussion we should have, and incorporate into the documentation for the project, at some point.)

[Harald Helfgott]

All right, but how does one cite "Prime Number Theorem And..."? It would help if there were a standard BibTeX entry.

[Terence Tao]

Fair enough. I just added a CITATION.cff file to my pull request, so when it is merged, the github repository should then magically acquire a "Cite this repository" link somewhere.

[Terence Tao]

... and, the link is now up.
image.png

[Harald Helfgott]

Thanks!

I see that many people are active - I suppose the project will eventually be formalized as something multi-authored rather than two-authored.

[Terence Tao]

Yeah, we need to discuss that properly at some point. In other projects (e.g., Equational Theories) we have set up a document for each contributor to record their contributions; here is the one for Equational theories (still under construction). I would be happy to see something similar set up here, but it hasn't been discussed yet. (For many of these projects we are basically laying the tracks simultaneously with the train moving forward, metaphorically speaking.)

[Harald Helfgott]

Very well. By the way, would people be interested in having an explicit fork (or perhaps that should be a different project, hosted elsewhere)?

[Harald Helfgott]

I'll put something in the arXiv (in collaboration with Andrés Chirre) in the next few weeks - it uses a mixture of Tauberian and complex techniques.

[Harald Helfgott]

I'd think formalizing explicit results is of particular interest in part because explicit results are a subarea of analytic number theory that sometimes has trust issues.

[Terence Tao]

I think explicit estimates are an excellent use case for formalization. Over at the Carleson project, they are finding that it is easier to formalize harmonic analysis estimates with explicit constants. I think we are very liberal with the "+" in "PrimeNumberTheorem+": if it looks like there is a critical mass of people interested in formalizing explicit number theory estimates, we could definitely add that into this project.

[Harald Helfgott]

And of course the blueprint structure would encourage us to keep everything as clean as possible.