Skip to the content.

Carleson’s theorem

WIP formalization of a generalized Carleson’s theorem

Build the Lean files

To build the Lean files of this project, you need to have a working version of Lean. See the installation instructions (under Regular install).

To build the project, run lake exe cache get and then lake build.

Build the blueprint

The blueprint is automatically built on each push to the project. You can test whether the build is working by building the pdf locally: xelatex blueprint/src/print.tex.