OAI/Analysis/RieszRectifiability/Foundations/DyadicPropagationRadii.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic descendant radii

The radius at depth j is the original radius divided by 2 ^ j. Rescaling by another dyadic power either returns to a shallower descendant or passes to a larger original scale. Positivity and the support-diameter bound ensure that an admissible dyadic horizon remains admissible for every descendant.

  1. def OAI.RieszRectifiability.descendantRadius line 22
  2. theorem OAI.RieszRectifiability.descendantRadius_pos line 24
  3. theorem OAI.RieszRectifiability.descendantRadius_zero line 28
  4. theorem OAI.RieszRectifiability.descendantRadius_half line 31
  5. theorem OAI.RieszRectifiability.descendantRadius_mul_dyadic_small line 36
  6. theorem OAI.RieszRectifiability.descendantRadius_mul_dyadic_large line 43
  7. theorem OAI.RieszRectifiability.descendantRadius_admissible_horizon line 50