OAI/Analysis/RieszRectifiability/Limits/GlobalLowerMeasureLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Global lower growth in measure limits

Compact-test convergence transfers lower ball-mass bounds to support points of the limit, with the explicit factor 4 ^ n. Combined with global upper growth and an origin normalization, this produces a nonzero subsequential limit with both growth estimates.

  1. theorem OAI.RieszRectifiability.compactTestConvergence_global_lower line 23
  2. theorem OAI.RieszRectifiability.exists_global_growth_measure_limit line 51