OAI/Geometry/RCD/Transport/ScaledPlanHessianLimit.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Scaled canonical Hessians paired against normalized compressed laws
- theorem
OAI.RegularPointCoordinates.scaled_plan_hessian_limitline 13