The finite-dimensional representations carried by convolution eigenspaces

A compact group G acts on L²(G) by right translation, (π g f) x = f (x * g) (TauCeti.rightRegularLp). This action is isometric and strongly continuous, but nothing makes g ↦ π g continuous for the operator norm, so L²(G) itself does not come with the continuity hypothesis that Mathlib's ContRepresentation is usually paired with. Restricted to an eigenspace of a convolution operator at a nonzero eigenvalue it does: that eigenspace is finite-dimensional, right-translation invariant, and made of continuous functions, all of which TauCeti.RepresentationTheory.Compact.Convolution supplies.

This file assembles those three facts into the representation itself, and reads off the consequence the Peter-Weyl theorem needs: the continuous representative μ⁻¹ • (k * f) of an eigenvector f is the conjugate of a matrix coefficient of that representation, hence a representative function, so it lies in the representative ring 𝓡(G). Since the eigenspaces of a symmetric kernel span a dense subspace of L²(G) and convolution is bounded from L²(G) into the uniform norm, every function of the form k * f lies in the uniform closure of 𝓡(G).

This is where the finite-dimensional representations of a compact group come from. Nothing here presupposes that G has any: the representation is manufactured out of the spectral theory of a compact self-adjoint operator, and no point-separation property is used, so the argument does not quietly assume the theorem it serves.

Main definitions

• TauCeti.convolutionEigenspaceRepresentation: the restriction of the right regular representation to an eigenspace of a convolution operator.

Main statements

• TauCeti.convolutionCLM_rightRegularLp: convolution intertwines right translation on L²(G) with right translation of continuous functions.
• TauCeti.continuous_convolutionEigenspaceRepresentation: at a nonzero eigenvalue the eigenspace representation is continuous, so it is a genuine finite-dimensional continuous representation of G.
• TauCeti.exists_smul_convolutionCLM_eq_star_matrixCoeff: the continuous representative of an eigenvector at a nonzero eigenvalue is the conjugate of a matrix coefficient of that representation, at a vector independent of the eigenvector.
• TauCeti.isRepresentative_smul_convolutionCLM_of_mem_eigenspace: consequently it is a representative function.
• TauCeti.convolutionCLM_mem_representativeSubmodule_of_mem_iSup_eigenspace: convolving a finite sum of eigenvectors gives an element of the representative ring 𝓡(G).
• TauCeti.convolutionCLM_mem_closure_representativeSubmodule: for a symmetric kernel, k * f lies in the uniform closure of 𝓡(G) for every f ∈ L²(G).

Implementation notes

Continuity of g ↦ π g on the eigenspace is checked pointwise, which is enough because the eigenspace is finite-dimensional (continuous_clm_apply); pointwise it is the strong continuity TauCeti.continuous_rightRegularLp_apply of the right regular representation, so no separate argument about continuous representatives is needed.

The matrix coefficient is produced from the linear functional h ↦ μ⁻¹ • (k * h) 1, evaluation of the continuous representative at the identity. Its Riesz vector y satisfies ⟪y, π g f⟫ = μ⁻¹ • (k * f) g, and Mathlib's inner product is conjugate linear in its first argument, so what appears directly is the conjugate of the matrix coefficient g ↦ ⟪π g f, y⟫. The representative functions are closed under conjugation (TauCeti.IsRepresentative.star), so nothing is lost.

References

This is the nonzero_eigenspace_finite_dim_continuous_rep step of Layer 5 of the compact-groups roadmap, which asks for each nonzero eigenspace to be finite-dimensional and translation invariant, "so it carries a continuous finite-dimensional representation whose functions lie in 𝓡(G)". Combined with an approximate identity it gives the uniform density of 𝓡(G) in C(G), the analytic core of the Peter-Weyl theorem.

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC (2016), §5.2.
• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapters 3-4.

Convolution against the right regular representation

theorem TauCeti.convolutionCLM_rightRegularLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (g : G) : (convolutionCLM k) (((rightRegularLp 𝕜 G) g) f) = ((convolutionCLM k) f).comp (ContinuousMap.mulRight g)

Convolution intertwines right translation on L²(G) with right translation of continuous functions. This is TauCeti.convolutionCLM_compMeasurePreserving_mul_right phrased in terms of TauCeti.rightRegularLp.

theorem TauCeti.rightRegularLp_mem_eigenspace_convolutionOperator {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (μ : 𝕜) (g : G) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ) : ((rightRegularLp 𝕜 G) g) f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ

The eigenspaces of a convolution operator are invariant under the right regular representation. This is TauCeti.compMeasurePreserving_mul_right_mem_eigenspace_convolutionOperator phrased in terms of TauCeti.rightRegularLp.

The representation on an eigenspace of a convolution operator

