OAI/Geometry/RCD/Sobolev/WeightedRecoveryEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp compactly weighted energy upper bounds

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.weighted_recovery_energy_upper line 21