LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

No-return sets have disjoint null preimage towers

Statement

Let $(X, A, μ, T)$ be a measure-preserving system with $μ (X) < \infty$ . For $E \in A$ put $W = E ∖ ⋃_{n \geq 1} T^{- n} E$ . Then the measurable sets $T^{- n} W$ , $n \geq 0$ , are pairwise disjoint and all have measure zero.

Facts & Assumptions

[F1]

Nonnegative iterates preserve the original measure; only that choice-free clause is used. Compositions, iterates and completions preserve invariance.

[F2]

Countable additivity gives finite additivity by padding with empty sets. Measures on sigma-algebras.

[F3]

The measure of a measurable subset is bounded by that of its ambient set. Measures are monotone.

Proof

Given: Let $(X, A, μ, T)$ be a measure-preserving system with $μ (X) < \infty$ . For $E \in A$ put $W = E ∖ ⋃_{n \geq 1} T^{- n} E$ . Then the measurable sets $T^{- n} W$ , $n \geq 0$ , are pairwise disjoint and all have measure zero.

1.1

Each $T^{n}$ is measurable and preserves $μ$ , so $W$ and every $T^{- n} W$ are measurable and $μ (T^{- n} W) = μ (W)$ . Here $T^{0}$ is the identity.

F1given

2.1

For $0 \leq i < j$ , membership of $x$ in both $T^{- i} W$ and $T^{- j} W$ would give $T^{i} x \in W \subseteq E$ and $T^{j - i} (T^{i} x) \in W \subseteq E$ . This contradicts the absence of every positive return from $W$ . Thus the tower sets are pairwise disjoint.

step 1.1given

3.1

For every positive integer $N$ , finite additivity and monotonicity give $N μ (W) = μ (⋃_{n = 0}^{N - 1} T^{- n} W) \leq μ (X)$ . Since the right side is finite, a positive $μ (W)$ would violate this bound for an integer $N > μ (X) / μ (W)$ . Hence $μ (W) = 0$ , and step 1.1 makes every tower level null. This also covers $E = \emptyset$ and $μ (X) = 0$ .

step 1.1step 2.1F2F3algebra∎

Depends on

Used by

Poincare recurrence for finite measure-preserving systems Theorem

Dependency tree · two levels

12 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

E–W Theorem 2.11 p.21 (standard reference, not scraped)