= Spectral measure of a Koopman observable
{title2=$\langle U^nf,f\rangle=\int e^{2\pi int}\,d\sigma_f(t)$}
The finite positive measure representing an observable's autocorrelation sequence by the <Bochner–Herglotz theorem>. For a probability <measure-preserving system>, the <Koopman operator> is an <isometry>, so its forward autocorrelations, extended by complex conjugation to negative indices, form a <positive-definite function> on $\mathbb Z$. The measure has mass $\|f\|_2^2$, and its atoms are squared norms of projections onto <Koopman operator> eigenspaces, including for noninvertible transformations.
Back to article page
