Matrix coefficients in L² of a compact group

A matrix coefficient g ↦ ⟪π g v, w⟫ of a continuous representation of a compact group is a continuous function on a probability space, hence square integrable. This file records its image in L²(G) for normalized Haar measure, and the identities that turn L²-statements about matrix coefficients into integrals.

The L² picture is what the Schur orthogonality relations are stated in: they compute the inner product of two matrix coefficients, and inner_matrixCoeffLp below rewrites that inner product as the Haar integral the orthogonality argument evaluates.

Main definitions

• ContRepresentation.matrixCoeffLp: the matrix coefficient g ↦ ⟪π g v, w⟫ as an element of Lp 𝕜 2 (haarProb G).
• ContRepresentation.matrixCoeffLpₛₗ: the matrix coefficients of a fixed representation bundled as a sesquilinear map V →ₗ⋆[𝕜] V →ₗ[𝕜] Lp 𝕜 2 (haarProb G).

Main statements

• ContRepresentation.inner_matrixCoeffLp: the L² inner product of two matrix coefficients is the Haar integral of their pointwise product, in Mathlib's convention ⟪F, H⟫ = ∫ H · conj F.
• ContRepresentation.norm_matrixCoeffLp_sq: the squared L² norm is the Haar integral of the squared modulus.
• ContRepresentation.norm_matrixCoeffLp_le: for a unitary representation the L² norm is at most ‖v‖ * ‖w‖, because normalized Haar measure has total mass one.
• ContRepresentation.matrixCoeffLp_eq_zero_iff: passing to L² loses no information, since Haar measure is positive on nonempty open sets.
• ContRepresentation.matrixCoeffLp_map_map: moving both defining vectors by π h reparametrizes the matrix coefficient by a conjugation.

