OAI/Analysis/MatrixSigning/Matrices/InnerMonoRightPsd.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Hermitian.inner_mono_right_psd line 17
2. lemma OAI.CurrentKS.Hermitian.inner_le_trace_mul_trace line 23
3. lemma OAI.CurrentKS.Hermitian.sandwich_inverse_left line 29
4. lemma OAI.CurrentKS.Hermitian.sandwich_inverse_right line 37
5. lemma OAI.CurrentKS.Hermitian.exists_psd_square line 48
6. lemma OAI.CurrentKS.Hermitian.inner_sandwich_square line 55
7. lemma OAI.CurrentKS.Hermitian.sandwich_inner_nonneg line 65
8. lemma OAI.CurrentKS.Hermitian.inner_sandwich_le line 75