OAI/Geometry/RCD/Sobolev/SupportedGradientL2Error.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L2 value errors against the gradients of compact recoveries

The inner support and the outer normalization are kept separate. The second factor needs a gradient bound only on the inner region.

  1. theorem OAI.RegularPointCoordinates.supported_gradient_l2_error line 17