OAI/Analysis/RieszRectifiability/Restart/ActiveRegionPositiveScaleCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A lower stopping-scale bound lets finite-stage charts capture a nearby part of the limit surface. The resulting chart retains the quantitative Lipschitz bound from the transition maps.

  1. theorem OAI.RieszRectifiability.exists_active_region_positive_scale_chart line 18