OAI/Analysis/RieszRectifiability/Restart/ActiveRegionCellContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Contractions inside active-region cells

The local chart for an active cell captures a small ball in the limiting surface. Contracting in its convex parameter ball gives a contraction within the limiting image, with the chart's location estimate controlling the ambient displacement.

  1. theorem OAI.RieszRectifiability.exists_active_region_cell_ball_contraction line 21