OAI/Geometry/RCD/Sobolev/ContainingMassPoissonComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local strong gradient comparison from the actual Poisson equation

Sharp recovery energies and the lower bound for the original function, together with vanishing value error, force the cutoff gradient error to vanish. The constant source and cutoff commutator are both retained.

  1. theorem OAI.RegularPointCoordinates.poisson_strong_cutoff_comparison_containing_mass line 21