OAI/Analysis/RieszRectifiability/Projections/PlaneChangeProjectedMap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parameter maps under a change of plane

The disk lift and orthogonal projection transfer a parametrization to another plane. Normal Lipschitz control and the distance between projections bound its deviation from the identity parameter map.

  1. def OAI.RieszRectifiability.planeChangedParameterMap line 21
  2. theorem OAI.RieszRectifiability.planeChangedParameterMap_error_lipschitz line 25