OAI/Analysis/RieszRectifiability/Restart/BadDepthAndRestartLossBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Combined bad-depth and restart loss budgets

For a fixed AD-regular measure with a bounded Riesz transform, a multiplicity threshold makes the mass at large bad-beta depth arbitrarily small. Splitting the prescribed tolerance in half combines this estimate with the summed losses over restart cells, uniformly over admissible root cells.

  1. theorem OAI.RieszRectifiability.original_AD_Riesz_bad_depth_loss_budget line 23
  2. theorem OAI.RieszRectifiability.original_AD_Riesz_combined_restart_loss_budget line 54