OAI/Geometry/RCD/Sobolev/SharpRecoveryEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp normalized energy upper bound for the actual recovered tests

The fixed interior support extends the local slope estimate to the whole physical ball. Measured convergence then gives the Euclidean Dirichlet energy with no multiplicative loss.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.recovery_energy_upper line 20