OAI/Probability/BinarySweep/MatrixBounds/SchattenBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_mul_pow_comm line 12
2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_star line 20
3. def OAI.BinaryCoordinateSweeps.TraceHolder.schatten line 25
4. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_nonneg line 28
5. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_star line 31
6. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_pow line 34
7. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_zero line 38
8. lemma OAI.BinaryCoordinateSweeps.TraceHolder.prod_ofFn_sum line 42
9. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_holder_sums line 60
10. lemma OAI.BinaryCoordinateSweeps.TraceHolder.prod_alternating line 73
11. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_le_sum_pow line 90
12. theorem OAI.BinaryCoordinateSweeps.TraceHolder.schatten_sum_le line 114
13. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrix_one_norm_le line 122
14. theorem OAI.BinaryCoordinateSweeps.TraceHolder.trace_holder_contractions line 126
15. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_contraction_left line 163
16. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_contraction_left line 188
17. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_smul_real line 193
18. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_smul_nonneg line 200
19. theorem OAI.BinaryCoordinateSweeps.TraceHolder.schatten_mul_le_op_left line 206
20. theorem OAI.BinaryCoordinateSweeps.TraceHolder.schatten_mul_le_op_right line 222
21. lemma OAI.BinaryCoordinateSweeps.TraceHolder.op_norm_le_schatten line 227
22. theorem OAI.BinaryCoordinateSweeps.TraceHolder.schatten_triple_le line 254