OAI/Geometry/RCD/Heat/CanonicalGaussianDifference.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian finite differences for the canonical heat kernel

The upper Gaussian bound and actual reverse Poincaré now supply the finite-difference estimate without any Gaussian premise.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_upper_five line 23
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_gaussian_difference line 41