OAI/Analysis/RieszRectifiability/Uniformity/RestartBudgets.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform budgets for bad cells and restarts

The class-uniform bad-beta packing constant controls multiplicity tails and the total mass of restart roots. A relative loss tolerance and a finite bad-depth budget are chosen before the measure, using only the fixed geometric and Riesz bounds. Splitting the desired deficit into two halves pays separately for the discarded high-multiplicity set and the remainders of selected restart regions. These budgets feed the recursive chart assembly without changing its image or Lipschitz conclusions.

  1. theorem OAI.RieszRectifiability.quantitative_bad_beta_total_mass line 23
  2. theorem OAI.RieszRectifiability.quantitative_bad_beta_stopping line 39
  3. theorem OAI.RieszRectifiability.quantitative_bad_beta_restart_mass line 67
  4. theorem OAI.RieszRectifiability.quantitative_restart_loss_budget line 85
  5. theorem OAI.RieszRectifiability.quantitative_bad_depth_loss_budget line 107
  6. theorem OAI.RieszRectifiability.quantitative_cell_bad_count_budget line 139
  7. theorem OAI.RieszRectifiability.quantitative_selected_restart_uniform_deficit line 179
  8. theorem OAI.RieszRectifiability.quantitative_recursive_chart_from_surface_pieces line 228