{"id":"palomar/PALOMAR-2026-09-06-000003","url":"https://github.com/roos-j/lean-stein-bourgain-palomar/tree/3c29098b6660e97ca52fdf71856be8eecb32e122","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-06-000003-v1.json","repo":"https://github.com/roos-j/lean-stein-bourgain-palomar","tags":["math.CA","msc:42B25","harmonic-analysis","maximal-functions","lean-formalization"],"score":0,"title":"Spherical maximal functions: theorems of Stein and Bourgain","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-06","reactions":{},"formalized":true,"formalizes":[{"title":"Maximal functions: spherical means","identifier":"https://doi.org/10.1073/pnas.73.7.2174","relationship":"formalizes"},{"title":"Averages in the plane over convex curves and maximal operators","identifier":"https://doi.org/10.1007/BF02792533","relationship":"formalizes"},{"title":"Wave front sets, local smoothing and Bourgain's circular maximal theorem","identifier":"https://doi.org/10.2307/2946549","relationship":"adapts"}]}