OAI/Analysis/RieszRectifiability/Restart/ActiveRegionHighScaleLocalArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local charts at high stopping scales

Two active projection steps transport a root-plane disk to a bilipschitz chart covering the high-stopping-scale part of the limit model in a given ball. The distance bounds on this chart yield local Hausdorff measure estimates.

  1. theorem OAI.RieszRectifiability.exists_active_region_high_scale_local_bilipschitz_chart line 36
  2. theorem OAI.RieszRectifiability.active_region_high_scale_local_ball_area_le line 109