OAI/Analysis/RieszRectifiability/Flatness/AffinePlaneCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Affine plane coordinates

A linear isometric embedding determines an affine plane parametrization and an adjoint coordinate map. These maps are Lipschitz and recover every parameter on the plane; their composition also gives a Lipschitz distance-to-plane function.

  1. def OAI.RieszRectifiability.affinePlaneSection line 20
  2. def OAI.RieszRectifiability.affinePlaneCoordinates line 24
  3. theorem OAI.RieszRectifiability.affinePlaneSection_lipschitz line 29
  4. theorem OAI.RieszRectifiability.affinePlaneCoordinates_lipschitz line 38
  5. theorem OAI.RieszRectifiability.affinePlaneCoordinates_leftInverse line 49
  6. theorem OAI.RieszRectifiability.affinePlaneHeight_lipschitz line 58