OAI/Geometry/RCD/Sobolev/SobolevPointedTestRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual zero-boundary Sobolev recovery of Euclidean tests

The recovered function belongs to the original Dirichlet space. Both its uniform value error and its rescaled gradient bound are explicit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_sobolev_test_recovery line 18