# Formalization of a generalized Carleson’s theorem

A (WIP) formalized proof of a generalized Carleson’s theorem in Lean.

- Zulip channel for coordination
- Blueprint
- Blueprint as pdf
- Dependency graph
- Doc pages for this repository

## Carleson’s theorem

The classical statement of Carleson’s theorem is easy. One phrasing is that if you have a continuous periodic function `f : ℝ → ℝ`

then the Fourier series of `f`

converges pointwise to `f`

almost everywhere. However, the proof is very hard! In this project we will prove this theorem, from a much more general theorem, which was recently proved by Christoph Thiele and his group (it has not been published yet at the moment). This generalization proves the boundedness of a generalized Carleson operator on doubling metric measure spaces.

## Contribute

To get the repository, make sure you have installed Lean. Then get the repository using `git clone https://github.com/fpvandoorn/carleson.git`

and run `lake exe cache get!`

inside the repository. Run `lake build`

to build all files in this repository. See the README of my course repository for more detailed instructions.

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.