OAI/Analysis/RieszRectifiability/Restart/ActiveRegionMatchedProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Matched projection at every scale

The large-, high-, positive-, and low-stopping-scale constructions combine to give one plane with a uniform forward flatness estimate and projected disk coverage at every positive radius of an active-region limit surface.

  1. theorem OAI.RieszRectifiability.exists_active_region_matched_projection_all_scales line 23