OAI/Geometry/RCD/Sobolev/PointedTestRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz recovery of Euclidean tests on pointed source balls

The approximation map need not be Lipschitz. Infimum extension repairs its pullback with the correct radius scaling and a uniform vanishing error.

  1. theorem OAI.RegularPointCoordinates.pointed_lipschitz_test_recovery line 17