OAI/Geometry/RCD/Heat/HeatDaviesKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise Davies bound for the constructed kernel

Reciprocal exponential weights pair the two half-time rows. The resulting bound has the sharp quadratic cost before optimizing the weight parameter.

  1. theorem OAI.RegularPointCoordinates.radialWeight_half_sq line 19
  2. theorem OAI.RegularPointCoordinates.radialWeight_neg_mul line 25
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_davies_bound line 36