OAI/Analysis/MatrixSigning/Matrices/Sandwich.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Hermitian.isOpen_pd line 19
2. def OAI.CurrentKS.Hermitian.sandwich line 32
3. lemma OAI.CurrentKS.Hermitian.sandwich_val line 38
4. lemma OAI.CurrentKS.Hermitian.sandwich_psd line 41
5. def OAI.CurrentKS.Hermitian.matrixTraceCLM line 46
6. lemma OAI.CurrentKS.Hermitian.matrixTraceCLM_apply line 49
7. lemma OAI.CurrentKS.Hermitian.hasDerivAt_matrix_inverse line 51
8. lemma OAI.CurrentKS.Hermitian.inner_sandwich line 81
9. lemma OAI.CurrentKS.Hermitian.hasDerivAt_trace_inverse line 89