VibeMathedMath problems solved with AI
Sign in

The Hilbert transform-UMD dependence problem

For fixed 1<p<∞1<p<\infty and a Banach space XX, Burkholder and Bourgain showed in 1983 that the UMD property is equivalent to boundedness of the Hilbert transform on Lp(R;X)L^p(\mathbb{R};X), with the quadratic comparisons ℏp,X≲βp,X2\hbar_{p,X}\lesssim\beta_{p,X}^{2} and βp,X≲ℏp,X2\beta_{p,X}\lesssim\hbar_{p,X}^{2} between the Hilbert transform constant and the UMD constant. What is the optimal dependence between ℏp,X\hbar_{p,X} and βp,X\beta_{p,X}, uniformly over all UMD spaces XX: can either quadratic bound be improved, in the best case to a linear one?

Result
Proved(see note)
Status
Resolved
AI contribution
AI co-developed
Method
Construction
Field
Banach space geometry and harmonic analysis
Posed by
Implicit in Burkholder's and Bourgain's 1983 quadratic bounds; stated as an open problem in Burkholder's 2001 Handbook survey
Year posed
1983
Years open
43y
Solved
2026-09-09
Model
GPT-6 Astra
Vendor
OpenAI
Collaborators
Emiel Lorist, Jan van Neerven
Verification
Lean-verified
Publication
Preprint
Significance
25 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Neither exponent can be lowered. Theorem 1.1 constructs explicit 2n2^{n}-dimensional spaces XnX_n and YnY_n with ℏ2,Xn≍n\hbar_{2,X_n}\asymp n, β2,Xn≍n\beta_{2,X_n}\asymp\sqrt n and β2,Yn≍n\beta_{2,Y_n}\asymp n, ℏ2,Yn≍n\hbar_{2,Y_n}\asymp\sqrt n, with universal comparison constants, so both quadratic comparisons are sharp at p=2p=2; Corollary 1.3 extends the growth rates to every fixed 1<p<∞1<p<\infty by extrapolation, with constants depending on pp. The spaces are built from the summation operators Wenzel had proposed as candidates for exactly this separation. The Lean formalisation covers Theorem 1.1 at p=2p=2 over both real and complex scalars; the extrapolation to other pp and the exact coefficients of Remark 1.2 are outside it.

What the AI did

The paper's AI disclosure: "The examples proving the quadratic dependencies were found in conversations with OpenAI's Astra model. All statements and proofs in the final manuscript have been reviewed by the authors and subsequently proof-checked in Lean 4 using OpenAI's Astra model." The repository README adds that the Lean code, documentation, scripts and tests were generated with GPT-6 Astra under human direction. Co-developed: the decisive constructions came out of conversations with the model, and two named authors reviewed and take responsibility for the manuscript.

Verification

Checked here on 12 September 2026 by reading the repository at commit 055d95e. Main/PaperStatement.lean states the theorem as the two dimensions and all eight inequalities, with nn and n\sqrt n literally as in the paper and universal constants. Mathlib has no UMD constant, so the two constants are project definitions and are the trust surface; both were read. umdConstant is the infimum of CC over all σ\sigma-finite sample spaces, filtrations, LpL^p martingales and unimodular coefficients for which the martingale transform is bounded by CC times the difference sum, and hilbertConstant is the infimum of CC over all C1C^1 compactly supported ff admitting a principal-value Hilbert transform in LpL^p with norm at most C ∥f∥pC\,\|f\|_p; these are the standard notions. No sorry, no axiom declarations, no native_decide anywhere; tests/AxiomAudit.lean walks every project declaration transitively and fails on any admission or any axiom beyond propext, Classical.choice and Quot.sound. GitHub Actions ran the build and that audit on Ubuntu and Windows at the reviewed commit, both green, which puts the kernel check on machines other than the authors'. The build was not repeated here. Not formalised: Corollary 1.3 and the exact coefficients of Remark 1.2.

Sources

Submitted by RustyKestrel290 on

Changelog2 changes

Discussion