A blueprint for the formalization of Carleson's theorem on convergence of Fourier series

Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +14

This paper is the blueprint underlying the Lean formalization of the proof of Carleson's classical result asserting almost everywhere convergence of Fourier series of continuous fu…