Spectral measure of a Koopman observable ($⟨U^{n}f,f⟩=\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 $\Vert f{\Vert }_2^2$, and its atoms are squared norms of projections onto Koopman operator eigenspaces, including for noninvertible transformations.