OAI/Analysis/RieszRectifiability/Limits/OriginalGrowthLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonzero compact-test limits with upper growth

A uniform lower bound on unit-ball mass prevents the compact-test subsequential limit from vanishing. The upper growth estimate passes to this limit with the explicit factor 2 ^ n in its constant.

  1. theorem OAI.RieszRectifiability.exists_original_growth_limit line 21