Papers With

← All papers
First page of The bounds $\hbar_{p,X}\lesssim(β_{p,X})^2$ and $β_{p,X}\lesssim(\hbar_{p,X})^2$ are sharp

The bounds $\hbar_{p,X}\lesssim(β_{p,X})^2$ and $β_{p,X}\lesssim(\hbar_{p,X})^2$ are sharp

Emiel Lorist, Jan van Neerven

math.FA Sep 9, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Statements and proofs of the sharpness results were proof-checked in Lean 4.
Abstract
It was proved in the 1980s by Burkholder and Bourgain that, for any Banach space $X$ and $1<p<\infty$, the UMD$_p$ property for $X$ is equivalent to boundedness of the Hilbert transform on $L^p(\R;X)$, and that the UMD constant $β_{p,X}$ and the Hilbert transform constant $\hbar_{p,X}$ are related by the quadratic bounds \begin{equation*} \hbar_{p,X}\lesssim(β_{p,X})^2, \qquad β_{p,X}\lesssim(\hbar_{p,X})^2. \end{equation*} In this paper we present examples showing that both bounds are sharp. More precisely, we construct explicit $2^n$-dimensional Banach spaces for which the Hilbert transform constant grows like $n$ and the UMD constant like $\sqrt n$, and a second family with the reverse behaviour.
Problem

Burkholder and Bourgain showed the UMD constant and Hilbert transform constant for Banach spaces satisfy quadratic bounds hbar ≲ β² and β ≲ hbar². It was open whether these quadratic dependencies could be improved to linear.

Approach

Explicit 2^n-dimensional Banach spaces are constructed by reducing the problem to operator estimates for summation and dyadic matrices viewed as maps from ℓ¹_N to ℓ^∞_N. Scalar cancellation estimates and Cotlar's identity yield the required L² operator bounds, with lower bounds obtained by testing on explicit step functions. All statements and proofs were proof-checked in Lean 4 using OpenAI's Astra model.

Results

Both quadratic bounds are shown to be sharp: one family of spaces has Hilbert transform constant growing like n and UMD constant like √n, and a second family exhibits the reverse behaviour.