I'm giving some lectures on the trace formula. Here's something I proved in the last lecture. Let $G$ be a locally compact Hausdorff unimodular topological group (e.g. a reductive Lie group), let $\Gamma$ be a discrete subgroup with $\Gamma\backslash G$ compact, and let $H$ be $L^2(\Gamma\backslash G)$, considered as a representation of $G$ via the right regular action. Then $H$ is a Hilbert space direct sum $H=\oplus m_\pi\pi$ with $\pi$ running through irreducible unitary Hilbert space reps of $G$ and each $m_\pi<\infty$.
Although I don't think I need it for my course, it seems to me that all I really used about $H$ was that it was a unitary Hilbert space rep of $G$ and that if $f\in C_c(G)$ (continuous functions on $G$ with compact support) then (fixing a Haar measure on $G$) the induced action of $f$ on $H$ is a Hilbert-Schmidt operator. I hope that's right because I'm no expert! The point is that you can use a kernel function argument to prove that if $H=L^2(\Gamma\backslash G)$ as above then each $f$ acts via a Hilbert-Schmidt operator, but that's all you seem to need in the proof, which now goes through for any $H$ with this property.
I am minded to actually revisit the proof and remark that the arguments all (seem to) go through in this generality---not least because I'm not sure in what generality I'll need this decomposition later.
I am also minded to make the following definition:
Definition: a unitary Hilbert space rep of $G$ is Hilbert-Schmidt if each $f\in C_c(G)$ acts via a Hilbert-Schmidt operator.
Then the theorem is that Hilbert-Schmidt reps decompose into direct sums of irreps each occurring with finite multiplicity.
I am not at all sure that this is standard terminology though! Is there standard terminology to describe such reps? That's the question! Even less mathematical: is $L^2(\Gamma\backslash G)$ a representation which has some standard property $P$ (I want $P$ to be "Hilbert-Schmidt!") and the real theorem is that every rep with property $P$ decomposes into irreps each occurring with finite multiplicity?
Finally a technical point: if $H$ is a unitary rep of $G$ and $f\in C_c(G)$ then I want to define an action of $f$ on $H$ by $fv=\int_Gf(g)gv dv$. The question is how to give this integral a formal definition. Initially I had got the following definition in my mind: $fv$ is the unique element of $H$ with the property that $(fv,w)=\int_Gf(g)(gv,w) dg$ for all $w$. But now I realise there might be a "genuine" definition of $fv$ involving approximating $f$ by step functions and so on and so on. Am I right?