2 papers
math.CA2026
Formalizing Carleson's Theorem in Lean
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +11
We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the m…
math.CA2024
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…