We give a spectral proof of square-difference recurrence for finite colourings, proving the auxiliary results it uses. Extend the colouring arbitrarily to nonpositive integers, and let be the indicator of colour . By successively taking subsequences of the interval lengths, followed by a diagonal subsequence, we may arrange that all the limits
exist, for every integer . This uses only sequential compactness of bounded real sequences: list the countably many quantities, choose a convergent subsequence for each in turn, and take the diagonal. All limits below are along this common subsequence. We have , , and . Translating a fixed interval endpoint changes a normalized average by .
The sequence is a positive-definite function on . Indeed, for finitely many complex numbers ,
We next prove the required Bochner–Herglotz theorem for this sequence. The trigonometric polynomial
is nonnegative by positive definiteness, and its integral on the circle is . Thus is a probability measure. Such measures on a compact interval have a weakly convergent subsequence. For completeness, take a diagonal subsequence on all rational points of their nondecreasing distribution functions. The right-continuous extension of the limiting rational values is a distribution function and defines a probability measure by its interval increments. At its continuity points the original distribution functions converge, by sandwiching between rational endpoints. Approximating continuous functions by step functions with such endpoints proves convergence of their integrals. Identify the interval endpoints to obtain a measure on the circle. This proves the compactness of probability measures on a compact metric space in the case needed here.
For a fixed , the Fourier coefficient of is once . Taking the weak limit therefore supplies a positive probability measure such that
No spectral representation has been assumed without proof.
Its atom at zero has positive mass. For each ,
The last inequality is Cauchy-Schwarz on each colour's interval average. The integrand is at most one and tends to zero for every nonzero point of the circle, by the geometric-series formula, while it is one at zero. Bounded convergence gives
We also prove that quadratic phases with an irrational coefficient average to zero. For bounded by one, extended by zero, Cauchy-Schwarz applied to yields
This identity follows by expanding the square of the inner shifted sum and grouping pairs by their difference; it is the needed finite Van der Corput inequality for finite scalar sequences. If and is irrational, each fixed nonzero lag correlation is a geometric sum with frequency , hence is bounded independently of . The geometric bound follows from with . Dividing by and letting tend to infinity gives . Letting tend to infinity proves the asserted cancellation. Rational coefficients instead give periodic sequences and therefore have convergent averages.
Choose a finite set of rational points of the circle, including zero, such that the total mass of the remaining rational atoms is below . This is possible because the rational points are countable and is finite. Let be a common multiple of their denominators. For , for every integer . For irrational the preceding cancellation applies to ; at every other rational point the average exists by periodicity and has modulus at most one. Bounded convergence consequently gives
Here the inequality takes real parts; itself is real. Thus some has . By its definition as a limit of nonnegative averages, at least one actual positive has . The same colour occurs at both points, proving
The arbitrary extension to nonpositive integers played no role in this final pair.
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
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 . The measure has mass , and its atoms are squared norms of projections onto Koopman operator eigenspaces, including for noninvertible transformations.