OAI/Analysis/RieszRectifiability/Limits/FiniteMeasureSequentialCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sequential compactness of finite measures

Normalization converts uniform tail estimates and a positive mass lower bound into tightness of probability measures. A further subsequence of the masses recovers a finite-measure limit while preserving the uniform mass bounds.

  1. theorem OAI.RieszRectifiability.finiteMeasure_normalize_set_bound line 21
  2. theorem OAI.RieszRectifiability.exists_normalized_measure_subsequence line 33
  3. theorem OAI.RieszRectifiability.exists_finite_measure_subsequence line 62