PlaneChangeCharts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reparameterizing a chart over a nearby plane

Small normal slope and a small change of projection leave a positive disk covered in the new plane. The projection inverse defines a chart on this disk, with quantitative Lipschitz bounds for the chart and its normal component.

theorem OAI.RieszRectifiability.exists_chart_over_nearby_plane line 23