OAI/Probability/SKGap/Matrix/OpNormKernelMatrixSub.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.ComplexMatrix.opNorm_kernelMatrix_sub line 36
2. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_opNorm_lipschitz line 64
3. lemma OAI.SKGap.ComplexMatrix.opNorm_nonneg line 79
4. lemma OAI.SKGap.ComplexMatrix.opNorm_add line 80
5. lemma OAI.SKGap.ComplexMatrix.opNorm_sub line 84
6. lemma OAI.SKGap.ComplexMatrix.opNorm_mul line 89
7. lemma OAI.SKGap.ComplexMatrix.opNorm_neg line 93
8. lemma OAI.SKGap.ComplexMatrix.opNorm_one_le line 98
9. lemma OAI.SKGap.ComplexMatrix.sandwich_frobenius line 102
10. lemma OAI.SKGap.ComplexMatrix.sandwich_opNorm line 109
11. lemma OAI.SKGap.ComplexMatrix.sandwich_difference_frobenius line 116
12. lemma OAI.SKGap.ComplexMatrix.sandwich_difference_opNorm line 130
13. lemma OAI.SKGap.ComplexMatrix.product_four_point line 144