OAI/Analysis/MatrixSigning/Potential/PositiveMapMono.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.positiveMap_mono line 18
2. lemma OAI.CurrentKS.Variational.invH_order_bound line 24
3. lemma OAI.CurrentKS.Variational.value_center_neighborhood line 31
4. lemma OAI.CurrentKS.Variational.convex_feasible line 93
5. lemma OAI.CurrentKS.Variational.convex_orderBox_H line 106
6. lemma OAI.CurrentKS.Variational.convex_oracleBox line 119
7. lemma OAI.CurrentKS.Variational.convex_valueSpectrahedron line 125