{"id":"palomar/PALOMAR-2026-08-31-000015","url":"https://github.com/roos-j/lean-superorthogonality/tree/d6cebb0d1ec7cf96f7485b839f895f205c3857df","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000015-v1.json","repo":"https://github.com/roos-j/lean-superorthogonality","tags":["math.CA","msc:42B25","harmonic-analysis","square-functions","lean-formalization"],"score":0,"title":"roos-j/lean-superorthogonality","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"A Lean formalization of the main result (Theorem 1) of the paper \"A new type of superorthogonality\" by P. T. Gressman, L. B. Pierce, J. Roos, and P.-L. Yung; arXiv:2212.08956, Proc. Amer. Math. Soc. 152, 665-675, 2024. The theorem provides a simple criterion on a family of functions that implies a square function estimate on Lp for every even integer p ≥ 2. This defines a new type of superorthogonality that is verified by checking a less restrictive criterion than any other type of superorthogonality previously known.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"A new type of superorthogonality","identifier":"https://doi.org/10.1090/proc/16631","relationship":"formalizes"}]}