OAI/Analysis/RieszRectifiability/Restart/RestartCoverageInduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Restart coverage with a finite bad-cell budget

The iterated chart constant records the cost of assembling child charts. Induction on the bad-cell budget covers points outside the restart remainders, since passing a bad descendant reduces the remaining budget. Countable subadditivity then bounds the uncovered mass by the original deficit and the sum of all remainder masses.

  1. def OAI.RieszRectifiability.badBudgetChartConstant line 24
  2. theorem OAI.RieszRectifiability.exists_restart_chart_of_bad_budget line 50
  3. theorem OAI.RieszRectifiability.exists_restart_chart_with_original_mass_deficit line 101