OAI/Probability/BinarySweep/YoungTheory/HookInducedMoment.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinaryCoordinateSweeps.Young.HookPlacements line 18
2. abbrev OAI.BinaryCoordinateSweeps.Young.HookHilbertInducedSpace line 19
3. def OAI.BinaryCoordinateSweeps.Young.hookHilbertInduced line 21
4. def OAI.BinaryCoordinateSweeps.Young.hookHilbertFiberEquiv line 26
5. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbertInduced_inner line 32
6. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbertInduced_unitary line 36
7. lemma OAI.BinaryCoordinateSweeps.Young.hook_hilbert_multiplicity line 40
8. theorem OAI.BinaryCoordinateSweeps.Young.hook_induced_moment_le line 57
9. def OAI.BinaryCoordinateSweeps.Irrep.fiberInclude line 82
10. def OAI.BinaryCoordinateSweeps.Irrep.fiberProject line 85
11. def OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock line 88
12. lemma OAI.BinaryCoordinateSweeps.Irrep.fiberInclude_apply line 93
13. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_coind line 97
14. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_average line 109