OAI/Geometry/RCD/Heat/CanonicalRoughGaussianLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A global Gaussian lower rate at short times

The number of near-diagonal steps grows linearly in squared distance over time. The resulting power bound gives a genuine exponential lower rate. No sharp value of the exponent is needed for the logarithmic estimates.

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