OAI/Geometry/RCD/Heat/BoundedHeatQuantitativeHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative local Bochner measures for the actual heat Hessian

One coefficient controls every radius. The very same measures dominate all bounded regular direction pairs, with their singular mass retained.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_quantitative_hessian line 28