Formalization of a generalized Carleson's theorem

A formalized proof of a generalized Carleson's theorem in the Lean interactive theorem prover.

Links

• Zulip channel for coordination
• Webpage
• Blueprint
• Blueprint as pdf
• Dependency graph
• Documentation pages for this repository

What is Carleson's theorem?

Carleson's theorem is a statement about Fourier analysis: given a continuous periodic function $f\colon ℝ\to ℝ$, its Fourier converges to $f$ point-wise at almost every point. More precisely, let $f\colon\mathbb{R}\to \mathbb{C}$ be a $2\pi$-periodic bounded Borel measurable function. For each integer $n\in\mathbb{Z}$, define the $n$-th Fourier coefficient as

$$\widehat{f}_n := \frac{1}{2\pi} \int_0^{2\pi} f(x) e^{- i nx} dx.$$

For $N\geq 0$, define the partial Fourier sum as

$$s_Nf(x):=\sum_{n=-N}^N \widehat{f}_n e^{i nx}.$$

Then Carleson's theorem states $\lim_{N\to\infty} s_N f(x) = f(x)$ for almost all $x\in\mathbb{R}$.

Despite being simple to state, its proof is very hard. (It is also quite subtle: for instance, asking for point-wise convergence everywhere makes this false.) The detailed statement can be found here, the corresponding Lean statement is here. TODO: link to it after re-organising the main files!

How do we prove it?

In this project, we deduce this statement from the boundedness of a certain linear operator, the so-called Carleson operator. This boundedness holds in much greater generality: we formalise a new generalisation (due to the harmonic analysis group in Bonn) to doubling metric measure spaces. The precise technical result we prove is the metric spaces Carleson theorem (precise statement, Lean statement).

We also prove a linearised metric space Carleson theorem (precise statement, Lean statement), which allows proving a generalisation of Carleson's theorem to Walsh functions.

Verifying the formalisation

This proof has been formalised in the Lean theorem prover. To confirm the correctness and completeness yourself, follow these steps.

1. Make sure you have installed Lean.
2. Download the repository using git clone https://github.com/fpvandoorn/carleson.git.
3. Open the directory where you downloaded the repository (but not any further sub-directory). Open a terminal in this directory and run lake exe cache get! to download built dependencies.
4. Determine which Lean statement you want to verify: the Lean statements of the main theorems above are classical_carleson, metric_carleson and linearized_metric_carleson, respectively. Open the file Carleson.lean in a text editor of your choice. Add the end of the file, add a line #print axioms linearized_metric_carleson (or similar). This will tell Lean to verify that the proof of this result was completed correctly.
5. In the terminal from step 3, run lake build to build all files in this repository. This will likely take 5-30 minutes. When the process is complete, at the very end of the output, you will see a line 'linearized_metric_carleson' depends on axioms: [propext, Classical.choice, Quot.sound] (followed by Build completed successfully). This shows the proof is complete and correct. Had the build failed or the output included sorryAx, this would have indicated an error resp. an incomplete proof. (For the experts: this shows which axioms Lean used in the course of the proof. propext and Quot.sound are built into Lean's type theory, Classical.choice tells you that Lean's version of the axiom of choice was used.)

Contribute

Locally

1. Make sure you have installed Lean.
2. Download the repository using git clone https://github.com/fpvandoorn/carleson.git.
3. Run lake exe cache get! to download built dependencies (this speeds up the build process).
4. Run lake build to build all files in this repository.

See the README of Floris van Doorn's course repository for more detailed instructions.

In github codespaces

If you prefer, you can use online development environment:

To make changes to this repository, please make a pull request. There are more tips in the file Contributing.md. To push your changes, the easiest method is to use the Source Control panel in VSCode. Feel free to make pull requests with code that is work in progress, but make sure that the file(s) you've worked have no errors (having sorry's is fine of course).

Build the blueprint

To test the Blueprint locally, you can compile print.tex using XeLaTeX (i.e. xelatex print.tex in the folder blueprint/src). If you have the Python package invoke you can also run inv bp which puts the output in blueprint/print/print.pdf. If you want to build the web version of the blueprint locally, you need to install some packages by following the instructions here. But if the pdf builds locally, you can also just make a pull request and use the online blueprint.