The discrete Bochner–Herglotz theorem says that a sequence is a positive-definite function, meaning
if and only if there is a unique finite positive Borel measure on such that
The mass is . The necessity of positive definiteness follows by integrating .
For sufficiency, positive definiteness makes the relevant Gram matrices Hermitian positive semidefinite, so and . Define
Taking in the positive-definiteness condition gives , while . Moreover,
Thus the integrals against every trigonometric polynomial converge. These polynomials are uniformly dense in continuous functions on the circle: smooth periodic approximation followed by Fourier inversion for smooth functions gives this density. The uniform mass bound then makes the integrals against every continuous converge as well. Their limit is a positive linear functional with . The standard Riesz-Markov-Kakutani representation theorem gives a finite positive Borel measure with . The preceding coefficient computation proves its required Fourier coefficients. Finally, two such measures agree on all trigonometric polynomials, hence on all continuous functions by uniform density, and therefore are identical. This proves the Bochner–Herglotz theorem, including existence and uniqueness; if , the estimate gives the zero measure directly.
Now let be the Koopman operator on the complex L2 space of the probability measure-preserving system. We use , linear in the first entry. Since is an isometry, the sequence for , extended by , is positive-definite: its matrix is the Gram matrix of . The Bochner–Herglotz theorem gives its spectral measure of a Koopman observable .
We first prove exactly how an atom of a measure detects an eigenfunction. Fix and set
The mean ergodic theorem, applied to the isometry , says these averages converge in L2 space to the orthogonal projection onto . Its usual Hilbert-space proof works without invertibility: the orthogonal complement of is , and the averages of telescope to . The equality of the two kernels follows from being an isometry, by expanding when .
Expanding the averaged norm through the spectral measure of a Koopman observable gives
The integrand is at most one and converges to . By the dominated convergence theorem,
Thus a nonzero atom corresponds to a nonzero Koopman operator eigenfunction, with eigenvalue , in the cyclic spectral data of .
We also need the Wiener Fourier coefficient lemma, which here has a short proof. For any finite positive circle measure with coefficients ,
The bracket is bounded in absolute value by one and tends to the indicator of the diagonal . Another application of the dominated convergence theorem gives
In particular the limit is zero for an atomless measure.
Suppose there are no nonconstant Koopman operator eigenfunctions. For every in the mean-zero L2 space, all its projections vanish: a nonzero projection would be a nonconstant eigenfunction, since it has mean zero. Hence is atomless, and the Wiener Fourier coefficient lemma gives
The Cauchy-Schwarz inequality also gives vanishing averaged absolute autocorrelations. For two mean-zero observables , the sesquilinear polarization identity
then gives vanishing averaged absolute cross-correlations. Taking and proves
which is weak mixing.
Conversely, this set formulation of weak mixing extends to all pairs of mean-zero L2 space observables by finite-simple-function approximation and the uniform estimate . If and , the isometry property gives . If , invariance of the integral gives . If and is nonconstant, replace it by , a nonzero mean-zero eigenfunction. But in either case
for every , contradicting weak mixing. We have proved weak mixing is equivalent to absence of nonconstant eigenfunctions, including for noninvertible transformations.
Finally, the doubling map preserves normalized Lebesgue measure, as substitution on its two inverse branches shows. Let be an eigenfunction, , with Fourier coefficients . The Fourier basis calculation gives
Since , all odd coefficients vanish. Every nonzero integer is with odd, and repeated use of makes all nonzero coefficients vanish. Completeness of the Fourier basis then says is constant. Therefore the doubling map has no nonconstant eigenfunctions, and