∑math20

Real and complex analysis · Result 083

Hilbert transforms along Lipschitz directions

1 paperLean

Proves a uniform strong L2 bound for the planar Hilbert transform along any Lipschitz unit vector field, at integration lengths bounded by an absolute multiple of its reciprocal Lipschitz constant. The estimate is uniform over inner truncations and yields an L2-bounded principal-value operator, establishing Stein's weak-type conjecture at this short scale.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A uniform Hilbert transform estimate for Lipschitz directions

A uniform Hilbert transform estimate for Lipschitz directions

OpenAI · September 25, 2026

We prove a uniform L2 bound for the Hilbert transform along a Lipschitz unit vector field in the plane, with integration restricted to a fixed absolute multiple of the reciprocal Lipschitz seminorm. The bound is uniform in the inner truncation and holds for fields depending on both coordinates. This gives an affirmative answer to Stein's weak-\((2,2)\) conjecture.

Read PDF Download Source

Cite
@misc{OAI:A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026,
  author = {{OpenAI}},
  title = {{A uniform Hilbert transform estimate for Lipschitz directions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026/main.pdf}{OAI:A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves uniform \(L^2\) bounds for short Hilbert transforms along Lipschitz unit vector fields in the plane, including fields depending on both coordinates. For Lipschitz constant \(K>0\), every hard truncation with \(0<\varepsilon\le R\le1/(10^6K)\) has one universal \(L^2\) bound on Schwartz functions, independent of the inner cutoff.

At a fixed short scale for \(1\)-Lipschitz fields, the formalization also gives principal-value and weak-\((2,2)\) estimates and bounded extensions to all of \(L^2\). These results establish the stated short-scale form of Stein's question.

Comparator links

ResultComparator statement
Uniform short Hilbert-transform bounds for Lipschitz directionsLipschitzHilbert.lean

Scope note on GitHub →