OAI/Analysis/MatrixSigning/Optimization/RationalAtoms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalSDP.rationalAtoms line 18
2. lemma OAI.CurrentKS.RationalSDP.complexSum_rationalAtoms line 21
3. lemma OAI.CurrentKS.RationalSDP.complexEta_rationalAtoms line 27
4. lemma OAI.CurrentKS.RationalSDP.valuePencil_feasible line 35
5. lemma OAI.CurrentKS.RationalSDP.valuePencil_ball line 45
6. lemma OAI.CurrentKS.RationalSDP.valueOuterRadius_le line 64
7. lemma OAI.CurrentKS.RationalSDP.valueLipschitz_le line 70
8. def OAI.CurrentKS.RationalSDP.valueQueryPoint line 77
9. def OAI.CurrentKS.RationalSDP.valueQuery line 86
10. lemma OAI.CurrentKS.RationalSDP.valueQueryPoint_correct line 89