OAI/Geometry/RCD/Heat/KernelHeatComplementMonotone.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Li--Yau time monotonicity also holds for the bounded complement

The complement is obtained through its actual L2 truncations, so no constant L2 function or finite total ambient measure is required.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.kernelHeat_complement_monotone line 22