OAI/Analysis/RieszRectifiability/Surfaces/PerturbedBallCoverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ball coverage by a Lipschitz perturbation

A map with bounded displacement whose error from the identity is a strict contraction covers a smaller concentric closed ball. A fixed point of the associated correction map provides the preimage of each target point.

  1. theorem OAI.RieszRectifiability.closedBall_covered_by_lipschitz_perturbation line 21