CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Parseval and Fourier inversion for compact groups

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a compact Hausdorff group with normalized Haar probability $μ$ , with normalized matrix coefficient family $B = (u_{i j}^{π})$ (The normalized irreducible matrix coefficient family). For $f \in L^{2} (K)$ and each $π \in \hat{K}$ put $π (f) : = \int_{K} f (k) π (k)^{- 1} d μ (k) \in End (H_{π})$ (the $L^{1}$ action of The L1 action of a strongly continuous unitary representation applied to the reflected representative).

Parseval/Plancherel. For every $f \in L^{2} (K)$ , $\sum_{π \in \hat{K}} \sum_{i, j = 1}^{d_{π}} ∣ ⟨ f, u_{i j}^{π} ⟩ ∣^{2} = ∥ f ∥_{2}^{2}$ , equivalently $\sum_{π \in \hat{K}} d_{π} ∥ π (f) ∥_{H S}^{2} = ∥ f ∥_{2}^{2}$ , where $∥ \cdot ∥_{H S}$ is the Hilbert–Schmidt norm (Hilbert–Schmidt operator and Hilbert–Schmidt norm).
Fourier inversion in $L^{2}$ . The finite-subset net of spectral partial sums $\sum_{π, i, j} ⟨ f, u_{i j}^{π} ⟩ u_{i j}^{π}$ converges to $f$ in $L^{2} (K)$ .
Exactness on the coefficient algebra. If $f \in R (K)$ is a finite linear combination of the $u_{i j}^{π}$ , its expansion is that finite sum and equals $f$ pointwise; in particular no uniform convergence of partial sums is asserted for arbitrary continuous $f$ .

Facts & Assumptions

[F1]

$L^{2} (K, μ; C) \subseteq L^{1} (K, μ; C)$ because $2 ∣ f ∣ \leq ∣ f ∣^{2} + 1$ and $μ (K) = 1$ , and the coefficients are $⟨ f, u_{i j}^{π} ⟩ = \int_{K} f (k) \overline{u_{i j}^{π} (k)} d μ (k)$ with $u_{i j}^{π} (k) = \sqrt{d_{π}} ⟨ π (k) e_{i}^{π}, e_{j}^{π} ⟩$ and $c_{v, w}^{π} (k) = ⟨ π (k) v, w ⟩$ linear in the first argument. (Complex Haar L^p spaces and compactly supported functions, The normalized irreducible matrix coefficient family, Matrix coefficient of a unitary representation)

[F2]

A strongly measurable Banach-valued function with finite norm integral is Bochner integrable, the norm of the integral is at most the integral of the norm, and every bounded linear operator commutes with the Bochner integral. (Bochner integrability criterion, Bochner integral norm inequality, Bounded linear maps commute with Bochner integration)

[F3]

The normalized family $B = (u_{i j}^{π})$ is an orthonormal basis of $L^{2} (K)$ : it is orthonormal, its closed linear span is $L^{2} (K)$ , and consequently the Parseval identity $\sum_{π, i, j} ∣ ⟨ f, u_{i j}^{π} ⟩ ∣^{2} = ∥ f ∥_{2}^{2}$ holds and the finite-subset net of partial sums $\sum_{π, i, j} ⟨ f, u_{i j}^{π} ⟩ u_{i j}^{π}$ converges to $f$ in $L^{2} (K)$ for every $f$ . (The normalized matrix coefficients form an orthonormal basis of L2(K), Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space)

[F4]

For an operator on a finite-dimensional Hilbert space with orthonormal basis $e_{1}, \dots, e_{d}$ , expansion in that basis gives the Hilbert–Schmidt square-sum $∥ T ∥_{H S}^{2} = \sum_{i = 1}^{d} ∥ T e_{i} ∥^{2} = \sum_{i, j = 1}^{d} ∣ ⟨ T e_{i}, e_{j} ⟩ ∣^{2}$ . (Hilbert–Schmidt operator and Hilbert–Schmidt norm)

[F5]

$R (K)$ is the linear span of the matrix coefficients of finite-dimensional continuous unitary representations of $K$ , hence consists of continuous functions. (Representative functions on a compact group)

Proof

Given: AC, a compact Hausdorff group $K$ with normalized Haar probability $μ$ , the normalized family $B$ , and a class $f \in L^{2} (K, μ; C)$ .

1.1F1F2

The map $k \mapsto f (k) π (k)^{- 1}$ into the finite-dimensional Banach space $End (H_{π})$ is strongly measurable: its finitely many matrix entries are products of a measurable scalar function with continuous scalar functions, and finite-valued measurable approximations to those entries give simple approximations to the operator-valued map. Its operator norm is $∣ f (k) ∣$ , so [F1] gives $\int_{K} ∥ f (k) π (k)^{- 1} ∥ d μ (k) = ∥ f ∥_{1} < \infty$ . The criterion and norm inequality [F2] therefore define $π (f) = \int_{K} f (k) π (k)^{- 1} d μ (k)$ with $∥ π (f) ∥ \leq ∥ f ∥_{1}$ . Applying the bounded linear functional $T \mapsto ⟨ T e_{j}^{π}, e_{i}^{π} ⟩$ and [F2] gives $⟨ π (f) e_{j}^{π}, e_{i}^{π} ⟩ = \int_{K} f (k) ⟨ π (k)^{- 1} e_{j}^{π}, e_{i}^{π} ⟩ d μ (k) = \int_{K} f (k) \overline{⟨ π (k) e_{i}^{π}, e_{j}^{π} ⟩} d μ (k) = \frac{1}{\sqrt{d_{π}}} ⟨ f, u_{i j}^{π} ⟩$ , where unitarity gives the second equality.

2.1F3F4step 1.1

By step 1.1 and [F4], $\sum_{i, j} ∣ ⟨ f, u_{i j}^{π} ⟩ ∣^{2} = d_{π} \sum_{i, j} ∣ ⟨ π (f) e_{j}^{π}, e_{i}^{π} ⟩ ∣^{2} = d_{π} ∥ π (f) ∥_{H S}^{2}$ for every class $π$ , and the Parseval identity of the orthonormal basis [F3] gives $\sum_{π, i, j} ∣ ⟨ f, u_{i j}^{π} ⟩ ∣^{2} = ∥ f ∥_{2}^{2}$ ; substituting the first identity into the second yields $\sum_{π} d_{π} ∥ π (f) ∥_{H S}^{2} = ∥ f ∥_{2}^{2}$ , so the two forms of (1) are equivalent and both hold.

3.1F3F5step 2.1∎

The Parseval identity of step 2.1 is, by the equivalences for a complete orthonormal family [F3], equivalent to the convergence of the finite-subset net of partial sums $\sum_{π, i, j} ⟨ f, u_{i j}^{π} ⟩ u_{i j}^{π}$ to $f$ in $L^{2} (K)$ , which is (2); and if $f = \sum_{a \in F} c_{a} u_{a}$ is a finite linear combination of basis elements $u_{a} \in B$ , then orthonormality of $B$ gives $⟨ f, u_{a} ⟩ = c_{a}$ for $a \in F$ and $⟨ f, u_{b} ⟩ = 0$ for $b \notin F$ , so the expansion is the same finite sum and equals $f$ as a function at every point, which is (3); no uniform convergence is claimed for arbitrary continuous $f$ , since the argument uses only the $L^{2}$ basis property. The Axiom of Choice is inherited through the fixed representatives and bases and the cited suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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