{"id":"palomar/PALOMAR-2026-09-07-000007","url":"https://github.com/roos-j/lean-spherical/tree/ddd4afde232f264dfe650aaebcab17ea562e39b5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000007-v3.json","repo":"https://github.com/roos-j/lean-spherical","tags":["math.CA","msc:42B25","msc:28A80","harmonic-analysis","maximal-functions","lean-formalization"],"score":0,"title":"Formalization of power weight inequalities for spherical maximal functions","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 \"Power weight inequalities for spherical maximal functions\" by Marco Fraccaroli, Joris Roos, and Andreas Seeger, arXiv:2602.17613. The formalized result concerns boundedness of spherical maximal functions with arbitrary sets of dilations and radial power weights. The allowable exponent and weight ranges are characterized, apart from endpoint boundedness, by the Legendre-Assouad function of the dilation set. This resolved an open problem of Duoandikoetxea and Seijo up to endpoints. The main theorem statement in Lean was…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-08","reactions":{},"formalized":true,"formalizes":[{"title":"Power weight inequalities for spherical maximal functions","identifier":"Mathematische Zeitschrift 314, article 4 (2026). https://doi.org/10.1007/s00209-026-04106-4. arXiv:2602.17613v2, https://arxiv.org/abs/2602.17613v2.","relationship":"formalizes"}]}