Fourier decay, and what it confirms about real-analysis gaps

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Going forward, we will need basic estimates on the decay of Fourier transforms under differentiability assumptions of different strengths. Let me focus on the base case $k=2$. The versions with weaker assumptions in what follows are, by definition, the more useful ones, in that they can be applied to more cases; in particular, in analytic number theory, we often do not live in $C^2$ or even in a Sobolev space such as $W^{2,1}$.

[Harald Helfgott]

Let $f:\mathbb{R}\to \mathbb{C}$ with $f\in L^1$, and write $\widehat{f}(t)$ for its Fourier integral $\int f(x) e(- t x) dx$, where $e(\alpha) = e^{2\pi i \alpha}$. This is the same definition of the Fourier transform as in Mathlib.

[Harald Helfgott]

(a) Assume $f\in C^2$, $f', f''\in L^1$. Then $|\widehat{f}(t)|\leq \frac{|f''|_1}{(2\pi |t|)^2}$ for all $t\ne 0$.

Where are we now? I can't see quite this statement in Mathlib, but I see statements from which this can be deduced very easily. In fact, I just fed the statement to Aristotle with the cheeky "proof":

\begin{proof} I think you can figure this out. \end{proof}

and it proved it in a matter of minutes.

[Harald Helfgott]

b) Assuming $f$ is in the Sobolev space $W^{2,1}$, prove the same bound.

Where are we now? It doesn't look as if Sobolev spaces were defined as such in Mathlib. I'll leave this question to other people; for my purposes, $W^{2,1}$ is too restrictive. Typical example: the triangle function is not in $W^{2,1}$. I will focus on (c) and (d).

[Harald Helfgott]

