The Peter-Weyl theorem: the matrix coefficients are a Hilbert basis of L²(G)

Let G be a compact group. Schur orthogonality (TauCeti/RepresentationTheory/Compact/Orthonormal.lean) says that the normalized matrix coefficients √(dim V_i) · (π i)_{ab} of a family of pairwise inequivalent finite-dimensional irreducible unitary continuous representations form an orthonormal system in L²(G). This file proves that when the family is moreover exhaustive the system is complete, so it is a Hilbert basis of L²(G): the Peter-Weyl theorem. Hausdorffness is nowhere needed, here or in the unconditional standard basis at the end: what the density argument runs on are the mollifiers of Compact/ApproximateIdentity.lean, which are built without it.

"One representative per equivalence class" is data

The index of the basis is not free. It hides a choice of model spaces, of unitary irreducible representations on them, and of orthonormal bases; a theorem that merely asserts the existence of such a family says nothing about which functions the basis consists of. Both are pinned here.

• TauCeti.IrrepModel is one chosen model: a natural number dim, a continuous unitary irreducible representation on the standard Hilbert space EuclideanSpace 𝕜 (Fin dim), whose orthonormal basis is therefore EuclideanSpace.basisFun, not a further choice.
• TauCeti.IsIrrepSkeleton models says the family models is a skeleton of the unitary dual: pairwise inequivalent, and exhaustive in the sense that every continuous unitary irreducible representation on a standard model space is carried onto some models i by a linear isometry equivalence. Exhaustion is asked for in unitary form, which is no restriction: between irreducible unitary representations Schur's lemma makes every intertwining isomorphism a scalar multiple of an isometry (ContRepresentation.exists_linearIsometryEquiv_congr_eq).
• TauCeti.peterWeylBasis is a HilbertBasis, defined outright rather than existentially, and TauCeti.coe_peterWeylBasis identifies its elements as the normalized matrix coefficients TauCeti.peterWeylFamily. The element-level content is therefore available on the nose.

Nothing here is conditional on a skeleton being available: one is built at the end of the file. Because a model's carrier is a standard space EuclideanSpace 𝕜 (Fin n), unitary equivalence is an equivalence relation on the type TauCeti.IrrepModel 𝕜 G, and choosing a representative in each class gives TauCeti.IrrepClass.model, a skeleton by TauCeti.isIrrepSkeleton_model. Feeding it to TauCeti.peterWeylBasis gives TauCeti.stdPeterWeylBasis, a Hilbert basis of L²(G) for every compact G with no hypothesis left over. Pairwise inequivalence of the representatives is the point where the rescaling above is used.

The completeness argument

Orthonormality is quoted from Schur. Completeness is what is proved here, and it factors through the span TauCeti.modelSubmodule of the matrix coefficients of the models inside C(G, 𝕜).

1. Irreducible representations. A continuous unitary irreducible representation on any finite-dimensional inner product space is carried to a standard model by stdOrthonormalBasis, hence onto some models i by exhaustion, and matrix coefficients are unchanged along an isometry (LinearIsometryEquiv.matrixCoeff_congr).
2. Unitary representations. An arbitrary continuous unitary representation splits as an orthogonal direct sum of irreducible subrepresentations (ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition), and for a vector v in one block the functional ⟪·, w⟫ only sees the orthogonal projection of w onto that block, so every matrix coefficient reduces to matrix coefficients of the blocks.
3. Density. The analytic core of Peter-Weyl (TauCeti/RepresentationTheory/Compact/RepresentativeDensity.lean) approximates a continuous function by convolutions, and expands each convolution along the eigenspaces of the convolution operator. Those eigenspace representations are unitary (TauCeti.isUnitary_convolutionEigenspaceRepresentation), so step 2 applies to them and the models' coefficients are already uniformly dense: no unitarization of an arbitrary representation is needed anywhere.
4. Passage to L². Continuous functions are dense in L² of a finite measure on a compact space, so the span of the models' coefficients is dense in L²(G) and its orthogonal complement vanishes, which is the hypothesis of HilbertBasis.mkOfOrthogonalEqBot.

Main definitions

