OAI/Analysis/MatrixSigning/Matrices/HermitianMat.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Hermitian.Mat line 12
2. def OAI.CurrentKS.Hermitian.hermitianSubmodule line 14
3. abbrev OAI.CurrentKS.Hermitian.H line 22
4. instance OAI.CurrentKS.Hermitian.(instance at line 26) line 26
5. instance OAI.CurrentKS.Hermitian.(instance at line 28) line 28
6. instance OAI.CurrentKS.Hermitian.(instance at line 30) line 30
7. theorem OAI.CurrentKS.Hermitian.matrix_hermitian line 32
8. def OAI.CurrentKS.Hermitian.one line 34
9. theorem OAI.CurrentKS.Hermitian.one_val line 36
10. def OAI.CurrentKS.Hermitian.realTrace line 38
11. def OAI.CurrentKS.Hermitian.psdCone line 40
12. theorem OAI.CurrentKS.Hermitian.mem_psdCone line 47
13. theorem OAI.CurrentKS.Hermitian.zero_mem_psdCone line 49
14. theorem OAI.CurrentKS.Hermitian.one_mem_psdCone line 51
15. theorem OAI.CurrentKS.Hermitian.trace_mul_nonneg line 56
16. theorem OAI.CurrentKS.Hermitian.posDef_mem_interior line 65
17. def OAI.CurrentKS.Hermitian.asL2 line 102
18. instance OAI.CurrentKS.Hermitian.matrixInnerProduct line 105
19. instance OAI.CurrentKS.Hermitian.matrixRealInnerProduct line 116
20. lemma OAI.CurrentKS.Hermitian.inner_smul_leftH line 119
21. lemma OAI.CurrentKS.Hermitian.inner_smul_rightH line 123
22. theorem OAI.CurrentKS.Hermitian.matrix_inner line 127
23. theorem OAI.CurrentKS.Hermitian.inner_eq_trace line 134
24. theorem OAI.CurrentKS.Hermitian.inner_one line 139
25. theorem OAI.CurrentKS.Hermitian.inner_one' line 143
26. theorem OAI.CurrentKS.Hermitian.inner_nonneg_of_psd line 147
27. def OAI.CurrentKS.Hermitian.rankOne line 152
28. theorem OAI.CurrentKS.Hermitian.rankOne_mem_psdCone line 155
29. theorem OAI.CurrentKS.Hermitian.inner_rankOne line 158
30. theorem OAI.CurrentKS.Hermitian.psd_of_inner_nonneg line 164
31. theorem OAI.CurrentKS.Hermitian.positive_dual_matrix line 173
32. theorem OAI.CurrentKS.Hermitian.isClosed_psdCone line 190