OAI/Geometry/WeakHessian/LocalBounds/SubConst.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.RelaxedProx.sub_constline 45 - lemma
OAI.WeakHessian.centeredLp_massline 60 - lemma
OAI.WeakHessian.centeredLp_boundline 70 - lemma
OAI.WeakHessian.CurvatureDimension.prox_weak_pairingline 77 - lemma
OAI.WeakHessian.CurvatureDimension.prox_gradient_norm_leline 88