OAI/Analysis/RieszRectifiability/Restart/ActiveRegionStopMassArea.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Stopping-cell mass controlled by model area

Global growth bounds and the lower area of stopping cores control the mass of stopping cells by Hausdorff measure on the limit model. Disjoint cores allow these estimates to be summed over countable families inside a prescribed region.

  1. def OAI.RieszRectifiability.activeRegionStopMassAreaConstant line 22
  2. theorem OAI.RieszRectifiability.activeRegionStopMassAreaConstant_lt_top line 25
  3. theorem OAI.RieszRectifiability.cellRegionStops_small_cores_pairwise_disjoint line 30
  4. theorem OAI.RieszRectifiability.active_region_stop_cell_mass_le_core_area line 64
  5. theorem OAI.RieszRectifiability.active_region_stop_subfamily_mass_le_area line 96