OAI/Analysis/RieszRectifiability/Restart/ActiveSurfaceChartStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One active surface chart step

A local chart capturing the original surface near an active cell gives a chart for its projected image. Shrinking the tangential disk leaves room for the projection displacement while retaining exact local image capture. The new chart has controlled normal slope, stays in the reference plane tube, and remains inside the prescribed ambient ball.

  1. theorem OAI.RieszRectifiability.exists_active_surface_chart_step line 26