OAI/Geometry/RCD/Heat/CanonicalKernelConstruction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Construction of the continuous heat kernel

The actual heat semigroup supplies all the fields of the published continuous-kernel premise without a Gaussian assumption. The convolution identity holds at every pair of points by L² continuity and full support, rather than only for almost every endpoint.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_product_integrable line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_convolution_eq_inner line 36
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_convolution_ae line 48
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_convolution line 61
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_isContinuousHeatKernel line 79

    Source documentation

    The continuous-kernel premise follows from the actual semigroup, local heat smoothing, and uniform L² tails.

    theorem canonicalHeatKernel_isContinuousHeatKernel :
    IsContinuousHeatKernel (hausdorff n X) hX.quadratic (hX.canonicalHeatKernel hn p) where
…

    Mentions: OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.hausdorff