OAI/Analysis/RieszRectifiability/Flatness/BetaDescendantTotalMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Total mass of bad-beta descendants

Bad-beta descendants are the support-cell descendants whose enlarged-ball bilateral beta number exceeds the threshold. Taking the supremum over finite subsets upgrades the uniform finite Carleson estimate to their full ENNReal mass sum, with the constant still chosen before the measure.

  1. def OAI.RieszRectifiability.BadBetaDescendant line 22
  2. theorem OAI.RieszRectifiability.exists_uniform_bad_beta_total_mass line 26