• TauCeti.IrrepModel, TauCeti.IsIrrepSkeleton: the chosen data and the exhaustion property.
• TauCeti.modelSubmodule: the span of the models' matrix coefficients in C(G, 𝕜).
• TauCeti.peterWeylFamily: the normalized matrix coefficients, indexed by Σ i, Fin (models i).dim × Fin (models i).dim.
• TauCeti.peterWeylBasis: the Peter-Weyl Hilbert basis of L²(G).
• TauCeti.peterWeylCoeff: the Fourier coefficient against a normalized matrix coefficient.
• TauCeti.IrrepClass, TauCeti.IrrepClass.model: the models up to unitary equivalence, and the representative chosen in each class.
• TauCeti.stdPeterWeylBasis: the Peter-Weyl basis of L²(G) on the chosen representatives, with no skeleton assumed.

Main statements

• TauCeti.IrrepModel.dim_pos: a model has positive dimension, its carrier being nonzero.
• TauCeti.IsIrrepSkeleton.matrixCoeff_mem: every matrix coefficient of a finite-dimensional unitary continuous representation is a linear combination of the models' matrix coefficients.
• TauCeti.IsIrrepSkeleton.dense_modelSubmodule: those coefficients are uniformly dense in C(G, 𝕜).
• TauCeti.IsIrrepSkeleton.orthogonal_span_peterWeylFamily_eq_bot: the completeness of the orthonormal system.
• TauCeti.coe_peterWeylBasis, TauCeti.coe_stdPeterWeylBasis: the basis is the normalized matrix coefficients.
• TauCeti.peterWeylFamily_eq_toLp: each family element is the L² class of its normalized continuous matrix coefficient.
• TauCeti.coeFn_peterWeylFamily: the almost-everywhere representative of a normalized matrix coefficient.
• TauCeti.peterWeylBasis_repr_apply, TauCeti.stdPeterWeylBasis_repr_apply: the abstract basis coordinates are the explicit Haar-integral Fourier coefficients.
• TauCeti.hasSum_peterWeyl_expansion: reconstruction of an L² function from its Peter-Weyl coefficients.
• TauCeti.tsum_conj_peterWeylCoeff_mul_peterWeylCoeff, TauCeti.tsum_norm_sq_peterWeylCoeff: polarized and norm-square Parseval identities.
• TauCeti.isIrrepSkeleton_model: the chosen representatives are a skeleton, so the hypothesis of TauCeti.peterWeylBasis is satisfiable and the theorem is not conditional.

References

• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 2.
• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC (2016), §5.2.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter III.

Chosen models of the irreducible representations

structure TauCeti.IrrepModel (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] : Type (max u_1 u_2)

A chosen model of a finite-dimensional irreducible unitary continuous representation. The carrier is the standard Hilbert space EuclideanSpace 𝕜 (Fin dim), so the model comes with a canonical orthonormal basis and no further choice is hidden in it.

• dim : ℕ

  The dimension of the model, which is also the size of its index type.

• rep : ContRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin self.dim))

  The representation carried by the model.

• continuous_rep : Continuous ⇑self.rep

  The model's action is continuous.

• isUnitary : self.rep.IsUnitary

  The model's action is by unitary operators.

• isIrreducible : (ContRepresentation.toRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin self.dim)) self.rep).IsIrreducible

  The model is irreducible.

noncomputable def TauCeti.IrrepModel.oneDimensionalEquiv {𝕜 : Type u_1} [RCLike 𝕜] : 𝕜 ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 (Fin 1)

The canonical linear isometry from the scalar field to the standard one-dimensional carrier of an IrrepModel. It matches the standard orthonormal bases on the two spaces.

Equations

• TauCeti.IrrepModel.oneDimensionalEquiv = ((stdOrthonormalBasis 𝕜 𝕜).reindex (finCongr ⋯)).equiv (EuclideanSpace.basisFun (Fin 1) 𝕜) (Equiv.refl (Fin 1))

noncomputable def TauCeti.IrrepModel.basis {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] (m : IrrepModel 𝕜 G) : OrthonormalBasis (Fin m.dim) 𝕜 (EuclideanSpace 𝕜 (Fin m.dim))

The canonical orthonormal basis of the carrier of a model.

Equations

• m.basis = EuclideanSpace.basisFun (Fin m.dim) 𝕜

theorem TauCeti.IrrepModel.basis_def {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] (m : IrrepModel 𝕜 G) : m.basis = EuclideanSpace.basisFun (Fin m.dim) 𝕜

The canonical basis of an irreducible model is the standard Euclidean basis.

