A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions

First identify continuous compact-support Riemann and Lebesgue integrals locally. Extend a continuous compactly supported function on an open set by zero; this is continuous because its support is compact inside that open set. On a bounding closed box it is bounded and Riemann integrable by [L1]. Its lower and upper grid step functions, disjointifying cells along null coordinate faces, have Lebesgue integrals equal to the lower and upper Darboux sums. Their difference tends to zero. After adding a fixed constant to make all functions nonnegative, monotonicity squeezes the Lebesgue integral to the Riemann integral; subtract the constant using finite integrability. Apply this to $k\in C_c(V)$ and $(k\circ T)\mathrm{\mid }\det DT\mathrm{\mid }$, whose support is contained in the compact preimage of $\mathrm{supp}k$. Riemann substitution [L1] therefore proves the Lebesgue substitution formula for $k$.

For Borel $E\subseteq V$, let $\alpha (E)={\lambda }_n(E)$ and $\beta (E)={\int }_{T^{-1}(E)}Jdx$, with $J=\mathrm{\mid }\det DT\mathrm{\mid }$. These are Borel measures by [L5]. For an open rational box $R$ with compact closure in $V$, the continuous functions $k_j(y)=\min (1,j\mathrm{dist}(y,{\mathbb{R}}^n\setminus R))$ have support in $\bar{R}$ and increase to $1_R$. Step 1.1 and monotone convergence give $\alpha (R)=\beta (R)<\mathrm{\infty }$. List all such boxes as $(R_j)$ and set $W_j={\bigcup }_{i\le j}{R}_i$. They exhaust $V$; finite inclusion-exclusion, whose terms are finite and are boxes or empty, gives agreement on $W_j$ and $W_j\cap R$ for every such box $R$. Thus the finite measures $E\mapsto \alpha (E\cap W_j)$ and $E\mapsto \beta (E\cap W_j)$ agree on the pi-system of these boxes, the empty set and $V$. This pi-system generates the Borel sets because the boxes form a countable basis of $V$. The equality class is a lambda-system: equal finite total masses allow complements and countable additivity allows disjoint unions. Apply [L5], then take $j\to \mathrm{\infty }$, to obtain $\alpha =\beta$ on all Borel sets. If $V$ is empty there is nothing to prove.

The Borel set equality of step 2.1 gives substitution for nonnegative Borel simple functions by finite sums. Explicit increasing dyadic simple approximations and [L4] extend it to all nonnegative Borel functions. This establishes the Borel formula locally without a later-page supplier.

Put $J=\mathrm{\mid }\det DT\mathrm{\mid }$, continuous and strictly positive since $T$ is a diffeomorphism. If $Z\subseteq V$ is Borel null, step 3.1 gives ${\int }_U{1}_Z(T(x))J(x)dx=0$. By [L3] and positivity of $J$, the Borel set $T^{-1}(Z)$ is null. Countable choice is used in the Borel construction and the completion interface [L2], not in the finite real/imaginary decomposition below.

For Lebesgue measurable $E\subseteq V$, write $E=A\cup N$ with $A$ Borel and $N\subseteq Z$ for Borel null $Z$, intersecting all sets with $V$. Then $T^{-1}(E)$ is a Borel set modified inside the Borel null set $T^{-1}(Z)$, hence measurable by [L2]. The indicator functions of $E,A$ and their pullbacks agree off the respective null sets, so [L3] and step 3.1 give ${\lambda }_n(E)={\int }_U{1}_E(T(x))J(x)dx$.

Finite nonnegative sums give substitution for nonnegative simple Lebesgue measurable functions. For any nonnegative measurable $h$, the explicit simple functions $s_k=2^{-k}\lfloor 2^k\min (h,k)\rfloor$ increase to $h$. Step 5.1 ensures measurability of their pullbacks, hence of $h\circ T$. By [L4], passing to the increasing limits proves ${\int }_{V}h={\int }_U(h\circ T)J$.

Apply step 6.1 first to $\mathrm{\mid }f\mathrm{\mid }$. It gives ${\int }_U\mathrm{\mid }f\circ T\mathrm{\mid }J={\int }_V\mathrm{\mid }f\mathrm{\mid }<\mathrm{\infty }$, so the transformed complex function is integrable. Write $f=u-v+i(p-q)$ using the nonnegative positive and negative parts of its real and imaginary parts; each is bounded by $\mathrm{\mid }f\mathrm{\mid }$. Apply step 6.1 to these four functions and recombine their finite integrals by [L4]. This proves the stated identity.