 Compact averaging of a rank-one operator

For a strongly continuous unitary representation of a compact group, this Bochner integral exists in the Hilbert-Schmidt norm and is a positive compact operator commuting with the representation. It is nonzero if $\xi \ne 0$, because $⟨K_{\xi }\xi ,\xi ⟩={\int }_G|⟨U_g\xi ,\xi ⟩{|}^{2}dg>0$. A nonzero eigenspace is finite-dimensional and invariant. Applying this on orthogonal complements yields an orthogonal direct sum of finite-dimensional irreducible representations, with no separability assumption on the represented Hilbert space.