OAI/Analysis/RieszRectifiability/Surfaces/ImmediateChildChartRescaling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Immediate-child charts on a parent ball

Rescaling immediate-child charts to the parent lattice ball preserves their images and divides their Lipschitz bounds by the fixed radius ratio of 64. Restricting the rescaled maps to the open parent ball gives a common parameter domain for all children.

  1. theorem OAI.RieszRectifiability.exists_immediate_child_charts_on_parent_ball line 22