OAI/Analysis/RieszRectifiability/Projections/NoncollapsingPlaneProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Noncollapsing projections of pairwise plane approximations

A contraction bounded below on an approximating plane separates nearby points up to the plane-fitting error. Under a quantitative smallness condition, this separation yields a Lipschitz ball map covering a set with pairwise plane fits.

  1. theorem OAI.RieszRectifiability.projection_lower_bound_of_pairwise_plane line 21
  2. theorem OAI.RieszRectifiability.projection_separates_of_lower_bound line 61
  3. theorem OAI.RieszRectifiability.exists_ball_cover_of_noncollapsing_pairwise_planes line 76