Averaging an operator into an intertwiner

Given continuous representations π on V and ρ on W of a compact group G, any continuous linear map T : V →L[𝕜] W can be averaged against normalized Haar measure into

averageOperator π hπ ρ hρ T = ∫ g, ρ g⁻¹ ∘ T ∘ π g ∂(haarProb G),

which is an intertwiner: averageOperator … ∘ π g = ρ g ∘ averageOperator …. This is the tool the Schur orthogonality relations run on, and it is the exact analogue for compact groups of the finite average |G|⁻¹ ∑ g, ρ g⁻¹ ∘ T ∘ π g behind Mathlib's Maschke theorem (LinearMap.sumOfConjugates), with the Haar integral in place of the finite sum.

The target W is not assumed complete. averageOperator is TauCeti.haarAverage of a continuous family valued in the operator space V →L[𝕜] W, so it inherits that average's convention: it is the displayed Haar integral when that space is complete, and the Bochner integral's junk value 0 otherwise. [CompleteSpace W] is what supplies completeness of V →L[𝕜] W, so the statements that read the average's actual value, from ContRepresentation.averageOperator_apply onwards, carry it.

The construction is a projection onto the intertwiners: it is linear in T, it fixes every intertwiner, and — when V = W and π = ρ and V is finite-dimensional — it preserves the trace. That last fact is what pins the constant d⁻¹ in the first Schur orthogonality relation.

Main definitions

• ContRepresentation.averageOperator: the Haar average ∫ g, ρ g⁻¹ ∘ T ∘ π g.
• ContRepresentation.averageOperatorₗ: the same, bundled as a linear map in T.
• ContRepresentation.averageIntertwiner: the average packaged as a term of Mathlib's ContIntertwiningMap π ρ.

Main statements

• ContRepresentation.averageOperator_comp: the average intertwines π with ρ.
• ContRepresentation.averageOperator_eq_self: the average fixes an operator that already intertwines, so averageOperator is idempotent (ContRepresentation.averageOperator_averageOperator).
• ContRepresentation.trace_averageOperator: averaging a self-map of a finite-dimensional representation preserves the trace.
• ContRepresentation.inner_matrixCoeffLp_eq_inner_averageOperator: the L² inner product of two matrix coefficients is a matrix entry of the average of a rank-one operator. This is the identity that turns Schur orthogonality into a statement about intertwiners.
• ContRepresentation.schur_orthogonality_distinct: the second Schur orthogonality relation. If there is no nonzero continuous intertwiner π → ρ, every matrix coefficient of π is L²-orthogonal to every matrix coefficient of ρ.

Schur's lemma itself is not used here: schur_orthogonality_distinct takes the vanishing of the intertwiner space as a hypothesis, which is precisely what Schur's lemma supplies for inequivalent irreducibles.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.averageOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] (T : V →L[𝕜] W) : V →L[𝕜] W

The Haar average of an operator over a pair of representations, ∫ g, ρ g⁻¹ ∘ T ∘ π g ∂(haarProb G).

On a complete W this is always defined — the integrand is continuous and Haar measure is finite — and it always intertwines π with ρ (ContRepresentation.averageOperator_comp). W is not assumed complete. The average is taken in the operator space V →L[𝕜] W, so it is TauCeti.haarAverage's junk value 0 unless that space is complete, which [CompleteSpace W] supplies; that is why the results below that read the average's actual value carry it.

Equations

• π.averageOperator hπ ρ hρ T = (TauCeti.haarAverage G) (ContRepresentation.conjFamily✝ π hπ ρ hρ T)

Linearity in the averaged operator

@[simp]

theorem ContRepresentation.averageOperator_zero {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] : π.averageOperator hπ ρ hρ 0 = 0

@[simp]

theorem ContRepresentation.averageOperator_add {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] (T₁ T₂ : V →L[𝕜] W) : π.averageOperator hπ ρ hρ (T₁ + T₂) = π.averageOperator hπ ρ hρ T₁ + π.averageOperator hπ ρ hρ T₂

@[simp]

theorem ContRepresentation.averageOperator_smul {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] (c : 𝕜) (T : V →L[𝕜] W) : π.averageOperator hπ ρ hρ (c • T) = c • π.averageOperator hπ ρ hρ T

noncomputable def ContRepresentation.averageOperatorₗ {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] : (V →L[𝕜] W) →ₗ[𝕜] V →L[𝕜] W

Haar averaging over a pair of representations, bundled as a linear map in the averaged operator. Bundling supplies the remaining additive identities (map_neg, map_sub, map_sum) through the LinearMap API.

Equations

• π.averageOperatorₗ hπ ρ hρ = { toFun := π.averageOperator hπ ρ hρ, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContRepresentation.averageOperatorₗ_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] (T : V →L[𝕜] W) : (π.averageOperatorₗ hπ ρ hρ) T = π.averageOperator hπ ρ hρ T

theorem ContRepresentation.averageOperator_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (v : V) : (π.averageOperator hπ ρ hρ T) v = ∫ (g : G), (ρ g⁻¹) (T ((π g) v)) ∂TauCeti.haarProb G

The average of an operator, evaluated at a vector.

The average is an intertwiner

The proof is the same shape as the invariance half of Weyl's unitarian trick: conjugation by a fixed pair of action operators is a continuous linear map on operators, so it commutes with Haar averaging, and on the integrand it acts as right translation of the group variable, which the Haar average does not see.

