OAI/Analysis/RieszRectifiability/Packing/OriginalADBetaPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bad-beta packing for the original AD hypotheses

For nontrivial support, AD regularity supplies global growth and converts the uniform bad-descendant estimate to the original Riesz hypotheses. Subsingleton support has no positive admissible core radius, so that branch follows directly from the diameter condition.

  1. theorem OAI.RieszRectifiability.original_AD_Riesz_bad_beta_total_mass line 22