OAI/Geometry/RCD/Harmonic/SupportedCoefficientL2Error.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L2 errors in a coefficient supported in the interior

The two weak gradients need bounds only on the support of the coefficient. The original outer-ball normalization is retained.

  1. theorem OAI.RegularPointCoordinates.supported_coefficient_l2_gamma_error line 17