OAI/Analysis/RieszRectifiability/Packing/AffinePlaneNormalFrame.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Normal coordinates for affine planes

Isometric tangent and normal frames express affine orthogonal projection and distance to a plane in Euclidean coordinates. The frame construction chooses the point of the plane nearest the origin as its base point.

  1. theorem OAI.RieszRectifiability.exists_euclidean_isometric_embedding line 22
  2. theorem OAI.RieszRectifiability.affine_plane_projection_of_frame line 32
  3. theorem OAI.RieszRectifiability.affine_plane_distance_normal_frame line 47
  4. theorem OAI.RieszRectifiability.exists_affine_plane_normal_frame line 58