OAI/Analysis/RieszRectifiability/Restart/ActiveRegionAllScaleForwardFlatness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Forward flatness at arbitrary scales

Parallel translates of fitting planes pass through the requested center while their height errors remain controlled by the original plane distances. Active-cell selection handles small radii, and the root plane handles large radii, both with the same quantitative forward-flatness bound.

  1. theorem OAI.RieszRectifiability.infDist_parallel_plane_through_point_le line 23
  2. theorem OAI.RieszRectifiability.active_region_limit_height_on_enlarged_active_ball line 43
  3. theorem OAI.RieszRectifiability.exists_active_region_low_stopping_scale_plane line 69
  4. theorem OAI.RieszRectifiability.exists_active_region_large_radius_plane line 105
  5. theorem OAI.RieszRectifiability.exists_active_region_high_stopping_scale_plane line 132
  6. theorem OAI.RieszRectifiability.exists_active_region_all_scale_forward_plane line 199