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

The circle: the Peter-Weyl basis is the integer characters

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $K = T = R / Z$ with its normalized Haar measure (The one-dimensional torus and its normalized Haar integral), a compact abelian Hausdorff group, and write $z^{n}$ for the continuous characters $[t] \mapsto \exp (2 π i n t)$ , $n \in Z$ ; each $z^{n}$ is a one-dimensional continuous unitary representation. Then:

every irreducible continuous unitary representation of $T$ is one-dimensional, and its normalized matrix coefficient is a continuous character (Schur lemma for complex unitary representations);
the characters ${z^{n} : n \in Z}$ form a complete orthonormal family of $L^{2} (T)$ (The trigonometric characters are orthonormal in $L^{2}$ of the torus, The trigonometric system is complete in $L^{2}$ of the torus);
hence the normalized coefficient family of The normalized matrix coefficients form an orthonormal basis of L2(K) equals ${z^{n} : n \in Z}$ : a complete orthonormal subfamily of an orthonormal basis is the whole basis, so no other irreducible classes occur. Therefore the unitary dual of $T$ is $Z$ realized by these characters, consistent with the general duality statement that compact abelian groups have discrete duals (The Pontryagin dual with the compact-open topology, Compact groups have discrete duals and discrete groups have compact duals, The multiplicative unit circle is a compact metrizable topological abelian group), and the Peter-Weyl decomposition of $L^{2} (T)$ is exactly the classical Fourier series decomposition ${⨁^{^}}_{n \in Z} C z^{n}$ . Parseval's identity and Fourier inversion are the classical Fourier statements (The Parseval identity for Fourier series); the example verifies the general theorem against the familiar model without reproving Pontryagin duality.

Facts & Assumptions

[F1]

$T$ is a compact metrizable topological abelian group and a compact Hausdorff group, so it carries a normalized Haar probability and the Peter-Weyl theory of the compact case applies to it. (The multiplicative unit circle is a compact metrizable topological abelian group, The one-dimensional torus and its normalized Haar integral)

[F2]

The characters $z^{n} ([t]) = \exp (2 π i n t)$ , $n \in Z$ , are continuous homomorphisms $T \to T$ ; they are orthonormal in $L^{2} (T)$ and their closed linear span is $L^{2} (T)$ . (The trigonometric characters are orthonormal in $L^{2}$ of the torus, The trigonometric system is complete in $L^{2}$ of the torus, Fourier coefficients and trigonometric polynomials on the torus)

[F3]

Schur's lemma: every bounded self-intertwiner of an irreducible strongly continuous unitary representation on a nonzero Hilbert space is a scalar multiple of the identity. (Schur lemma for complex unitary representations)

[F4]

The normalized coefficient family $B$ of the compact group is an orthonormal basis of $L^{2}$ , every irreducible continuous unitary representation of a compact group is finite dimensional, its class lies in the unitary dual, and matrix coefficients are $c_{v, w}^{π} (k) = ⟨ π (k) v, w ⟩$ . (The normalized matrix coefficients form an orthonormal basis of L2(K), The normalized irreducible matrix coefficient family, Matrix coefficient of a unitary representation)

[F5]

For an abelian group every $π (k)$ commutes with every $π (k^{'})$ ; a one-dimensional continuous unitary representation is a continuous character $χ : T \to T$ with $∣ χ (k) ∣ = 1$ for all $k$ . (Strongly continuous unitary representations, invariant linear subspaces and intertwiners, The Pontryagin dual with the compact-open topology)

[F6]

A complete orthonormal subfamily of an orthonormal basis is the whole basis: an element of the basis outside the subfamily is orthogonal to the closed span of the subfamily, which is the whole Hilbert space, hence is zero, contradicting unit norm. (Orthonormal families, complete orthonormal systems and Hilbert bases)

[F7]

If $G$ is a compact abelian topological group, its Pontryagin dual is discrete; the circle's Pontryagin dual is its set of continuous characters with the compact-open topology. (Compact groups have discrete duals and discrete groups have compact duals, The Pontryagin dual with the compact-open topology)

Verification

Given: AC, the compact abelian group $T = R / Z$ with normalized Haar measure, and the characters $z^{n}$ , $n \in Z$ .

1.1F1F3F4F5

By [F1] the group $T$ is a compact abelian topological group, so it carries normalized Haar probability and every irreducible continuous unitary representation of it is subject to the compact theory; let $π$ be such a representation on a nonzero Hilbert space $H$ ; for all $s, t \in T$ the operators commute, $π (t) π (s) = π (t s) = π (s t) = π (s) π (t)$ , so every $π (t)$ is a bounded self-intertwiner and [F3] makes it a scalar $χ (t)$ times the identity; then every one-dimensional subspace of $H$ is $π (T)$ -invariant, so irreducibility forces $\dim H = 1$ , and $χ : T \to T$ is a continuous character because $π$ is strongly continuous and unitary [F5], with $∣ χ (t) ∣ = 1$ . The normalized matrix coefficient of the one-dimensional representation $π = χ$ at the unit vector is $\sqrt{1} ⟨ χ (t) e_{1}, e_{1} ⟩ = χ (t)$ ; this proves (1).

1.2F2

By [F2] the family ${z^{n} : n \in Z}$ is orthonormal with closed linear span $L^{2} (T)$ , that is, it is a complete orthonormal family; this is (2).

2.1F2F4F6F7step 1.1step 1.2∎

By [F2] each $z^{n}$ is a continuous character, hence a one-dimensional continuous unitary representation of $T$ , and step 1.1 shows that its normalized matrix coefficient is $z^{n}$ itself; therefore ${z^{n}} \subseteq B$ . Since $B$ is an orthonormal basis by [F4] and ${z^{n}}$ is a complete orthonormal subfamily by step 1.2, [F6] gives $B = {z^{n} : n \in Z}$ ; consequently the unitary dual of $T$ is exactly ${z^{n} : n \in Z}$ , which is in bijection with $Z$ because $z^{n} = z^{m}$ fails at $[t] = 1 / (2 (n - m))$ when $n \neq m$ . The Pontryagin dual of the compact abelian group $T$ is discrete by [F7], consistent with this dual being the discrete family of integer characters; the example does not recompute ${Hom}_{c t s} (T, T)$ . The Peter-Weyl decomposition of $L^{2} (T)$ is therefore the Hilbert direct sum of the one-dimensional blocks $C z^{n}$ , $n \in Z$ , the classical Fourier series decomposition, and the Parseval identity of the compact theory specializes to the classical Parseval identity for Fourier series and the expansion to Fourier inversion in $L^{2}$ (The Parseval identity for Fourier series); this completes the verification. The Axiom of Choice is inherited through the cited suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

131 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)
Constantin Teleman, Representation Theory (Berkeley lecture notes, 60 pp.) (standard reference, not scraped)