PerMeasure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Per-measure Riesz rectifiability

This endpoint retains the original per-measure statement. For nontrivial support, AD regularity supplies global upper growth; uniform restart surface pieces and the hard-truncated Riesz bound then yield Lipschitz ball maps. Subsingleton support is handled separately, so the theorem does not require a positive or finite support diameter. Uniform choices before the measure belong to the separate quantitative endpoint.

theorem OAI.RieszRectifiability.exact_higher_codimension_riesz_rectifiability line 24
Source documentation
The hard-truncated Riesz bound gives Lipschitz ball maps for each measure.
```
theorem exact_higher_codimension_riesz_rectifiability : FullStatement := by
…
```
Mentions: OAI.RieszRectifiability.FullStatement