OAI/Analysis/MatrixSigning/Optimization/Affine.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.RationalSDP.vector_eq_sum_single line 14
2. def OAI.CurrentKS.RationalSDP.Pencil.ofAffine line 20
3. lemma OAI.CurrentKS.RationalSDP.Pencil.ofAffine_eval line 28
4. def OAI.CurrentKS.RationalSDP.blockDiagonal line 37
5. lemma OAI.CurrentKS.RationalSDP.blockDiagonal_symm line 41
6. lemma OAI.CurrentKS.RationalSDP.blockDiagonal_posSemidef line 46
7. lemma OAI.CurrentKS.RationalSDP.blockDiagonal_realMap line 74
8. def OAI.CurrentKS.RationalSDP.Pencil.blockDiagonal line 84
9. lemma OAI.CurrentKS.RationalSDP.Pencil.blockDiagonal_realEval line 90