OAI/Analysis/RieszRectifiability/Restart/ActiveSurfaceInnerCone.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inner-ball cone bounds for active surfaces

The capture property places surface points in the inner ball inside an active chart. Its normal-component Lipschitz bound and the contraction of orthogonal coordinates control normal increments by ambient distances.

  1. theorem OAI.RieszRectifiability.HasActiveCellSurfaceChart.normal_increment_on_inner_ball line 21