OAI/Analysis/RieszRectifiability/Surfaces/ParentToChildInputChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Parent-to-child input charts

A parent chart is reparametrized over the nearby child plane and restricted to the child disk. Projection and height estimates preserve the exact restricted range, the Lipschitz and normal-component bounds, and containment in the physical child ball.

  1. theorem OAI.RieszRectifiability.exists_parent_to_child_input_chart line 24