OAI/Analysis/RieszRectifiability/Restart/ActiveCellChildImageMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Image-mass estimates for selected stopping cells

Pairwise disjointness controls the total mass omitted by child pieces. Combining that bound with the active-cell representation estimates the mass still missing from a glued image in terms of discarded surface area and child-cell losses.

  1. def OAI.RieszRectifiability.activeCellSelectedStopSet line 22
  2. theorem OAI.RieszRectifiability.selected_stop_deficit_sum_le_cell_mass line 31
  3. theorem OAI.RieszRectifiability.active_cell_mass_le_selected_image_add_losses line 65
  4. theorem OAI.RieszRectifiability.exists_active_cell_glued_chart_with_mass_losses line 97