OAI/Geometry/RCD/Heat/HeatFisherCurvature.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Curvature controls the derivative of the actual Fisher interpolation

The logarithm, its source, and its squared gradient are the previously constructed Sobolev functions. The test is the actual product of the two heat evolutions, with the same positive regularization.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regularizedFisherInterpolation_curvature line 26