OAI/Analysis/RieszRectifiability/Restart/ActiveRegionPositiveMatchedProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Matched projection at positive stopping scales

A local chart at a positive stopping scale supplies an approximating plane and covers a disk in that plane by projecting the nearby limit surface. The same plane controls the surface's normal deviation on the larger comparison ball.

  1. theorem OAI.RieszRectifiability.exists_active_region_positive_matched_projection line 22