OAI/Geometry/RCD/Heat/ExactEntropyPower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact entropy-power interpolation on the actual bounded transport plan

The pointwise CD* bound and the proved Gaussian midpoint estimate imply the hyperbolic interpolation, with the flat case obtained by an actual limit. No entropic curvature-dimension premise is assumed here.

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