OAI/Probability/SKGap/Matrix/OpNorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.mul_symmetricElementary_mul line 19
2. lemma OAI.SKGap.goe_inverse_contraction line 24
3. def OAI.SKGap.opNorm line 31
4. def OAI.SKGap.colVec line 32
5. lemma OAI.SKGap.colVec_eq line 34
6. lemma OAI.SKGap.colVec_norm_le line 39
7. lemma OAI.SKGap.matrix_entry_le_opNorm line 44
8. lemma OAI.SKGap.opNorm_mul line 49
9. lemma OAI.SKGap.goe_cross_contraction_bound line 57
10. lemma OAI.SKGap.trace_mul_diagonal line 68
11. theorem OAI.SKGap.goe_inverse_loop_raw line 72