OAI/Geometry/RCD/Coordinates/HeatLiYauRegularized.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The regularized Li--Yau estimate almost everywhere

Finite-measure indicators identify the actual generator and gradient representatives. All source integrals are justified locally in L².

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_liYau_regularized line 24