theorem TauCeti.IrrepModel.dim_pos {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] (m : IrrepModel 𝕜 G) : 0 < m.dim

A model of an irreducible representation has positive dimension. Equivalently, its carrier EuclideanSpace 𝕜 (Fin dim) is nonzero, so its index type Fin dim is nonempty.

def TauCeti.modelCoeffs {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] (models : ι → IrrepModel 𝕜 G) : Set C(G, 𝕜)

The set of all matrix coefficients of the members of a family of models.

Equations

• TauCeti.modelCoeffs models = {f : C(G, 𝕜) | ∃ (i : ι) (v : EuclideanSpace 𝕜 (Fin (models i).dim)) (w : EuclideanSpace 𝕜 (Fin (models i).dim)), f = (models i).rep.matrixCoeff ⋯ v w}

noncomputable def TauCeti.modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] (models : ι → IrrepModel 𝕜 G) : Submodule 𝕜 C(G, 𝕜)

The span, inside C(G, 𝕜), of the matrix coefficients of a family of models. Peter-Weyl is the statement that for a skeleton of the unitary dual this is dense.

Equations

• TauCeti.modelSubmodule models = Submodule.span 𝕜 (TauCeti.modelCoeffs models)

theorem TauCeti.matrixCoeff_mem_modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] (models : ι → IrrepModel 𝕜 G) (i : ι) (v w : EuclideanSpace 𝕜 (Fin (models i).dim)) : (models i).rep.matrixCoeff ⋯ v w ∈ modelSubmodule models

A matrix coefficient of a model lies in the span of the models' matrix coefficients.

structure TauCeti.IsIrrepSkeleton {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] (models : ι → IrrepModel 𝕜 G) : Prop

A skeleton of the unitary dual of G. The family models is pairwise inequivalent and exhausts the finite-dimensional irreducible unitary continuous representations: every one of them on a standard model space is carried onto some models i by a linear isometry equivalence.

Exhaustion in unitary form is no restriction. Between finite-dimensional irreducible unitary representations Schur's lemma makes any intertwining isomorphism a scalar multiple of a unitary one (ContRepresentation.exists_linearIsometryEquiv_congr_eq), so a family exhaustive up to isomorphism is exhaustive up to unitary isomorphism.

• pairwise_isEmpty_equiv : Pairwise fun (i j : ι) => IsEmpty ((models i).rep.Equiv (models j).rep)

  Distinct members of the family are inequivalent.

• exists_congr_eq (n : ℕ) (π : ContRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin n))) (hπ : Continuous ⇑π) (hu : π.IsUnitary) (hirr : (ContRepresentation.toRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin n)) π).IsIrreducible) : ∃ (i : ι) (e : EuclideanSpace 𝕜 (Fin n) ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 (Fin (models i).dim)), (↑e).congr π = (models i).rep

  Every continuous unitary irreducible representation on a standard model space is carried onto a member of the family by a linear isometry equivalence.

theorem TauCeti.IsIrrepSkeleton.matrixCoeff_mem_of_isIrreducible {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) (hu : π.IsUnitary) (hirr : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible) (v w : V) : π.matrixCoeff hπ v w ∈ modelSubmodule models

The matrix coefficients of an irreducible representation are accounted for. A finite-dimensional irreducible unitary continuous representation is carried to a standard model by stdOrthonormalBasis, and from there onto a member of the skeleton; matrix coefficients survive both isometries.

theorem TauCeti.IsIrrepSkeleton.matrixCoeff_mem_of_mem_of_isIrreducible {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) {W : Submodule 𝕜 V} [FiniteDimensional 𝕜 ↥W] (hU : ∀ (g : G), ∀ y ∈ W, (π g) y ∈ W) (hu : (π.subrepresentation W hU).IsUnitary) {x : V} (hx : x ∈ W) (hirr : (ContRepresentation.toRepresentation 𝕜 G (↥W) (π.subrepresentation W hU)).IsIrreducible) (w : V) : π.matrixCoeff hπ x w ∈ modelSubmodule models

A matrix coefficient of a vector in an irreducible invariant subspace is accounted for. If W is a finite-dimensional subspace invariant under π, on which π restricts to a unitary irreducible representation, then for x ∈ W and any w the matrix coefficient of π at x, w lies in the span of the skeleton's coefficients.

