OAI/Analysis/RieszRectifiability/Surfaces/FiniteBallChartUnion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite unions of ball charts

Separated parameter islands encode finitely many bounded Lipschitz charts in a single ball chart. The union constant combines the packing factor, the gluing estimate, and the ambient Lipschitz extension constant. Extension followed by a nonexpansive retraction also handles charts initially defined on subsets of the parameter ball.

  1. def OAI.RieszRectifiability.finiteBallChartUnionConstant line 24
  2. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_finite_ball_charts line 28
  3. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_finite_partial_charts line 46