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. (Lean)

Manuscript

An Endpoint Gradient Bound for the Centered Disk Maximal Operator

September 26, 2026 · source · Lean formalization available · cite as \cite{OAI:An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026}

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.

Result 085 · Real and complex analysis. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.