TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Mixing is checkable on a generating pi-system

Statement

Let $(X, A, μ, T)$ be a measure-preserving probability system and $P$ a generating pi-system containing X. Strong mixing is equivalent to $d_{n} (A, B) \to 0$ for $A, B \in P$ . Weak mixing is equivalent to $N^{- 1} \sum_{n < N} ∣ d_{n} (A, B) ∣ \to 0$ for $A, B \in P$ , where $d_{n} (A, B) = μ (A \cap T^{- n} B) - μ (A) μ (B)$ .

Facts & Assumptions

[F1]

The two properties quantify convergence of correlations or their absolute averages over all measurable pairs Strong and weak mixing on a probability space.

[F2]

On a finite measure space every measurable set has arbitrarily accurate algebra approximants Approximation in symmetric difference by a generating algebra.

[F3]

The measure of a finite union is at most the sum of its measures Finite and countable subadditivity of measures.

[F4]

Integration of finite linear combinations of integrable functions is linear The Lebesgue integral is linear on $L^{1} (μ)$ .

Proof

Given: The objects and hypotheses in the statement.

1.1given

Let $C$ consist of finite Boolean combinations of members of $P$ . Each indicator of an atom of a finite Boolean partition is a product of factors $1_{P}$ and $1 - 1_{P}$ . Expanding the product expresses it as a finite integer linear combination of indicators of intersections of members of $P$ . Empty intersections are X, which lies in $P$ , and all other intersections lie in $P$ by the pi-system property. Finite sums of these atom indicators express every $1_{C}$ , $C \in C$ , in this way.

2.1F1step 1.1F4

Integration and multiplication of finite sums now express $d_{n} (C, D)$ as a finite linear combination $\sum_{j, k} a_{j} b_{k} d_{n} (P_{j}, Q_{k})$ . In the strong case each summand tends to zero. In the weak case the average of the absolute value is at most $\sum_{j, k} ∣ a_{j} b_{k} ∣ N^{- 1} \sum_{n < N} ∣ d_{n} (P_{j}, Q_{k}) ∣$ , which tends to zero. The respective test therefore holds on $C$ .

3.1F2step 2.1givenF3

The family $C$ is an algebra generating $A$ . For measurable A,B and $δ > 0$ , choose C,D in it with $μ (A △ C), μ (B △ D) < δ$ . Measure preservation gives $μ (T^{- n} (B △ D)) = μ (B △ D)$ by repeated pullback. Thus the difference of the intersection measures is bounded by the sum of these two errors. Also $∣ μ (A) μ (B) - μ (C) μ (D) ∣ \leq μ (A △ C) + μ (B △ D)$ , since all masses are at most one. Consequently $∣ d_{n} (A, B) - d_{n} (C, D) ∣ < 4 δ$ uniformly in n.

4.1F1step 2.1step 3.1∎

In the strong case the limsup of $∣ d_{n} (A, B) ∣$ is at most $4 δ$ . In the weak case the same bound holds for the limsup of its absolute Cesaro averages. Letting $δ$ decrease to zero proves the full respective property. Conversely either full property restricts to the pairs in $P$ by its definition.

Depends on

Used by

Dependency tree · two levels

17 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

Einsiedler–Ward Exercise 2.7.3(1)–(2), pp.52–53; local Boolean-algebra extension from a pi-system (standard reference, not scraped)