Fejér's theorem has just been formalized

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Aristotle and I have just managed to formalize Fejér's theorem. Or, should I say: I just served as an intermediary, choosing a good source (Wheeden-Zygmund), resolving an issue when Aristotle got stuck, and insisting until it got done.

Quick recall - Fejér's theorem: given an integrable, periodic function $f$, the arithmetic means $\sigma_n(f)$ of the partial sums $s_n(f)$ of the Fourier series of $f$ converge to $f$ at every point of continuity -- uniformly on any interval $[a,b]$ on which $f$ is continuous; moreover, if $f$ has a jump discontinuity at $x$, the sequence $\sigma_n(f)$ converges to $(f(x_0^-)+f(x_0^+))/2$.

This is often the first 'modern' or 'hard' theorem taught in a Fourier analysis course; it's at the basis of very many things. My immediate motivation was to use it to formalize a proof of the Dirichlet-Jordan theorem (basically: if $f$ is of bounded variation, then the partial sums $s_n(f)$ themselves tend to $f$ at every point of continuity, etc.), which I need, in turn, to formalize the proof of the Poisson summation formula in its general form, that is, the form that is valid even when $\widehat{f}$ is not in $L^1$; that, in turn, comes up all the time in analytic number theory. That is what is next on the menu.

Another element of the proof of Dirichlet-Jordan theorem is Hardy's Tauberian lemma. Aristotle has also formalized its proof, in one pass, starting from the proof in Wheeden-Zygmund. (Aristotle needed three passes for Fejer's theorem, not counting false starts.) I am attaching the sources (in Markdown) and the Lean files. The Markdown files are essentially verbatim for Wheeden-Zygmund, except for one important clarification that I needed to give to get Aristotle unstuck:

When Wheeden-Zygmund say that a function $f$ is continuous on $I=[a,b]$ (where, as they themselves explain, $b$ may equal $a$), they mean that $f$ is continuous at every point of $I$.

When Mathlib (and a fair number of our contemporaries, I'd say) say that $f$ is continuous on $I$, they mean that the restriction $f|_I$ is continuous as a function on $$I^$; in other words, there continuity conditions at the end of a closed interval $I$ are only one-sided.)

I have little doubt that the Lean code can be slimmed down significantly. Let's discuss when Aristotle was particularly roundabout; in my (scant) experience, that often means that Aristotle stalled due to a gap in our standard libraries, and cleverly found a more complicated argument to prove something whose human-provided proof Aristotle couldn't "understand".

At any rate, enjoy! Comments are very welcome.

Incidentally, the Fejer .lean file also includes Hardy's Tauberian theorem, since we are going to combine the two to prove Dirichlet-Jordan.

Uploading Fejer verbatim building on DJstep1, step 2.lean…
Fejer in Wheeden-Zygmund, nearly verbatim.md
Hardy_Tauberian_theorem.lean
Hardy's Tauberian theorem.md

[Terence Tao]

Would you like to upload it to PNT+ (in a Mathlib subdirectory, perhaps) to help with other number theory formalizations? Or is the plan to send it directly to Mathlib? I guess it would need a lot of golfing first.

[Lawrence Wu (llllvvuu)]

I requested from Aristotle to re-prove a "mathlib generality" version of the above Tauberian theorem. I didn't include the informal text, so the proof strategy may be less efficient this time around. Then, I ran an internal tool to clean up the proof. So now hopefully the distance from mathlib acceptability is reduced, or at least it's a more pleasant starting point for a human golfer.

https://gist.github.com/llllvvuu/671e9c3214adb6583c8672266ef859fa

I would do the same for the Fejer formalization, but it seems like it failed to upload.

[Harald Helfgott]

Terence Tao said:

Would you like to upload it to PNT+ (in a Mathlib subdirectory, perhaps) to help with other number theory formalizations?

With pleasure - newbie question: how and where do I upload?

Or is the plan to send it directly to Mathlib? I guess it would need a lot of golfing first.

Exactly - yes, but not right away; I was hoping we would golf communally - and, as a result, I'd learn to golf (or at least I'd learn more Lean).

It apparently failed to upload last night - here it is.
Fejer verbatim building on DJstep1, step 2.lean

[Harald Helfgott]

We will want to translate all of this so that it is about functions on $\mathbb{R}/\mathbb{Z}$, rather than about functions on $\mathbb{R}$ of period $2\pi$. Of course that's all trivially equivalent, so we can simply deduce the final results in the form we want from the final results in the form we have, but it is arguably more elegant to work with $\mathbb{R}/\mathbb{Z}$ throughout. Is it a good or a bad idea to ask AI to do a first pass in that direction?

PS. Since the fact that Aristotle can translate passages from a textbook essentially verbatim is itself noteworthy, we should probably store these lean files in some permanent place before we start fiddling with them.

[Lawrence Wu (llllvvuu)]

Could use AddCircle T -> E, similar to docs#fourierCoeff