Riesz transforms and rectifiability in higher codimension

1 paperLean

Resolves the remaining higher-codimension Riesz-transform rectifiability problem: for d ≥ 4 and \(2\le n\le d-2\), an n-Ahlfors–David regular Radon measure on ℝ^d is uniformly n-rectifiable whenever its n-dimensional Riesz transform is uniformly L²-bounded over all positive hard truncations. The rectifiability bounds depend only on dimension, regularity and operator bounds.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Riesz transforms and uniform rectifiability in higher codimension

OpenAI · September 24, 2026

We prove that an n-Ahlfors–David regular Radon measure on ℝ^d is uniformly n-rectifiable if its n-dimensional Riesz transform is uniformly bounded from scalar \(L^2(\mu)\) to vector-valued \(L^2(\mu)\) over all positive hard truncations, for integers d ≥ 4 and \(2\le n\le d-2\). This gives a positive answer to the David–Semmes Riesz-transform question in its remaining higher-codimension range. The conclusion gives uniform big pieces of Lipschitz images of Euclidean balls.

Read PDF Download Source

Cite

@misc{OAI:Riesz-transforms-and-uniform-rectifiability-in-higher-codimension-September-24-2026,
  author = {{OpenAI}},
  title = {{Riesz transforms and uniform rectifiability in higher codimension}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Riesz-transforms-and-uniform-rectifiability-in-higher-codimension-September-24-2026/paper.pdf}{OAI:Riesz-transforms-and-uniform-rectifiability-in-higher-codimension-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

Riesz transforms and uniform rectifiability in higher codimension

Scope

The formalized result proves that bounded Riesz transforms force quantitative uniform rectifiability in higher codimension. For \(d\ge4\) and \(2\le n\le d-2\), an \(n\)-Ahlfors–David regular measure whose positive hard truncations have one uniform \(L^2\) operator bound has big pieces of Lipschitz images. The mass fraction and Lipschitz constant depend only on the dimensions and the stated regularity and operator bounds, and work at every support point and admissible radius, including unbounded support. The variation and principal-value corollary is not included.

Comparator links

Result	Comparator statement
Quantitative higher-codimension Riesz rectifiability	RieszQuantitative.lean

Scope note on GitHub →