Positive-definite function on a group

Summary

A positive-definite function on a group $G$ is a complex function $\varphi$ on $G$ with the following property. For all $g_1, \dots, g_n \in G$, the matrix $\big(\varphi(g_i^{-1}g_j)\big)_{i,j}$ is positive semidefinite. The diagonal matrix coefficients $g \mapsto \ip{\pi(g)v}{v}$ of unitary representations are positive-definite, and conversely every continuous positive-definite function arises in this way. This correspondence links functions on a group with its representations, and it underlies Bochner's theorem and the Gelfand–Raikov theorem.