OAI/Analysis/RieszRectifiability/Foundations/CoordinatePieceParameterization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parameterizing pieces from separating coordinates

Coordinates taking a set into a Euclidean ball and satisfying an antilipschitz bound have a Lipschitz inverse on their image. Extending this inverse to the ball produces a Lipschitz map whose range covers the original set.

  1. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_coordinates line 21
  2. theorem OAI.RieszRectifiability.uniformlyRectifiable_of_big_coordinate_pieces line 46