OAI/Analysis/RieszRectifiability/Surfaces/BoundedNormalizedBallCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded normalized ball charts

Metric projection onto a nonempty complete convex set gives a nonexpansive retraction. Composing this retraction with a rescaled ball chart bounds its range by a closed ball while preserving every point of the original image in that ball. The normalization halves the domain radius and multiplies the Lipschitz bound by two.

  1. theorem OAI.RieszRectifiability.exists_nonexpansive_retraction_of_complete_convex line 22
  2. theorem OAI.RieszRectifiability.exists_bounded_normalized_ball_chart line 49