OAI/Analysis/RieszRectifiability/Restart/BadBetaRestartPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mass packing for bad-beta restart roots

For an AD-regular measure with an L²-bounded Riesz transform, the total mass of restart roots triggered by large bilateral beta numbers is bounded by a constant times the initial clean cell mass. The descendant packing estimate contributes K, while the initial root contributes the additional 1. The estimate retains the admissibility condition on the initial cell's core radius.

  1. theorem OAI.RieszRectifiability.original_AD_Riesz_bad_beta_restart_mass line 24