OAI/Geometry/RCD/Sobolev/PoissonStrongComparison.lean

GitHub source file

2 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. def OAI.RegularPointCoordinates.normalizedCutoffEnergy line 20
  2. theorem OAI.RegularPointCoordinates.poisson_strong_cutoff_comparison line 24