OAI/Analysis/RieszRectifiability/Restart/ActiveRegionLargeScaleCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Large-scale charts for active-region limits

The portion of an active-region limit model with large stopping scale is covered by a root-plane disk chart transported through two active projection steps. The resulting chart has Lipschitz bound equal to the square of the global projection bound.

  1. theorem OAI.RieszRectifiability.exists_active_region_large_scale_chart line 21