OAI/Geometry/RCD/Heat/CompactHeatHessianTails.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform tails of the original scaled heat Hessian

The estimates concern the actual globally defined factor Hessians in the second derivative formula, for every noise index and every interior time.

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