Characters are class functions in L²(G)

The character of a finite-dimensional continuous representation of a compact group is a class function: it is constant on conjugacy classes. Passing to L²(G) this becomes a statement about an almost-everywhere equivalence class, and the correct home for it is the closed subspace TauCeti.classFunctionLp of classes fixed by every conjugation.

This file proves that a continuous class function lands in that subspace, and specializes to characters. Together with the orthogonality relations of TauCeti/RepresentationTheory/Compact/Character/Basic.lean this says the irreducible characters form an orthonormal system inside classFunctionLp; that they are a Hilbert basis of it -- the compact-group form of "the irreducible characters are a basis of the class functions" -- needs the Peter-Weyl theorem and is proved in TauCeti/RepresentationTheory/Compact/Character/Basis.lean.

Main statements

• TauCeti.toLp_mem_classFunctionLp: a continuous class function on a compact group defines an element of classFunctionLp.
• ContRepresentation.characterLp_mem_classFunctionLp: the character of a finite-dimensional continuous representation is a class function in L²(G).

References

• Daniel Bump, Lie Groups, second edition, Chapter 2.

theorem TauCeti.toLp_mem_classFunctionLp {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} [NormedRing 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SecondCountableTopologyEither G E] (p : ENNReal) [Fact (1 ≤ p)] (F : C(G, E)) (hF : ∀ (g h : G), F (h * g * h⁻¹) = F g) : (ContinuousMap.toLp p (haarProb G) 𝕜) F ∈ classFunctionLp 𝕜 E p (haarProb G)

A continuous class function is a class function in Lp. A continuous function on a compact group that is constant on conjugacy classes has a class in Lp fixed by every conjugation.

theorem ContRepresentation.characterLp_mem_classFunctionLp {𝕜 : 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] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.characterLp hπ ∈ TauCeti.classFunctionLp 𝕜 𝕜 2 (TauCeti.haarProb G)

A character is a class function in L²(G). The class of the character of a finite-dimensional continuous representation of a compact group is fixed by every conjugation, the almost-everywhere form of its pointwise invariance on conjugacy classes.