OAI/Analysis/RieszRectifiability/Surfaces/BallChartPartialMap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ball charts as ambient parameter maps

A chart on a parameter ball is extended by zero outside its domain. On the ball, this ambient map agrees with the chart and retains its Lipschitz bound.

  1. def OAI.RieszRectifiability.ballChartPartialMap line 20
  2. theorem OAI.RieszRectifiability.ballChartPartialMap_apply line 25
  3. theorem OAI.RieszRectifiability.ballChartPartialMap_lipschitzOn line 30
  4. theorem OAI.RieszRectifiability.ballChartPartialMap_image line 38