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

Weyl integration formula

Statement

Assume the Axiom of Choice. Let G be a compact connected Lie group with maximal torus T, let dg and dt be normalized Haar measures on G and T, and let d(xT) be the unique G-invariant probability measure on G/T characterized by the Weil identity GF(x)dg=G/TTF(xt)dtd(xT) for every continuous F on G. Then for every continuous f on G Gf(g)dg=1W(G,T)TG/Tf(xtx1)d(xT)J(t)dt, and if f is a class function the inner integral equals f(t), so that Gfdg=W(G,T)1Tf(t)J(t)dt.

Facts & Assumptions

Given: Assume the Axiom of Choice, a compact connected Lie group G with maximal torus T, normalized Haar measures dg on G, dt on T, the root system of (G,T), and the Weyl Jacobian J of the chosen positive system, which by The Weyl Jacobian is independent and invariant depends only on Φ and is W-invariant.

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the normalized Haar measures of [L1] and the differentiable structure of [L3].

[L1]

dg is the unique regular Borel probability on G invariant under left and right translations and inversion, dt is the corresponding measure on T, 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).

[L2]

Conjugacy classes meet T, and two points of T are conjugate exactly when they are in the same W(G,T)-orbit (Conjugacy classes meet T in Weyl orbits). The group W(G,T) is finite and acts faithfully on T (The compact Weyl group is finite); its action is by Lie-group automorphisms (Compact Weyl group).

[L3]

The quotient Q=G/T is a smooth manifold of dimension dimGdimT, the quotient map π:GQ 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).

[L4]

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

[L5]

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 CG(T)=T, the real fixed algebra of T is t and hence the complex zero weight space is tC. 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 dα, while the inverse circle character α1 has that differential; characters are determined by their differentials, so the opposite root character is α1. Their product J(t)=α>01α(t)12 is independent of positive system and W-invariant (The Weyl Jacobian is independent and invariant).

[L6]

Smooth density pullback under a local diffeomorphism uses the absolute determinant. Euclidean C1 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).

[L7]

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

technique · normalized quotient densities and finite sheets of the conjugation map
1.1

Define dQ=πdg. It is a G-invariant Borel probability by equivariance and [L1]. For continuous F on G, F(xT)=TF(xt)dt is independent of representative by Haar invariance, and is continuous by local sections [L3] and continuity on compact sets. Fubini and right invariance give QFdQ=GTF(xt)dtdg(x)=GFdg. If ν is another invariant Borel probability, then for hC(Q), Fubini and invariance give hdν=QGh(gxT)dgdν(xT). The inner integral is Gh(gT)dg=QhdQ 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 F=hπ likewise characterizes dQ uniquely.

L1L3L4L6L7
1.2

Choose a bi-invariant metric as in [L4] and put m=t. Its restriction is Ad(T)-invariant, so transporting it by the left G-action defines a smooth invariant metric on Q: at eT use the isometry dπe:mTeTQ, 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 dvG,dvT,dvQ and VG,VT,VQ. 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.

L1L3L4
2.1

On the compact manifold Q×T define q(xT,t)=xtx1. This is well defined because T is abelian and smooth by local sections [L3]. Use g=mt and left translation by t1 at the target. Differentiating exp(sX)texp(sY)exp(sX) at zero gives dq(eT,t)(X,Y)=(Ad(t1)I)X+Y. The first summand lies in m by Ad(T)-invariance; the second lies in t. By [L5] the determinant on m is αΦ(α(t)11)=α>01α(t)12=J(t). 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 (xT,t) for the unnormalized product densities. Thus q is locally a diffeomorphism precisely when tTreg:={J>0}.

L3L4L5step 1.2
3.1

We verify the volume normalization, rather than assuming a product decomposition of Haar measure. Over a smooth local section s:UG, the map b:U×Tπ1U, b(u,t)=s(u)t, is a diffeomorphism: its inverse is g(πg,s(πg)1g). At (u,t), project its base tangent vectors orthogonally to the horizontal complement of the fibre tangent. Since πb 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 bdvG=dvQdvT. 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 VG=VQVT. By uniqueness in step 1.1 the normalized quotient density is dQ. Consequently the normalized product measure dQdt and dg have the same relative Jacobian J under q on its regular locus.

L3L4L6step 1.1step 1.2step 2.1
3.2

Let CG(t) be the closed centralizer. Its Lie algebra is ker(Ad(t)I): differentiating commutation gives one inclusion and exponential naturality gives the converse by one-parameter subgroups. By [L5], for tTreg this is t. Since TCG(t)0 has the same Lie algebra, exponential charts and connectedness imply CG(t)0=T. 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 dimT exactly for tTreg, and is larger for singular t. Dimension is invariant under conjugation. By [L2] every element is conjugate into T, so Greg:=q(Q×Treg) is the complement of q(Q×(TTreg)). 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 Greg is open and of full Haar measure. No null-set assertion is transported through a singular local map.

L2L3L4L5L7step 2.1
4.1

Fix q(xT,t) in Greg. If q(yT,t)=q(xT,t), put m=x1y; then m1tm=t. Conjugation preserves regularity by step 3.2, and the uniqueness of the maximal torus containing t shows mTm1=T. Conversely each mNG(T) gives the preimage (xmT,m1tm), and two such pairs agree exactly when the cosets mT agree. Thus every fibre of qr:Q×TregGreg has exactly W 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 W sheets. This proves the covering directly and does not assert that its open source is compact.

L2L3step 2.1step 3.2
5.1

Choose a countable cover of Greg 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 W sheets gives WGregf(g)dg=Q×Tregf(xtx1)J(t)dQdt. For continuous f on compact G all integrals are absolutely finite because f and J are bounded and the normalized source measure is finite.

L4L6step 3.1step 4.1
6.1

The target complement is Haar-null by step 3.2; on the omitted source Q×(TTreg) one has J=0 pointwise. Hence step 5.1 already extends to integration over all of G and Q×T, without any uniform approximation by functions supported in Greg. 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 g=t, 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.

A1L3L5L6step 1.1step 3.2step 5.1

Depends on

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