CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Each vector has at most countably many nonzero isotypic components

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a compact Hausdorff group and let $π$ be a strongly continuous unitary representation of $K$ on a complex Hilbert space $H$ , with isotypic decomposition $H = {⨁^{^}}_{σ \in \hat{K}} H_{(σ)}$ (Unitary representations of compact groups are discrete Hilbert sums of irreducibles). For every $v \in H$ the set ${σ \in \hat{K} : v_{(σ)} \neq 0}$ of classes whose isotypic component meets $v$ nontrivially is at most countable, where $v_{(σ)}$ is the orthogonal projection of $v$ to $H_{(σ)}$ . In particular each single $f \in L^{2} (K)$ has nonzero components in at most countably many isotypic summands of the Peter-Weyl decomposition (Peter-Weyl decomposition of the regular representation). No countability of $\hat{K}$ and no countability of a Hilbert basis of $H$ is asserted.

Facts & Assumptions

[F1]

The isotypic decomposition of an arbitrary representation: $H = {⨁^{^}}_{σ \in \hat{K}} H_{(σ)}$ is a Hilbert direct sum of pairwise orthogonal closed invariant subspaces, the $H_{(σ)}$ are the ranges of the orthogonal projections $P_{σ}$ , and every $σ$ with $H_{(σ)} \neq {0}$ occurs as the class of a subrepresentation. (Unitary representations of compact groups are discrete Hilbert sums of irreducibles, Hilbert direct sums of unitary representations)

[F2]

For a family $(x_{i})_{i \in I}$ in a Hilbert space whose squared norms have finite finite-subset-supremum $S = \sum_{i} ∥ x_{i} ∥^{2} < \infty$ , the set ${i : x_{i} \neq 0}$ is at most countable: for each $n \geq 1$ the set $F_{n} = {i : ∥ x_{i} ∥ > 1 / n}$ is finite, because a nonempty finite subset $F \subseteq F_{n}$ contributes more than $∣ F ∣ / n^{2}$ to $S$ while a finite subsum never exceeds $S$ , so every finite subset of $F_{n}$ has at most $n^{2} S$ elements and hence $F_{n}$ itself is finite; the support is the countable union of the $F_{n}$ , at most countable by Countable Choice supplied by AC. (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Hilbert space)

[F3]

For $v$ in the Hilbert direct sum, the components satisfy $∥ v ∥^{2} = \sum_{i} ∥ v_{i} ∥^{2}$ in the finite-subset-supremum convention, and the component in the summand $H_{(σ)}$ is the orthogonal projection $v_{(σ)} = P_{σ} v$ . (Hilbert direct sums of unitary representations, Unitary representations of compact groups are discrete Hilbert sums of irreducibles)

[F4]

The regular representation $λ$ of $K$ on $L^{2} (K)$ has Peter-Weyl decomposition $L^{2} (K) = {⨁^{^}}_{π \in \hat{K}} M_{π}$ , where $M_{π}$ is the span of the matrix coefficients of $π$ and $λ ∣_{M_{π}} ≅ d_{π} \overline{π}$ , so the same countable-support conclusion applies to the components of a single $L^{2}$ class. (Peter-Weyl decomposition of the regular representation, Parseval equivalences for an orthonormal family)

Proof

Given: AC, a compact Hausdorff group $K$ , a strongly continuous unitary representation $π$ of $K$ on $H$ , and a vector $v \in H$ .

1.1F2

Let $(x_{i})_{i \in I}$ be any family in a Hilbert space with $\sum_{i} ∥ x_{i} ∥^{2} < \infty$ in the finite-subset-supremum convention [F2]; for each $n \geq 1$ put $F_{n} = {i : ∥ x_{i} ∥ > 1 / n}$ and let $F \subseteq F_{n}$ be a nonempty finite subset with $m$ elements: then $\sum_{i \in F} ∥ x_{i} ∥^{2} > m / n^{2}$ , while every finite subsum is at most the supremum $S = \sum_{i} ∥ x_{i} ∥^{2}$ , so $m < n^{2} S$ ; consequently every finite subset of $F_{n}$ has at most $n^{2} S$ elements, which forces $F_{n}$ to be finite (an infinite $F_{n}$ would contain a finite subset with at least $n^{2} S + 1$ elements), and the support ${i : x_{i} \neq 0} = ⋃_{n \geq 1} F_{n}$ is at most countable by Countable Choice supplied by AC.

2.1F1F3F4step 1.1∎

Applying step 1.1 to the components of $v$ in the Hilbert direct sum $H = {⨁^{^}}_{σ \in \hat{K}} H_{(σ)}$ is legitimate because $\sum_{σ} ∥ v_{(σ)} ∥^{2} = ∥ v ∥^{2} < \infty$ by [F3], so the set of $σ$ with $v_{(σ)} \neq 0$ is at most countable and the component is the orthogonal projection $P_{σ} v$ ; and applying it to the components of a class $f \in L^{2} (K)$ in the Peter-Weyl decomposition $L^{2} (K) = {⨁^{^}}_{π \in \hat{K}} M_{π}$ of [F4] gives the stated special case, because the squared norms of the components have finite sum equal to $∥ f ∥_{2}^{2}$ . No countability of the index sets $\hat{K}$ or of a Hilbert basis is used or asserted. The Axiom of Choice is inherited through the decomposition theorems and the cited suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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

Emmanuel Kowalski, An Introduction to the Representation Theory of Groups (author-hosted draft, 338 pp.) (standard reference, not scraped)
David A. Vogan, Review of Harmonic Analysis on Compact Groups (MIT lecture notes, 12 pp.) (standard reference, not scraped)