OAI/Geometry/RCD/Heat/CanonicalKernelIdentification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identification with every published continuous heat-kernel representative

The canonical half-time overlap agrees pointwise with any continuous kernel representing the actual Cheeger semigroup. Thus published Gaussian estimates for such a kernel transfer to the canonical representative.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_ae_kernel line 26
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_eq_of_isContinuousHeatKernel line 62
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_gaussian_of_published_kernel line 84