OAI/Geometry/RCD/Heat/ScaledHeatAllTimes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every interior time of the actual small-noise heat limit

The one-sided time error tends to zero along the original subsequence. Thus the continuous limit removes the exceptional times from convergence, as well as from the transport comparison.

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