`OAI/Geometry/RCD/Heat/CompactHeatGlobalIntrinsicHessian.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full scaled heat Hessian has the canonical local action pairing

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.global_scaled_intrinsic_hessian_limit line 22