OAI/Geometry/RCD/Heat/HeatHamiltonPositive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the logarithmic regularization on the positive heat locus

A single countable full-measure set retains the Hamilton bounds as the positive regularization decreases to zero.

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