theorem TauCeti.IsIrrepSkeleton.matrixCoeff_mem {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) (hu : π.IsUnitary) (v w : V) : π.matrixCoeff hπ v w ∈ modelSubmodule models

The matrix coefficients of a unitary representation are accounted for. Complete reducibility splits the representation into irreducible blocks orthogonally, and the inner product against a fixed vector only sees that vector's component in the block, so every matrix coefficient of the whole is a sum of matrix coefficients of the blocks.

Density

theorem TauCeti.IsIrrepSkeleton.convolutionCLM_mem_modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (k : C(G, 𝕜)) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ ⨆ (μ : 𝕜), Module.End.eigenspace (↑(convolutionOperator k)) μ) : (convolutionCLM k) f ∈ modelSubmodule models

Convolving a finite sum of eigenvectors of a convolution operator lands in the span of the models' matrix coefficients: each nonzero eigenspace carries a unitary finite-dimensional continuous representation, so TauCeti.IsIrrepSkeleton.matrixCoeff_mem applies to it.

theorem TauCeti.IsIrrepSkeleton.convolutionCLM_mem_closure_modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (k : C(G, 𝕜)) (hk : ∀ (g : G), k g⁻¹ = (starRingEnd 𝕜) (k g)) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : (convolutionCLM k) f ∈ closure ↑(modelSubmodule models)

Every convolution by a symmetric kernel lies in the uniform closure of the span of the models' matrix coefficients.

theorem TauCeti.IsIrrepSkeleton.dense_modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : Dense ↑(modelSubmodule models)

The models' matrix coefficients are uniformly dense in C(G, 𝕜). This is the Peter-Weyl density theorem sharpened from "all finite-dimensional representations" to "the chosen irreducible ones": convolving by an approximate identity moves a continuous function arbitrarily little, and every convolution is already a uniform limit of the models' coefficients.

