A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916883520815104 |
|---|---|
| author | Becker, Lars de Frutos-Fernández, María Inés Diedering, Leo van Doorn, Floris Gouëzel, Sébastien Jamneshan, Asgar Karunus, Evgenia van de Meent, Edward Monticone, Pietro Mulder-Sohn, Jasper Portegies, Jim Roos, Joris Rothgang, Michael Srivastava, Rajula Sundstrom, James Tan, Jeremy Thiele, Christoph |
| author_facet | Becker, Lars de Frutos-Fernández, María Inés Diedering, Leo van Doorn, Floris Gouëzel, Sébastien Jamneshan, Asgar Karunus, Evgenia van de Meent, Edward Monticone, Pietro Mulder-Sohn, Jasper Portegies, Jim Roos, Joris Rothgang, Michael Srivastava, Rajula Sundstrom, James Tan, Jeremy Thiele, Christoph |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_06423 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A blueprint for the formalization of Carleson's theorem on convergence of Fourier series Becker, Lars de Frutos-Fernández, María Inés Diedering, Leo van Doorn, Floris Gouëzel, Sébastien Jamneshan, Asgar Karunus, Evgenia van de Meent, Edward Monticone, Pietro Mulder-Sohn, Jasper Portegies, Jim Roos, Joris Rothgang, Michael Srivastava, Rajula Sundstrom, James Tan, Jeremy Thiele, Christoph Classical Analysis and ODEs 42B20 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. |
| title | A blueprint for the formalization of Carleson's theorem on convergence of Fourier series |
| topic | Classical Analysis and ODEs 42B20 |
| url | https://arxiv.org/abs/2405.06423 |