LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

A measurable direct integral of unitary representations is strongly continuous

Statement

Assume the Axiom of Choice. Let $G$ be a second-countable locally compact Hausdorff group, let $(X, B, μ)$ be a sigma-finite standard-Borel measure space, let $(H_{x}, e_{n} (x))_{x \in X}$ be a measurable complex Hilbert field with countable fundamental family and direct integral $H = \int_{X}^{\oplus} H_{x} d μ (x)$ , and let $(π_{x})_{x \in X}$ be a measurable field of strongly continuous unitary representations of $G$ in the sense of Direct integrals of unitary representations, with direct integral $π = \int_{X}^{\oplus} π_{x} d μ (x)$ . Then $g \mapsto π (g)$ is strongly continuous: whenever $g_{k} \to g$ in $G$ , $π (g_{k}) \to π (g)$ in the strong operator topology. Equivalently, $π$ is a strongly continuous unitary representation of $G$ on $H$ (Strongly continuous unitary representations, invariant linear subspaces and intertwiners).

Facts & Assumptions

[F1]

For each fixed $g \in G$ , the field $x \mapsto π_{x} (g)$ is weakly measurable and induces the unitary operator $π (g)$ on $H$ (Direct integrals of unitary representations, Measurable and decomposable operator fields, Measurable essentially bounded operator fields act decomposably).

[F2]

Each $π_{x} (g)$ is unitary. Thus $∥ π_{x} (g) v ∥ = ∥ v ∥$ on every nonzero fibre, and on a zero fibre both sides are zero (Direct integrals of unitary representations, Strongly continuous unitary representations, invariant linear subspaces and intertwiners).

[F3]

A weakly measurable essentially bounded operator field sends every measurable section to a measurable section under its pointwise action (Measurable essentially bounded operator fields act decomposably).

[F4]

The direct-integral norm is $∥ [η] ∥_{H}^{2} = \int_{X} ∥ η (x) ∥_{H_{x}}^{2} d μ (x)$ (Direct integral of a measurable Hilbert field).

[F5]

For every $x$ , $g \mapsto π_{x} (g)$ is a strongly continuous representation (Direct integrals of unitary representations, Strongly continuous unitary representations, invariant linear subspaces and intertwiners).

[F6]

If measurable functions converge pointwise almost everywhere and are dominated by one integrable function, their integrals converge (Dominated convergence).

[F7]

Second countability means having an at most countable basis (Second countability: an at most countable basis for the topology), and every second-countable space is first countable (Every second countable space is first countable).

[F8]

AC (The Axiom of Choice) implies Countable Choice (AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Assuming Countable Choice, sequential continuity at a point is equivalent to continuity at that point on a first-countable domain (Assuming Countable Choice, in a first countable space sequential closure equals closure and sequential continuity at a point equals continuity there, Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).

[F9]

The fibre norm satisfies the triangle inequality (The inner-product norm is definite, homogeneous, and satisfies the triangle inequality).

[F10]

A sequence of operators converges in the strong operator topology exactly when it converges in norm on every fixed vector (Strong and weak operator topologies).

[F11]

Measurable sections are closed under pointwise linear combinations and have measurable pointwise norms (Measurable sections have measurable pointwise inner products).

Proof

technique · dominated convergence on each orbit vector, followed by the first-countable sequential-continuity criterion

Given: The field, its direct integral, and the hypotheses in the statement.

1.1F1F2F3F5F11

Fix $ξ \in H$ , choose a measurable square-integrable representative $x \mapsto ξ (x)$ , and let $g_{k} \to g$ in $G$ . For each $k$ , the weakly measurable fields $x \mapsto π_{x} (g_{k})$ and $x \mapsto π_{x} (g)$ have norms at most $1$ by [F1,F2], so [F3] makes $η_{k} (x) : = π_{x} (g_{k}) ξ (x)$ and $η (x) : = π_{x} (g) ξ (x)$ measurable sections. By [F11], $η_{k} - η$ is measurable and its squared norm is measurable. For every $x$ , strong continuity of the fibre representation gives $∥ η_{k} (x) - η (x) ∥ \to 0$ by [F5]. Thus these measurable functions converge pointwise to zero.

2.1F2F4F6F9F11step 1.1

Unitarity [F2] and the fibre norm triangle inequality [F9] give $0 \leq ∥ η_{k} (x) - η (x) ∥^{2} \leq 4 ∥ ξ (x) ∥^{2}$ for every $x$ , including zero fibres. The majorant is integrable because $ξ \in H$ and [F4] gives $\int_{X} ∥ ξ (x) ∥^{2} d μ (x) = ∥ ξ ∥_{H}^{2} < \infty$ . Applying dominated convergence [F6] and then the direct-integral norm formula [F4] yields $∥ π (g_{k}) ξ - π (g) ξ ∥_{H}^{2} = \int_{X} ∥ η_{k} (x) - η (x) ∥^{2} d μ (x) \to 0$ . Thus every orbit map is sequentially continuous.

3.1F7F8F10step 2.1∎

The group $G$ is first countable by [F7]. The stated AC hypothesis gives Countable Choice by [F8], so the first-countable criterion in [F8] turns sequential continuity of each orbit map into continuity. Hence $g \mapsto π (g) ξ$ is continuous for every $ξ \in H$ , which is strong continuity of $π$ . Conversely, continuity of each orbit map implies its sequential continuity, also by [F8]; by [F10], this is equivalent to $π (g_{k}) \to π (g)$ in the strong operator topology. This proves the stated equivalence.

Boundary cases

If $X = \emptyset$ , if $μ (X) = 0$ , or if every fibre is zero, then $H = {0}$ and the unique integrated representation is strongly continuous; the proof above also applies with $ξ = 0$ . A one-point measure base and a trivial group are covered by the same calculation, and constant sequences $g_{k} = g$ give zero difference. There is no endpoint parameter in the assertion. The statement's sequential-continuity/continuity equivalence has both directions proved in step 3.1; the direction from continuity to sequential continuity uses no choice, while the reverse direction uses AC only through Countable Choice. No additional Choice is used in the dominated-convergence estimate.

Source qualifications

Bekka–de la Harpe, Chapter 1 §1.G, printed p. 61 (PDF p. 60), states that the direct-integral homomorphism is strongly continuous and cites Dixmier–von Neumann, Proposition 18.7.4, for that assertion. The passage does not provide the proof. The measurable-section action and direct-integral norm convention are laid out immediately before it in Definitions 1.G.3–1.G.4, printed pp. 60–61. This item supplies its own proof from fibrewise strong continuity, the integrable bound $4 ∥ ξ (x) ∥^{2}$ , dominated convergence, and the explicitly choice-dependent first-countable criterion; the citation is context, not a substitute for that argument.

Depends on

Used by

Non-type-I groups have non-smooth irreducible disintegration Theorem

Dependency tree · two levels

89 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

Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (arXiv:1912.07262v1, 16 December 2019; author-hosted complete book draft) (standard reference, not scraped)