fpvandoorncarleson

A formalized proof of Carleson's theorem in Lean

Formalization of a generalized Carleson's theorem

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

What is Carleson's theorem?

Carleson's theorem is a statement about Fourier analysis: given a continuous periodic function , its Fourier converges to point-wise at almost every point. More precisely, let be a -periodic bounded Borel measurable function. For each integer , define the -th Fourier coefficient as

For , define the partial Fourier sum as

Then Carleson's theorem states for almost all .

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 precise English statement statement can be found as Theorem 1.0.1, the corresponding Lean statement is here, and the Lean proof here.

Metric space Carleson theorem

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 (Theorem 1.1.1, Lean statement, Lean proof).

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

The new definitions needed to verify the statements of these theorems are in the file Carleson.Defs

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. These three axioms are built into Lean's type theory.)

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.