OAI/Geometry/RCD/Heat/HeatFisherDimensional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Dimensional curvature controls 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. The square of the actual logarithmic Laplacian is retained.

  1. def OAI.RegularPointCoordinates.regularizedHeatLogSource line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regularizedFisherInterpolation_dimensional line 37