OAI/Geometry/RCD/Heat/CanonicalGaussianUpper.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp Gaussian upper bound for the canonical kernel

This proves the upper half of Jiang--Li--Zhang (2016), Theorem 1.2 and Corollary 1.2, for the actual RCD heat kernel. The constants depend on dimension, curvature and epsilon. No Gaussian assumption is used.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_gaussian_upper line 25