OAI/Geometry/RCD/Heat/HeatOffDiagonalL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sharp off-diagonal L² decay for the actual heat semigroup

Optimizing the established Davies exponential weight gives the squared L² tail with exponent -d²/(2t) and the pairing estimate with exponent -d²/(4t). No heat-kernel or Gaussian premise is used.

  1. theorem OAI.RegularPointCoordinates.heatAt_radial_L2_tail line 21
  2. theorem OAI.RegularPointCoordinates.integral_mul_sq_le_integral_sq line 56
  3. theorem OAI.RegularPointCoordinates.heatAt_radial_pairing_sq line 77
  4. theorem OAI.RegularPointCoordinates.heatAt_radial_pairing line 106