Pushforward of product measure I am having some trouble with the following.
Suppose $X$ is a bounded metric space with Borel probability measure $\mu_X$. Let us suppose there is another probability space $(Y,\mu_Y)$ such that $\pi_Y:Y\to X$ is surjective and satisfies $\mu_X=(\pi_Y)_\star(\mu_Y)=\mu_Y(\pi_Y^{-1}(.))$
Suppose $G$ is a compact connected Lie group with Haar measure $\nu$ and let $f:Y\to G$ be a measurable function. Let $\pi:Y\times G\to X\times G$ be given by $\pi(y,g)=(\pi_Y(y),gf(y))$. It is immediate that $\pi$ is surjective.
Let us define the product measure $\rho=\mu_X\times \nu$ on $X\times G$. I want to show that $\rho=\pi_\star(\mu_Y\times \nu)$, but I m unsure how to proceed. Can anyone help? I believe the invariance of the Haar measure will come into play.
 A: To compute push-forward of measures, I like to integrate functions. Let $\varphi : X \times G \to \mathbb{R}_+$ be measurable. Then, using first Fubini's theorem:
$$\int_{Y \times G} \varphi \circ \pi (y,g) \ d (\mu_Y \otimes \nu) (y,g) 
= \int_Y \int_G \varphi (\pi_Y (y),gf(y)) \ d \nu (g) \ d \mu_Y (y).$$
For fixed $y$, we do the change of variables $g' = g f(y)$. Since the Haar measure is invariant, we get:
$$\int_G \varphi (\pi_Y (y),gf(y)) \ d \nu (g) \ d \mu_Y (y) 
= \int_G \varphi (\pi_Y (y),g') \ d \nu (g') \ d \mu_Y (y).$$
Plugging this into the first equality, and using Fubini again:
$$\int_{Y \times G} \varphi \circ \pi (y,g) \ d (\mu_Y \otimes \nu) (y,g) 
= \int_Y \int_G \varphi (\pi_Y (y),g) \ d \nu (g) \ d \mu_Y (y) 
= \int_G \int_Y \varphi (\pi_Y (y),g) \ d \mu_Y (y) \ d \nu (g).$$
For fixed $g$, since $\mu_X = \pi_{Y*} \mu_Y$:
$$\int_Y \varphi (\pi_Y (y),g) \ d \mu_Y (y) = \int_X \varphi (x,g) \ d \mu_X (x).$$
Coming back again to the first equality:
$$\int_{Y \times G} \varphi \circ \pi (y,g) \ d (\mu_Y \otimes \nu) (y,g) 
= \int_G \int_X \varphi (x,g) \ d \mu_X (x) \ d \nu (g) = \int_{X \times G} \varphi (x,g) \ d \rho (x,g),$$
so that $\rho = \pi_* (\mu_Y \otimes \nu)$.
