Convolution operators on L² of a compact group

For a continuous kernel k : C(G, 𝕜) on a compact group G and an L² function f, the convolution

(k * f) x = ∫ y, k (x * y⁻¹) * f y ∂(haarProb G)

makes sense at every point x, not merely almost everywhere: the integral is the L² pairing of f against the continuous function y ↦ conj (k (x * y⁻¹)), and that function varies continuously with x in the uniform norm. Convolution therefore smooths L²(G) into C(G), and the resulting map convolutionCLM k : L²(G) →L[𝕜] C(G) is bounded by the uniform norm of the kernel.

Composing with ContinuousMap.toLp gives the convolution operator convolutionOperator k on L²(G). Its properties are proved here: it is self-adjoint when the kernel is symmetric (k g⁻¹ = conj (k g)), it commutes with right translation, and it is a compact operator. Together these say that the eigenspace of a symmetric convolution operator at a nonzero eigenvalue is a finite-dimensional right-translation-invariant subspace of L²(G) all of whose elements have continuous representatives, and that such eigenspaces exist; the eigenspaces at all eigenvalues, the possibly infinite-dimensional kernel included, together span a dense subspace. This is how the Peter-Weyl theorem manufactures finite-dimensional representations of G without presupposing that any exist.

Main definitions

• TauCeti.convolutionCLM: convolution against a continuous kernel, as a bounded linear map Lp 𝕜 2 (haarProb G) →L[𝕜] C(G, 𝕜).
• TauCeti.convolutionOperator: the convolution operator f ↦ k * f on Lp 𝕜 2 (haarProb G).

Main statements

• TauCeti.convolutionCLM_apply_apply: the pointwise formula (k * f) x = ∫ y, k (x * y⁻¹) * f y.
• TauCeti.convolutionCLM_toLp_apply: the translated formula (k * f) x = ∫ z, k z * f (z⁻¹ * x) when f is continuous.
• TauCeti.norm_convolutionCLM_apply_le: ‖k * f‖_∞ ≤ ‖k‖_∞ * ‖f‖₂, so convolution against a continuous kernel is bounded from L²(G) into the uniform norm of C(G).
• TauCeti.isSelfAdjoint_convolutionOperator: a symmetric kernel gives a self-adjoint operator.
• TauCeti.convolutionCLM_compMeasurePreserving_mul_right: convolution commutes with right translation.
• TauCeti.isCompactOperator_convolutionCLM and TauCeti.isCompactOperator_convolutionOperator: convolution against a continuous kernel is a compact operator, into C(G) and into L²(G).
• TauCeti.finiteDimensional_eigenspace_convolutionOperator: consequently the eigenspace of convolutionOperator k at a nonzero eigenvalue is finite-dimensional.
• TauCeti.ae_eq_smul_convolutionCLM_of_mem_eigenspace: an eigenvector at a nonzero eigenvalue is almost everywhere equal to the continuous function μ⁻¹ • (k * f).
• TauCeti.convolutionCLM_eq_zero_of_mem_eigenspace_zero: an eigenvector at the eigenvalue 0 convolves to the zero function.
• TauCeti.compMeasurePreserving_mul_right_mem_eigenspace_convolutionOperator: the eigenspaces are invariant under right translation.
• TauCeti.exists_hasEigenvalue_ne_zero_convolutionOperator: a nonzero symmetric convolution operator has a nonzero eigenvalue, so such an eigenspace really exists.
• TauCeti.orthogonalComplement_iSup_eigenspaces_convolutionOperator_eq_bot: the eigenspaces of a symmetric convolution operator, at every eigenvalue, span a dense subspace of L²(G).

Implementation notes

Compactness is read off the same kernel sections, with no separate uniform-continuity argument: the value (k * f) x is the L² pairing of f against the section at x, and the sections depend continuously on x in the uniform norm, so the images of the unit ball are equicontinuous by inspection. Arzelà-Ascoli (BoundedContinuousFunction.arzela_ascoli) then applies, in G →ᵇ 𝕜, to which C(G, 𝕜) is isometric because G is compact.

Mathlib's convolution (Mathlib/Analysis/Convolution.lean) is the convolution of two functions on an additive group against a bilinear pairing, and does not apply here: G is multiplicative, and one of the two arguments is an L² class rather than a function. The kernel sections y ↦ conj (k (x * y⁻¹)) are assembled with ContinuousMap.curry, whose continuity is exactly the statement that they depend continuously on x, so no uniform-continuity argument is needed.

