OAI/Probability/SignedSweeps/IsotypicDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.orthogonalSubrepresentation line 14
2. lemma OAI.SignedSweeps.specht_isotypic_orthogonal line 24
3. theorem OAI.SignedSweeps.specht_isotypic_iSup_eq_top line 48
4. lemma OAI.SignedSweeps.specht_isotypic_projection_on line 84
5. theorem OAI.SignedSweeps.specht_isotypic_projection_sum line 98
6. lemma OAI.SignedSweeps.wordTypeProjection_sum line 128
7. lemma OAI.SignedSweeps.wordTypeProjection_orthogonal line 132
8. lemma OAI.SignedSweeps.word_first_column_collision line 141
9. lemma OAI.SignedSweeps.word_intertwiner_zero_of_height line 160
10. lemma OAI.SignedSweeps.wordTypeProjection_zero_of_height line 170
11. lemma OAI.SignedSweeps.word_isotypic_finrank_le line 183