noncomputable def TauCeti.convolutionEigenspaceRepresentation {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (μ : 𝕜) : ContRepresentation 𝕜 G ↥(Module.End.eigenspace (↑(convolutionOperator k)) μ)

The representation of G on an eigenspace of a convolution operator: the right regular representation restricted to the eigenspace, which is right-translation invariant because convolution commutes with right translation.

Equations

• TauCeti.convolutionEigenspaceRepresentation k μ = (TauCeti.rightRegularLp 𝕜 G).subrepresentation (Module.End.eigenspace (↑(TauCeti.convolutionOperator k)) μ) ⋯

@[simp]

theorem TauCeti.coe_convolutionEigenspaceRepresentation_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (μ : 𝕜) (g : G) (f : ↥(Module.End.eigenspace (↑(convolutionOperator k)) μ)) : ↑(((convolutionEigenspaceRepresentation k μ) g) f) = ((rightRegularLp 𝕜 G) g) ↑f

theorem TauCeti.isUnitary_convolutionEigenspaceRepresentation {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (μ : 𝕜) : (convolutionEigenspaceRepresentation k μ).IsUnitary

The eigenspace representation is unitary, being a restriction of the unitary right regular representation.

theorem TauCeti.continuous_convolutionEigenspaceRepresentation {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) {μ : 𝕜} (hμ : μ ≠ 0) : Continuous ⇑(convolutionEigenspaceRepresentation k μ)

The eigenspace representation at a nonzero eigenvalue is continuous. The eigenspace is finite-dimensional, so continuity for the operator norm may be checked one vector at a time; on a vector it is the strong continuity of the right regular representation.

Together with TauCeti.finiteDimensional_eigenspace_convolutionOperator this is the statement that a nonzero eigenspace of a convolution operator carries a finite-dimensional continuous representation of G.

The eigenvectors are representative functions

theorem TauCeti.exists_smul_convolutionCLM_eq_star_matrixCoeff {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) {μ : 𝕜} (hμ : μ ≠ 0) : ∃ (y : ↥(Module.End.eigenspace (↑(convolutionOperator k)) μ)), ∀ (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (hf : f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ), μ⁻¹ • (convolutionCLM k) f = star ((convolutionEigenspaceRepresentation k μ).matrixCoeff ⋯ ⟨f, hf⟩ y)

The continuous representative of an eigenvector is a matrix coefficient of the eigenspace representation. For a nonzero eigenvalue μ, one vector y of the eigenspace serves for every eigenvector at once: it is the Riesz vector of the functional "evaluate the continuous representative at the identity", and μ⁻¹ • (k * f) is the conjugate of the matrix coefficient at (f, y).

Naming the representation, rather than only the conclusion that the function is representative, is what records that the finite-dimensional representations produced by the density argument are unitary (TauCeti.isUnitary_convolutionEigenspaceRepresentation), so that a statement proved for unitary representations can be fed back into it.

theorem TauCeti.isRepresentative_smul_convolutionCLM_of_mem_eigenspace {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) {μ : 𝕜} {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ) : IsRepresentative (μ⁻¹ • (convolutionCLM k) f)

The continuous representative of an eigenvector is a representative function. For a nonzero eigenvalue μ, the continuous function μ⁻¹ • (k * f) representing an eigenvector f is the conjugate of a matrix coefficient of TauCeti.convolutionEigenspaceRepresentation. At μ = 0 the function is 0, which is representative for trivial reasons.

This is the point of the whole construction: at a nonzero eigenvalue the continuous representative of an eigenvector is not merely continuous, it is a matrix coefficient of a finite-dimensional continuous representation. At μ = 0 the statement carries no information about f beyond TauCeti.convolutionCLM_eq_zero_of_mem_eigenspace_zero, which is what makes it 0.

theorem TauCeti.convolutionCLM_mem_representativeSubmodule_of_mem_iSup_eigenspace {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ ⨆ (μ : 𝕜), Module.End.eigenspace (↑(convolutionOperator k)) μ) : (convolutionCLM k) f ∈ representativeSubmodule 𝕜 G

Convolving a finite sum of eigenvectors lies in the representative ring 𝓡(G). Each nonzero eigenvalue contributes a matrix coefficient, and the zero eigenspace contributes nothing.

theorem TauCeti.convolutionCLM_mem_closure_representativeSubmodule {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (hk : ∀ (g : G), k g⁻¹ = (starRingEnd 𝕜) (k g)) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : (convolutionCLM k) f ∈ closure ↑(representativeSubmodule 𝕜 G)

Every convolution by a symmetric kernel lies in the uniform closure of the representative ring. The eigenspaces of a symmetric convolution operator span a dense subspace of L²(G), each of them convolves into 𝓡(G), and convolution is continuous from L²(G) into the uniform norm of C(G).

With an approximate identity, which lets a continuous function be uniformly approximated by such convolutions, this gives the uniform density of 𝓡(G) in C(G), the analytic core of the Peter-Weyl theorem.