OAI/Geometry/RCD/Heat/BoundedHeatDiagonalHessianDifference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Diagonal Hessian stability along bounded regular directions

Two actual regular directions with vanishing weighted gradient difference have the same limiting diagonal Hessian action against a fixed heat test. The conclusion is independent of the chosen local Gram representatives.

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