OAI/Analysis/RieszRectifiability/Restart/ActiveRegionLimitFlatness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local flatness of active-region limits

Finite-stage charts lift into the limiting parameterization with controlled tangential displacement and normal error. These estimates bound the height of the limit over each active fitting plane and, conversely, approximate nearby points of that plane by points of the limit.

  1. theorem OAI.RieszRectifiability.exists_active_region_limit_chart_with_normal_error line 35
  2. theorem OAI.RieszRectifiability.active_region_limit_height_on_active_ball line 78
  3. theorem OAI.RieszRectifiability.active_fitting_plane_approximated_by_limit line 106