OAI/RepresentationTheory/FiniteUnitary/Coefficients.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.UnitaryFinite.IsUnitary line 12

   Distinct definitions of this name: ComparatorChallenges/OccupiedOverlap.lean:169 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.UnitaryFinite.IsUnitary@path.

2. lemma OAI.CubeShuffle.UnitaryFinite.unitary_inner_inv line 16
3. def OAI.CubeShuffle.UnitaryFinite.averageMap line 26
4. lemma OAI.CubeShuffle.UnitaryFinite.averageMap_self_trace line 42
5. lemma OAI.CubeShuffle.UnitaryFinite.averageMap_scalar line 51
6. theorem OAI.CubeShuffle.UnitaryFinite.coefficient_orthogonality line 64

   Source documentation

   Schur orthogonality in an actual unitary irreducible, obtained by averaging a rank-one operator and applying the proved algebraic Schur lemma.

   theorem coefficient_orthogonality (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
       (hρ : IsUnitary ρ) (u v w z : V) :
       (Module.finrank ℂ V:ℂ) * ∑ g, inner ℂ u (ρ g v) * inner ℂ (ρ g w) z =
         (Fintype.card G:ℂ) * inner ℂ w v * inner ℂ u z := by
   …

7. def OAI.CubeShuffle.UnitaryFinite.representative line 90
8. lemma OAI.CubeShuffle.UnitaryFinite.representative_apply line 93
9. lemma OAI.CubeShuffle.UnitaryFinite.orbit_sum line 97
10. def OAI.CubeShuffle.UnitaryFinite.IsFixed line 117
11. def OAI.CubeShuffle.UnitaryFinite.coefficient line 119
12. lemma OAI.CubeShuffle.UnitaryFinite.coefficient_at line 123
13. lemma OAI.CubeShuffle.UnitaryFinite.coefficient_inner line 138
14. lemma OAI.CubeShuffle.UnitaryFinite.coefficient_action line 165
15. def OAI.CubeShuffle.UnitaryFinite.normalizedCoefficient line 173
16. lemma OAI.CubeShuffle.UnitaryFinite.normalizedCoefficient_inner line 176
17. lemma OAI.CubeShuffle.UnitaryFinite.normalizedCoefficient_orthonormal line 193
18. lemma OAI.CubeShuffle.UnitaryFinite.normalizedCoefficient_norm line 203