OAI/Analysis/MatrixSigning/Potential/LagrangianObjective.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.lagrangian_le_objective line 17
2. lemma OAI.CurrentKS.Variational.lagrangian_eq_objective_of_tight line 28
3. theorem OAI.CurrentKS.Variational.minimizer_unique line 33
4. lemma OAI.CurrentKS.PositiveMap.cone_smul_nonneg line 76
5. lemma OAI.CurrentKS.PositiveMap.interior_absorbs line 82
6. theorem OAI.CurrentKS.PositiveMap.mem_of_supersolution line 98
7. theorem OAI.CurrentKS.PositiveMap.positive_inverse line 120
8. theorem OAI.CurrentKS.PositiveMap.positive_inverse_of_gap line 152