OAI/Analysis/MatrixSigning/Potential/Lagrangian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.convex_domain line 16
2. lemma OAI.CurrentKS.Variational.convex_objective line 20
3. lemma OAI.CurrentKS.Variational.residual_coneConvex line 28
4. lemma OAI.CurrentKS.Variational.unit_le_slack line 43
5. lemma OAI.CurrentKS.Variational.invH_one line 49
6. lemma OAI.CurrentKS.Variational.exists_strict_feasible line 53
7. def OAI.CurrentKS.Variational.lagrangian line 89
8. theorem OAI.CurrentKS.Variational.exists_matrix_multipliers line 92