OAI/Probability/SignedSweeps/PiTensorMatrix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.piTensorMatrix line 11
2. lemma OAI.SignedSweeps.piTensorMatrix_mul line 14
3. lemma OAI.SignedSweeps.piTensorMatrix_one line 21
4. lemma OAI.SignedSweeps.piTensorMatrix_star line 31
5. lemma OAI.SignedSweeps.piTensorMatrix_idempotent line 36
6. lemma OAI.SignedSweeps.piTensorMatrix_commute line 41
7. lemma OAI.SignedSweeps.piTensorMatrix_scale line 48
8. lemma OAI.SignedSweeps.piTensorMatrix_trace line 53
9. lemma OAI.SignedSweeps.kernel_product_positive line 59
10. lemma OAI.SignedSweeps.piTensorMatrix_positive line 80
11. lemma OAI.SignedSweeps.kernel_product_lower line 87
12. lemma OAI.SignedSweeps.piTensorMatrix_lower line 117