theorem ContRepresentation.averageOperator_comp {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (g : G) : π.averageOperator hπ ρ hρ T ∘SL π g = ρ g ∘SL π.averageOperator hπ ρ hρ T

The Haar average of an operator intertwines the two representations.

theorem ContRepresentation.averageOperator_isIntertwining {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (g : G) (v : V) : (π.averageOperator hπ ρ hρ T) ((π g) v) = (ρ g) ((π.averageOperator hπ ρ hρ T) v)

The intertwining identity, applied to a vector, in the shape of Mathlib's ContIntertwiningMap.isIntertwining.

noncomputable def ContRepresentation.averageIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) : ContIntertwiningMap π ρ

The Haar average of an operator, packaged as a term of Mathlib's ContIntertwiningMap.

Equations

• π.averageIntertwiner hπ ρ hρ T = { toContinuousLinearMap := π.averageOperator hπ ρ hρ T, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.toContinuousLinearMap_averageIntertwiner {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) : (π.averageIntertwiner hπ ρ hρ T).toContinuousLinearMap = π.averageOperator hπ ρ hρ T

@[simp]

theorem ContRepresentation.averageIntertwiner_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (v : V) : (π.averageIntertwiner hπ ρ hρ T) v = (π.averageOperator hπ ρ hρ T) v

The bundled average, evaluated at a vector.

Averaging is a projection onto the intertwiners

theorem ContRepresentation.averageOperator_eq_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (hT : ∀ (g : G), T ∘SL π g = ρ g ∘SL T) : π.averageOperator hπ ρ hρ T = T

Averaging fixes an operator that already intertwines. The integrand is then constant, and normalized Haar measure has total mass one.

@[simp]

theorem ContRepresentation.averageOperator_toContinuousLinearMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (f : ContIntertwiningMap π ρ) : π.averageOperator hπ ρ hρ f.toContinuousLinearMap = f.toContinuousLinearMap

Averaging fixes every continuous intertwiner.

@[simp]

theorem ContRepresentation.averageOperator_averageOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) : π.averageOperator hπ ρ hρ (π.averageOperator hπ ρ hρ T) = π.averageOperator hπ ρ hρ T

Averaging is idempotent: it is a projection of the operators onto the intertwiners.

@[simp]

theorem ContRepresentation.averageOperator_id {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.averageOperator hπ π hπ (ContinuousLinearMap.id 𝕜 V) = ContinuousLinearMap.id 𝕜 V

Averaging the identity over a single representation returns the identity.

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

Completeness of V is not an extra hypothesis on the trace results below: a finite-dimensional normed space over an RCLike field is already complete. Mathlib keeps FiniteDimensional.complete out of the global instance set, so it is installed here as a local instance instead.

theorem ContRepresentation.trace_averageOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →L[𝕜] V) : (LinearMap.trace 𝕜 V) ↑(π.averageOperator hπ π hπ T) = (LinearMap.trace 𝕜 V) ↑T

Averaging preserves the trace. In finite dimensions each conjugate π g⁻¹ ∘ T ∘ π g has the trace of T, and averaging a constant returns that constant. This is what fixes the normalizing factor (dim V)⁻¹ in the first Schur orthogonality relation.

theorem ContRepresentation.inner_averageOperator {𝕜 : 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] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (T : V →L[𝕜] W) (v : V) (w : W) : inner 𝕜 w ((π.averageOperator hπ ρ hρ T) v) = ∫ (g : G), inner 𝕜 w ((ρ g⁻¹) (T ((π g) v))) ∂TauCeti.haarProb G

A matrix entry of the averaged operator is the Haar integral of the matrix entries of the integrand.

theorem ContRepresentation.inner_averageOperator_of_isUnitary {𝕜 : 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] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : ρ.IsUnitary) (T : V →L[𝕜] W) (v : V) (w : W) : inner 𝕜 w ((π.averageOperator hπ ρ hρ T) v) = ∫ (g : G), inner 𝕜 ((ρ g) w) (T ((π g) v)) ∂TauCeti.haarProb G

For a unitary ρ the inverse action can be moved to the other side of the inner product, which is the form the matrix-coefficient computation needs.

theorem ContRepresentation.inner_matrixCoeffLp_eq_inner_averageOperator {𝕜 : 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] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : ρ.IsUnitary) (v w : V) (v' w' : W) : inner 𝕜 (π.matrixCoeffLp hπ v w) (ρ.matrixCoeffLp hρ v' w') = inner 𝕜 v' ((π.averageOperator hπ ρ hρ (((InnerProductSpace.rankOne 𝕜) w') w)) v)

The L² inner product of two matrix coefficients is a matrix entry of an averaged rank-one operator. For the rank-one operator InnerProductSpace.rankOne 𝕜 w' w = ⟪w, ·⟫ • w' the integrand ⟪ρ g v', T (π g v)⟫ is exactly the pointwise product ⟪ρ g v', w'⟫ · conj ⟪π g v, w⟫ computed by ContRepresentation.inner_matrixCoeffLp.

This is the identity that reduces Schur orthogonality to a statement about the intertwiner space: the operator on the right is an intertwiner π → ρ by ContRepresentation.averageOperator_comp.

theorem ContRepresentation.schur_orthogonality_distinct {𝕜 : 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] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : ρ.IsUnitary) (hdistinct : ∀ (f : ContIntertwiningMap π ρ), f.toContinuousLinearMap = 0) (v w : V) (v' w' : W) : inner 𝕜 (π.matrixCoeffLp hπ v w) (ρ.matrixCoeffLp hρ v' w') = 0

Schur orthogonality for inequivalent representations. If the only continuous intertwiner π → ρ is zero, then every matrix coefficient of π is L²-orthogonal to every matrix coefficient of ρ.

Schur's lemma is not invoked here; it is what supplies the hypothesis for a pair of inequivalent irreducibles. Only ρ is required to be unitary: unitarity of ρ is what lets the inverse action be moved across the inner product, and nothing in the argument constrains π.