OAI.ContinuousCircleWeight.main_theorem

The theorem states that the defined proposition MainStatement holds, namely that there exist an irrational θ with 0<θ<1, a continuous function f from the circle ℝ/ℤ to ℝ, unitaries U and V on the Hilbert space ℓ²(ℤ×ℤ; ℂ), and a vector e, such that the following hold. First, (U,V,e) is a tracial rotation for θ: VU = exp(2πiθ)·UV, the inner product ⟨e, U^m V^n e⟩ equals 1 when m=n=0 and 0 otherwise for all integers m,n, and the vectors U^m V^n e span a dense subspace. Second, 0≤f≤1 everywhere, and f vanishes at exactly one point z of the circle. Third, the Lebesgue-measure integral over the circle of the extended-real function negativeLog(f(x)), which is −log f(x) when f(x)≠0 and ∞ when f(x)=0, equals ∞, so f has divergent logarithmic integral. Fourth, writing the weighted rotation as W = U·f(V), where f(V) is the continuous functional calculus of V applied to f transported to the unit circle (and set to 0 off the circle), every projection p (self-adjoint idempotent) lying in the double commutant of {U,V} that satisfies (1−p)·W·p = 0 must be 0 or 1. Thus W has no nontrivial invariant projection in that double commutant.