Floris van Doorn: Towards a formalized proof of Carleson's theorem

A fundamental question in Fourier analysis is when the Fourier series converges to the original function. This is true for continuously differentiable functions, but not always true for continuous functions. In 1966 Lennart Carleson proved that it is true for functions on the real line for almost all points. This follows from the boundedness of the Carleson operator. Carleson's proof is famously hard to read, and there are no known easy proofs of this theorem. Furthermore, generalizations of the theorem to higher dimensions are subtle. Christoph Thiele et al. proved in 2024 a generalized version of the boundedness of the Carleson's operator in doubling metric measure spaces, and I will lead a project to formalize this theorem in Lean. Thiele and his collaborators wrote a detailed blueprint that we will use as the basis for the formalization.