OAI/Geometry/RCD/Heat/CompactHeatScaledHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scaled Hessian formula with its actual vanishing remainder

All directions represent the original compact heat factors. The test is a fixed heat regularization, independent of the interpolation time.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationMean_hessian line 27