The Carleson project: a collaborative formalization

A well-known result in Fourier analysis establishes that the partial Fourier sums of a smooth periodic function $f$ converge uniformly to $f$, but the situation is a lot more subtle for e.g. continuous functions. However, in 1966 Carleson proved that they do converge at almost all points for $L^2$ periodic functions on the real line. Carleson’s proof is famously hard to read, and there are no known easy proofs of this theorem.

As a large collaborative project, we have formalized in Lean a generalization of Carleson’s theorem in the setting of doubling metric measure spaces (proven in 2023), and Carleson’s original result as a corollary. In this talk I will give an overview of the project, with a focus on how the collaboration was organized.

Zoom Link: https://harvard.zoom.us/j/96815917772?pwd=p8G9kqh0QfW3VoPh5399Ur2wnzNyLV.1