OAI/Analysis/RieszRectifiability/Surfaces/FittingPlaneInputChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Input charts on fitting planes

A small bilateral plane error bounds the offset of a support center from the fitting plane. The located affine chart then gives the input disk, with constant normal component, exact projected range, and image contained in the ambient ball of radius 3 * r.

  1. theorem OAI.RieszRectifiability.exists_fitting_plane_input_chart line 21