OAI/Analysis/RieszRectifiability/Restart/ActiveRegionPieceLoss.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mass lost outside an active-region piece

Stopping cells whose inner balls miss a chosen piece are charged to discarded surface area. Combining this estimate with Hausdorff domination bounds the mass of both the uncovered limit set and the unrepresented stopping cells.

  1. theorem OAI.RieszRectifiability.active_region_missed_stop_mass_le_discarded_area line 36
  2. theorem OAI.RieszRectifiability.active_region_unrepresented_mass_le_discarded_area line 55