OAI/Analysis/RieszRectifiability/Foundations/BlowupMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rescaled measures and their growth bounds

The blowup at a center and positive scale pushes a measure forward by translation and dilation, then normalizes by the scale to the power n. Exact ball formulas transport the support and preserve global upper and lower growth estimates.

  1. def OAI.RieszRectifiability.blowupMeasure line 21
  2. theorem OAI.RieszRectifiability.blowup_preimage_ball line 25
  3. theorem OAI.RieszRectifiability.blowupMeasure_ball line 37
  4. theorem OAI.RieszRectifiability.blowupMeasure_growth line 46
  5. theorem OAI.RieszRectifiability.blowupMeasure_support_iff line 61
  6. theorem OAI.RieszRectifiability.blowupMeasure_origin_mem_support line 76
  7. theorem OAI.RieszRectifiability.blowupMeasure_lower_global line 82