Proof of Image Measures, Measures with Densities, and Change of Variables

Throughout we use Linearity and Monotonicity of the Lebesgue Integral (linearity and monotonicity of the integral) and Monotone Convergence Theorem, together with the notation and $[0,\infty]$ conventions of the statement.

Step 0 (dyadic approximation). For a natural number $L\ge1$ let $G_L=\{j\,2^{-L}:j=0,1,\dots,L\,2^{L}\}$, a finite set of nonnegative reals containing $0$, and for $t\in[0,\infty]$ let $\varphi_L(t)$ be the largest element of $G_L$ not exceeding $t$ (this exists, $G_L$ being finite and containing $0\le t$). Then:

(i) $\varphi_L(t)\le\varphi_{L+1}(t)\le t$ for all $t$, since $G_L\subseteq G_{L+1}$: indeed $j2^{-L}=(2j)2^{-L-1}$, and $j\le L2^{L}$ implies $2j\le(L+1)2^{L+1}$.

(ii) $\varphi_L(t)\to t$ as $L\to\infty$ for every $t\in[0,\infty]$: for real $t\ge0$ and every natural number $L\ge t$ the elements of $G_L$ have spacing $2^{-L}$ throughout $[0,L]\supseteq[0,t]$, so $t-\varphi_L(t)\le2^{-L}$; and $\varphi_L(\infty)=L\to\infty$.

(iii) If $u:Z\to[0,\infty]$ is measurable on a measurable space $(Z,\mathcal{Z})$, then $\varphi_L\circ u$ takes finitely many values, and for $c=j2^{-L}$ with $j<L2^{L}$ one has $\{\varphi_L\circ u=c\}=\{u\ge c\}\setminus\{u\ge c+2^{-L}\}$, while $\{\varphi_L\circ u=L\}=\{u\ge L\}$; each set $\{u\ge c\}=\bigcap_{n\ge1}\{u>c-1/n\}$ is measurable. A real-valued function with finitely many values whose level sets are measurable is measurable (every preimage of a set is the finite union of the relevant level sets), so $\varphi_L\circ u$ is a nonnegative simple function. By (i) and (ii), $\varphi_L\circ u\uparrow u$ pointwise.

Step 1 (claim 1). $\mu_T(\varnothing)=\mu(\varnothing)=0$. If $B_1,B_2,\dots\in\mathcal{S}$ are pairwise disjoint, the preimages $T^{-1}(B_m)$ are pairwise disjoint members of $\mathcal{F}$ with $T^{-1}(\bigcup_m B_m)=\bigcup_m T^{-1}(B_m)$, so countable additivity of $\mu$ gives countable additivity of $\mu_T$. Finally $\mu_T(S)=\mu(T^{-1}(S))=\mu(X)$, and a probability measure is exactly a measure of total mass $1$ (Measure, Measure Space, and Probability Measure).

Step 2 (claim 2). For $B\in\mathcal{S}$ one has $\mathbf{1}_B\circ T=\mathbf{1}_{T^{-1}(B)}$ pointwise, so by the integral of simple functions,

For a nonnegative simple $s=\sum_{m=1}^{n}c_m\mathbf{1}_{B_m}$ the identity follows by linearity, since $s\circ T=\sum_m c_m\mathbf{1}_{T^{-1}(B_m)}$ is again simple. For measurable $g:S\to[0,\infty]$: $g\circ T$ is measurable, since for real $a$ one has $\{g\circ T>a\}=T^{-1}(\{g>a\})\in\mathcal{F}$; Step 0 gives nonnegative simple $\varphi_L\circ g\uparrow g$ with $(\varphi_L\circ g)\circ T=\varphi_L\circ(g\circ T)\uparrow g\circ T$; and two applications of Monotone Convergence Theorem give

For measurable $g:S\to\mathbb{R}$, apply this to the positive and negative parts $g^{\pm}$, noting $(g\circ T)^{\pm}=g^{\pm}\circ T$ pointwise. The two resulting identities show $\int g^{\pm}\,d\mu_T$ and $\int g^{\pm}\circ T\,d\mu$ are finite together, which is the stated equivalence of integrability (Integrable Function and the Lebesgue Integral), and in that case subtracting them gives the display in $\mathbb{R}$.

Step 3 (claim 3). $\nu_h(\varnothing)=0$, the integrand being $0$. For pairwise disjoint $A_1,A_2,\dots\in\mathcal{F}$, pointwise $\mathbf{1}_{\bigcup_m A_m}\,h=\sup_n\sum_{m=1}^{n}\mathbf{1}_{A_m}h$ with nondecreasing partial sums, so Monotone Convergence Theorem and linearity give

so $\nu_h$ is a measure. Here and below, sums and products of real-valued measurable functions are measurable by Sequentially Continuous Functions of Measurable Euclidean Maps are Measurable, the maps $(u,v)\mapsto u+v$ and $(u,v)\mapsto uv$ being continuous on $\mathbb{R}^{2}$. Next, for nonnegative simple $s=\sum_{m}c_m\mathbf{1}_{B_m}$ ($B_m\in\mathcal{F}$), linearity gives

For measurable $f:X\to[0,\infty]$, Step 0 gives simple $\varphi_L\circ f\uparrow f$; then $(\varphi_L\circ f)\,h\uparrow fh$ pointwise: where $f$ is finite this is continuity of multiplication, where $f=\infty$ and $h>0$ one has $(\varphi_L\circ f)h=Lh\uparrow\infty=fh$ (convention $\infty\cdot a=\infty$ for $a>0$), and where $f=\infty$ and $h=0$ both sides vanish (convention $\infty\cdot0=0$). Hence $fh=\sup_L(\varphi_L\circ f)h$ pointwise, so for real $a$ the set $\{fh>a\}$ equals $X$ for $a<0$ and $\bigcup_L\{(\varphi_L\circ f)h>a\}$ for $a\ge0$ (the sequence being nondecreasing), and $fh$ is measurable, each $(\varphi_L\circ f)h$ being a product of real-valued measurable functions. Monotone Convergence Theorem on both sides, with the simple case just proved, gives

Finally, for measurable $f:X\to\mathbb{R}$: pointwise $(fh)^{\pm}=f^{\pm}h$ since $h\ge0$, so $\int f^{\pm}\,d\nu_h=\int f^{\pm}h\,d\mu$; both sides are finite together, giving the integrability equivalence, and subtraction gives the final display. $\blacksquare$