ExampleConstruction: Literature-sourcedVerification: 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.

Canonical compact-group decompositions are atomic Hilbert sums

Example

Assume the Axiom of Choice. Let $K$ be a second-countable compact group with normalized Haar measure and let $(π, H)$ be a strongly continuous unitary representation on a separable complex Hilbert space. Its canonical isotypic decomposition is $π ≅ ⨁_{α \in I} m_{α} π_{α},$ with $I \subseteq \hat{K}$ at most countable, $π_{α}$ finite dimensional and $m_{α} \in {1, 2, \dots, \infty}$ . In fact $\hat{K}$ is countable. Give it its discrete sigma-algebra and counting measure, and put $H_{α} = C^{m_{α}} \otimes V_{α}$ for occurring classes, where $C^{\infty}$ means $ℓ^{2} (N)$ , and $H_{α} = 0$ for the others. This measurable field realizes $π$ as the atomic direct integral of $m_{α} π_{α}$ over the full dual. Its Hilbert space is the completed square-summable orthogonal sum. For the left regular representation $m_{α} = \dim V_{α}$ .

Facts & Assumptions

[F1]

The compact corollary supplies the canonical countable isotypic Hilbert decomposition and its regular multiplicities (Compact groups are type I and their direct integrals collapse to discrete Hilbert sums).

[F2]

The compact dual is the set of finite-dimensional irreducible classes, and Peter--Weyl assigns every class a nonzero coefficient block in $L^{2} (K)$ ; distinct blocks are orthogonal (The unitary dual of a compact group, Peter-Weyl decomposition of the regular representation).

[F3]

A sigma-finite countably generated measure space has separable real $L^{2}$ under Countable Choice (If $μ$ is sigma-finite and $A$ is countably generated, then $L^{p} (μ)$ is separable for $1 \leq p < \infty$ ). AC implies Countable Choice (The Axiom of Choice, AC implies DC implies countable choice).

[F4]

A countable fundamental family defines a measurable Hilbert field, and its direct integral consists of measurable sections with integrable squared norm, modulo Borel null sets. A measurable field of unitary representations acts fibrewise (Measurable Hilbert field from a countable fundamental family, Direct integral of a measurable Hilbert field, Direct integrals of unitary representations). The Hilbert direct sum uses square-summable components (Hilbert direct sums of unitary representations).

Verification

Given: AC, $K$ , normalized Haar measure, and $(π, H)$ as in the Example.

1.1F2F3choose

A countable open base generates the Borel sigma-algebra of $K$ , and normalized Haar measure is finite. By [F3] real $L^{2} (K)$ has a countable dense subset $D$ ; the set $D + i D$ is countable and dense in complex $L^{2} (K)$ , since real and imaginary parts can be approximated separately. Choose a unit vector in each nonzero Peter--Weyl coefficient block [F2]. These vectors are orthogonal, so pairwise disjoint balls of radius $1 / 3$ each meet a countable dense set. Assigning the first dense point in each ball proves that $\hat{K}$ is at most countable.

2.1F1F4step 1.1construct

Use [F1] to choose the representatives and multiplicity spaces stated above. The countable dual with discrete metric is complete and separable, hence standard Borel, and its counting measure is sigma-finite. Choose an orthonormal basis in each nonzero separable fibre and enumerate all pairs consisting of an atom and a basis vector. The section associated with a pair equals that vector at its atom and zero elsewhere. Their Gram coefficients are measurable and their values span densely at each atom, so they form a countable fundamental family in [F4]; if all fibres are zero, use a sequence of zero sections. Every section is measurable because every scalar function on a countable discrete space is measurable. For fixed $k \in K$ , all matrix coefficients of the fibre action are likewise measurable.

3.1F1F4step 2.1∎

Counting integration gives $∥ ξ ∥^{2} = \sum_{α \in \hat{K}} ∥ ξ (α) ∥^{2}$ , and its only null subset is empty. Thus the direct integral is exactly the completed Hilbert direct sum, with precisely the isotypic action of [F1]. This action is strongly continuous: approximate a vector by its finitely many nonzero coordinates, use continuity on those coordinates, and bound the remaining displacement by twice the tail norm. The regular multiplicity assertion follows from [F1], including its conjugate-class reindexing convention.

Remarks

The full-dual counting presentation is redundant at classes outside $I$ : these are positive-measure atoms with zero Hilbert fibre. The canonical effective measure class is supported on the occurring set $I$ ; equivalently give zero measure to $\hat{K} ∖ I$ , or discard those zero-carrier atoms, before applying uniqueness results requiring nonzero fibres.

“Atomic” describes the effective canonical isotypic model. It does not force an original redundant parameter measure to be atomic: the constant trivial one-dimensional representation over a nonatomic probability interval integrates to the trivial representation on $L^{2} ([0, 1])$ , a countably infinite multiple of the trivial irreducible. Nor is a countable Hilbert sum merely its algebraic finite-support subspace.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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) (standard reference, not scraped)