OAI/Analysis/RieszRectifiability/Restart/OriginalADRestartCoverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Selected restart assembly with controlled mass deficit

HasSelectedRestartAssembly records how parent charts incorporate selected child charts while preserving range and Lipschitz bounds. For a fixed regular AD measure with a bounded Riesz transform, restart-loss and bad-count budgets then produce a root-ball chart with arbitrarily small relative mass deficit.

  1. def OAI.RieszRectifiability.HasSelectedRestartAssembly line 23
  2. theorem OAI.RieszRectifiability.original_AD_Riesz_selected_restart_uniform_deficit line 38