{"id":"palomar/PALOMAR-2026-10-16-000005","url":"https://github.com/roos-j/lean-superorthogonality/tree/97b539920a2e141f1caa6d7be187bd878ff3c89e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000005-v2.json","repo":"https://github.com/roos-j/lean-superorthogonality","tags":["math.CA","msc:42B10","msc:42B25","harmonic-analysis","square-function","formal-verification","lean"],"score":0,"title":"Formalization of a sharp cone square-function estimate via superorthogonality","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of Theorems 1.1 and 1.4 from the paper \"Diameter-free reverse inequalities and superorthogonality\" by A. Cushman, C. Demeter and S. Wu. Theorem 1.1 is a reverse square-function estimate in L^4 under a superorthogonality hypothesis that is weaker than the Type IV superorthogonality of Gressman-Pierce-Roos-Yung. Theorem 1.4 applies a similar estimate to the three-dimensional light cone, yielding a refinement of the reverse cone square-function estimate of Guth-Wang-Zhang.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"Diameter-free reverse inequalities and superorthogonality","identifier":"arXiv:2609.13105v1 (2026), https://arxiv.org/abs/2609.13105v1","relationship":"formalizes"}]}