OAI/Analysis/RieszRectifiability/Restart/ActiveCellDeficitAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Deficit bounds for active-cell chart assembly

The uncovered mass of an active cell splits into discarded parent surface area and deficits of the selected stopping children. Gluing the parent pieces and child charts preserves their covered sets and transfers this estimate to a bounded ball chart, with the stated finite-piece Lipschitz constant.

  1. theorem OAI.RieszRectifiability.active_cell_deficit_le_selected_losses line 36
  2. theorem OAI.RieszRectifiability.exists_active_cell_chart_with_deficit_bound line 68
  3. theorem OAI.RieszRectifiability.exists_active_cell_finite_piece_deficit_assembly line 115