Alphabeta MathHow 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.
Normalized Haar probability on a compact group
Statement
Assume AC. Every compact Hausdorff group has a unique left Haar probability measure. It is right invariant and inversion invariant as well.
Facts & Assumptions
Given: A compact Hausdorff group and AC.
A left Haar measure exists under AC. (Existence of left and right Haar measures)
The whole compact nonempty group has positive finite Haar mass. (Haar measure is positive on nonempty open sets and finite on compact sets)
Left Haar measures differ by a positive scalar. (Uniqueness of left Haar measure up to scale)
AC is assumed in the choice-function form stated in the cited definition. (The Axiom of Choice)
Proof
Under the assumed AC, take a left Haar measure . Since is open, nonempty and compact, . Put ; it is left Haar and . Any other left Haar probability is , and evaluation on forces .
For fixed , is Radon by the right-translation homeomorphism and is a probability. Left and right translations commute, so . Uniqueness gives , proving right invariance. Now is a Radon probability and by right invariance; uniqueness again gives .
Sources
Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13. Local argument and conventions as displayed above.
Depends on
Used by
- Normalized Haar measure on a compact Lie group Corollary
- Averaged Hermitian form for a compact group Definition
- Compact-group isotypic projection Definition
- Haar averaging of bounded operators as a weak operator integral Definition
- Representative functions on a compact group Definition
- A circle representation with an averaged orthogonal weight form Example
- A Kazhdan pair for a compact group via Haar averaging Example
- Convolution of matrix coefficients on a compact group Example
- Haar measure on an infinite product of compact groups Example
- Isotypic Haar projections specialize to finite character sums Example
- Iwasawa coordinates and Haar density on SL2(R) Example
- Normalized Haar measure on a finite group Example
- Normalized Haar measure on a torus Example
- Peter-Weyl for a profinite group Example
- Peter-Weyl for an infinite product of finite groups Example
- Property (T) for finite groups via normalized counting measure Example
- Compact Haar measure is bi-invariant False statement
- A positive rank-one Haar average is a nonzero compact intertwiner Lemma
- Averaging a Hermitian form unitarizes a finite-dimensional compact-group representation Lemma
- Cayley Charts on the Unitary Matrix Group Lemma
- Compact convolution operators commute with right translations and have conjugate-kernel adjoints Lemma
- Haar averaging projects contractively onto the bounded intertwiners Lemma
- L² convolution on a compact group is Hilbert–Schmidt Lemma
- Matrix coefficients of finite-dimensional representations separate points of a compact group Lemma
- The L1 action of a strongly continuous unitary representation Lemma
- Compact, discrete and abelian groups are unimodular Proposition
- Compact groups have property (T) by Haar averaging Theorem
- Complete reducibility of finite-dimensional compact-group representations Theorem
- Irreducible unitary representations of compact groups are finite dimensional Theorem
- Isotypic projections are mutually orthogonal equivariant projections Theorem
- Schur orthogonality for general compact groups Theorem
- Symmetric Subspace Dimension And Haar Moment Theorem
- The SL2(Q3) Iwahori convolution corner has affine parameters 3 Theorem
- Uniform density of representative functions (topological Peter-Weyl theorem) Theorem
Dependency tree · two levels
17 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
- Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13 (standard reference, not scraped)