OAI/Analysis/RieszRectifiability/Restart/CleanCellChartTargetBridge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

From clean-cell deficits to ball charts

A relative chart deficit ζ leaves at least the fraction 1 - ζ of a finite cell's mass in the chart image. For a support ball of radius r, a clean cell at scale r / 4 lies inside that ball and contains a core of radius r / 32. The lower AD bound supplies the retained mass fraction (1 - ζ) / (C * 32 ^ n); rescaling the chart domain to radius r multiplies its Lipschitz bound by 1 / 4.

  1. theorem OAI.RieszRectifiability.retained_mass_of_chart_deficit line 24
  2. theorem OAI.RieszRectifiability.uniformlyRectifiable_of_uniform_clean_cell_deficits line 38