OAI/Geometry/RCD/Heat/CanonicalNearDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform near-diagonal lower bounds at small times

The diagonal mass bound and the proved Gaussian finite difference estimate give a dimensional neighborhood of strict positivity. No lower heat-kernel estimate is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_near_diagonal line 24