theorem TauCeti.IsIrrepSkeleton.dense_image_toLp_modelSubmodule {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : Dense (⇑(ContinuousMap.toLp 2 (haarProb G) 𝕜) '' ↑(modelSubmodule models))

The models' matrix coefficients are dense in L²(G).

The Peter-Weyl basis

noncomputable def TauCeti.peterWeylFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The normalized matrix coefficients of a family of models, indexed by Σ i, Fin (models i).dim × Fin (models i).dim. The scalar √(dim) is what Schur orthogonality normalizes away.

Equations

• TauCeti.peterWeylFamily models x = ↑√↑(models x.fst).dim • (models x.fst).rep.matrixCoeffLp ⋯ ((models x.fst).basis x.snd.1) ((models x.fst).basis x.snd.2)

@[simp]

theorem TauCeti.peterWeylFamily_apply {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : peterWeylFamily models x = ↑√↑(models x.fst).dim • (models x.fst).rep.matrixCoeffLp ⋯ ((models x.fst).basis x.snd.1) ((models x.fst).basis x.snd.2)

The elements of the Peter-Weyl family, on the nose.

theorem TauCeti.peterWeylFamily_eq_toLp {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : peterWeylFamily models x = (ContinuousMap.toLp 2 (haarProb G) 𝕜) (↑√↑(models x.fst).dim • (models x.fst).rep.matrixCoeff ⋯ ((models x.fst).basis x.snd.1) ((models x.fst).basis x.snd.2))

A Peter-Weyl family element is the L² class of its normalized continuous matrix coefficient.

theorem TauCeti.coeFn_peterWeylFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : ↑↑(peterWeylFamily models x) =ᵐ[haarProb G] fun (g : G) => ↑√↑(models x.fst).dim * inner 𝕜 (((models x.fst).rep g) ((models x.fst).basis x.snd.1)) ((models x.fst).basis x.snd.2)

A normalized Peter-Weyl matrix coefficient in L² is represented almost everywhere by its defining continuous function.

theorem TauCeti.matrixCoeffLp_mem_span_peterWeylFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (i : ι) (v w : EuclideanSpace 𝕜 (Fin (models i).dim)) : (models i).rep.matrixCoeffLp ⋯ v w ∈ Submodule.span 𝕜 (Set.range (peterWeylFamily models))

Every L² matrix coefficient of a model lies in the span of the normalized ones: expand both defining vectors in the canonical orthonormal basis and use sesquilinearity.

theorem TauCeti.IsIrrepSkeleton.orthonormal_peterWeylFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} [IsAlgClosed 𝕜] (h : IsIrrepSkeleton models) : Orthonormal 𝕜 (peterWeylFamily models)

The normalized matrix coefficients of a skeleton are orthonormal. This is Schur orthogonality; only pairwise inequivalence of the family is used.

theorem TauCeti.IsIrrepSkeleton.orthogonal_span_peterWeylFamily_eq_bot {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : (Submodule.span 𝕜 (Set.range (peterWeylFamily models)))ᗮ = ⊥

The normalized matrix coefficients of a skeleton are complete. Their span is dense in L²(G), so its orthogonal complement vanishes. This is the completeness half of Peter-Weyl, in the form HilbertBasis.mkOfOrthogonalEqBot consumes.

noncomputable def TauCeti.peterWeylBasis {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : HilbertBasis ((i : ι) × Fin (models i).dim × Fin (models i).dim) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The Peter-Weyl theorem. For a skeleton of the unitary dual of a compact group, the normalized matrix coefficients √(dim V_i) · (models i)_{ab} are a Hilbert basis of L²(G), indexed by Σ i, Fin (models i).dim × Fin (models i).dim.

Algebraic closedness of the scalars is Schur's lemma, and enters through the orthonormality half.

Equations

• TauCeti.peterWeylBasis h = HilbertBasis.mkOfOrthogonalEqBot ⋯ ⋯

@[simp]

theorem TauCeti.coe_peterWeylBasis {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : ⇑(peterWeylBasis h) = peterWeylFamily models

The Peter-Weyl basis is the normalized matrix coefficients. Its elements are the L² classes represented by the continuous functions g ↦ √(dim V_i) · ⟪(models i).rep g e_a, e_b⟫.

noncomputable def TauCeti.peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : 𝕜

The Peter-Weyl Fourier coefficient of f at the normalized matrix coefficient indexed by x, written as a Haar integral.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.peterWeylCoeff_def {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : peterWeylCoeff models f x = ∫ (g : G), (starRingEnd 𝕜) (↑√↑(models x.fst).dim * ((models x.fst).rep.matrixCoeff ⋯ ((models x.fst).basis x.snd.1) ((models x.fst).basis x.snd.2)) g) * ↑↑f g ∂haarProb G

The Peter-Weyl coefficient is the Haar integral against the conjugate of the normalized continuous matrix coefficient.

theorem TauCeti.peterWeylCoeff_eq_inner {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : peterWeylCoeff models f x = inner 𝕜 (peterWeylFamily models x) f

A Peter-Weyl coefficient is the L² inner product against the corresponding normalized matrix coefficient. This characterization does not require the models to form a skeleton.

@[simp]

theorem TauCeti.peterWeylBasis_repr_apply {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) : ↑((peterWeylBasis h).repr f) x = peterWeylCoeff models f x

The abstract coordinate in the Peter-Weyl Hilbert basis is the explicit Haar-integral Fourier coefficient.

theorem TauCeti.hasSum_peterWeyl_expansion {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : HasSum (fun (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) => peterWeylCoeff models f x • peterWeylFamily models x) f

The Peter-Weyl expansion. Every L² function is the sum of its Fourier coefficients times the corresponding normalized matrix coefficients.

theorem TauCeti.hasSum_conj_peterWeylCoeff_mul_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f g : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : HasSum (fun (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) => (starRingEnd 𝕜) (peterWeylCoeff models f x) * peterWeylCoeff models g x) (inner 𝕜 f g)

Polarized Parseval for the Peter-Weyl basis. The coordinate pairing of two L² functions sums to their inner product.

theorem TauCeti.tsum_conj_peterWeylCoeff_mul_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f g : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ∑' (x : (i : ι) × Fin (models i).dim × Fin (models i).dim), (starRingEnd 𝕜) (peterWeylCoeff models f x) * peterWeylCoeff models g x = inner 𝕜 f g

Polarized Parseval for the Peter-Weyl basis (tsum form).

theorem TauCeti.summable_conj_peterWeylCoeff_mul_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f g : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : Summable fun (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) => (starRingEnd 𝕜) (peterWeylCoeff models f x) * peterWeylCoeff models g x

The products of the conjugated Peter-Weyl coefficients of f with those of g are summable.

theorem TauCeti.hasSum_norm_sq_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : HasSum (fun (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) => ‖peterWeylCoeff models f x‖ ^ 2) (‖f‖ ^ 2)

Norm-square Parseval for the Peter-Weyl basis. The squared norms of the Fourier coefficients of f sum to ‖f‖², as a convergent series.

theorem TauCeti.tsum_norm_sq_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ∑' (x : (i : ι) × Fin (models i).dim × Fin (models i).dim), ‖peterWeylCoeff models f x‖ ^ 2 = ‖f‖ ^ 2

Norm-square Parseval for the Peter-Weyl basis (tsum form).

theorem TauCeti.summable_norm_sq_peterWeylCoeff {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : Summable fun (x : (i : ι) × Fin (models i).dim × Fin (models i).dim) => ‖peterWeylCoeff models f x‖ ^ 2

The squared Peter-Weyl Fourier coefficients of an L² function are summable.

A skeleton exists

@[instance_reducible]

instance TauCeti.IrrepModel.instSetoid (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] : Setoid (IrrepModel 𝕜 G)

Unitary equivalence of models. Two models are equivalent when some linear isometry equivalence of their carriers transports one representation onto the other; by ContRepresentation.congr_refl and ContinuousLinearEquiv.congr_congr this is an equivalence relation.

Asking the carriers to be the standard spaces is what makes this a relation on a type, so that one representative per class may be chosen; on "all irreducible unitary representations on all inner product spaces" there is no such type to quotient.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.IrrepClass (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] : Type (max u_1 u_2)

The unitary dual of G in its standard models: the models of finite-dimensional irreducible unitary continuous representations, up to unitary equivalence. This is the index of the Peter-Weyl basis.

Equations

• TauCeti.IrrepClass 𝕜 G = Quotient (TauCeti.IrrepModel.instSetoid 𝕜 G)

noncomputable def TauCeti.IrrepClass.model {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] (i : IrrepClass 𝕜 G) : IrrepModel 𝕜 G

The model chosen in a class. Choice enters exactly here, and only to pick a representative of an equivalence class; everything the representative carries -- the carrier, the orthonormal basis, the representation -- is pinned by TauCeti.IrrepModel.

Equations

• i.model = Quotient.out i

theorem TauCeti.isIrrepSkeleton_model (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsAlgClosed 𝕜] : IsIrrepSkeleton IrrepClass.model

A skeleton of the unitary dual exists: the chosen representatives of the unitary equivalence classes form one.

Pairwise inequivalence is the substance. Distinct classes are inequivalent unitarily by construction, and ContRepresentation.exists_linearIsometryEquiv_congr_eq upgrades that to inequivalence outright, since between irreducible unitary representations every intertwining isomorphism can be rescaled to an isometry. Exhaustion is then the tautology that every model lies in its own class.

noncomputable def TauCeti.stdPeterWeylBasis (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : HilbertBasis ((i : IrrepClass 𝕜 G) × Fin i.model.dim × Fin i.model.dim) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The Peter-Weyl theorem, unconditionally. The normalized matrix coefficients of the models chosen in the unitary equivalence classes are a Hilbert basis of L²(G), indexed by Σ i, Fin (IrrepClass.model i).dim × Fin (IrrepClass.model i).dim. No skeleton is assumed: isIrrepSkeleton_model supplies one.

TauCeti.coe_stdPeterWeylBasis identifies the elements of this basis with TauCeti.peterWeylFamily IrrepClass.model.

Equations

• TauCeti.stdPeterWeylBasis 𝕜 G = TauCeti.peterWeylBasis ⋯

@[simp]

theorem TauCeti.coe_stdPeterWeylBasis (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : ⇑(stdPeterWeylBasis 𝕜 G) = peterWeylFamily IrrepClass.model

The unconditional Peter-Weyl basis is the normalized matrix coefficients of the chosen representatives. As for TauCeti.coe_peterWeylBasis, its elements are the L² classes represented by the functions g ↦ √(dim V_i) · ⟪(IrrepClass.model i).rep g e_a, e_b⟫.

@[simp]

theorem TauCeti.stdPeterWeylBasis_repr_apply (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) (x : (i : IrrepClass 𝕜 G) × Fin i.model.dim × Fin i.model.dim) : ↑((stdPeterWeylBasis 𝕜 G).repr f) x = peterWeylCoeff IrrepClass.model f x

A coordinate in the unconditional Peter-Weyl basis is its explicit Fourier coefficient.