The orthonormal systems cut out by Schur orthogonality

Fix a family π i of pairwise inequivalent finite-dimensional irreducible unitary representations of a compact group G, one for each index i. This file assembles the two orthogonality relations of TauCeti/RepresentationTheory/Compact/SchurOrthogonality.lean and TauCeti/RepresentationTheory/Compact/Character/Basic.lean into Orthonormal families in L²(G):

• the normalized matrix coefficients √(dim V_i) • (π i)_{ab}, indexed by Σ i, Fin (dim V_i) × Fin (dim V_i);
• the characters χ_(π i), indexed by i.

The family is arbitrary apart from being pairwise inequivalent, so the first is a subsystem of the system that the Peter-Weyl theorem proves complete: it is the whole of it only when the family runs over one representative of every irreducible equivalence class. The second lies in the central subspace of L²(G).

Main statements

• TauCeti.ContRepresentation.orthonormal_matrixCoeffLp: the normalized matrix coefficients of a family of pairwise inequivalent irreducible unitary representations form an orthonormal system in L²(G).
• ContRepresentation.orthonormal_characterLp: the characters of such a family form an orthonormal system in L²(G).

Implementation notes

Inequivalence is the hypothesis Pairwise fun i j ↦ IsEmpty (ContRepresentation.Equiv (π i) (π j)). Nothing here selects the family: "one representative per equivalence class" is chosen data, supplied by the caller as π together with the orthonormal bases e, exactly as the Peter-Weyl basis uses it.

Both systems live in the same L²(G), so the index of the matrix-coefficient system is a sigma type over the family rather than a product: different i contribute different numbers of coefficients.

The normalizing scalar is √(n i), where n i is the cardinality of the index type of the chosen basis of V i and so equals Module.finrank 𝕜 (V i) by Module.finrank_eq_card_basis. Taking the basis index as data rather than reading it off Module.finrank is what lets the caller keep whatever indexing the representation came with.

The completeness of the first system is proved in TauCeti/RepresentationTheory/Compact/PeterWeyl.lean for a family that also exhausts the irreducibles; the completeness of the second (class-function completeness) is proved in TauCeti/RepresentationTheory/Compact/Character/Basis.lean. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

theorem TauCeti.ContRepresentation.instCompleteSpaceOrthonormalSystem {𝕜 : Type u_1} {ι : Type u_3} {V : ι → Type u_4} [RCLike 𝕜] [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → InnerProductSpace 𝕜 (V i)] [∀ (i : ι), FiniteDimensional 𝕜 (V i)] (i : ι) : CompleteSpace (V i)

theorem TauCeti.ContRepresentation.orthonormal_matrixCoeffLp {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} {V : ι → Type u_4} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → InnerProductSpace 𝕜 (V i)] [(i : ι) → NormedSpace ℝ (V i)] [∀ (i : ι), SMulCommClass ℝ 𝕜 (V i)] [∀ (i : ι), FiniteDimensional 𝕜 (V i)] (π : (i : ι) → ContRepresentation 𝕜 G (V i)) (hπ : ∀ (i : ι), Continuous ⇑(π i)) {n : ι → ℕ} (hunitary : ∀ (i : ι), (π i).IsUnitary) (hirr : ∀ (i : ι), (ContRepresentation.toRepresentation 𝕜 G (V i) (π i)).IsIrreducible) (hne : Pairwise fun (i j : ι) => IsEmpty ((π i).Equiv (π j))) (e : (i : ι) → OrthonormalBasis (Fin (n i)) 𝕜 (V i)) : Orthonormal 𝕜 fun (x : (i : ι) × Fin (n i) × Fin (n i)) => ↑√↑(n x.fst) • (π x.fst).matrixCoeffLp ⋯ ((e x.fst) x.snd.1) ((e x.fst) x.snd.2)

The normalized matrix coefficients are orthonormal. For a family π of pairwise inequivalent finite-dimensional irreducible unitary representations of a compact group, with a chosen orthonormal basis e i of each carrier, the functions √(dim V_i) • ⟪(π i) · (e i a), e i b⟫ form an orthonormal system in L²(G) indexed by Σ i, Fin (n i) × Fin (n i).

Within a single i this is the first Schur orthogonality relation, whose value (n i)⁻¹ on the diagonal is exactly what the normalization √(n i) cancels; across distinct i it is the second relation, whose hypothesis Schur's lemma supplies from inequivalence.

The family is not asked to be exhaustive, so this is in general a subsystem of the system that the Peter-Weyl theorem completes to a Hilbert basis of L²(G); it is that whole system exactly when π contains a representative of every irreducible equivalence class.

theorem ContRepresentation.orthonormal_characterLp {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} {V : ι → Type u_4} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → InnerProductSpace 𝕜 (V i)] [(i : ι) → NormedSpace ℝ (V i)] [∀ (i : ι), SMulCommClass ℝ 𝕜 (V i)] [∀ (i : ι), FiniteDimensional 𝕜 (V i)] (π : (i : ι) → ContRepresentation 𝕜 G (V i)) (hπ : ∀ (i : ι), Continuous ⇑(π i)) (hunitary : ∀ (i : ι), (π i).IsUnitary) (hirr : ∀ (i : ι), (toRepresentation 𝕜 G (V i) (π i)).IsIrreducible) (hne : Pairwise fun (i j : ι) => IsEmpty ((π i).Equiv (π j))) : Orthonormal 𝕜 fun (i : ι) => (π i).characterLp ⋯

The irreducible characters are orthonormal. The characters of a family of pairwise inequivalent finite-dimensional irreducible unitary representations of a compact group form an orthonormal system in L²(G).

This is the system form of the two character orthogonality relations: normalization is the first, and orthogonality across the family is the second, whose intertwiner hypothesis Schur's lemma supplies from inequivalence. For a finite group it is the statement that the irreducible characters are an orthonormal set of class functions.