Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Weak mixing is equivalent to absence of nonconstant eigenfunctions

Statement

Assume AC. For a measure-preserving transformation T on a completed Lebesgue probability space the following are equivalent: (i) weak mixing in the absolute-Cesaro sense; (ii) no nonconstant complex L2 eigenfunction; (iii) ergodicity of T×T on the completed product. Equivalently, for each pair f,g∈L2 its centered correlations tend to zero outside a set of integers of natural density zero; the exceptional set may depend on the pair. Invertibility is not required.

Facts & Assumptions

[F1]

Eigenfunctions and the closed zero-mean space H0 have the stated conventions Eigenfunction for a probability system.

[F2]

Cesaro averages of an isometry converge to the orthogonal projection onto its fixed space Hilbert cesaro averages converge to the fixed subspace.

[F4]

An invariant kernel gives compact intertwiners commuting with U, and zero marginals give the stated nonzero restriction to H0 Invariant square integrable kernel produces a compact intertwiner.

[F5]

A nonzero invariant kernel with zero marginals gives a nonzero finite-dimensional invariant subspace of H0 Compact intertwiners produce finite dimensional invariant subspaces.

[F6]

Such a subspace contains a nonconstant eigenfunction Nonzero finite dimensional complex invariant subspaces have unitary eigenvectors.

[F7]

Ergodicity is equivalent to constancy a.e. of invariant measurable complex functions Equivalent invariant-set and invariant-function criteria for ergodicity.

[F8]

Weak mixing is equivalent to absolute-Cesaro convergence of centered complex L2 correlations Mixing correlations extend to L2 functions.

[F9]

Weak mixing keeps the absolute value inside the average Strong and weak mixing on a probability space.

[F10]
[F11]
[F12]

On a finite measure space, preservation on a generating pi-system implies preservation on the generated sigma-algebra Measure preservation can be checked on a generating pi-system.

[F13]

The local canonical-simple and monotone-convergence argument proves that pullback by a measure-preserving map is a linear isometry on complex L2 Eigenfunction for a probability system.

[F14]

Every set in a completion has the form A∪N, where A is base measurable and N is contained in a base null set The completion domain and proposed completed set function of a measure space.

[F15]

A square-integrable kernel defines a compact operator, and the zero operator has only the zero kernel Square integrable kernels define bounded compact integral operators.

Proof

Given: The completed Lebesgue probability system and AC.

1.1F1F8F9

If f is a nonconstant eigenfunction, center it when its eigenvalue is one; when the eigenvalue differs from one its mean already vanishes. This gives a nonzero f0∈H0 with Unf0=λnf0 and ∣λ∣=1. Thus ∣⟨Unf0,f0⟩∣=∥f0∥2>0 for every n. Its absolute-Cesaro average cannot tend to zero. F8–F9 therefore prove (i) implies (ii).

1.2F12F13F14

On every measurable rectangle E×F, the product map S=T×T satisfies (μ×μ)(S−1(E×F))=μ(T−1E)μ(T−1F)=μ(E)μ(F). The inverse images of rectangles are measurable, so the sets whose inverse images are product measurable form a sigma-algebra; hence S is measurable because rectangles generate the product sigma-algebra. Rectangles together with X2 form a generating pi-system, and F12 makes S measure preserving on the uncompleted product. If A∪N is completed measurable as in F14, with N⊆Z and (μ×μ)(Z)=0, then S−1N⊆S−1Z and the latter is a base null set. Thus S−1(A∪N) is completed measurable and has the same completed measure as A∪N. Therefore S preserves the completed product, and F13 makes its Koopman operator W a complex L2 isometry.

2.1F1F4F5F6F7F10F11F15step 1.2

Assume (ii). Every invariant indicator is an eigenfunction of eigenvalue one unless zero, so it is constant a.e.; its set is null or conull. Thus T is ergodic. If Wk=k and k is nonconstant, subtract its total mean to make ∬k=0, still with k≠0. F15 gives a nonzero compact kernel operator K, while F4 gives KU=UK and K∗U=UK∗. Since U1=1, the images K1 and K∗1 are invariant L2 functions. Ergodicity makes both constant. Their means are ∬k=0 and its conjugate, respectively, by Fubini; hence both are zero. These are exactly the two zero-marginal conditions. F5 and F6 would then produce a nonconstant eigenfunction, contradicting (ii). Every W-fixed L2 class is consequently constant. In particular each product-invariant indicator is constant, so (iii) follows. The kernel is integrable because its L2 norm is finite and the product mass is one.

2.2F1F7F10step 1.1step 1.2

Assume (iii). If a nonconstant eigenfunction existed, center it as in step 1.1 to obtain f0≠0 of mean zero. Put F(x,y)=f0(x)f0(y)‾. Tonelli gives ∥F∥22=∥f0∥24>0, and Fubini gives ∬F=∣∫f0∣2=0. Its pullback is WF=∣λ∣2F=F; factor-null exceptional sets pull back to null subsets of the square by the completed-product preservation in step 1.2. Product ergodicity and F7 force F to be constant, and its zero mean forces that constant to be zero, a contradiction. Thus (iii) implies (ii).

3.1F1F2F7F10F11step 1.2step 2.2

Under (iii), F7 says the fixed space of W consists exactly of constants. For arbitrary f,g∈L2, let f0=f−(∫f)1, F=f0⊗f0‾ and G=g⊗g‾. As in step 2.2, these are in product L2 and F has integral zero. Its projection onto constants is therefore zero. Since step 1.2 proves that W is an isometry, F2 yields N−1∑n<NWnF→0 in norm, so its pairing with G tends to zero by Cauchy–Schwarz. Fubini computes ⟨WnF,G⟩=∣⟨Unf0,g⟩∣2: each factor f0∘Tn g‾ is integrable by Cauchy–Schwarz, and the absolute double integral is the square of its finite L1 norm.

4.1F8F9step 1.1step 1.2step 2.1step 2.2step 3.1

Finite Cauchy–Schwarz on the N real nonnegative numbers bn=∣⟨Unf0,g⟩∣ gives N−1∑n<Nbn≤(N−1∑n<Nbn2)1/2→0. The correlation here equals Cn(f,g) of F8 because U1=1. Thus F8 proves (i). Together with steps 1.1, 2.1 and 2.2 this closes all three implications. If f0=0 or g=0, both sides of the estimate are zero. The assumed AC supplies every cited projection, compactness and completion result that requires it; no spectral-measure construction is used.

5.1F8step 4.1∎

For completeness let an=∣Cn(f,g)∣, bounded by M=∥f−(∫f)1∥2∥g∥2. If its Cesaro mean tends to zero, each Ej={n:an>1/j} has density zero since ∣Ej∩[0,N)∣/N≤jN−1∑n<Nan. Choose Nj recursively as the least integer larger than Nj−1 such that this density is below 1/j for every N≥Nj; the convergence just proved ensures existence. Put D=⋃j≥1(Ej∩[Nj,Nj+1)). For Nj≤N<Nj+1, the increasing property Ei⊆Ej for i≤j implies D∩[0,N)⊆Ej∩[0,N), so D has density zero. Off D on its jth interval, an≤1/j, proving the claimed convergence. Conversely, if D has density zero and an→0 off D, choose N0 so that an<ε off D for n≥N0. Then N−1∑n<Nan≤MN0/N+M∣D∩[0,N)∣/N+ε. Its limsup is at most every positive ε, hence zero. This proves the pairwise density-zero equivalent criterion without asserting one exceptional set for all uncountably many pairs. Least integer cutoffs add no choice use.

Depends on

Used by

Dependency tree · two levels

56 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources