we-solve (beta)

Math-2942 · mathematics · Analysis

Endpoint gradient regularity of the planar disk maximal operator

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For the centered Hardy-Littlewood maximal operator M over Euclidean disks in $R^2$, does every real f in $W^{1,1}(R^2)$ have M f in $W_loc^{1,1}(R^2)$ and ||gradient M $f||_L1$ $<=$ C||gradient $f||_L1$ for one absolute C?

Short English statement

For the centered Hardy-Littlewood maximal operator M over Euclidean disks in $R^2$, does every real f in $W^{1,1}(R^2)$ have M f in $W_loc^{1,1}(R^2)$ and ||gradient M $f||_L1$ $<=$ C||gradient $f||_L1$ for one absolute C?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2942-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2942

Endpoint gradient of disk maxima: The primary statement says: For every real f in W11(R2), the centered disk maximal function belongs to Wloc11 and has L1 gradient at most an absolute constant times that of f. The target retains these quantified objects and hypotheses, so its positive assertion is covered.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Endpoint gradient regularity of the planar disk maximal operator

OpenAI's claim

Endpoint gradient of disk maxima: The paper claims that the centered disk maximal function of a real $W^{1,1}(\mathbb R^2)$ function has an integrable weak gradient controlled by the original gradient. Local Sobolev membership of the maximal output is also included.

Mathematical statement of the claimed result

Mathematical claim 1.
For the centered disk maximal operator $Mf(x)=\sup_{r>0}(\pi r^2)^{-1}\int_{B(x,r)}|f(y)|\,dy$, every real $f\in W^{1,1}(\mathbb R^2)$ is claimed to satisfy $Mf\in W^{1,1}_{\mathrm{loc}}(\mathbb R^2)$ and \[\int_{\mathbb R^2}|\nabla Mf|\le C\int_{\mathbb R^2}|\nabla f|\] with an absolute constant. The distributional gradient is globally integrable; global $L^1$ integrability of $Mf$ is not claimed.

Outline of the argument

Endpoint gradient of disk maxima: Scalar cancellation is arranged across dyadic cells using common nonnegative prices with a total variation budget. A different path measure represents vector gradient masses and charges changes of direction in both space and scale. Averaging over direction histories assembles the radius bands while canceling the differentiated weight terms.

Formal verification

Family 085 describes Lean coverage for the centered-disk Sobolev gradient estimate, together with the earlier finite-band statement.

Endpoint gradient of disk maxima: The manuscript links DiskMaximal.lean, SignedFiniteBand.lean (declaration OAI.SignedDisk.CenteredDiskEndpoint.main_signed_finite_band).

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →