OAI/Geometry/RCD/Heat/CompactHeatPowerRateBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform differential inequality for the actual heat-density powers

This is the power estimate in Gigli--Tamanini, Proposition 4.6, equations (4.19)--(4.21), on the first half of the interpolation.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationPowerMean_deriv_le line 27