OAI/Geometry/RCD/Heat/HeatFisherRiccati.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The dimensional scalar inequality along the actual heat interpolation

The mass and source moment are constant along the forward/backward heat pairing. No probability normalization or nonzero-mass assumption is needed.

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