OAI/Geometry/RCD/Heat/HeatShiftedHessianBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform quantitative Hessian errors from full shifted heat mass

The estimate is simultaneous for every compact Lipschitz direction with the same gradient bound. The positive shifted density is derived from the actual scalar dimensional Bochner theorem.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_shifted_hessian_eventual_bound line 22