OAI/Analysis/RieszRectifiability/Restart/ActiveRegionLowMatchedProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Matched projections at low stopping scales

An active cell at the requested radius supplies a fitting direction with small forward height error. Its limiting chart also covers a definite projected ball, so both estimates hold for the same plane through the requested center.

  1. theorem OAI.RieszRectifiability.exists_active_region_low_matched_projection line 21