OAI/Probability/BinarySweep/YoungTheory/YoungHilbert.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.spechtHilbertInclude line 18
2. lemma OAI.BinaryCoordinateSweeps.Young.spechtHilbertInclude_injective line 21
3. abbrev OAI.BinaryCoordinateSweeps.Young.SpechtHilbert line 24
4. def OAI.BinaryCoordinateSweeps.Young.spechtHilbertEquiv line 26
5. def OAI.BinaryCoordinateSweeps.Young.hilbertSpecht line 29
6. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 33) line 33
7. lemma OAI.BinaryCoordinateSweeps.Young.spechtHilbertEquiv_coeff line 37
8. lemma OAI.BinaryCoordinateSweeps.Young.hilbertSpecht_coeff line 40
9. instance OAI.BinaryCoordinateSweeps.Young.hilbertNormed line 48
10. instance OAI.BinaryCoordinateSweeps.Young.hilbertInner line 50
11. lemma OAI.BinaryCoordinateSweeps.Young.hilbertSpecht_inner line 53
12. lemma OAI.BinaryCoordinateSweeps.Young.hilbertSpecht_unitary line 59
13. lemma OAI.BinaryCoordinateSweeps.Young.hilbertSpecht_finrank line 63
14. def OAI.BinaryCoordinateSweeps.Signed.koszulSign line 78
15. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_one line 82
16. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_inv line 89
17. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_mul line 99
18. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_sq line 113
19. lemma OAI.BinaryCoordinateSweeps.Signed.adjacent_swap_inversion line 127
20. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_swap_adjacent line 133
21. lemma OAI.BinaryCoordinateSweeps.Signed.mask_swap line 148
22. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_conjugate line 154
23. lemma OAI.BinaryCoordinateSweeps.Signed.exists_perm_pair line 164
24. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_swap line 177