Schur orthogonality for irreducible compact-group representations

This file proves the first Schur orthogonality relation for matrix coefficients of a finite-dimensional irreducible unitary representation of a compact group. Haar-averaging a rank-one operator produces a self-intertwiner. Schur's lemma makes that intertwiner scalar, and preservation of the trace determines the scalar to be the reciprocal of the dimension.

The coordinate-free result is accompanied by its orthonormal-basis form. The latter fixes both the order of the Kronecker deltas and the placement of complex conjugation in Mathlib's convention that the inner product is conjugate-linear in its first argument.

The second relation, for a pair of representations, is proved in TauCeti/RepresentationTheory/Compact/Intertwiner/Basic.lean from the vanishing of the intertwiners between them; the last section here packages it with the hypothesis Schur's lemma actually discharges, namely that the two irreducibles are inequivalent.

Main statements

• ContRepresentation.averageOperator_eq_finrank_inv_mul_trace_smul_id: the average of a self-map is its normalized trace times the identity.
• ContRepresentation.schur_orthogonality_self: the coordinate-free first Schur orthogonality relation.
• ContRepresentation.schur_orthogonality_basis: the corresponding Kronecker-delta formula in an orthonormal basis.
• ContRepresentation.schur_orthogonality: the second Schur orthogonality relation, for a pair of inequivalent irreducible unitary representations.

The basis identity follows from the coordinate-free statement, in the same inner-product convention. The mathematical argument follows Daniel Bump, Lie Groups, second edition, Chapter 2.

theorem ContRepresentation.instCompleteSpaceSchurAverage {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

The scalar selected by Haar averaging

theorem ContRepresentation.averageOperator_eq_finrank_inv_mul_trace_smul_id {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) (T : V →L[𝕜] V) : π.averageOperator hπ π hπ T = ((↑(Module.finrank 𝕜 V))⁻¹ * (LinearMap.trace 𝕜 V) ↑T) • ContinuousLinearMap.id 𝕜 V

On an irreducible finite-dimensional representation, the Haar average of a self-map is its normalized trace times the identity.

theorem ContRepresentation.instCompleteSpaceSchurOrthogonality {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

The first Schur orthogonality relation

theorem ContRepresentation.schur_orthogonality_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) (v₁ w₁ v₂ w₂ : V) : inner 𝕜 (π.matrixCoeffLp hπ v₁ w₁) (π.matrixCoeffLp hπ v₂ w₂) = (↑(Module.finrank 𝕜 V))⁻¹ * ((starRingEnd 𝕜) (inner 𝕜 v₁ v₂) * inner 𝕜 w₁ w₂)

Schur orthogonality for one irreducible representation, in coordinate-free form.

For a unitary irreducible representation of dimension d, the L² inner product of the matrix coefficients determined by (v₁, w₁) and (v₂, w₂) is d⁻¹ * conj ⟪v₁, v₂⟫ * ⟪w₁, w₂⟫. The conjugation on the first vector factor is forced by Mathlib's inner-product convention.

theorem ContRepresentation.schur_orthogonality_basis {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) {d : ℕ} (e : OrthonormalBasis (Fin d) 𝕜 V) (i j k l : Fin d) : inner 𝕜 (π.matrixCoeffLp hπ (e j) (e i)) (π.matrixCoeffLp hπ (e l) (e k)) = (↑d)⁻¹ * ((if j = l then 1 else 0) * if i = k then 1 else 0)

Schur orthogonality in an orthonormal basis. If πᵢⱼ(g) = ⟪π(g)eⱼ, eᵢ⟫, then ⟪πᵢⱼ, πₖₗ⟫_{L²} = d⁻¹ δⱼₗ δᵢₖ.

This is the convention check for schur_orthogonality_self: Kronecker deltas are real, so the coordinate-free conjugation becomes invisible here, while the order of all four indices remains explicit.

theorem ContRepresentation.schur_orthogonality {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : ρ.IsUnitary) (hirrπ : (toRepresentation 𝕜 G V π).IsIrreducible) (hirrρ : (toRepresentation 𝕜 G W ρ).IsIrreducible) (hne : IsEmpty (π.Equiv ρ)) (v w : V) (v' w' : W) : inner 𝕜 (π.matrixCoeffLp hπ v w) (ρ.matrixCoeffLp hρ v' w') = 0

The second Schur orthogonality relation. Matrix coefficients of inequivalent finite-dimensional irreducible representations of a compact group are L²-orthogonal, provided the second one is unitary.

This is ContRepresentation.schur_orthogonality_distinct with its hypothesis discharged: the vanishing half of Schur's lemma turns inequivalence into the vanishing of every continuous intertwiner π → ρ. Algebraic closedness is not needed, since only the vanishing half of Schur's lemma is used.