{"id":"palomar/PALOMAR-2026-09-30-000034","url":"https://github.com/roos-j/lean-discretesw/tree/b2c652acaf76541089e1b09079e5c0b3c86b98a8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000034-v2.json","repo":"https://github.com/roos-j/lean-discretesw","tags":["math.CA","msc:42B20","msc:42B25","msc:42B15","harmonic-analysis","discrete-carleson","lean-formalization"],"score":0,"title":"Formalization of a discrete Carleson theorem of Stein-Wainger type","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of the main theorem of the papers arXiv:1907.00405 and arXiv:2107.14616 by Ben Krause and Joris Roos. The result concerns l^p boundedness for a discrete maximal singular oscillatory operator of Stein-Wainger type, also called a discrete Carleson operator.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"Discrete analogues of maximally modulated singular integrals of Stein-Wainger type: l^p bounds for p > 1","identifier":"J. Funct. Anal. 285 (2023), no. 10, Paper No. 110123, doi:10.1016/j.jfa.2023.110123; arXiv:2107.14616v2","relationship":"formalizes"},{"title":"Discrete analogues of maximally modulated singular integrals of Stein-Wainger type","identifier":"J. Eur. Math. Soc. (JEMS) 24 (2022), no. 9, 3183-3213, doi:10.4171/JEMS/1160; arXiv:1907.00405v3","relationship":"formalizes"}]}