Independence Fubini: Integration in an Independent Random Vector Given a Sub-Sigma-Algebra

Let $(\Omega,\mathcal{F},P)$ be a probability space, let $\mathcal{G}$ be a $\sigma$-algebra on $\Omega$ with $\mathcal{G}\subseteq\mathcal{F}$, let $n\ge1$ be a natural number, and let $X:\Omega\to\mathbb{R}^n$ be measurable with respect to $\mathcal{F}$ and the $n$-fold Borel $\sigma$-algebra $\mathcal{B}_n$, such that the $\sigma$-algebra $\sigma(X)$ generated by $X$ is independent of $\mathcal{G}$. Let $\mu_X$ denote the image measure of $P$ under $X$, a probability measure on $(\mathbb{R}^n,\mathcal{B}_n)$.

Let $\Psi:\Omega\times\mathbb{R}^n\to[0,\infty]$ be measurable with respect to the product $\sigma$-algebra $\mathcal{G}\otimes\mathcal{B}_n$, in the sense of Lebesgue Integral of a Nonnegative Measurable Function. Then:

1. The map $\omega\mapsto\Psi(\omega,X(\omega))$ is $\mathcal{F}$-measurable.

2. The map $\omega\mapsto\int_{\mathbb{R}^n}\Psi(\omega,u)\,d\mu_X(u)$ is $\mathcal{G}$-measurable, the inner integral being defined for every $\omega$ since the section $u\mapsto\Psi(\omega,u)$ is $\mathcal{B}_n$-measurable.

3. With expectations of $[0,\infty]$-valued measurable maps understood as their integrals with respect to $P$, $\mathbb{E}\bigl[\Psi(\cdot,X(\cdot))\bigr]=\mathbb{E}\Bigl[\int_{\mathbb{R}^n}\Psi(\cdot,u)\,d\mu_X(u)\Bigr]\qquad\text{in }[0,\infty].$