OAI/Geometry/RCD/Coordinates/HeatHamiltonRegularized.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The regularized Hamilton bound almost everywhere

Finite-measure indicators test the actual entropy inequality. The bounded regularized logarithm makes every such local integral finite, even when the ambient measure is infinite.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_hamilton_regularized_integrableOn line 26
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_hamilton_regularized line 54