OAI/Analysis/MatrixSigning/Potential/Pack.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CurrentKS.Variational.packline 17 - def
OAI.CurrentKS.Variational.unpackline 20 - lemma
OAI.CurrentKS.Variational.identityPair_ne_zeroline 22 - lemma
OAI.CurrentKS.Variational.hessian_strict_posline 28 - theorem
OAI.CurrentKS.Variational.kkt_regularline 56 - lemma
OAI.CurrentKS.Variational.pack_kktline 80