OAI/Probability/BinarySweep/Representations/MultiplicityBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Irrep.intertwiner_retraction line 20
  2. theorem OAI.BinaryCoordinateSweeps.Irrep.multiplicity_le_commutant line 29
  3. def OAI.BinaryCoordinateSweeps.Irrep.isotypicSpan line 53
  4. def OAI.BinaryCoordinateSweeps.Irrep.evaluation line 56
  5. lemma OAI.BinaryCoordinateSweeps.Irrep.evaluation_range line 66
  6. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypicSpan_finrank line 79
  7. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypicSpan_stable line 85
  8. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypicSpan_map line 100
  9. def OAI.BinaryCoordinateSweeps.Irrep.schurScalar line 122
  10. lemma OAI.BinaryCoordinateSweeps.Irrep.schurScalar_smul line 127
  11. lemma OAI.BinaryCoordinateSweeps.Irrep.schurScalar_one line 133
  12. def OAI.BinaryCoordinateSweeps.Irrep.intertwinerPairing line 139
  13. lemma OAI.BinaryCoordinateSweeps.Irrep.intertwinerPairing_injective line 144
  14. lemma OAI.BinaryCoordinateSweeps.Irrep.exists_intertwiner_dual line 159
  15. theorem OAI.BinaryCoordinateSweeps.Irrep.evaluation_injective line 171
  16. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypicSpan_finrank_eq line 194