OAI/Geometry/RCD/Heat/CompactHeatLocalScaledHessianLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The local limit of the original scaled factor Hessian

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_scaled_hessian_limit_of_forward line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_scaled_intrinsic_hessian_limit line 99
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_scaled_hessian_limit line 162