OAI/Geometry/RCD/Sobolev/LocalPoissonEnergyDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local Poisson energy densities with the original gradient bound

The compact extension supplies Sobolev regularity and Bochner positivity. Clipping its energy density keeps the original local gradient bound on the whole space without changing any interior test pairing.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_energy_density_continuous_tests line 25
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_energy_density line 91