OAI/Geometry/RCD/Heat/DimensionalEVI.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated dimensional EVI for the actual heat flow

This is the squared-distance rate form of EKS (2.20), for compact bounded reference densities. The entropy ratio is retained exactly.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_dimensional_EVI line 18