OAI/Analysis/RieszRectifiability/Restart/ActiveCellMassArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Active-cell mass controlled by limit-model area

An active cell splits into its limiting region and a countable family of stopping descendants. Hausdorff domination on the limiting region and the stopping-core mass estimate bound its original measure by nearby area of the limit model.

  1. theorem OAI.RieszRectifiability.active_cell_original_mass_le_limit_area line 37
  2. theorem OAI.RieszRectifiability.active_cell_radius_power_le_limit_area line 91