OAI/Geometry/RCD/Sobolev/PoissonCutoffEnergyBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The quantitative cutoff bound for a squared-distance replacement

The full positive source of the boundary datum supplies the sign. Only the already controlled energy-density error of the replacement is needed.

  1. theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.poisson_energy_bound line 19