OAI/Analysis/RieszRectifiability/Restart/ActiveRegionPositiveScaleContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A positive stopping scale supplies a bilipschitz chart on a convex plane ball. Contracting inside that chart gives a controlled small-ball contraction; finite-stage stabilization keeps its image on the limiting active-region surface.

  1. theorem OAI.RieszRectifiability.exists_active_region_positive_scale_small_ball_contraction line 20