Jump to content

Endpoint Sobolev regularity of the centered maximal function

From OpenAI Aftermath

The endpoint Sobolev regularity question for the centered maximal function, asked by Hajłasz and Onninen in 2004, is whether the gradient of the centered Hardy–Littlewood maximal function is controlled in L1 by the gradient of the input: is u ↦ |∇Mu| bounded from W1,1(Rn) to L1(Rn)? A manuscript dated 26 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the planar case for the centered disk maximal operator. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

  • As recounted in the introduction of the manuscript:
    • Kinnunen proved that the maximal operator is bounded on W1,p for 1 < p < ∞, using the pointwise control of the gradient of Mf by the maximal function of |∇f|. At p = 1 that argument fails, and Hajłasz and Onninen asked whether the gradient estimate nevertheless survives (their Question 1).
    • In one dimension, Tanaka proved an L1 derivative bound for the uncentered maximal operator, Aldaz and Pérez Lázaro extended it to functions of bounded variation with the sharp constant, and Kurka proved a variation bound for the centered operator together with local Sobolev regularity.
    • In higher dimensions, earlier results cover special inputs or other operators: block-decreasing inputs (Aldaz and Pérez Lázaro), radial inputs for the uncentered ball operator (Luiro), the dyadic and the uncentered cube maximal operators (Weigt), and fractional maximal operators (Beltran and Madrid; Weigt). Lahti and Weigt proved that local bounded variation of the centered maximal function upgrades to local Sobolev regularity for Sobolev inputs.

The original result

  • An endpoint gradient bound for the centered disk maximal operator (26 September 2026). Theorem 1.1 of the manuscript states that there is an absolute constant C such that, for every real-valued f in W1,1(R2), the centered disk maximal function Mf is locally integrable, belongs to W1,1loc and satisfies ‖∇Mf‖1 ≤ C‖∇f‖1. The manuscript describes this as a positive resolution of the planar centered-disk case of the Hajłasz–Onninen question. It states that the argument concerns disks in the plane and that the optimal constant is not determined.
    • Method, as described: the proof first bounds the gradient of the signed envelope of averages over a finite band of radii, uniformly in the number of dyadic scales. At a locally maximizing radius a moment identity holds; mass on the boundary shell is shown to concentrate near one point outside a small exceptional set of centers; and two multiscale constructions control scalar cancellation and the choice of directions. Approximation then extends the estimate to Sobolev inputs, and a separate argument removes the singular part of the derivative measure.
  • Source. Commit 1581d4c of the openai/math repository, folder An endpoint gradient bound for the centered disk maximal operator.
  • Formalization, as described by the repository. The scope note lean/docs/085.md states that the formalization proves that every real f in W1,1(R2) has a maximal function that is finite almost everywhere, belongs to W1,1loc and has a globally integrable weak gradient with ‖∇Mf‖1 ≤ C‖∇f‖1, and that it also retains the signed finite-band estimate; a BV extension is outside these statements. Its Comparator challenges are DiskMaximal.lean and SignedFiniteBand.lean.

Public follow-up work

Date Work Relation Public claim Public status (checked 18 October 2026)
2026-10-08 MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) Review (fidelity of the formal statements) Rates both challenges "full", notes that weak gradients are defined by hand against smooth compactly supported test functions, which is the standard definition, and that the BV extension is not claimed; records a sandboxed Comparator pass for each. MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14 con-leche development journal (task #348) Verification (second kernel) In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither DiskMaximal nor SignedFiniteBand, so both challenges were accepted by con-leche and by Lean's official kernel. Development journal.
2026-10-08 (manuscript); 2026-10-11 (Lean proof) Kenta Kitamura (GitHub KitaKen1), centered-ball-maximal-endpoint (Lean proof commit fb93537) Extension (every dimension; Lean) States a complete Lean 4 proof, for every dimension d ≥ 1, of the Hajłasz–Onninen question for the centered Euclidean-ball maximal operator in the form ‖∇Mf‖1 ≤ Cd(‖f‖1 + ‖∇f‖1), and of the homogeneous bound ‖∇Mf‖1 ≤ Cd‖∇f‖1 for every d ≥ 2. It cites the OpenAI manuscript as a source. The repository reports that both targets build with Lean v4.33.1 and as a 64,483-line standalone file with Lean v4.35.0-rc4, and that the final #print axioms commands report only propext, Classical.choice and Quot.sound. It states that global integrability of Mf is not asserted, and discloses development with assistance from ChatGPT and OpenAI Codex. The repository states that independent mathematical review and upstream adoption remain pending.
2026-10-11 Formal Conjectures pull request #7129 (KitaKen1) Catalogue (formal statement) Proposes a file FormalConjectures/Paper/HajlaszOnninen.lean stating the question for every dimension and its homogeneous variant, marked "research solved" with formal_proof links to the repository above. Open.

Notes

  • The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
Retrieved from "https://openai-aftermath.mathnt.net/index.php?title=Endpoint_Sobolev_regularity_of_the_centered_maximal_function&oldid=309"