OAI/Geometry/RCD/Sobolev/LocalCutoffLipschitz.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform cutoff bounds for locally Lipschitz functions

Only values and Lipschitz control on the support of the cutoff are needed. The constants are uniform over a family with the same local bounds.

  1. theorem OAI.RegularPointCoordinates.local_lipschitz_cutoff line 17
  2. theorem OAI.RegularPointCoordinates.radial_local_lipschitz_cutoff line 59