Self-adjointness is proved by writing convolutionOperator k H, for a continuous H, as the Bochner integral of the kernel sections weighted by H, and then extending to all of L²(G) by density (ContinuousMap.toLp_denseRange). The more direct Fubini argument on G × G is not available: the product of two Borel spaces is Borel only under a second-countability hypothesis, which a compact group need not satisfy, whereas a continuous function on a compact space is integrable with no such hypothesis (TauCeti.integrable_continuousMap).

The conjugation in the kernel sections is bookkeeping for Mathlib's convention that the inner product is conjugate linear in its first argument; it is invisible in the pointwise formula convolutionCLM_apply_apply.

References

This is the opening of Layer 5 of the compact-groups roadmap, which names convolutionOperator, its self-adjointness for a symmetric kernel (there spelled convolutionOperator_isSelfAdjoint, renamed here to isSelfAdjoint_convolutionOperator for the predicate-prefix convention), its compactness (convolutionOperator_isCompact) and the finite dimensionality of its nonzero eigenspaces (convolutionOperator_eigenspace_finiteDimensional) as milestones on the non-circular route to 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.

Preliminaries on L² against normalized Haar measure

The kernel sections

The section of the kernel k at x is y ↦ conj (k (x * y⁻¹)). Currying the continuous function (x, y) ↦ conj (k (x * y⁻¹)) on G × G is exactly the statement that the section depends continuously on x in the uniform norm.

Convolution as a map into continuous functions

noncomputable def TauCeti.convolutionCLM {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G)) →L[𝕜] C(G, 𝕜)

Convolution against a continuous kernel, as a bounded linear map from L²(G) into C(G).

The value at x is the L² pairing of f against the kernel section at x, so it is defined at every point of G and depends continuously on that point: convolving an L² class against a continuous kernel produces a genuine continuous function, not another almost-everywhere class.

Equations

• TauCeti.convolutionCLM k = (TauCeti.convolutionₗ✝ k).mkContinuous ‖k‖ ⋯

theorem TauCeti.convolutionCLM_apply_apply {𝕜 : 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))) (x : G) : ((convolutionCLM k) f) x = ∫ (y : G), k (x * y⁻¹) * ↑↑f y ∂haarProb G

The pointwise formula for convolution against a continuous kernel.

theorem TauCeti.convolutionCLM_toLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k f : C(G, 𝕜)) (x : G) : ((convolutionCLM k) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f)) x = ∫ (z : G), k z * f (z⁻¹ * x) ∂haarProb G

Convolution written by translating the function rather than the kernel: (k * f) x = ∫ z, k z * f (z⁻¹ * x).

This form follows from TauCeti.convolutionCLM_apply_apply by the substitution y = z⁻¹ * x, which preserves normalized Haar measure because it is inversion followed by right translation.

theorem TauCeti.convolutionCLM_toLp_sub_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k f : C(G, 𝕜)) (hk : ∫ (g : G), k g ∂haarProb G = 1) (x : G) : ((convolutionCLM k) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f)) x - f x = ∫ (z : G), k z * (f (z⁻¹ * x) - f x) ∂haarProb G

The error of an approximation of f by k * f, when the kernel k has unit mass: the average against k of the increments of f.

@[simp]

theorem TauCeti.convolutionCLM_zero {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : convolutionCLM 0 = 0

Convolution is zero when its kernel is zero.

@[simp]

theorem TauCeti.convolutionCLM_add {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k₁ k₂ : C(G, 𝕜)) : convolutionCLM (k₁ + k₂) = convolutionCLM k₁ + convolutionCLM k₂

Convolution is additive in its kernel.

@[simp]

theorem TauCeti.convolutionCLM_smul {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (c : 𝕜) (k : C(G, 𝕜)) : convolutionCLM (c • k) = c • convolutionCLM k

Convolution is compatible with scalar multiplication of its kernel.

theorem TauCeti.norm_convolutionCLM_apply_le {𝕜 : 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))) : ‖(convolutionCLM k) f‖ ≤ ‖k‖ * ‖f‖

Convolution is bounded from L²(G) into C(G): the uniform norm of k * f is at most the product of the uniform norm of the kernel and the L² norm of f. Normalized Haar measure is a probability measure, so no measure-dependent constant appears.

