OAI/Probability/SignedSweeps/MarkedSector.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.wordTypeProjection_intertwiner line 11
2. lemma OAI.SignedSweeps.pairTypeProjection_embedding line 17
3. lemma OAI.SignedSweeps.pairTypeProjection_fixes_specht_pair line 36
4. lemma OAI.SignedSweeps.markedTypeProjection_insertion line 51
5. def OAI.SignedSweeps.markedPairSpechtMap line 62
6. lemma OAI.SignedSweeps.markedPairSpechtMap_fixed line 72
7. lemma OAI.SignedSweeps.markedPairSpechtMap_intertwines line 92
8. lemma OAI.SignedSweeps.markedPairSpechtMap_nonzero line 109
9. def OAI.SignedSweeps.MarkedSectorSpace line 128
10. instance OAI.SignedSweeps.(instance at line 132) line 132
11. instance OAI.SignedSweeps.(instance at line 137) line 137
12. instance OAI.SignedSweeps.(instance at line 142) line 142
13. def OAI.SignedSweeps.markedSectorRepresentation line 147
14. def OAI.SignedSweeps.markedSectorIntertwiner line 152
15. lemma OAI.SignedSweeps.markedSectorIntertwiner_nonzero line 169
16. lemma OAI.SignedSweeps.markedSectorIntertwiner_off line 183
17. lemma OAI.SignedSweeps.markedTypeSubrepresentation_norm line 196
18. lemma OAI.SignedSweeps.marked_sector_isometric_fiber_from_maps line 202
19. theorem OAI.SignedSweeps.marked_sector_isometric_fiber line 228