OAI/Analysis/MatrixSigning/Optimization/ComplexValueProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.RationalSDP.scalar_one_psd_iff line 14
2. lemma OAI.CurrentKS.RationalSDP.lowerMatrixPencil_psd line 22
3. lemma OAI.CurrentKS.RationalSDP.upperMatrixPencil_psd line 29
4. def OAI.CurrentKS.RationalSDP.complexValueProgram line 37
5. lemma OAI.CurrentKS.RationalSDP.valuePencil_psd line 47
6. lemma OAI.CurrentKS.RationalSDP.trace_decode line 63
7. lemma OAI.CurrentKS.RationalSDP.valueObjective_complex line 67