Definition 5

Let $\varphi$ be a function of positive type on G. A Hilbert realization of $\varphi$ is a pair $(\varrho , x)$ where $\varrho$ is a unitary representation of G in a Hilbert space E and $x\in E$, such that $\varphi (g) =\langle x|\varrho (g)x\rangle$ for all $g\in G$.

If $x$ is a cyclic vector of $\varrho$, one says that this is a cyclic Hilbert realization of $\varphi$.