theorem TauCeti.norm_convolutionCLM_le {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : ‖convolutionCLM k‖ ≤ ‖k‖

The operator norm of convolution against k, as a map into the uniform norm of C(G), is at most the uniform norm of k.

The convolution operator on L²(G)

noncomputable def TauCeti.convolutionOperator {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G)) →L[𝕜] ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The convolution operator f ↦ k * f on L²(G), for a continuous kernel k.

It factors through C(G): convolutionCLM produces a continuous function, and ContinuousMap.toLp reads that function back into L²(G).

Equations

• TauCeti.convolutionOperator k = ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜 ∘SL TauCeti.convolutionCLM k

theorem TauCeti.convolutionOperator_apply {𝕜 : 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))) : (convolutionOperator k) f = (ContinuousMap.toLp 2 (haarProb G) 𝕜) ((convolutionCLM k) f)

The convolution operator is convolutionCLM followed by ContinuousMap.toLp.

@[simp]

theorem TauCeti.convolutionOperator_zero {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : convolutionOperator 0 = 0

The convolution operator is zero when its kernel is zero.

@[simp]

theorem TauCeti.convolutionOperator_add {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k₁ k₂ : C(G, 𝕜)) : convolutionOperator (k₁ + k₂) = convolutionOperator k₁ + convolutionOperator k₂

The convolution operator is additive in its kernel.

@[simp]

theorem TauCeti.convolutionOperator_smul {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (c : 𝕜) (k : C(G, 𝕜)) : convolutionOperator (c • k) = c • convolutionOperator k

The convolution operator is compatible with scalar multiplication of its kernel.

theorem TauCeti.coeFn_convolutionOperator {𝕜 : 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))) : ↑↑((convolutionOperator k) f) =ᵐ[haarProb G] ⇑((convolutionCLM k) f)

The convolution operator is represented, almost everywhere, by the continuous function convolutionCLM k f.

theorem TauCeti.norm_convolutionOperator_le {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : ‖convolutionOperator k‖ ≤ ‖k‖

The convolution operator on L²(G) has operator norm at most the uniform norm of its kernel.

Self-adjointness for a symmetric kernel

For a continuous weight H the kernel sections may be averaged against H, giving a Bochner integral in C(G) and, after ContinuousMap.toLp, one in L²(G). Symmetry of the kernel identifies that average with k * H, which is the adjoint relation on the dense subspace of continuous functions; the general case follows because both sides of the relation are continuous in their second argument.

theorem TauCeti.isSelfAdjoint_convolutionOperator {𝕜 : 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)) : IsSelfAdjoint (convolutionOperator k)

Self-adjointness of the convolution operator for a symmetric kernel. A kernel is symmetric when k g⁻¹ = conj (k g); the pointwise identity conj (k (x * y⁻¹)) = k (y * x⁻¹) it supplies is what turns the average of the kernel sections weighted by H back into k * H.

Equivariance under right translation

theorem TauCeti.convolutionCLM_compMeasurePreserving_mul_right {𝕜 : 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₀ x : G) : ((convolutionCLM k) ((MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => x * g₀) ⋯) f)) x = ((convolutionCLM k) f) (x * g₀)

Convolution commutes with right translation. Translating f on the right by g₀ and then convolving is the same as convolving and then translating the result, because the kernel (x, y) ↦ k (x * y⁻¹) is unchanged by right translation of both variables.

This is what makes every eigenspace of a convolution operator a right-translation-invariant subspace of L²(G), hence, once the eigenspace is known to be finite-dimensional, the carrier of a finite-dimensional representation of G.

theorem TauCeti.convolutionOperator_compMeasurePreserving_mul_right {𝕜 : 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) : (convolutionOperator k) ((MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => x * g₀) ⋯) f) = (MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => x * g₀) ⋯) ((convolutionOperator k) f)

The convolution operator commutes with right translation on L²(G). This is convolutionCLM_compMeasurePreserving_mul_right read in L²(G); it is the form in which the eigenspaces of convolutionOperator k are seen to be right-translation-invariant.

Compactness of the convolution operator

Convolution against a continuous kernel carries the closed unit ball of L²(G) to a family of continuous functions bounded by ‖k‖ and equicontinuous: the increment of k * f between two points is controlled by the distance between the corresponding kernel sections, uniformly in f. The Arzelà-Ascoli theorem makes that family relatively compact in C(G), hence in L²(G).

