OAI/Geometry/RCD/Heat/PoissonHeatShiftedMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative shifted mass for the actual heat of a Poisson replacement

The full positive heat Bochner measures are constructed, including singular mass. Their shifted cutoff integrals have a limit bounded by the original distance-source energy error and the explicit curvature term.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_heat_shifted_mass line 21