OAI/Probability/BinarySweep/TensorBounds/SignedCommutant.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Signed.invariantSubspace line 18
2. abbrev OAI.BinaryCoordinateSweeps.Signed.RealizedType line 30
3. def OAI.BinaryCoordinateSweeps.Signed.typeRepresentative line 33
4. lemma OAI.BinaryCoordinateSweeps.Signed.typeRepresentative_type line 35
5. def OAI.BinaryCoordinateSweeps.Signed.invariantCode line 38
6. lemma OAI.BinaryCoordinateSweeps.Signed.invariantCode_injective line 44
7. lemma OAI.BinaryCoordinateSweeps.Signed.invariantSubspace_finrank line 67
8. lemma OAI.BinaryCoordinateSweeps.Signed.act_single_comp line 79
9. lemma OAI.BinaryCoordinateSweeps.Signed.intertwiner_matrix_invariant line 94
10. def OAI.BinaryCoordinateSweeps.Signed.commutantToInvariant line 108
11. lemma OAI.BinaryCoordinateSweeps.Signed.commutantToInvariant_injective line 115
12. theorem OAI.BinaryCoordinateSweeps.Signed.tensor_commutant_finrank line 122
13. abbrev OAI.BinaryCoordinateSweeps.Signed.TensorSpace line 138
14. def OAI.BinaryCoordinateSweeps.Signed.coeffEquiv line 140
15. def OAI.BinaryCoordinateSweeps.Signed.wordReorder line 143
16. def OAI.BinaryCoordinateSweeps.Signed.actHilbert line 149
17. lemma OAI.BinaryCoordinateSweeps.Signed.actHilbert_apply line 152
18. lemma OAI.BinaryCoordinateSweeps.Signed.actHilbert_inner line 155
19. def OAI.BinaryCoordinateSweeps.Signed.actionIsometry line 168
20. def OAI.BinaryCoordinateSweeps.Signed.hilbertSubspace line 171
21. lemma OAI.BinaryCoordinateSweeps.Signed.hilbertSubspace_finrank line 174
22. lemma OAI.BinaryCoordinateSweeps.Signed.hilbertSubspace_map line 179