OAI/Analysis/RieszRectifiability/Limits/DyadicSourceExcessLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normalized excess along dyadic source limits

The common affine limits of normal coordinates determine improved approximating planes. Dyadic source moments provide uniform local second-moment bounds, allowing the normal-frame excess estimate to show that squared excess divided by the original scale squared tends to zero along one subsequence at every nonnegative radius.

  1. theorem OAI.RieszRectifiability.exists_dyadic_source_excess_limit line 23