OAI/Geometry/RCD/Heat/ScaledHeatGlobalCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One global measurable limit of the actual scaled heat potentials

On every compact spatial ball and every positive interior time interval, the same subsequence converges uniformly in space outside one countable exceptional set of times. The limiting function is locally Lipschitz in space at those times.

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