OAI/Geometry/RCD/Heat/ScaledHeatTransportLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous transport limit of the actual scaled heat potentials

One subsequence and one exceptional countable time set serve every compact spatial ball. The original continuous limit satisfies the endpoint comparison for every bounded compressed geodesic plan.

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