OriginalADLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compact-test limits retain the original upper growth and lower AD mass bounds along a subsequence whose support diameters eventually admit every fixed positive radius.

theorem OAI.RieszRectifiability.exists_original_AD_growth_limit line 20