[proofplan] We start from the normalized [Weyl integration formula](/theorems/9714) on the maximal torus, which applies to the measurable $\mu_G$-integrable class function $f$ and supplies both the weighted torus integrability of $t\mapsto f(t)D(t)$ and the formula with the factor $1/|W|$. The main point is to show that this weighted integrand is $W$-invariant: this uses conjugation-invariance of $f$ and the fact that the Weyl group permutes the roots while the product defining $D$ may be rewritten over unordered root pairs. A finite-group fundamental-domain decomposition then rewrites the integral over $T$ as $|W|$ times the integral over $C$, cancelling the factor in the Weyl integration formula. [/proofplan]

[step:Rewrite the Weyl denominator as a product over root pairs] Let $\Phi/\{\pm 1\}$ denote the set of unordered pairs $\{\alpha,-\alpha\}$ with $\alpha\in\Phi$. Since $\Phi^+$ contains exactly one root from each pair $\{\alpha,-\alpha\}$, and since $-\alpha$ corresponds to the inverse character $\alpha^{-1}:T\to S^1$, we have, for every $t\in T$, \begin{align*} D(t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(t)|^2. \end{align*} This expression is independent of the choice of representative of the pair. Indeed, if $\alpha(t)\in S^1$, then \begin{align*} |1-\alpha(t)^{-1}|=|\alpha(t)^{-1}||\alpha(t)-1|=|1-\alpha(t)|. \end{align*} Thus replacing $\alpha$ by $-\alpha$ does not change the factor. [/step]

[step:Prove that the weighted torus integrand is invariant under the Weyl group]Define the [measurable function](/page/Measurable%20Function) $F:T\to\mathbb C$ by $F(t):=f(t)D(t)$. We prove that $F$ is $W$-invariant. Let $w\in W$, and choose a representative $n\in N_G(T)$ of $w$. The Weyl [group action](/page/Group%20Action) is given by \begin{align*} w\cdot t=ntn^{-1}. \end{align*} Since $f$ is a class function on $G$, \begin{align*} f(w\cdot t)=f(ntn^{-1})=f(t). \end{align*} It remains to check the density. The Weyl group acts on $\Phi$ by \begin{align*} (w\alpha)(t):=\alpha(w^{-1}\cdot t), \end{align*} and this action permutes the unordered pairs $\{\alpha,-\alpha\}$. Using the root-pair expression for $D$, \begin{align*} D(w\cdot t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(w\cdot t)|^2. \end{align*} As $\{\alpha,-\alpha\}$ runs through $\Phi/\{\pm 1\}$, so does $\{w^{-1}\alpha,-w^{-1}\alpha\}$. Therefore the product is unchanged, and \begin{align*} D(w\cdot t)=D(t). \end{align*} Hence \begin{align*} F(w\cdot t)=F(t) \end{align*} for every $w\in W$ and every $t\in T$.[/step]

[guided]We need the function integrated over the torus to be constant on Weyl orbits, because the next step replaces the torus by one representative chamber. Define the measurable function $F:T\to\mathbb C$ by $F(t):=f(t)D(t)$. We verify $F(w\cdot t)=F(t)$ for each $w\in W$. Choose $w\in W$ and choose an element $n\in N_G(T)$ whose coset in $N_G(T)/T$ is $w$. By definition of the Weyl action on $T$, \begin{align*} w\cdot t=ntn^{-1}. \end{align*} Since $f:G\to\mathbb C$ is a class function, it is invariant under conjugation in $G$. Therefore \begin{align*} f(w\cdot t)=f(ntn^{-1})=f(t). \end{align*} Now we check the Weyl denominator. The subtle point is that $w$ need not preserve the chosen positive roots $\Phi^+$, so we should not argue directly with the positive-root product. Instead, we use the equivalent product over unordered pairs $\{\alpha,-\alpha\}$. This is legitimate because $\Phi^+$ contains exactly one root from each such pair, and for $z=\alpha(t)\in S^1$, \begin{align*} |1-z^{-1}|=|z^{-1}||z-1|=|1-z|. \end{align*} Thus the factor attached to $\alpha$ is the same as the factor attached to $-\alpha$. The Weyl group permutes the root system $\Phi$, and therefore it permutes the set of unordered pairs $\Phi/\{\pm 1\}$. With the induced action on roots defined by $(u\alpha)(s):=\alpha(u^{-1}\cdot s)$ for $u\in W$ and $s\in T$, we have \begin{align*} \alpha(w\cdot t)=(w^{-1}\alpha)(t). \end{align*} Hence \begin{align*} D(w\cdot t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-(w^{-1}\alpha)(t)|^2. \end{align*} As $\{\alpha,-\alpha\}$ runs through $\Phi/\{\pm 1\}$, the pair $\{w^{-1}\alpha,-w^{-1}\alpha\}$ also runs through $\Phi/\{\pm 1\}$. Therefore this is the same product as \begin{align*} D(t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(t)|^2, \end{align*} only with the factors reindexed. Therefore \begin{align*} D(w\cdot t)=D(t). \end{align*} Combining this with the class-function identity gives \begin{align*} F(w\cdot t)=f(w\cdot t)D(w\cdot t)=f(t)D(t)=F(t). \end{align*}[/guided]

[step:Apply the normalized Weyl integration formula to obtain torus integrability] Apply the normalized Weyl integration formula [citetheorem:9714] to the $\mu_G$-integrable measurable class function $f:G\to\mathbb C$. Its measurable $L^1$ hypotheses are exactly the compact connected Lie group $G$, the maximal torus $T$, the normalized Haar probability measures $\mu_G$ and $\mu_T$, the chosen positive root system $\Phi^+$, and the assumption that $f$ is a $\mu_G$-integrable measurable class function. Therefore the function $F:T\to\mathbb C$, $t\mapsto f(t)D(t)$, is $\mu_T$-integrable and \begin{align*} \int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}\int_T F(t)\,d\mu_T(t). \end{align*} [/step]

[step:Replace the torus integral by the chamber integral] By the fundamental-domain hypothesis, there exists a measurable $\mu_T$-null set $E\subset T$ such that \begin{align*} T\setminus E=\bigsqcup_{w\in W}w(C\setminus E). \end{align*} Since Haar measure on $T$ is invariant under the continuous automorphisms induced by $W$, for each $w\in W$ one has \begin{align*} \int_{w(C\setminus E)}F(t)\,d\mu_T(t)=\int_{C\setminus E}F(w\cdot t)\,d\mu_T(t). \end{align*} Using $W$-invariance of $F$, \begin{align*} \int_{w(C\setminus E)}F(t)\,d\mu_T(t)=\int_{C\setminus E}F(t)\,d\mu_T(t). \end{align*} Summing over the disjoint decomposition of $T\setminus E$ gives \begin{align*} \int_T F(t)\,d\mu_T(t)=\sum_{w\in W}\int_{w(C\setminus E)}F(t)\,d\mu_T(t). \end{align*} Therefore \begin{align*} \int_T F(t)\,d\mu_T(t)=|W|\int_{C\setminus E}F(t)\,d\mu_T(t). \end{align*} Because $E$ is $\mu_T$-null and $F$ is $\mu_T$-integrable, this is \begin{align*} \int_T f(t)D(t)\,d\mu_T(t)=|W|\int_C f(t)D(t)\,d\mu_T(t). \end{align*} [/step]

[step:Substitute the chamber identity into the normalized Weyl integration formula] From the earlier application of the normalized Weyl integration formula [citetheorem:9714], \begin{align*} \int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}\int_T f(t)D(t)\,d\mu_T(t). \end{align*} Using the chamber identity from the preceding step, \begin{align*} \int_T f(t)D(t)\,d\mu_T(t)=|W|\int_C f(t)D(t)\,d\mu_T(t). \end{align*} Substitution gives \begin{align*} \int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}|W|\int_C f(t)D(t)\,d\mu_T(t). \end{align*} Since $W$ is finite and nonempty, $|W|\ge 1$, and cancellation yields \begin{align*} \int_G f(g)\,d\mu_G(g)=\int_C f(t)D(t)\,d\mu_T(t). \end{align*} This is the claimed Weyl chamber form of the Weyl integration formula. [/step]