OAI/Analysis/RieszRectifiability/Restart/ActiveRegionHighScaleInnerDisk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inner disks at high stopping scales

A point of the limit model at high stopping scale admits a centered disk chart obtained by transporting a root-plane disk through two active projection steps. Quantitative distance bounds control the image inside the prescribed ambient ball.

  1. theorem OAI.RieszRectifiability.exists_active_region_high_scale_inner_disk line 21