OAI/Combinatorics/MatchingPSD/PSDDuality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffinePSD.evaluationCone_convex line 13
2. lemma OAI.AffinePSD.evaluationCone_zero line 17
3. lemma OAI.AffinePSD.evaluationCone_smul line 21
4. lemma OAI.AffinePSD.trace_evaluation_duality line 27
5. lemma OAI.AffinePSD.psd_of_trace_nonneg line 33
6. lemma OAI.AffinePSD.exists_psd_evaluation line 44