OAI/Probability/BinarySweep/MatrixBounds/SchattenTriangle.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_sum_le line 12
2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_mul_left line 37
3. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_mul_right line 44
4. lemma OAI.BinaryCoordinateSweeps.TraceHolder.norm_le_schatten line 49
5. lemma OAI.BinaryCoordinateSweeps.TraceHolder.schatten_sandwich line 68