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.
Weyl integration formula
Statement
Assume the Axiom of Choice. Let be a compact connected Lie group with maximal torus , let and be normalized Haar measures on and , and let be the unique -invariant probability measure on characterized by the Weil identity for every continuous on . Then for every continuous on and if is a class function the inner integral equals , so that .
Facts & Assumptions
Given: Assume the Axiom of Choice, a compact connected Lie group with maximal torus , normalized Haar measures on , on , the root system of , and the Weyl Jacobian of the chosen positive system, which by The Weyl Jacobian is independent and invariant depends only on and is -invariant.
The Axiom of Choice is The Axiom of Choice; it enters through the normalized Haar measures of [L1] and the differentiable structure of [L3].
is the unique regular Borel probability on invariant under left and right translations and inversion, is the corresponding measure on , and integrals against them are invariant under translations and conjugation (Normalized Haar measure on a compact Lie group, Haar integration is translation and conjugation invariant).
Conjugacy classes meet , and two points of are conjugate exactly when they are in the same -orbit (Conjugacy classes meet T in Weyl orbits). The group is finite and acts faithfully on (The compact Weyl group is finite); its action is by Lie-group automorphisms (Compact Weyl group).
The quotient is a smooth manifold of dimension , the quotient map is a submersion, and its proof supplies smooth local sections. Closed subgroups are embedded Lie subgroups; a smooth map with invertible differential is locally a diffeomorphism; exponentials are natural (Quotient manifold by a closed Lie subgroup, Cartan closed subgroup theorem, The smooth inverse function theorem on manifolds, Exponential map is natural for Lie-group homomorphisms).
G has a bi-invariant Riemannian metric, whose identity inner product is Ad-invariant. Riemannian densities define Radon measures finite on compact sets, and their Borel integrals are computed by their local smooth density coefficients (Compact Lie groups admit bi-invariant metrics, Riemannian volume is the radon measure of the riemannian density, Measurable integration extends smooth density integration).
The compact adjoint representation has its finite character-space decomposition and infinitesimal bracket formula by Roots of a compact connected Lie group. Since [L2] gives , the real fixed algebra of is and hence the complex zero weight space is . The compact-root theorem identifies the nonzero infinitesimal weights with a semisimple reduced root system; its nonzero root spaces are one-dimensional by Root spaces of a complex semisimple Lie algebra are one-dimensional and Compact roots form a reduced crystallographic root system. If is a root, the opposite infinitesimal root is , while the inverse circle character has that differential; characters are determined by their differentials, so the opposite root character is . Their product is independent of positive system and W-invariant (The Weyl Jacobian is independent and invariant).
Smooth density pullback under a local diffeomorphism uses the absolute determinant. Euclidean change of variables holds for nonnegative measurable functions; localization with the density chart formula of [L4] gives the same formula in manifold charts. Fubini holds for integrable complex functions on sigma-finite product spaces (Pullback of densities by local diffeomorphisms, A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, Fubini's theorem for L^1 functions on a sigma-finite product).
Critical values of a smooth map of manifolds form a manifold-null set. Borel probabilities on a compact metric space are determined by their integrals of continuous real functions (Morse-Sard for smooth manifolds, Continuous functions determine Borel probabilities on compact metric spaces).
Proof
Define . It is a G-invariant Borel probability by equivariance and [L1]. For continuous F on G, is independent of representative by Haar invariance, and is continuous by local sections [L3] and continuity on compact sets. Fubini and right invariance give If is another invariant Borel probability, then for , Fubini and invariance give . The inner integral is by right invariance, independently of x. Hence both measures agree on continuous tests. The compact quotient is metrizable: the Ad(T)-invariant inner product of [L4] descends to a smooth invariant quotient metric via the local sections of [L3], whose distance gives the manifold topology. Thus [L7] proves uniqueness. Applying the Weil identity to likewise characterizes dQ uniquely.
Choose a bi-invariant metric as in [L4] and put . Its restriction is Ad(T)-invariant, so transporting it by the left G-action defines a smooth invariant metric on Q: at use the isometry , and invariance under the isotropy T makes the transport independent of representative. Local sections from [L3] give smoothness. The metric on T is the restriction of the group metric. Write the resulting unnormalized densities and volumes as and . They have finite positive total masses by compactness and [L4]. The normalized densities on G and T are their Haar probabilities by invariance and [L1]; on Q the normalized density is a G-invariant Borel probability.
On the compact manifold define . This is well defined because T is abelian and smooth by local sections [L3]. Use and left translation by at the target. Differentiating at zero gives The first summand lies in by Ad(T)-invariance; the second lies in . By [L5] the determinant on is . The real determinant equals that of its complexification; each root occurs once. Equivariance and isometries from the bi-invariant metric give the same absolute Jacobian at every for the unnormalized product densities. Thus q is locally a diffeomorphism precisely when .
We verify the volume normalization, rather than assuming a product decomposition of Haar measure. Over a smooth local section , the map , , is a diffeomorphism: its inverse is . At , project its base tangent vectors orthogonally to the horizontal complement of the fibre tangent. Since is projection, their horizontal components map isometrically onto the base vectors by the definition of the quotient metric. The fibre tangent vectors are obtained by left translation from T and are isometric to its tangent vectors. The additional vertical components of base vectors give a block triangular change-of-frame matrix with identity diagonal, hence determinant 1. Therefore . Take a finite section cover of compact Q and replace it by a disjoint Borel partition subordinate to the cover. The chart formulas and [L6], applied also to indicators of these sets, yield . By uniqueness in step 1.1 the normalized quotient density is dQ. Consequently the normalized product measure and dg have the same relative Jacobian J under q on its regular locus.
Let be the closed centralizer. Its Lie algebra is : differentiating commutation gives one inclusion and exponential naturality gives the converse by one-parameter subgroups. By [L5], for this is . Since has the same Lie algebra, exponential charts and connectedness imply . Any torus containing t lies in this identity component, so T is the unique maximal torus containing t. More generally the dimension of this fixed algebra is exactly for , and is larger for singular t. Dimension is invariant under conjugation. By [L2] every element is conjugate into T, so is the complement of . The latter compact set is precisely the critical-value set of q by step 2.1; it is null by [L7], hence Haar-null by the smooth positive density chart formula [L4]. Thus is open and of full Haar measure. No null-set assertion is transported through a singular local map.
Fix in . If , put ; then . Conjugation preserves regularity by step 3.2, and the uniqueness of the maximal torus containing t shows . Conversely each gives the preimage , and two such pairs agree exactly when the cosets mT agree. Thus every fibre of has exactly points. To obtain an evenly covered neighborhood of any g, choose disjoint local-diffeomorphism neighborhoods at its finitely many preimages, and intersect their open images. After restriction each supplies one preimage of every point of this intersection; the constant fibre count just proved leaves no other preimages. These are the required sheets. This proves the covering directly and does not assert that its open source is compact.
Choose a countable cover of by evenly covered coordinate neighborhoods small enough that each of their finitely many sheets lies in a coordinate neighborhood of the source; second countability permits this refinement. Subtract preceding sets to obtain a disjoint Borel partition. On each set and each sheet apply [L6] to the nonnegative measurable function, or to the four nonnegative parts of an integrable complex function. The normalized density Jacobian is J by step 3.1. Summing the countable disjoint pieces and the sheets gives For continuous f on compact G all integrals are absolutely finite because f and J are bounded and the normalized source measure is finite.
The target complement is Haar-null by step 3.2; on the omitted source one has pointwise. Hence step 5.1 already extends to integration over all of G and , without any uniform approximation by functions supported in . Fubini [L6] puts the torus integral outside and gives the formula in the statement with the unique probability of step 1.1. For a class function the integrand is independent of xT, giving the stated specialization; independence of positive roots follows from [L5]. If there are no roots, the adjoint decomposition makes , hence connected G equals T by exponential charts, Q is a point, W is trivial, and J is the empty product 1. This includes the trivial group. Choice supplies the assumptions of the stated Lie, Haar, density and countable-chart interfaces.
Depends on
- Conjugacy classes meet T in Weyl orbits
- The Weyl Jacobian is independent and invariant
- Normalized Haar measure on a compact Lie group
- Haar integration is translation and conjugation invariant
- Compact Lie groups admit bi-invariant metrics
- Quotient manifold by a closed Lie subgroup
- Riemannian volume is the radon measure of the riemannian density
- The Axiom of Choice
- Compact Weyl group
- The compact Weyl group is finite
- Fubini's theorem for L^1 functions on a sigma-finite product
- Morse-Sard for smooth manifolds
- A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions
- Measurable integration extends smooth density integration
- Pullback of densities by local diffeomorphisms
- Continuous functions determine Borel probabilities on compact metric spaces
- Cartan closed subgroup theorem
- Exponential map is natural for Lie-group homomorphisms
- The smooth inverse function theorem on manifolds
- Roots of a compact connected Lie group
- Root spaces of a complex semisimple Lie algebra are one-dimensional
- Compact roots form a reduced crystallographic root system
Used by
Dependency tree · two levels
142 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
- Brian Conrad and Aaron Landesman, Compact Lie Groups (standard reference, not scraped)
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)