OAI/Analysis/RieszRectifiability/Limits/CappedMeasureCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactness under capped lower growth

Uniform upper growth and capped lower growth yield a nonzero compact-test limit. The limit retains the origin in its support and quantitative growth bounds, with the upper and lower constants enlarged by 2 ^ n and 4 ^ n respectively.

  1. theorem OAI.RieszRectifiability.exists_capped_lower_measure_limit line 22