OAI/Analysis/MatrixSigning/Optimization/SqSum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalRoot.sqSum line 13
2. def OAI.CurrentKS.RationalRoot.initialScale line 15
3. def OAI.CurrentKS.RationalRoot.normalize line 17
4. def OAI.CurrentKS.RationalRoot.realVector line 21
5. lemma OAI.CurrentKS.RationalRoot.sqSum_nonneg line 23
6. lemma OAI.CurrentKS.RationalRoot.sqSum_pos line 26
7. lemma OAI.CurrentKS.RationalRoot.sqSum_initialScale line 35
8. lemma OAI.CurrentKS.RationalRoot.initialScale_spec line 39
9. lemma OAI.CurrentKS.RationalRoot.norm_realVector line 48
10. lemma OAI.CurrentKS.RationalRoot.realVector_div line 53
11. theorem OAI.CurrentKS.RationalRoot.normalize_spec line 60