Cyclic unitary representation of a positive-definite function (source code)

= Cyclic unitary representation of a positive-definite function
{title2=$p(x)=\langle U_xv,v\rangle$}

For an Abelian group, on finite formal sums of group points, define $\langle[x],[y]\rangle=p(xy^{-1})$, with the first variable linear. Quotient by the null space of this <positive semidefinite> form and complete to a <Hilbert space>. Left translation is unitary, and $v=[e]$ generates a dense span of translated vectors. For continuous $p$, the equality $\|U_x[y]-[y]\|^2=2(p(e)-\operatorname{Re}p(x))$ gives <strong continuity>. This realizes $p$ as a <matrix coefficient> without assuming its integral representation.