Open Research Index

Spherical maximal functions: theorems of Stein and Bourgain

Joris Roos

Palomar Registrypalomar/PALOMAR-2026-09-06-000003Sep 6, 2026math.CAscore 0

This is a Lean 4 formalization of Stein's spherical maximal theorem and Bourgain's circular maximal theorem. The result concerns the sharp range of Lp boundedness of spherical maximal functions in Euclidean space and was first proved by Stein in dimensions three and greater. The much more subtle two-dimensional theorem was first proved by Bourgain. The proof of Bourgain's theorem in this formalization is via Mockenhaupt-Seeger-Sogge's classical argument via a local smoothing estimate for the wave equation. This required first formalizing various underlying standard results from harmonic…

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-06-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-06-000003/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-06-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'