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.

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

• Thank you - I was toiling away working with preimages but this method is much nicer. Sep 28, 2019 at 20:33
• PS, do you not mean $\phi$ should be integrable? Sep 28, 2019 at 20:34
• I took $\varphi$ nonnegative, so that I could use Fubini's theorem wihout having to worry about integrability. Sep 28, 2019 at 20:39