OAI/Geometry/RCD/Sobolev/BoundaryDirichletLocal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A boundary-layer estimate for the actual Dirichlet difference

Metric approximation furnishes an exterior ball at each shell point. The proved volume comparison makes its relative mass uniform, and the zero-fraction Poincare inequality gives the squared boundary scale.

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