OAI/Geometry/RCD/Heat/CompactHeatCommonHessianLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The forward Hessian limit on the fixed common-time law subsequence

There is no further extraction after the continuous law curve has been selected. The original spatial L1 Hessian limit is retained.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.forward_hessian_intrinsic_limit line 27
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.forward_hessian_common_limit line 90