OAI/Analysis/RieszRectifiability/Restart/ActiveRegionLimitCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local charts for active-region limits

Finite-stage charts lift to the limiting model to give closed embedded charts on active cells. Their projection error and ambient location remain quantitatively controlled, and each chart agrees locally with the image of the full limiting map.

  1. theorem OAI.RieszRectifiability.exists_active_region_limit_cell_chart line 22