OAI/Geometry/WeakHessian/LocalBounds/PotentialPairing.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.norm_gradient_le_supported_lipschitzline 23 - lemma
OAI.WeakHessian.integral_gamma_localizationline 39 - lemma
OAI.WeakHessian.CurvatureDimension.potential_pairing_tendstoline 53