A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions

On Borel subsets $E$ of $V$ define $\nu (E):={\int }_U{\mathbf{1}}_E(T(x))\mathrm{\mid }\det DT(x)\mathrm{\mid }d{\lambda }_n(x)\mathrm{.}$ This is a measure: the nonnegative Jacobian weight is measurable, inverse images under $T$ take disjoint countable unions to disjoint countable unions, [L6] gives finite additivity, and [L2] passes the increasing finite sums through the integral.

Let $W=V\cap R$ for a bounded open rectangle $R$ with rational endpoints. Write $d(y,W^c)$ for Euclidean distance to the complement and $\mathrm{\parallel }y{\mathrm{\parallel }}_{\mathrm{\infty }}$ for the maximum coordinate modulus. The functions ${\phi }_j(y)=\min \{1,\max (0,jd(y,W^c)-1)\}\min \{1,\max (0,j+1-\mathrm{\parallel }y{\mathrm{\parallel }}_{\mathrm{\infty }})\}$ are continuous, nonnegative and increase pointwise to ${\mathbf{1}}_W$. Each support is contained in the compact set $\{d(y,W^c)\ge 1\mathrm{/}j,\mathrm{\parallel }y{\mathrm{\parallel }}_{\mathrm{\infty }}\le j+1\}\subset W$, so ${\phi }_j{\mathrm{\mid }}_V$ has compact support in $V$. Applying [L1] to each ${\phi }_j$ and [L2] to the two monotone limits gives $\nu (W)={\lambda }_n(W)$. The empty $W$ is immediate.

The sets $V\cap R$ above form a pi-system generating the Borel sigma-algebra of $V$. The increasing members $P_j=V\cap (-j,j{)}^n$ cover $V$ and satisfy ${\lambda }_n(P_j)<\mathrm{\infty }$; step 2.1 gives $\nu (P_j)={\lambda }_n(P_j)$. Hence [L5] makes $\nu (E)={\lambda }_n(E)$ for every Borel $E\subseteq V$. This proves the set formula without assuming that an infinite-measure equality class is closed under decreasing intersections.

Let $s={\sum }_{j=1}^m{c}_j{\mathbf{1}}_{E_j}$ be a nonnegative simple Lebesgue measurable function. By [L4], replace each $E_j$ by a Borel set differing from it only by a null set. The set formula from step 3.1 and null-set invariance in [L4] then give the change-of-variables formula for $s$.

Choose simple functions $s_k\uparrow f$ by [L3]. Step 4.1 applies to each $s_k$, and [L2] lets $k\to \mathrm{\infty }$ on both sides. This yields the formula for $f$.