OAI/Probability/BinarySweep/Representations/IsotypicDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.coeff_actHilbert line 18
2. lemma OAI.BinaryCoordinateSweeps.Signed.coeff_symm_act line 22
3. def OAI.BinaryCoordinateSweeps.Signed.projectionIntertwiner line 25
4. lemma OAI.BinaryCoordinateSweeps.Signed.projectionMatrix_invariant line 39
5. def OAI.BinaryCoordinateSweeps.Signed.isotypicProjection line 51
6. lemma OAI.BinaryCoordinateSweeps.Signed.isotypicProjection_psd line 56
7. lemma OAI.BinaryCoordinateSweeps.Signed.isotypicProjection_invariant line 60
8. lemma OAI.BinaryCoordinateSweeps.Signed.isotypicProjection_trace line 66
9. lemma OAI.BinaryCoordinateSweeps.Signed.isotypicSpan_rank_bound line 72
10. theorem OAI.BinaryCoordinateSweeps.Signed.isotypic_density_domination line 79