OAI/Analysis/RieszRectifiability/Kernel/HeightTailSplit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Annular integrability for height-tail estimates

Lipschitz height functions are bounded on each dyadic annulus. The finite annular mass supplied by upper growth then gives the square integrability needed to apply shell estimates in the height-tail decomposition.

  1. theorem OAI.RieszRectifiability.lipschitz_height_memLp_on_annulus line 22
  2. theorem OAI.RieszRectifiability.weighted_height_closed_tail_bound line 40
  3. theorem OAI.RieszRectifiability.finiteShellRegion_union_closedExterior line 78
  4. theorem OAI.RieszRectifiability.finiteShellRegion_disjoint_closedExterior line 96
  5. theorem OAI.RieszRectifiability.improved_weighted_height_tail_bound line 102