OAI/Geometry/RCD/Sobolev/DyadicSupportCoercivity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Support-sensitive coercivity on dyadic scales

A support set small compared with the CD lower volume of a dyadic ball leaves a large zero set in every covering ball. The resulting coercivity constant gains the square of that smaller radius.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dyadic_support_coercivity line 21