OAI/Analysis/RieszRectifiability/Restart/ActiveCellSurfaceApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bilateral approximation by active-cell surfaces

Exact tangential chart coordinates and the reference-plane height bound locate surface points near support points. Conversely, surface points in the inner ball remain close to the support by projecting onto the bilaterally approximating plane. Both estimates retain the explicit error constant at the cell radius.

  1. theorem OAI.RieszRectifiability.active_cell_support_point_near_surface line 31
  2. theorem OAI.RieszRectifiability.active_cell_surface_point_near_support line 58