OAI/Analysis/RieszRectifiability/Restart/ActiveRegionPositiveScaleProjectionCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Projection charts at positive stopping scales

Transporting a local surface chart through three active-region transitions gives a bi-Lipschitz chart containing the limit surface where the stopping scale stays positive. Its tangential displacement and normal component retain quantitative Lipschitz bounds controlled by the active projection error.

  1. theorem OAI.RieszRectifiability.exists_active_region_positive_scale_projection_chart line 23