Alphabeta Math
TheoremStatement: 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.

Uniform density of representative functions (topological Peter-Weyl theorem)

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let K be a compact Hausdorff topological group. The representative functions R(K) (Representative functions form a self-adjoint translation-invariant algebra) are uniformly dense in C(K,C): for every f∈C(K,C) and every ε>0 there is h∈R(K) with sup⁡k∈K∣f(k)−h(k)∣<ε.

Facts & Assumptions

[F1]

R(K) is a unital self-adjoint complex function algebra of continuous complex functions on the compact Hausdorff space K, closed under pointwise products and complex conjugation and containing the constants. (Representative functions form a self-adjoint translation-invariant algebra, Self-adjoint complex function algebras, unitality, and point separation)

[F2]

If K is equipped with normalized Haar probability, then for distinct x,y∈K there are a finite-dimensional continuous unitary representation π of K and vectors v,w in its carrier with ⟨π(x)v,w⟩≠⟨π(y)v,w⟩, and the function k↦⟨π(k)v,w⟩ lies in R(K). (Matrix coefficients of finite-dimensional representations separate points of a compact group)

[F3]

Complex Stone–Weierstrass: if X is a nonempty compact Hausdorff space and A⊆C(X,C) is a point-separating self-adjoint complex function algebra, then the uniform closure of A is all of C(X,C) when A is unital. (Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense, Self-adjoint complex function algebras, unitality, and point separation)

[F4]

Under AC, every compact Hausdorff group has a normalized Haar probability. (Normalized Haar probability on a compact group)

Proof

Given: AC, A compact Hausdorff topological group K and its algebra R(K) of representative functions.

1.1F1F2F4

Equip K with the normalized Haar probability supplied by [F4]. By [F1] the set R(K) is a self-adjoint complex function algebra on the compact Hausdorff space K, and it is unital because it contains the constants; it separates points, since for distinct x,y∈K the representation and vectors supplied by [F2] give the element k↦⟨π(k)v,w⟩ of R(K) with different values at x and y.

2.1F3step 1.1∎

The space K is nonempty because it is a topological group, so the unital case of complex Stone–Weierstrass [F3] applies to A=R(K) and shows that its uniform closure is C(K,C); for the given ε>0, uniform closure provides h∈R(K) with ∣f(k)−h(k)∣<ε/2 for every k, hence sup⁡k∈K∣f(k)−h(k)∣≤ε/2<ε. The Axiom of Choice is inherited through normalized Haar existence and the cited separation and algebra suppliers; this proof adds no further choice.

Depends on

Used by

Dependency tree · two levels

43 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