OAI/Analysis/MatrixSigning/Optimization/RealVector.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalSDP.realVector line 15
2. def OAI.CurrentKS.RationalSDP.l1 line 18
3. def OAI.CurrentKS.RationalSDP.roundScalar line 20
4. def OAI.CurrentKS.RationalSDP.roundVector line 22
5. lemma OAI.CurrentKS.RationalSDP.norm_le_sum_abs line 24
6. lemma OAI.CurrentKS.RationalSDP.l1_bounds line 30
7. lemma OAI.CurrentKS.RationalSDP.l1_pos line 42
8. lemma OAI.CurrentKS.RationalSDP.roundScalar_error line 53
9. lemma OAI.CurrentKS.RationalSDP.realVector_round_error line 68
10. def OAI.CurrentKS.RationalSDP.normalized line 83
11. lemma OAI.CurrentKS.RationalSDP.normalized_norm_le_one line 86
12. lemma OAI.CurrentKS.RationalSDP.normalized_margin line 93
13. def OAI.CurrentKS.RationalSDP.Pencil.next line 131
14. lemma OAI.CurrentKS.RationalSDP.realVector_step line 136