OAI/Geometry/RCD/Heat/CompactFactorTimeRatio.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A scale-independent comparison for compact endpoint heat factors

The endpoint weight cancels by comparing the two kernels before integration. This is the ratio needed in the logarithmic gradient estimate.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_time_ratio line 21