OAI/Geometry/RCD/Sobolev/InteriorLipschitzTestProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported tests of locally Lipschitz functions

An exact bounded Lipschitz extension on the test support reduces products to the bounded Lipschitz class used by measured approximation.

  1. theorem OAI.RegularPointCoordinates.interior_lipschitz_test_product line 16