OAI/Probability/BinarySweep/YoungTheory/YoungResolution.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinaryCoordinateSweeps.Young.PartitionHilbert line 17
2. def OAI.BinaryCoordinateSweeps.Young.partitionHilbertRep line 19
3. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 23) line 23
4. def OAI.BinaryCoordinateSweeps.Young.partitionHilbertEquiv line 26
5. lemma OAI.BinaryCoordinateSweeps.Young.partitionHilbertRep_unitary line 37
6. lemma OAI.BinaryCoordinateSweeps.Young.partitionHilbertRep_equiv_injective line 41
7. lemma OAI.BinaryCoordinateSweeps.Young.partitionHilbertRep_complete line 46
8. lemma OAI.BinaryCoordinateSweeps.Young.partition_isotypic_top line 52
9. lemma OAI.BinaryCoordinateSweeps.Young.partition_isotypic_orthogonal line 60
10. theorem OAI.BinaryCoordinateSweeps.Young.partition_projection_sum line 73
11. def OAI.BinaryCoordinateSweeps.Signed.pairWeight line 91
12. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_eq_prod line 95
13. def OAI.BinaryCoordinateSweeps.Signed.sumPerm line 107
14. lemma OAI.BinaryCoordinateSweeps.Signed.sumPerm_left line 110
15. lemma OAI.BinaryCoordinateSweeps.Signed.sumPerm_right line 115
16. theorem OAI.BinaryCoordinateSweeps.Signed.koszulSign_sum line 120