OAI/Analysis/RieszRectifiability/Projections/ProjectionPieceParameterization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parameterizing pieces separated by projection

An orthogonal projection that separates points supplies Euclidean coordinates for a Lipschitz ball parameterization. Pairwise approximating planes with controlled angles provide a geometric criterion for this separation.

  1. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_projection line 22
  2. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_pairwise_planes line 52