OAI/Analysis/MatrixSigning/Optimization/BlockScalar.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalSDP.blockScalar line 14
2. lemma OAI.CurrentKS.RationalSDP.blockScalar_symm line 18
3. lemma OAI.CurrentKS.RationalSDP.blockScalar_posSemidef line 22
4. lemma OAI.CurrentKS.RationalSDP.blockScalar_realMap line 59
5. def OAI.CurrentKS.RationalSDP.Pencil.withLevel line 69
6. lemma OAI.CurrentKS.RationalSDP.Pencil.withLevel_realEval line 75
7. lemma OAI.CurrentKS.RationalSDP.Pencil.withLevel_feasible line 84