OAI/Probability/SKRatio/Matrices/OpNormNonneg.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_nonneg line 34
2. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_add line 35
3. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_sub line 39
4. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_mul line 44
5. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_neg line 48
6. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_one_le line 53
7. lemma OAI.SKRatioGaussian.ComplexMatrix.sandwich_frobenius line 57
8. lemma OAI.SKRatioGaussian.ComplexMatrix.sandwich_opNorm line 64
9. lemma OAI.SKRatioGaussian.ComplexMatrix.sandwich_difference_frobenius line 71
10. lemma OAI.SKRatioGaussian.ComplexMatrix.sandwich_difference_opNorm line 85
11. lemma OAI.SKRatioGaussian.ComplexMatrix.product_four_point line 99