The uniform-norm algebra is developed in TauCeti/RepresentationTheory/Continuous/MatrixCoefficient.lean. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.matrixCoeffLp {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ↥(MeasureTheory.Lp 𝕜 2 (TauCeti.haarProb G))

The matrix coefficient g ↦ ⟪π g v, w⟫ as an element of L²(G) for normalized Haar measure.

A matrix coefficient is continuous and G is compact, so ContinuousMap.toLp applies; the normalization of Haar measure to a probability measure is what makes the resulting L² norms comparable to the uniform norm without a measure-dependent constant.

Equations

• π.matrixCoeffLp hπ v w = (ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜) (π.matrixCoeff hπ v w)

theorem ContRepresentation.matrixCoeffLp_def {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : π.matrixCoeffLp hπ v w = (ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜) (π.matrixCoeff hπ v w)

theorem ContRepresentation.coeFn_matrixCoeffLp {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ↑↑(π.matrixCoeffLp hπ v w) =ᵐ[TauCeti.haarProb G] fun (g : G) => inner 𝕜 ((π g) v) w

A matrix coefficient in L² is represented, almost everywhere, by the function it comes from.

Sesquilinearity in the defining vectors

Passing to L² is linear, so the sesquilinearity of matrixCoeff transfers verbatim.

@[simp]

theorem ContRepresentation.matrixCoeffLp_zero_left {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (w : V) : π.matrixCoeffLp hπ 0 w = 0

@[simp]

theorem ContRepresentation.matrixCoeffLp_zero_right {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) : π.matrixCoeffLp hπ v 0 = 0

@[simp]

theorem ContRepresentation.matrixCoeffLp_add_left {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v₁ v₂ w : V) : π.matrixCoeffLp hπ (v₁ + v₂) w = π.matrixCoeffLp hπ v₁ w + π.matrixCoeffLp hπ v₂ w

@[simp]

theorem ContRepresentation.matrixCoeffLp_add_right {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w₁ w₂ : V) : π.matrixCoeffLp hπ v (w₁ + w₂) = π.matrixCoeffLp hπ v w₁ + π.matrixCoeffLp hπ v w₂

@[simp]

theorem ContRepresentation.matrixCoeffLp_smul_left {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (c : 𝕜) (v w : V) : π.matrixCoeffLp hπ (c • v) w = (starRingEnd 𝕜) c • π.matrixCoeffLp hπ v w

@[simp]

theorem ContRepresentation.matrixCoeffLp_smul_right {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) (c : 𝕜) (w : V) : π.matrixCoeffLp hπ v (c • w) = c • π.matrixCoeffLp hπ v w

noncomputable def ContRepresentation.matrixCoeffLpₛₗ {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : V →ₗ⋆[𝕜] V →ₗ[𝕜] ↥(MeasureTheory.Lp 𝕜 2 (TauCeti.haarProb G))

The L² matrix coefficients of a fixed representation, bundled as a sesquilinear map: conjugate linear in the first vector, linear in the second, exactly as Mathlib's innerₛₗ.

This is matrixCoeffₛₗ postcomposed with the linear map ContinuousMap.toLp, so the sesquilinearity is inherited rather than reproved; bundling supplies the remaining additive identities (map_neg, map_sub, map_sum) through the LinearMap API.

Equations

• π.matrixCoeffLpₛₗ hπ = (π.matrixCoeffₛₗ hπ).compr₂ₛₗ ↑(ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜)

@[simp]

theorem ContRepresentation.matrixCoeffLpₛₗ_apply_apply {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ((π.matrixCoeffLpₛₗ hπ) v) w = π.matrixCoeffLp hπ v w

Passing to L² loses no information

Haar measure is positive on nonempty open sets, so two continuous functions agreeing almost everywhere agree.

theorem ContRepresentation.matrixCoeffLp_eq_zero_iff {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : π.matrixCoeffLp hπ v w = 0 ↔ π.matrixCoeff hπ v w = 0

A matrix coefficient vanishes in L² exactly when the continuous function it comes from is the zero function: ContinuousMap.toLp is injective for a measure that is positive on nonempty open sets, and normalized Haar measure is one.

theorem ContRepresentation.matrixCoeffLp_eq_zero_iff_forall {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : π.matrixCoeffLp hπ v w = 0 ↔ ∀ (g : G), inner 𝕜 ((π g) v) w = 0

A matrix coefficient vanishes in L² exactly when it vanishes identically.

The inner product as a Haar integral

theorem ContRepresentation.inner_matrixCoeffLp {𝕜 : 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] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (v w : V) (v' w' : W) : inner 𝕜 (π.matrixCoeffLp hπ v w) (ρ.matrixCoeffLp hρ v' w') = ∫ (g : G), inner 𝕜 ((ρ g) v') w' * (starRingEnd 𝕜) (inner 𝕜 ((π g) v) w) ∂TauCeti.haarProb G

The L² inner product of two matrix coefficients is the Haar integral of their pointwise product. Mathlib's inner product is conjugate linear in its first argument and unfolds as ⟪F, H⟫ = ∫ H · conj F, which is where the conjugation sits below; this placement is what the Schur orthogonality relations are stated against.

theorem ContRepresentation.norm_matrixCoeffLp_sq {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ‖π.matrixCoeffLp hπ v w‖ ^ 2 = ∫ (g : G), ‖inner 𝕜 ((π g) v) w‖ ^ 2 ∂TauCeti.haarProb G

The squared L² norm of a matrix coefficient is the Haar integral of its squared modulus.

Bounds from the normalization of Haar measure

theorem ContRepresentation.norm_matrixCoeffLp_le {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (v w : V) : ‖π.matrixCoeffLp hπ v w‖ ≤ ‖v‖ * ‖w‖

The L² norm of a matrix coefficient of a unitary representation is at most the product of the norms of its defining vectors, with no constant: normalized Haar measure has total mass one, so ContinuousMap.toLp is a contraction from the uniform norm, where norm_matrixCoeff_le is the matching bound.

The trivial representation, and subrepresentations

theorem ContRepresentation.norm_matrixCoeffLp_trivial {𝕜 : 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] [InnerProductSpace 𝕜 V] (v w : V) : ‖(trivial 𝕜 G V).matrixCoeffLp ⋯ v w‖ = ‖inner 𝕜 v w‖

The matrix coefficients of the trivial representation are constants, and normalized Haar measure gives a constant its own norm. This is the sanity check that matrixCoeffLp carries the probability normalization rather than an unnormalized one.

@[simp]

theorem ContRepresentation.matrixCoeffLp_subrepresentation {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {U : Submodule 𝕜 V} (hU : ∀ (g : G), ∀ v ∈ U, (π g) v ∈ U) (v w : ↥U) : (π.subrepresentation U hU).matrixCoeffLp ⋯ v w = π.matrixCoeffLp hπ ↑v ↑w

A matrix coefficient of an invariant submodule is the matrix coefficient of the ambient representation at the underlying vectors, so passing to a subrepresentation creates no new elements of L²(G).

Moving both defining vectors

theorem ContRepresentation.matrixCoeffLp_map_map {𝕜 : 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] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (h : G) (v w : V) : π.matrixCoeffLp hπ ((π h) v) ((π h) w) = (TauCeti.conjLpₗᵢ 𝕜 h⁻¹) (π.matrixCoeffLp hπ v w)

Simultaneously moving the two vectors conjugates the argument of a matrix coefficient.