OAI/Probability/BinarySweep/TensorBounds/SignedBlock.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.sumPerm_inv line 16
2. lemma OAI.BinaryCoordinateSweeps.Signed.signC_sum line 27
3. def OAI.BinaryCoordinateSweeps.Signed.splitWord line 33
4. lemma OAI.BinaryCoordinateSweeps.Signed.splitWord_fst line 37
5. lemma OAI.BinaryCoordinateSweeps.Signed.splitWord_snd line 40
6. lemma OAI.BinaryCoordinateSweeps.Signed.splitWord_comp line 44
7. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_apply line 48
8. theorem OAI.BinaryCoordinateSweeps.Signed.actionMatrix_sum line 55
9. abbrev OAI.BinaryCoordinateSweeps.Signed.actionMatrix line 81
10. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_conjugate_apply line 83
11. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_unitary line 90
12. lemma OAI.BinaryCoordinateSweeps.Signed.actionMatrix_star_mul line 103
13. theorem OAI.BinaryCoordinateSweeps.Signed.even_tensor_covariance line 107