OAI/Analysis/RieszRectifiability/Flatness/QuantitativeFlatAnnularAlternative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform flat-ball or large-annulus alternative

Compactness upgrades the local annular flat-ball theorem to a radius chosen uniformly before the measure. A counterexample sequence would converge to a measure with bounded annular transforms but no admissible flat ball, contradicting the local theorem.

  1. theorem OAI.RieszRectifiability.exists_uniform_flat_annular_radius line 20