OAI/Probability/SignedSweeps/Isotypic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.isotypicSubrepresentation line 12
  2. lemma OAI.SignedSweeps.intertwiner_mem_isotypic line 27
  3. lemma OAI.SignedSweeps.isotypic_end_stable line 32
  4. def OAI.SignedSweeps.isotypicEvaluation line 46
  5. lemma OAI.SignedSweeps.isotypicEvaluation_tmul line 56
  6. lemma OAI.SignedSweeps.isotypicEvaluation_range line 60
  7. lemma OAI.SignedSweeps.isotypic_finrank_le line 72
  8. def OAI.SignedSweeps.adjointIntertwiner line 92
  9. lemma OAI.SignedSweeps.adjointIntertwiner_linearMap line 103
  10. lemma OAI.SignedSweeps.submodule_projection_commute line 106
  11. lemma OAI.SignedSweeps.isotypic_projection_commute line 122
  12. theorem OAI.SignedSweeps.intertwiner_isometric_scaling line 132
  13. theorem OAI.SignedSweeps.intertwiner_isometric_normalization line 168
  14. lemma OAI.SignedSweeps.adjoint_isometric_intertwiner line 174
  15. lemma OAI.SignedSweeps.multiplicity_le_commutant line 184
  16. theorem OAI.SignedSweeps.central_scalar_on_isotypic line 206
  17. lemma OAI.SignedSweeps.isotypic_finrank_le_commutant line 235