OAI/Analysis/MatrixSigning/Potential/JetBoundProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.jetBound_projection line 37
2. lemma OAI.CurrentKS.Variational.norm_tracePair_le line 45
3. lemma OAI.CurrentKS.Variational.jetBound_pairHilbert line 53
4. lemma OAI.CurrentKS.Variational.jetBound_tracePart line 60
5. lemma OAI.CurrentKS.Variational.kktJet_numeric line 72
6. lemma OAI.CurrentKS.Variational.jetBound_kktPrimal line 81
7. lemma OAI.CurrentKS.Variational.jetBound_kktDual line 112
8. lemma OAI.CurrentKS.Variational.jetBound_kktGiven line 143