OAI/Geometry/RCD/Sobolev/SharpTestRecoverySequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp local-gradient recovery for every interior smooth Euclidean test

The functions belong to the actual source Dirichlet spaces. Their values converge uniformly almost everywhere, and their rescaled minimal gradients are bounded by the differential of the target test plus an arbitrary error.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.sharp_test_recovery_sequence_supported line 19