theorem TauCeti.isCompactOperator_convolutionCLM {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : IsCompactOperator ⇑(convolutionCLM k)

Convolution against a continuous kernel is a compact operator from L²(G) to C(G).

The unit ball of L²(G) is carried to a uniformly bounded equicontinuous family of continuous functions, which Arzelà-Ascoli makes relatively compact for the uniform norm.

theorem TauCeti.isCompactOperator_convolutionOperator {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) : IsCompactOperator ⇑(convolutionOperator k)

The convolution operator on L²(G) is compact. It factors through the uniform norm of C(G), where isCompactOperator_convolutionCLM already gives compactness, and reading a continuous function back into L²(G) is bounded.

The eigenspaces of a convolution operator

Compactness bounds the dimension of each nonzero eigenspace; the pointwise formula shows every eigenvector at a nonzero eigenvalue is a continuous function; and equivariance makes the eigenspaces right-translation invariant. Together these are the three properties that turn a symmetric convolution operator into a source of finite-dimensional representations of G. The eigenspace at 0 is the complementary case: it convolves to nothing at all.

theorem TauCeti.finiteDimensional_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, 𝕜)) {μ : 𝕜} (hμ : μ ≠ 0) : FiniteDimensional 𝕜 ↥(Module.End.eigenspace (↑(convolutionOperator k)) μ)

A nonzero eigenspace of a convolution operator is finite-dimensional, because the operator is compact.

theorem TauCeti.ae_eq_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, 𝕜)) {μ : 𝕜} (hμ : μ ≠ 0) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ) : ↑↑f =ᵐ[haarProb G] μ⁻¹ • ⇑((convolutionCLM k) f)

Eigenvectors at a nonzero eigenvalue are continuous. An eigenvector f is μ⁻¹ times its own convolution k * f, and the latter is a genuine continuous function on G, not merely an almost-everywhere class. This supplies the continuous representatives that the later construction of the representative ring needs; membership in that ring additionally requires realizing the finite-dimensional invariant eigenspace as a continuous representation.

theorem TauCeti.convolutionCLM_eq_zero_of_mem_eigenspace_zero {𝕜 : 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)) 0) : (convolutionCLM k) f = 0

Convolving a 0-eigenvector gives the zero function. The convolution operator factors as ContinuousMap.toLp after convolutionCLM, and ContinuousMap.toLp is injective because normalized Haar measure is positive on nonempty open sets. This is the complement of ae_eq_smul_convolutionCLM_of_mem_eigenspace, which describes the eigenvectors at a nonzero eigenvalue.

theorem TauCeti.compMeasurePreserving_mul_right_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)) μ) : (MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => x * g₀) ⋯) f ∈ Module.End.eigenspace (↑(convolutionOperator k)) μ

The eigenspaces of a convolution operator are invariant under right translation, because the operator commutes with right translation.

The spectral consequences for a symmetric kernel

For a symmetric kernel the convolution operator is both compact and self-adjoint, so Mathlib's spectral theory of compact self-adjoint operators applies to it. Two consequences matter for Peter-Weyl: unless the operator vanishes it has a nonzero eigenvalue, and its eigenspaces together span a dense subspace of L²(G).

theorem TauCeti.exists_hasEigenvalue_ne_zero_convolutionOperator {𝕜 : 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)) (hne : convolutionOperator k ≠ 0) : ∃ (μ : 𝕜), μ ≠ 0 ∧ Module.End.HasEigenvalue (↑(convolutionOperator k)) μ

A nonzero symmetric convolution operator has a nonzero eigenvalue. For a compact self-adjoint operator the spectral radius is the operator norm and every nonzero spectral value is an eigenvalue, so a nonzero operator cannot have 0 as its only eigenvalue.

This is where finite-dimensional representations of G come from: by the results above, the eigenspace at such a μ is a nonzero, finite-dimensional, right-translation-invariant subspace of L²(G) all of whose elements are continuous. No point-separation property of G is used, so nothing is smuggled in from the Peter-Weyl theorem itself.

theorem TauCeti.orthogonalComplement_iSup_eigenspaces_convolutionOperator_eq_bot {𝕜 : 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)) : (⨆ (μ : 𝕜), Module.End.eigenspace (↑(convolutionOperator k)) μ)ᗮ = ⊥

The spectral theorem for a symmetric convolution operator: its eigenspaces span a dense subspace of L²(G), in the sense that their supremum has trivial orthogonal complement. Together with finiteDimensional_eigenspace_convolutionOperator this says that L²(G) is exhausted, up to the kernel of the operator, by finite-dimensional translation-invariant subspaces.