OAI/Analysis/RieszRectifiability/Limits/CompactnessWeightedMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite measures obtained from the compactness weight

The positive decaying compactness weight turns a globally growing measure into a finite measure. Integral formulas give quantitative tail control and transfer a lower mass bound on the unit ball to a lower bound for the weighted total mass.

  1. def OAI.RieszRectifiability.compactnessWeightedMeasure line 21
  2. theorem OAI.RieszRectifiability.compactnessWeightedMeasure_apply line 24
  3. theorem OAI.RieszRectifiability.compactnessWeightedMeasure_finite line 32
  4. def OAI.RieszRectifiability.compactnessFiniteMeasure line 40
  5. theorem OAI.RieszRectifiability.compactnessWeightedMeasure_real line 44
  6. theorem OAI.RieszRectifiability.compactnessFiniteMeasure_mass_bound line 51
  7. theorem OAI.RieszRectifiability.compactnessFiniteMeasure_tail_bound line 60
  8. theorem OAI.RieszRectifiability.compactnessWeight_lower_on_unit_ball line 76
  9. theorem OAI.RieszRectifiability.compactnessWeight_integral_lower line 84
  10. theorem OAI.RieszRectifiability.compactnessFiniteMeasure_mass_lower line 105