LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Ergodic systems with regular orbits concentrate on one orbit

Statement

Assume AC. Let $(U, P)$ be an ergodic system of imprimitivity for a Borel action of a group $G$ on a standard Borel space $X$ , acting on a nonzero separable Hilbert space, and suppose the orbit equivalence relation of the action is regular: there is a countable family $E_{1}, E_{2}, \dots$ of $G$ -invariant Borel subsets of $X$ such that every orbit is the intersection of the sets $E_{n}$ that contain it. Equivalently, some countable family of invariant Borel sets separates distinct orbits, which is the condition that the orbit space is countably separated. Then there is an orbit $C \subseteq X$ with $P (X ∖ C) = 0$ .

Facts & Assumptions

Given: AC, the Borel $G$ -space $X$ , the ergodic system of imprimitivity $(U, P)$ on a nonzero separable Hilbert space, and a countable family $(E_{n})$ of invariant Borel sets as in the statement.

[F1]

$(U, P)$ is a strongly continuous unitary representation together with a PVM with $U_{g} P (E) U_{g}^{- 1} = P (g E)$ , and ergodicity means that every Borel $E$ with $U_{g} P (E) U_{g}^{- 1} = P (E)$ for all $g$ satisfies $P (E) = 0$ or $P (E) = I$ ; for invariant Borel $E$ one has $P (E)$ invariant (Systems of imprimitivity for a Borel $G$ -space, Left group actions, transitive actions, and faithful actions, A measurable function between measurable spaces).

[F2]

Projections in the range of a PVM satisfy $P (A) P (B) = P (A \cap B)$ ; a projection $P (A)$ is zero exactly when the scalar measures $E_{x} (A) = ⟨ P (A) x, x ⟩$ vanish for all $x$ ; and $P$ is strongly countably additive (Scalar and complex measures from a pvm, Bounded borel pvm integral).

[F3]

$X$ is standard Borel, so Borel sets are closed under countable unions and intersections; invariance of a Borel set $E$ means $g E = E$ for all $g$ and implies invariance of its complement (Standard Borel spaces).

[F4]

AC is the standing hypothesis; it is inherited from the ambient system (The Axiom of Choice, Multiplicity model of a projection-valued measure over a standard Borel base).

Proof

technique · direct

Given: AC, the ergodic system $(U, P)$ and the countable invariant family $(E_{n})$ .

1.1F3

The two regularity formulations are equivalent. If every orbit is the intersection of the invariant Borel sets containing it, the family $(E_{n})$ separates distinct orbits: if $x, y$ lie in different orbits and $y$ belonged to every $E_{n}$ containing $x$ , then $y$ would lie in the intersection defining the orbit of $x$ . Conversely, adjoin the complements to a countable separating family and reenumerate it as $(E_{n})$ . Then for every $x$ the intersection $I_{x} = ⋂ {E_{n} : x \in E_{n}}$ is contained in the orbit of $x$ : a point $y \notin G x$ is separated from $x$ by some $E_{n}$ , and replacing $E_{n}$ by its complement if necessary (also invariant Borel by [F3]) gives $E_{n} ∋ x$ , $E_{n} ∌ y$ ; the reverse inclusion holds because each $E_{n}$ is invariant.

1.2F1

Each $P (E_{n})$ is $0$ or $I$ : since $E_{n}$ is invariant, $U_{g} P (E_{n}) U_{g}^{- 1} = P (g E_{n}) = P (E_{n})$ for every $g$ , so ergodicity applies.

2.1F2F3step 1.2

Define $F_{n} = E_{n}$ if $P (E_{n}) = I$ and $F_{n} = X ∖ E_{n}$ if $P (E_{n}) = 0$ ; each $F_{n}$ is invariant Borel and $P (F_{n}) = I$ . For $C : = ⋂_{n} F_{n}$ one has $X ∖ C = ⋃_{n} (X ∖ F_{n})$ with $P (X ∖ F_{n}) = 0$ ; strong countable additivity gives $P (⋃_{n} (X ∖ F_{n})) = \lim_{N} P (⋃_{n \leq N} (X ∖ F_{n}))$ and the scalar measures of each finite union vanish, so $P (X ∖ C) = 0$ .

3.1step 1.1step 2.1F3

$C$ is nonempty because $P (C) = I \neq 0$ on the nonzero Hilbert space, and $C$ is invariant. Choose $x \in C$ . Its orbit satisfies $G x \subseteq C$ since $C$ is invariant. Conversely, if $y \in C$ and $E_{n} ∋ x$ , then either $F_{n} = E_{n}$ , in which case $y \in C \subseteq E_{n}$ ; or $F_{n} = X ∖ E_{n}$ and $x \notin E_{n}$ , a contradiction. Hence $y$ belongs to every $E_{n}$ containing $x$ , so by regularity $y \in G x$ . Therefore $C = G x$ is a single orbit and is Borel as a countable intersection.

4.1step 2.1step 3.1F4∎

Combining [step 2.1] and [step 3.1]: the invariant Borel set $C$ is exactly one orbit and $P (X ∖ C) = 0$ , which is the concentration claim.

Depends on

Used by

Mackey little-group reduction for an abelian normal subgroup Corollary

Dependency tree · two levels

57 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

G. W. Mackey, Imprimitivity for Representations of Locally Compact Groups I, PNAS 35 (1949) 537-545 (Internet Archive capture of the PubMed Central scan) (standard reference, not scraped)
V. S. Sunder, Notes on the Imprimitivity Theorem (ISIBangalore/IMSc lecture notes, 22 pp.) (standard reference, not scraped)