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.
Normalized Haar measure on a compact Lie group
Statement
Assume the Axiom of Choice. Every compact Lie group has a unique regular Borel probability measure invariant under left and right translations and inversion.
Facts & Assumptions
Given: A compact Lie group with identity .
The Axiom of Choice is the choice principle of The Axiom of Choice; it is inherited here through [L1], which is proved under AC.
Every compact Hausdorff group has a unique left Haar probability measure, and that measure is right invariant and inversion invariant as well (Normalized Haar probability on a compact group).
A left Haar measure is by definition a nonzero left-invariant Borel measure that is finite on compact sets, outer regular on Borel sets and inner regular on open sets; a left Haar probability measure is a left Haar measure whose total mass is one (Left Haar integral and left Haar measure).
A finite Radon measure is left invariant when for all Borel and , right invariant when , inversion invariant when , and bi-invariant when both translation conditions hold; for a compact group a finite Radon measure is a probability measure exactly when its total mass is one (Left, right, and bi-invariant Borel measures).
Proof
A finite-dimensional Lie group is a Hausdorff topological group, and compactness is a topological property, so a compact Lie group is a compact Hausdorff group; by [L1] it therefore carries a unique left Haar probability measure , which is right invariant and inversion invariant.
Since is compact, every left Haar measure on has finite positive total mass and can be normalized by dividing by that mass; compactness alone does not make an arbitrary Haar measure a probability measure. For the normalized measure, outer regularity also gives inner regularity on every Borel : for choose open with ; then is compact, , and . Conversely, a regular Borel probability measure that is left invariant is a left Haar measure of total mass one in the sense of [L2]. Hence the uniqueness assertion of [L1] is exactly uniqueness among regular Borel probability measures that are left invariant.
By [L3] the measure of step 1.1 is bi-invariant satisfying all three invariance conditions, so a measure with the stated properties exists.
For uniqueness let be any regular Borel probability measure invariant under left and right translations and inversion. Then is a left Haar probability measure, so by the uniqueness in [L1], applied through step 1.2.
Existence and uniqueness are established, and the Axiom of Choice entered exactly through the uniqueness-and-existence statement [L1].
Depends on
Used by
- Left and right regular representations on L2(G) Definition
- Finite-group Schur orthogonality Example
- Normalized Haar measure on a torus Example
- Compact Haar measure is bi-invariant False statement
- Central continuous approximate identities Lemma
- Orthogonality identifies the Weyl numerator Lemma
- A compact-group moment map can be averaged to an equivariant one when the affine obstruction vanishes Proposition
- Compact Lie groups admit bi-invariant metrics Proposition
- Compact-group symplectic actions admit an invariant compatible almost-complex structure Proposition
- Haar integration is translation and conjugation invariant Proposition
- Weyl integration formula Theorem
Dependency tree · two levels
15 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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
- Brian Conrad and Aaron Landesman, Compact Lie Groups (standard reference, not scraped)