OAI/Geometry/RCD/Heat/CompactLipschitzHeatHessian.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A canonical Hessian action limit for compact Lipschitz directions
- theorem
OAI.RegularPointCoordinates.NoncollapsedRCD.compact_lipschitz_hessian_limitline 18