OAI/Analysis/RieszRectifiability/Restart/ActiveProjectionDiskCoverage.lean

Disk coverage by active projections

Affine projection preserves tangential coordinates in the reference plane. The tangential part of the active projection is therefore a small Lipschitz perturbation of the identity on a disk. Its displacement bound gives coverage of a shrunken disk, and the quantitative smallness condition yields coverage of the concentric half disk at the lattice scale.