Endpoint Sobolev regularity of centered disk averages

Taking the best disk average at each point never multiplies a surface's total slope by more than a fixed factor.

1 paper September 26, 2026 Explained by AI

Take a surface over the plane, and at each point record the highest average height over disks centered there. This new surface, the maximal function, spreads out and can have infinite volume. This paper proves its total slope is at most a fixed multiple of the original total slope (Lean proof listed). It answers, for disks in the plane, a question Piotr Hajłasz and Jani Onninen asked in 2004.

First step

2004

Piotr Hajłasz and Jani Onninen, who asked the question

Significance

Major

It settles the planar centered-disk case of a question open since 2004, after only special cases were known.

Trust

Formal proof listed

Field

Real and complex analysis

1 paper

The explanation

Picture a small pile of sand on a flat floor, shaped like a cone. Its peak is 1 unit high, and its base is a disk of radius 1. Its sides fall with slope exactly 1. So its total slope, added over the whole base, equals the base area: π, about 3.14. Its volume is π/3, about 1.05.

Now stand at any point and ask one question. Among all disks centered where you stand, which has the highest average height? That best average is the maximal function at your point. At the peak, tiny disks win, and the answer is 1. Ten units away, the floor around you is empty. But a disk of radius 11 swallows the whole pile. Its average height is π/3 divided by 121π, which is 1/363, about 0.0028.

So the maximal function smears the pile across the whole plane. Its height fades only like one over the squared distance. Add up the volume under it ring by ring, and the total never settles. Once R is 100 or more, each ring from distance R to 2R adds at least 1.4. The heights blow up in total. The open question was about slopes. Does the smeared surface still have a finite total slope?

Mathematicians measure slopes in several ways, labeled by a power p. Juha Kinnunen proved in 1997 that the maximal function keeps slopes under control for every p above 1. His argument bounds the slope at each point by the maximal function of the slope. Then it uses a fact about maximal functions that holds only for p above 1. At p equal to 1 that step fails, and the cone shows why. Its slope equals 1 across the unit disk. The maximal function of that slope fades just like the pile, so its total is infinite too. In 2004, Piotr Hajłasz and Jani Onninen asked whether the slope bound survives at p equal to 1 anyway.

On a line, earlier work said yes. Hitoshi Tanaka proved it in 2002 for the uncentered version, where intervals need only contain the point. Ondřej Kurka proved it for centered intervals in 2015. In higher dimensions, results needed special inputs or shapes. Hannes Luiro handled radially symmetric inputs with uncentered balls in 2018. Julian Weigt handled uncentered cubes in 2025. A total-variation bound measures total slope but also counts sharp creases. In 2025, Panu Lahti and Weigt showed such a bound would upgrade to genuine slopes. That bound was missing for centered disksSource 1.

The main obstacle is geometry. On a line, intervals can be lined up in order, and those proofs lean on that order. Disks centered at different points overlap in tangled ways, with no such orderSource 2. There is a second trap. A total-slope bound can still allow creases, where slope piles up on a set of zero areaSource 3.

This paper proves that the answer is yes for disks in the planeSource 4. Take any real function on the plane whose values and slopes have finite totals. Its centered disk maximal function then has a weak gradient (a slope function defined by averaging, which tolerates corners). The total of that slope is at most C times the input's total slopeSource 5. C is one fixed number for every input. The paper first bounds a simpler version that uses only a fixed range of radii. That version keeps the sign of the input, which lets it subtract a local averageSource 6 Source 7. Its bound does not grow as the range widensSource 8. Then the paper widens the range and shows that no slope hides in creasesSource 9.

Back to the pile. Its smeared shadow has infinite volume, yet its total slope is at most C times π. The paper does not compute C, so the factor stays unknownSource 10. The result covers disks in the plane only, not balls in space or other shapesSource 11.

How sure is this? A computer proof checker called Lean has a formal proof of the main theorem. It covers every real input whose values and slopes have finite totals. Lean also checks the simpler fixed-range estimate. An extension to functions of bounded variation, which may jump, is outside these statements. No specialist review of the paper has been published.

What it doesn't show. This does not find the best fixed factor, and it does not cover higher dimensions or other shapes.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major within the study of maximal functions, if the proof holds. Lean has a formal proof of the main statement. Specialists have not published a review, and the constant is unknown. It settles one case: centered disks in the plane.

Words used

Maximal function: At each point, the highest average of a function's size over all disks centered at that point.
Uncentered maximal function: A variant that averages over all disks or intervals containing the point, not only those centered there.
Weak gradient: A slope function defined through averaging, so it exists even for surfaces with corners.
Sobolev space W^{1,1}: The functions whose values and slopes both have finite totals over the whole plane.
Total variation: A measure of total slope that also counts sharp creases and jumps, not only smooth slope.
Absolute constant: One fixed number that works for every input, here written C.

The original paper

An Endpoint Gradient Bound for the Centered Disk Maximal Operator (PDF, opens in a new tab)
September 26, 2026 Formal proof listed

Lean notes

All quoted lines (11)

It assumes the requisite variation bound. We prove that bound and then remove the singular part directly using the signed localization above.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
The ordering of intervals used in these arguments does not directly organize a family of centered disks.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
Moreover, a variation estimate controls a derivative measure, which may still have a singular part.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
We give a positive resolution of the planar centered-disk case of their endpoint question.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
There is an absolute constant $C<\infty$ such that, for every real-valued $f\in W^{1,1}(\R^2)$ , the function $Mf$ is locally integrable, belongs to $W^{1,1}_{\mathrm{loc}}(\R^2)$ , and satisfies $\int_{\R^2}|\nabla Mf|\,\dd x \le C\int_{\R^2}|\nabla f|\,\dd x.$
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
The intermediate estimate retains the sign of the input.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
Signed averages also occur in Weigt's dyadic and uncentered cube estimates; their role here is to permit this local subtraction.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
The constant is independent of $a$ , $b$ , and the number of dyadic radius scales between them.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
To prove that this measure has no singular part, fix a compact null set and a positive radius threshold.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
The constant in (…) is finite and absolute; its optimal value is not determined.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text
The argument below concerns disks in the plane.
An Endpoint Gradient Bound for the Centered Disk Maximal Operator Back to text