Open Research Index

Formalization of power weight inequalities for spherical maximal functions

Joris Roos

Palomar Registrypalomar/PALOMAR-2026-09-07-000007Sep 8, 2026math.CAscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-07-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'