OAI/Geometry/RCD/Transport/DimensionalSlope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The dimensional evolution slope for the actual heat flow

The exact dimensional rate survives radial cutoff approximation. Both entropy and transport cost converge, including at zero distance.

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