OAI/Geometry/RCD/Sobolev/SharpWeightedTestRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual Dirichlet tests with exact compactly weighted energies

One recovered sequence works for every nonnegative compact interior weight. The sequence is the original Hopf--Lax recovery, with no energy convergence assumed of it.

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