Browse › Real and complex analysis › 085 Endpoint Sobolev regularity of centered disk averages
An Endpoint Gradient Bound for the Centered Disk Maximal Operator
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove the endpoint gradient bound $\|\nabla Mf\|_1\le C\|\nabla f\|_1$ for every real-valued $f\in W^{1,1}(\mathbb R^2)$, where $Mf(x)$ is the supremum of the averages of $|f|$ over disks centered at x, and C is an absolute constant. The maximal function belongs to $W^{1,1}_{\mathrm{loc}}(\mathbb R^2)$ and has a globally integrable weak gradient. This gives a positive resolution of the planar centered-disk case of the endpoint question of Hajłasz and Onninen.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Kenta Kitamura, centered-ball-maximal-endpoint (GitHub repository, October 2026). Proposes a Lean 4 proof of the centered Euclidean-ball endpoint gradient bound in every dimension, citing this paper as "a research starting point"; the repository says independent mathematical review is still pending. [AI-generated per source]
Formalization
- OpenAI math release, Lean scope notes for 085 (Endpoint Sobolev regularity of centered disk averages) (release Lean docs, 2026-10-06). Describes the formalizations of the signed finite-band estimate and the full planar Sobolev-input endpoint gradient bound, with links to their comparator statements; a BV-input extension is explicitly outside its scope. [family-level]
- OpenAI math release, DiskMaximal.lean comparator statement (openai/math, commit adc7f12). The Lean statement
OAI.CenteredDiskEndpoint.main_endpointgives the endpoint bound for integrable planar f with integrable weak gradient. - Kenta Kitamura, Add a conjecture: endpoint gradient bound for the centered ball maximal operator in every dimension (google-deepmind/formal-conjectures issue #6938, 2026-10-08). Proposes adding the d ≥ 2 centered-ball version of Hajłasz–Onninen Question 1 to formal-conjectures; the issue itself does not mention this paper. [AI-generated per source]
- Kenta Kitamura, Formalize the centered ball maximal endpoint and mark it as solved (google-deepmind/formal-conjectures PR #7129, opened 2026-10-11, open at time of collection). Formalizes Hajłasz–Onninen Question 1 for centered balls and links external Lean proofs, which a reviewer reports rebuilding with Lean 4.33.1 and passing the Comparator checks. [AI-generated per source]
Related prior literature mentioned by others
- Piotr Hajłasz and Jani Onninen, On boundedness of maximal functions in Sobolev spaces (Ann. Acad. Sci. Fenn. Math. 29 (2004)). The source of Question 1, which the follow-up repository, the formal-conjectures issue and the PR all take as their target statement; it is also in the paper's bibliography.
- Panu Lahti and Julian Weigt, The centered maximal operator removes the non-concave Cantor part from the gradient (arXiv:2510.01936v1, 2025-10-02). The AI Proved What? exposition highlights this work's conditional upgrade from BV to Sobolev regularity in connection with the manuscript's separate variation-bound and singular-part-removal steps.
Possibly relevant literature (found by the agent, not checked)
- Emanuel Carneiro, Regularity of maximal operators: recent progress and some open problems (arXiv:1912.04625, 2019). A survey with fifteen open problems in this area; relevant to the paper's account of the status of the Hajłasz–Onninen endpoint question and earlier endpoint results.
- Emanuel Carneiro and Cristian González-Riquelme, Gradient bounds for radial maximal functions (arXiv:1906.01487; Ann. Fenn. Math. 46 (2021)). Proves W^{1,1} gradient bounds for centered heat-flow and Poisson maximal operators on radial data in ℝ^d, a higher-dimensional centered endpoint result not listed in the paper's "Earlier endpoint results" subsection.
- Panu Lahti, On the regularity of the maximal function of a BV function (arXiv:2007.05752, 2020). Shows that if the non-centered maximal function of an SBV function is BV, then it is Sobolev, which bears on the paper's final step removing the singular part of the derivative measure of Mf.
- Emanuel Carneiro and Julian Weigt, On the variation and asymptotics of maximal functions (arXiv:2610.18544, 2026-10-13). A later paper on the variation of centered convolution-type maximal operators in higher dimensions; its introduction calls the Hajłasz–Onninen question generally open in higher dimensions and does not mention this paper.
Digests and expositions
- Latent Seminar, Endpoint gradients of the centered disk maximal function (2026-10-06). A graduate-level exposition outlining the signed finite-band estimate, disk-moment cancellation, multiscale accounting and removal of singular derivatives; it disclaims independent proof verification or a Lean audit. [family-level]
- AI Proved What?, How much steeper? The centered disk maximal function at p = 1 (Episode 085, October 2026). An animated exposition and transcript illustrating the endpoint claim with cone-function computations and outlining the proof strategy; it states that the project has not run the Lean check. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 085
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026,
author = {{OpenAI}},
title = {{An Endpoint Gradient Bound for the Centered Disk Maximal Operator}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026/article.pdf}{OAI:An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/085.md. The Lean statements have not been checked by people against the paper's claims.
Family 085: Endpoint Sobolev regularity of centered disk averages
Resolves the planar centered-disk case of the Hajłasz–Onninen maximal-function regularity problem. For every real $f\in W^{1,1}(\mathbb R^2)$, the centered disk maximal function satisfies $\|\nabla Mf\|_1\le C\|\nabla f\|_1$ with an absolute constant. It belongs locally to $W^{1,1}$ and has a globally integrable weak gradient.
This is the only paper in this family.