OAI/Analysis/RieszRectifiability/Surfaces/CenteredPerturbedBallCoverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Centered coverage for perturbed charts

Lipschitz perturbations of the identity cover balls centered at any parameter with sufficient room in the domain. Applied to tangential projection, this gives a disk covered by the portion of the surface inside a controlled ambient ball.

  1. theorem OAI.RieszRectifiability.centered_ball_covered_by_lipschitz_perturbation line 21
  2. theorem OAI.RieszRectifiability.centered_projection_disk_in_surface_ball line 68