OAI/Geometry/RCD/Heat/CanonicalAllTimeLogLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive-time rescaling of the compact kernel logarithmic limit

The truncation changes only finitely many terms. This permits the fixed reference time of the constructed heat potentials as well as interior times.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_compact_log_limit_allTimes line 20