Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Matrix coefficients are uniformly dense in C(G)

Statement

Assume the Axiom of Choice. Finite linear combinations of matrix coefficients of finite-dimensional unitary representations are uniformly dense in C(G) for a compact Lie group G.

Facts & Assumptions

Given: Assume the Axiom of Choice, a compact Lie group G with normalized Haar measure, and f∈C(G).

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the Haar and Hilbert-space theory cited.

[L1]

The normalized matrix coefficients form a Hilbert basis of L2(G), so every element of L2(G) is the finite-subset-net limit of finite matrix-coefficient sums (Peter–Weyl theorem).

[L2]

There are continuous central functions kn of integral one with Tknf→f uniformly for continuous f; C(G)⊆L2(G) because G is compact (Central continuous approximate identities).

Proof

technique · direct
1.1L2

Since f is continuous on the compact group, f∈L2(G) and ∥f∥2<+∞; fix ε>0 and choose n with sup⁡x∣Tknf(x)−f(x)∣<ε/2 by [L2], so that ∣f(x)−∫Gkn(u)f(xu) du∣<ε/2 for every x.

1.2L1

By [L1] applied to the L2 class of kn, there is a finite linear combination p of matrix coefficients with ∥kn−p∥2<ε/(2∥f∥2) when f≠0 (and the conclusion below is trivial when f=0).

2.1L1L2step 1.1step 1.2

For every x, the defining formula for the convolution operators gives ∣Tpf(x)−Tknf(x)∣≤∫G∣p(x−1y)−kn(x−1y)∣ ∣f(y)∣ dy≤∥p−kn∥2∥f∥2<ε/2 by Cauchy–Schwarz and Haar invariance. Hence ∥Tpf−f∥∞<ε by step 1.1. The function Tpf is a finite linear combination of matrix coefficients: if a summand of p is πij, then πij(x−1y)=∑kπik(x−1)πkj(y), so its contribution to Tpf(x) is a finite sum of the constants ∫Gπkj(y)f(y) dy times the matrix coefficients x↦πik(x−1) of the contragredient representation. Thus a finite matrix-coefficient sum lies within ε of f uniformly.

3.1A1L1L2step 2.1∎

The zero function is approximated by the zero linear combination, and the same argument includes the one-element group. All noncanonical existence used above is contained in the Haar, Hilbert-space and representation-theoretic suppliers invoked in [L1] and [L2], under the Axiom of Choice assumed in [A1].

Depends on

Used by

Dependency tree · two levels

19 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