OAI/Analysis/RieszRectifiability/Surfaces/InitialAffineCharts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Initial affine-plane charts

Orthogonal coordinates parametrize each affine-plane disk by a 1-Lipschitz chart with constant normal component and exact range. A distance estimate locates the chart near an ambient center, with error given by that center's distance to the plane.

  1. theorem OAI.RieszRectifiability.exists_affine_plane_disk_chart line 22
  2. theorem OAI.RieszRectifiability.affine_plane_dist_le_projection_add_offset line 47
  3. theorem OAI.RieszRectifiability.exists_located_affine_plane_disk_chart line 62