OAI/Geometry/RCD/Sobolev/BoundaryDirichletLayer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform squared-scale control on the whole boundary layer

The net consists of actual shell points. Volume comparison bounds the overlap of its enlarged balls independently of the thickness and scale.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundary_dirichlet_layer line 19