OAI/Geometry/RCD/Sobolev/WeakLaplacianLowerMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local absolute source mass from a one-sided Laplacian bound

The positive test and its exact weak pairing control both signs of the source. This is used with the uniform lower bounds on scaled heat logs.

  1. theorem OAI.RegularPointCoordinates.weakLaplacian_lower_weighted_mass line 18