A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
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.
Lars Becker、María Inés de Frutos-Fernández、Leo Diedering、Floris van Doorn、Sébastien Gouëzel、Asgar Jamneshan、Evgenia Karunus、Edward van de Meent、Pietro Monticone、Jasper Mulder-Sohn、Jim Portegies、Joris Roos、Michael Rothgang、Rajula Srivastava、James Sundstrom、Jeremy Tan、Christoph Thiele
数学
Lars Becker,María Inés de Frutos-Fernández,Leo Diedering,Floris van Doorn,Sébastien Gouëzel,Asgar Jamneshan,Evgenia Karunus,Edward van de Meent,Pietro Monticone,Jasper Mulder-Sohn,Jim Portegies,Joris Roos,Michael Rothgang,Rajula Srivastava,James Sundstrom,Jeremy Tan,Christoph Thiele.A blueprint for the formalization of Carleson's theorem on convergence of Fourier series[EB/OL].(2025-08-06)[2025-08-17].https://arxiv.org/abs/2405.06423.点此复制
评论