OAI/Analysis/RieszRectifiability/Projections/ProjectionTubeLocation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal projection and distances to an affine plane control ambient distances. The same estimate locates a chart from its planar coordinates and height bound.

  1. theorem OAI.RieszRectifiability.dist_le_projection_add_plane_distances line 17
  2. theorem OAI.RieszRectifiability.plane_chart_location_of_height line 37