PropositionStatement: 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.

Haar integration is translation and conjugation invariant

Statement

Assume the Axiom of Choice. Let $G$ be a compact Lie group with normalized Haar measure $μ$ , so that $μ$ is the unique regular Borel probability measure that is left, right and inversion invariant (Normalized Haar measure on a compact Lie group). Then for every integrable $f : G \to C$ and every $h \in G$ , $\int_{G} f (h x) d μ (x) = \int_{G} f (x h) d μ (x) = \int_{G} f (h x h^{- 1}) d μ (x) = \int_{G} f (x^{- 1}) d μ (x) = \int_{G} f (x) d μ (x) .$

Facts & Assumptions

Given: Assume the Axiom of Choice, a compact Lie group $G$ with normalized Haar measure $μ$ , an integrable $f : G \to C$ , and $h \in G$ .

[A1]

The Axiom of Choice is the choice principle of The Axiom of Choice; it is used exactly through [L1].

[L1]

Normalized Haar measure $μ$ is the unique regular Borel probability measure on $G$ that is invariant under left translations, right translations and inversion; in particular $μ (h E) = μ (E)$ , $μ (E h) = μ (E)$ and $μ (E^{- 1}) = μ (E)$ for every Borel $E \subseteq G$ (Normalized Haar measure on a compact Lie group).

[L2]

For nonnegative Borel $g$ the nonnegative integral is the supremum of the integrals of the simple Borel functions below it, the integral of a nonnegative simple function is its finite linear combination of measure values, and an increasing sequence of nonnegative Borel functions with pointwise limit $g$ has integrals converging to the integral of $g$ (The nonnegative integral agrees with the simple integral on simple functions, Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral).

[L3]

A complex-valued function is integrable exactly when the four nonnegative functions $(Re f)_{\pm}, (Im f)_{\pm}$ are integrable, and its integral is the corresponding signed combination of their integrals (Integrable real and complex functions, and their integrals).

Proof

technique · direct

1.1

Let $E \subseteq G$ be Borel. Since $x \mapsto 1_{E} (h x)$ is the indicator of $h^{- 1} E$ , the left invariance in [L1] gives $\int_{G} 1_{E} (h x) d μ (x) = μ (h^{- 1} E) = μ (E)$ ; since $x \mapsto 1_{E} (x h)$ is the indicator of $E h^{- 1}$ , the right invariance gives $\int_{G} 1_{E} (x h) d μ (x) = μ (E h^{- 1}) = μ (E)$ ; and since $x \mapsto 1_{E} (x^{- 1})$ is the indicator of $E^{- 1}$ , inversion invariance gives $\int_{G} 1_{E} (x^{- 1}) d μ (x) = μ (E^{- 1}) = μ (E)$ .

L1algebra

2.1

Let $g \geq 0$ be Borel. By [L2] choose an increasing sequence of nonnegative simple Borel functions $s_{n} ↗ g$ . Each $s_{n}$ is a finite linear combination of Borel indicators, so the three translation/inversion identities of step 1.1 and linearity of the simple integral give $\int s_{n} (h x) d μ = \int s_{n} (x h) d μ = \int s_{n} (x^{- 1}) d μ = \int s_{n} d μ$ ; the same sequences $s_{n} (h \cdot)$ , $s_{n} (\cdot h)$ , $s_{n} (\cdot^{- 1})$ increase to $g (h \cdot)$ , $g (\cdot h)$ , $g (\cdot^{- 1})$ , so two applications of monotone convergence in [L2] identify all four nonnegative integrals.

L2step 1.1

3.1

For the conjugation identity write $ϕ (x) = h x h^{- 1}$ . Applying step 2.1 to the nonnegative Borel function $x \mapsto g (h x)$ in place of $g$ and then the left-translation identity gives $\int g (h x h^{- 1}) d μ (x) = \int g (h x) d μ (x) = \int g (x) d μ (x)$ for nonnegative Borel $g$ .

step 2.1

4.1

Now let $f$ be integrable complex-valued. The functions $f (h \cdot), f (\cdot h), f (ϕ (\cdot)), f (\cdot^{- 1})$ are Borel because $x \mapsto h x$ , $x \mapsto x h$ , $ϕ$ and inversion are homeomorphisms of $G$ , and they are integrable because the identities of steps 2.1 and 3.1 applied to $∣ f ∣$ show that each of these four functions has the finite integral $\int ∣ f ∣ d μ$ . Splitting $f$ into its four nonnegative parts by [L3] and applying the corresponding identity of steps 2.1 and 3.1 to each part, then recombining, gives the displayed chain of equalities. The Axiom of Choice entered only through [L1].

A1L3step 2.1step 3.1∎

Depends on

Used by

Convolution operators Definition
Central continuous approximate identities Lemma
Continuous convolution operators are Hilbert–Schmidt Lemma
Spectral convolution eigenspaces are finite-dimensional and invariant 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
Finite-dimensional compact-group representations are unitarizable Theorem
Schur orthogonality Theorem
Weyl integration formula Theorem

Dependency tree · two levels

22 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)