OAI/Analysis/RieszRectifiability/Restart/GoodRegionRestartAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Restart chart assembly in a good region

Immediate-child charts first assemble at selected stopping cells, then join the finite pieces of the active region. The resulting ball chart covers both families; its uncovered mass is bounded by the omitted surface area and child deficits. The Lipschitz constant is controlled by two restart steps.

  1. def OAI.RieszRectifiability.goodRegionRestartAssemblyConstant line 22
  2. theorem OAI.RieszRectifiability.goodRegionRestartAssemblyConstant_le_two_steps line 25
  3. theorem OAI.RieszRectifiability.exists_good_region_restart_chart line 32