OAI/Probability/BinarySweep/TensorBounds/SignedConjugation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_mul line 18
2. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_one line 24
3. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_inv line 29
4. def OAI.BinaryCoordinateSweeps.Signed.signedConj line 36
5. lemma OAI.BinaryCoordinateSweeps.Signed.signedConj_mul line 40
6. lemma OAI.BinaryCoordinateSweeps.Signed.signedConj_psd line 47
7. lemma OAI.BinaryCoordinateSweeps.Signed.signedConj_fixed line 51
8. lemma OAI.BinaryCoordinateSweeps.Signed.signedConj_commutes line 57
9. lemma OAI.BinaryCoordinateSweeps.Signed.signedConj_sub_smul_sum line 63
10. def OAI.BinaryCoordinateSweeps.Density.matrixSlice line 79
11. lemma OAI.BinaryCoordinateSweeps.Density.matrixSlice_mul_left line 83
12. lemma OAI.BinaryCoordinateSweeps.Density.matrixSlice_mul_right line 90
13. theorem OAI.BinaryCoordinateSweeps.Density.kronecker_centrality line 97