{"id":"palomar/PALOMAR-2026-10-12-000008","url":"https://github.com/roos-j/lean-lt-carleson/tree/1fde1f341dfdde6e69500bfe909ea1f77159d163","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-12-000008-v2.json","repo":"https://github.com/roos-j/lean-lt-carleson","tags":["math.CA","msc:42B20","msc:42B25","msc:42A20","harmonic-analysis","carleson-theorem","lean-formalization"],"score":0,"title":"Formalization of Carleson's theorem via the Lacey-Thiele approach","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of Theorem 1.1 from the paper \"Bounds for anisotropic Carleson operators\" by J. Roos, which generalizes the Lacey-Thiele proof for Carleson's theorem. The classical Carleson theorem on pointwise almost everywhere convergence of Fourier series is derived as a special case.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"Bounds for anisotropic Carleson operators","identifier":"J. Fourier Anal. Appl. 25 (2019), no. 5, 2324-2355, doi:10.1007/s00041-018-09657-7; arXiv:1710.10962v1","relationship":"formalizes"}]}