OAI/Analysis/RieszRectifiability/Kernel/ShiftedHeightTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Height tails after a dyadic shift

Rescaling the initial radius reindexes the dyadic annuli. Applying the weighted height-tail estimate at this shifted radius yields a geometric decay term and a Lipschitz-controlled far tail for the normalized height.

  1. theorem OAI.RieszRectifiability.dyadicAnnulus_shift line 21
  2. theorem OAI.RieszRectifiability.normalized_weighted_height_tail_shifted line 26