OAI/Analysis/RieszRectifiability/Restart/ActiveCellFinitePieceMassFraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Retained mass from finite-piece assembly

For finite mass, two relative deficit bounds leave at least the fraction 1 - δ - η in the retained set. Applying this estimate to parent surface loss and uncovered child mass upgrades finite-piece assembly to a chart with an explicit retained cell-mass fraction, while preserving its Lipschitz bound and image containment.

  1. theorem OAI.RieszRectifiability.mass_fraction_of_two_deficits line 23
  2. theorem OAI.RieszRectifiability.exists_active_cell_chart_with_retained_mass_fraction line 35