OAI/Probability/BinarySweep/Representations/IsotypicSpectral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Irrep.commuting_eigenspace_map line 22
2. def OAI.BinaryCoordinateSweeps.Irrep.eigenspaceProjectionIntertwiner line 35
3. lemma OAI.BinaryCoordinateSweeps.Irrep.eigenvalue_multiplicity_ge line 49
4. theorem OAI.BinaryCoordinateSweeps.Irrep.isotypic_eigenvalue_trace_le line 77
5. def OAI.BinaryCoordinateSweeps.Irrep.commutingIntertwiner line 112
6. lemma OAI.BinaryCoordinateSweeps.Irrep.commuting_isotypic_invariant line 118
7. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypic_restrict_positive line 133
8. theorem OAI.BinaryCoordinateSweeps.Irrep.isotypic_restriction_cap line 139