OAI/Geometry/RCD/Sobolev/LocalLaplacianMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute local Laplacian mass from local gradient bounds

  1. theorem OAI.RegularPointCoordinates.local_laplacian_mass line 14