OAI/Geometry/RCD/Heat/PositiveKernelOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strict oscillation contraction of the positive kernel transform

The estimate compares two rows with one common exponent. Integrating the derivative along the line joining two exponents is the scalar step in the heat-kernel scaling construction.

  1. theorem OAI.RegularPointCoordinates.positiveKernelLogTilt_oscillation line 19