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

TL;DR

This paper provides a detailed blueprint for formalizing Carleson's theorem on the almost everywhere convergence of Fourier series using Lean, breaking down the proof into two main steps and guiding the formalization process.

Contribution

It introduces a structured blueprint for the Lean formalization of Carleson's theorem, facilitating rigorous proof development in a proof assistant.

Findings

Blueprint successfully guided Lean formalization

Breakdown of proof into reduction and main theorem

Collaborative refinement improved the formalization process

Abstract

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 functions. We break up the proof into two steps, a reduction of the classical result to a new theorem that appears in a sibling communication and a proof of this new theorem, which is also detailed as blueprint in this paper. An early version of this blueprint was used to initiate the Lean formalization. During the formalization, many contributors elaborated the blueprint with minor corrections, modifications and extensions. The final version is presented here as a guide through the accompanying Lean code.