(c) Assume $f$ is absolutely continuous and $f'$ has finite total variation $\textrm{TV}(f')<\infty$. Prove that, for $t\ne 0$, $|\widehat{f}(t)|\leq \frac{TV(f')}{(2\pi |t|)^k}$.

Where are we now? I gave this to Aristotle, with a bit of guidance, as one would give an advanced undergrad; here is the source file. It's been 5 hours - and no result yet. My guess is that it is getting stuck in the second integration-by-parts step, for exactly the same reason that it got stuck in IBP when formalizing the appendix I uploaded last week: support for Stieltjes integration (whether Riemann-Stieltjes or Lebesgue-Stieltjes) was poor in Mathlib-v.24.0, the version from 2-3 months ago that Aristotle uses. In fact, it is not completely clear to me how complete support for Stieltjes integration is right now. Let us discuss what needs to be done here. Perhaps someone wants to formalize this lemma by hand (in version (c), which we are discussing)? If the current framework is satisfactory, that should be very easy, so this is a good test case.

(d) Assuming $f$ is in $L^1$ and $D^2 f$ is a finite signed measure. Prove that $|\widehat{f}(t)|\leq \frac{\|df'\|}{(2\pi |t|)^k}$. This is equivalent to (c); it's just that the language in (c) is more classical, whereas (d) is unambiguously measure-theoretical.

Where are we now? I will try this now, but I suspect the solution is the same as in (c), or worse.

[Yongxi Lin (Aaron)]

Here is a PR #32305 for Sobolev spaces, people are working on it.

[Harald Helfgott]

Yongxi Lin (Aaron) said:

Here is a PR #32305 for Sobolev spaces, people are working on it.

Good, but, as I said, (c) and (d) are more useful in practice. At any rate measure theory is a basic human need, and, when one can't assume it (textbooks for advanced undergrads/beginning graduate students, or, it seems, Mathlib right now) one should have the right to have (c), at the very least.

[Terence Tao]

PNT#562 and PNT#563 are currently outstanding to establish the k=1,2 cases of (c) (with the appropriate corrections, namely that the TV norm needs to be applied to the k-1-fold definition of f). These issues have not yet been claimed by anyone.

[Yongxi Lin (Aaron)]

I have thought about these issues. PNT#562 needs integration by parts. PNT#562 needs $\widehat{f'}(\xi) = (2\pi i \xi)\,\widehat f(\xi)$, where $f$ is absolutely continuous and $f'$ is its almost everywhere defined derivative, which we also don't have in mathlib right now, we only have the smooth version: Real.fourier_deriv, and the proof of this also needs integration by part. Integration by parts constitutes the main obstruction :smiling_face_with_tear: .

[Harald Helfgott]

What do we do - contact the Mathlib team? (How?) Hack up integration by parts ourselves? Perform a rain dance?

[Ruben Van de Velde]

There's a number of integration by parts results in mathlib

[Moritz Doll]

Yongxi Lin (Aaron) said:

I have thought about these issues. PNT#562 needs integration by parts. PNT#562 needs $\widehat{f'}(\xi) = (2\pi i \xi)\,\widehat f(\xi)$, where $f$ is absolutely continuous and $f'$ is its almost everywhere defined derivative, which we also don't have in mathlib right now, we only have the smooth version: Real.fourier_deriv, and the proof of this also needs integration by part. Integration by parts constitutes the main obstruction :smiling_face_with_tear: .

We almost have this for tempered distributions, #34099. The question then is whether it is more painful to do some embedding stuff than proving the same result by hand.

[Harald Helfgott]

Ruben Van de Velde said:

There's a number of integration by parts results in mathlib

What we need for many of our applications is this:

Lemma. Let $f,g:[a,b]\to \mathbb{C}$ be such that $f$ is absolutely continuous and
$g$ is of bounded variation. Then

$$\int_a^b f'(x) g(x) dx = f(b) g(b) - f(a) g(a) - \int_a^b f(x) dg(x).$$

I've set Aristotle to run on this, but I am not optimistic; this seems to be a task for humans. We could often make do with stronger conditions of $f$ ($C^1$, etc.), but I don't think that's the problem.

[Terence Tao]

The bottleneck may be the existence of a human-generated informal proof of this statement which carefully addresses the low regularity of the situation. Once this is in place, I can add it to the blueprint and open up a task to prove it, and also add a note to PNT#562 to use this statement to complete that task. (One could try getting a separate AI to generate a proof of this statement, but I am not completely convinced that current AI models are reliable enough to manage the analysis subtleties in an appropriate fashion.)

[Harald Helfgott]

Well, one could say that's just real analysis/measure theory - but what would be really useful before we do that would be to have an informal sketch, in human terms, of what Mathlib already knows that is relevant to this, so that we know on what we can build.

[Harald Helfgott]

Incidentally, I just found that Aristotle refuses to make any progress on the following:

\begin{lemma}
Let $g:[a,b]\to \mathbb{C}$ be of bounded variation. Then
$\int_a^b |dg(x)| = TV(g),$
where $TV(g)$ denotes the total variation of $g$ on $[a,b]$.
\end{lemma}
\begin{proof}
Let us see whether you can do this on your own using Mathlib.
\end{proof}

I don't think the notation TV is the issue - it can provide a proof for the following (trivial) statement very quickly:
\begin{lemma}
Let $g:[a,b]\to \mathbb{C}$ be of bounded variation. Then
$\left|\int_a^b dg(x)\right|\leq TV(g),$
where $TV(g)$ denotes the total variation of $g$ on $[a,b]$.
\end{lemma}
\begin{proof}
Let us see whether you can do this on your own using Mathlib.
\end{proof}

What is going on?

[Moritz Doll]

Terence Tao said:

The bottleneck may be the existence of a human-generated informal proof of this statement which carefully addresses the low regularity of the situation. Once this is in place, I can add it to the blueprint and open up a task to prove it, and also add a note to PNT#562 to use this statement to complete that task. (One could try getting a separate AI to generate a proof of this statement, but I am not completely convinced that current AI models are reliable enough to manage the analysis subtleties in an appropriate fashion.)

What is actually needed? Are Lemma 2.1.4 and 2.1.5 used directly or are they only needed for Lemma 2.1.6?

[Harald Helfgott]

Moritz Doll said:

Terence Tao said:

The bottleneck may be the existence of a human-generated informal proof of this statement which carefully addresses the low regularity of the situation. Once this is in place, I can add it to the blueprint and open up a task to prove it, and also add a note to PNT#562 to use this statement to complete that task. (One could try getting a separate AI to generate a proof of this statement, but I am not completely convinced that current AI models are reliable enough to manage the analysis subtleties in an appropriate fashion.)

What is actually needed? Are Lemma 2.1.4 and 2.1.5 used directly or are they only needed for Lemma 2.1.6?

Well, I use Lemma 2.1.4 and 2.1.5 all the time, and presumably so does Terry. Ditto for the version with $\|\psi^{(k-1)}\|_{TV}/(2\pi |u|)^k$.

[Sébastien Gouëzel]

There are two bottlenecks to just make sense of the formula in Mathlib:
(1) we don't have the signed measure dg when g is a bounded variation function
(2) we don't have the integral with respect to a signed measure
Note that making sense of the formula is much harder than proving it, because crafting definitions is much harder than proving theorems.

These two bottlenecks disappear if, instead of BV functions, you are willing to work with monotone functions: we have the Stieltjes measure associated to a monotone function (this is a measure in the usual sense, not a signed measure) and we have integrals with respect to measures. For this case, Aristotle has already proved a version of the integration by parts formula if I understand correctly, and I could prepare a Mathlib version quite quickly if this useful to you.

(I am working on (1) above currently, but this is definitely non-trivial in the proper generality)

[Harald Helfgott]

It's not a matter of being willing - having to work with monotone functions alone is a huge restriction. Usually, that is a stepping stone when building the theory.

Thank you very much for the good work! What is happening with (2)?

[Harald Helfgott]

Aristotle has surprised me again by starting to develop a theory of Riemann-Stieltjes integration from scratch, literally overnight, rather than use Lebesgue-Stieltjes integrals - once again, I'm impressed by its resourcefulness.

[Sébastien Gouëzel]

There is an existing sequence of PRs for (2), but it's far from complete.

[Sébastien Gouëzel]

Note that if you're impatient for your specific needs, you can easily get the bounds for the Fourier coefficients you mention above, by hand, writing your BV function as a difference of monotone functions (we already have that in Mathlib) and working separately with each component. That's not the Mathlib way, because it will just work for real-valued functions and not for functions taking values in a general vector space.

[Harald Helfgott]

Sébastien Gouëzel said:

Note that if you're impatient for your specific needs, you can easily get the bounds for the Fourier coefficients you mention above, by hand, writing your BV function as a difference of monotone functions (we already have that in Mathlib) and working separately with each component. That's not the Mathlib way, because it will just work for real-valued functions and not for functions taking values in a general vector space.

Ah, thanks for confirming - Mathlib does know that every BV function on the reals is the difference of two monotone functions (Jordan decomposition). I was guessing that that must be very new (last two or three months), and so Aristotle wouldn't know that Mathlib knows that. However, ChatGPT (who may or may not be telling the truth) tells me that Mathlib knows that since October 2022, thanks to you. Is this right? Then I'm surprised that Aristotle doesn't know it should use that - I'll try to guide it.

[Ruben Van de Velde]

What's the name of the theorem you found?

[Sébastien Gouëzel]

Indeed, we have docs#LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn and it's been there for quite some time.

[Ruben Van de Velde]

Blame says it was moved to a new file in #19784 but was around in the port from lean 3 at #4824

[Ruben Van de Velde]

And mathlib3 blame points at !3#16683 from October 2022 indeed

[Harald Helfgott]

Well, we clearly need not just $f = f^+-f_-$ with $f^+$, $f^-$ monotone, but also that $Var(f) = Var(f^+)+Var(f^-)$. Do we have that in Mathlib?

[Sébastien Gouëzel]

The version we have is weaker: it takes $f^+$ to be the variation of $f$. So you have $Var(f^+) + Var(f^-) \le 2 Var(f)$.

[Harald Helfgott]

Hm, that's not fantastic, but it's already something. I'm not seeing it in the Mathlib result you referenced - where is it?

[Sébastien Gouëzel]

It's not there, but it follows from the proof of the decomposition: the function $f^+$ is exactly the variation, as you can see from the proof. I'm pretty sure that Aristotle could prove the bound for you (maybe with 3 instead of 2 as it's a little bit easier). But I expect Aristotle would also be able to provide you with the decomposition with the tight bound if you sketch the proof, it's not something complicated.

[Harald Helfgott]

Right, I'll try to nudge Aristotle into giving the decomposition with the tight bound.

[Harald Helfgott]

No doubt it and I will grope in the dark at first because we'll be guessing at what is and is not defined.

[(Tom de Groot) Tomodovodoo]

Terence Tao said:

PNT#562 and PNT#563 are currently outstanding to establish the k=1,2 cases of (c) (with the appropriate corrections, namely that the TV norm needs to be applied to the k-1-fold definition of f). These issues have not yet been claimed by anyone.

I am currently working on it, but I have not claimed them yet as I don't have much significant progress at the moment. Will update if I got more :D

[Sébastien Gouëzel]

It should just be enough to copy the definition of the variation, replacing \sum ||f (x_{i+1}) - f (x_i)|| by \sum \max 0 (f(x_{i+1}) - f (x_i).

[Lawrence Wu (llllvvuu)]

Would docs#LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn actually work for g : R -> C? It is only obvious to me for g : R -> R. FWIW the |dg| measure can probably be directly defined without figuring out what dg means for g : R -> C (EDIT: oh I see, that's the docs#MeasureTheory.VectorMeasure thing that had been mentioned before)

[(Tom de Groot) Tomodovodoo]

@Harald Helfgott I've got a working lean v4.24 backport of Wiener.lean, along with the missing mathlib entries that I've defined in a seperate file as a stand in. Currently used it to solve WeakPNT_AP_prelim, I don't see any luck for Aristotle in the remaining 3 defined worries inside Wiener.lean though, due to their complexity.

If you're interested, I can try to port the suggested additional lemmas from mathlib and other projects to v4.24 as an import for Aristotle to use over the coming days, would that be useful?

[(Tom de Groot) Tomodovodoo]

Then for a short time, just for Aristotle basically, I'd be maintaining a lean v4.24 Wiener project to draw upon when you want to use Aristotle

[Harald Helfgott]

I will try formalizing the decomposition with the tight bound using Aristotle, following the (simple, elegant) proof in chapter 2 of Wheeler-Zygmund. However, there seems to be something else that is missing. I asked Aristotle to prove IBP for f absolutely continuous and g a Stieltjes function (in particular, g monotone), without sketching a proof (deliberately), and Aristotle didn't get very far; see attached files.

I've just resubmitted, and I'll also look into sketching a proof, but the point is that IBP for f AC and g Stieltjes does not seem to be in the library. Or is it?
IBPStmono.lean
IBPStmono.txt

[Sébastien Gouëzel]

We don't really have absolutely continuous functions yet, in the sense that the definition is there but the fundamental theorem of calculus is not. It should land in pretty soon, though, see #29508.

[Lawrence Wu (llllvvuu)]

FWIW here is an Aristotle proof formalization of
$\int_a^b |dg(x)| = TV(g),$:

https://gist.github.com/llllvvuu/37a32add9485ec315ab39a0c822288d9

Of course, the fact that it took the shortcut of not actually going through vector measure makes it not very useful. Let's see if it can go through vector measure...

[Harald Helfgott]

Some good news - Aristotle formalized the following without ears:

\begin{lemma}
Let $f,g:[a,b]\to \mathbb{R}$ be such that $f$ is bounded and $g$ is a Stieltjes function. Then
$$\left|\int_a^b f(x) dg(x)\right|\leq |f|_\infty TV(g),$$
where $TV(g)$ denotes the total variation of $g$ on $[a,b]$.
\end{lemma}
\begin{proof}
Let us see whether you can do this on your own using Mathlib. Use
Lebesgue-Stieltjes, not Riemann-Stieltjes.
\end{proof}

I'm attaching the formalization.
BVmonobound.lean

[Harald Helfgott]

Actually, Wheeler-Zygmund seems to have also the Fourier-analysis fact we needed (as Theorem (12.50a), Dirichlet-Jordan) - maybe it will be profitable for our Mathlib comrades to take a look? It could prove a good resource for statements that can and should be formalized now, and haven't yet.