OAI/Probability/BinarySweep/Representations/MatrixIsotypicWhitening.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinaryCoordinateSweeps.Irrep.matrix_whitening_positive line 23
2. lemma OAI.BinaryCoordinateSweeps.Irrep.map_isotypic_le line 65
3. lemma OAI.BinaryCoordinateSweeps.Irrep.map_isotypic_equiv line 76
4. theorem OAI.BinaryCoordinateSweeps.Irrep.isotypicProjection_commutes line 98
5. def OAI.BinaryCoordinateSweeps.Irrep.algebraSubmoduleInclusion line 127
6. lemma OAI.BinaryCoordinateSweeps.Irrep.algebraSubmoduleInclusion_injective line 146
7. theorem OAI.BinaryCoordinateSweeps.Irrep.iSup_isotypic_eq_top line 160