OAI/Geometry/RCD/Heat/CompactHeatLaplacianRemainder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform disappearance of the test-Laplacian remainder

The density is the original scaling interpolation at every interior time. Its exact mass one makes the bound independent of that time and of the normalizing endpoint factors.

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.laplacianRemainder line 28
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.laplacianRemainder_bound line 33
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.laplacianRemainder_tendstoUniformly line 46