{"id":"palomar/PALOMAR-2026-10-20-000016","url":"https://github.com/roos-j/lean-spherical/tree/800b71afca91e42809c21e6e2fd9ae4f82467082","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000016-v1.json","repo":"https://github.com/roos-j/lean-spherical","tags":["math.CA","msc:42B25","msc:28A80","harmonic-analysis","spherical-maximal-functions","weighted-inequalities","lean-formalization"],"score":0,"title":"Endpoint power weight inequalities for spherical maximal functions in Lean","trust":"high","domain":"math.CA","source":"palomar","authors":["Marco Fraccaroli","Juyoung Lee","Nikou Lei","Joris Roos","Andreas Seeger"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of Theorems 1.1-1.4 from the paper \"Endpoint power weight inequalities for spherical maximal functions\" by M. Fraccaroli, J. Lee, N. Lei, J. Roos and A. Seeger. The theorem statements were human-written, while the proof was automatically generated directly from the paper using coding agents.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Endpoint power weight inequalities for spherical maximal functions","identifier":"arXiv:2610.18316v1 (2026), https://arxiv.org/abs/2610.18316v1","relationship":"formalizes"}]}