OAI/Analysis/RieszRectifiability/Foundations/UniformExcessPropagation.lean

Uniform propagation of small excess

The propagation index is chosen before the measure, for fixed growth, lower mass, and Riesz bounds. A hypothetical sequence of failures along the schedule has a subsequence whose normalized excess vanishes at the prescribed radius, contradicting the lower bound supplied by each failure.