OAI/Geometry/RCD/Heat/HeatLiYau.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The parameter-two Li--Yau bound for the actual heat generator

A countable positive regularization gives one full-measure set. The polynomial estimate also holds where the heat value vanishes.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_liYau line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_source_lower line 48