# Riesz transforms and rectifiability in higher codimension

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

- [Riesz transforms and uniform rectifiability in higher codimension](../../preprints/Riesz-transforms-and-uniform-rectifiability-in-higher-codimension-September-24-2026/paper.pdf)

## 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](../ComparatorChallenges/RieszQuantitative.lean) |