OAI/Probability/SKGap/Matrix/OpNormDiagonal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.opNorm_diagonal_eq line 59
2. lemma OAI.SKGap.opNorm_diagonal_le line 62
3. lemma OAI.SKGap.opNorm_one_le line 67
4. lemma OAI.SKGap.opNorm_sub line 72
5. lemma OAI.SKGap.real_sandwich_opNorm line 77
6. lemma OAI.SKGap.real_sandwich_stability_norm line 88