[proofplan] The strategy is to bootstrap the change of variables formula from the [Area Formula](/theorems/3075) by approximating $g$ by simple functions and applying the area formula to each level set. Step 1 establishes the formula for $g = \mathbf{1}_B$ where $B \subseteq \mathbb{R}^n$ is Borel, by applying the area formula to the set $A \cap f^{-1}(B)$ and exploiting the injectivity of $f$ on $A$ to identify the multiplicity function with the indicator of $f(A) \cap B$. Step 2 extends to non-negative simple functions by linearity of the integral. Step 3 extends to general non-negative $\mathcal{H}^m$-measurable $g$ by monotone approximation by simple functions and the monotone convergence theorem. Throughout, the injectivity hypothesis converts the multiplicity function $N(f, \cdot, y)$ in the area formula into a simple indicator, allowing the area formula to be applied as a substitution rule. [/proofplan]

[step:Establish the formula for $g = \mathbf{1}_B$ with $B \subseteq \mathbb{R}^n$ Borel] Let $B \subseteq \mathbb{R}^n$ be a Borel set. We compute both sides of the change of variables formula for $g := \mathbf{1}_B$. Set $E := A \cap f^{-1}(B) = \{x \in A : f(x) \in B\}$. This set is $\mathcal{L}^m$-measurable: $f$ is continuous (hence Borel measurable) since it is Lipschitz, so $f^{-1}(B)$ is Borel measurable, and the intersection with the measurable set $A$ is measurable. **Left-hand side**: substituting $g(f(x)) = \mathbf{1}_B(f(x)) = \mathbf{1}_{f^{-1}(B)}(x) = \mathbf{1}_E(x) \cdot \mathbf{1}_A(x)$ for $x \in A$ (and the integration is over $A$), \begin{align*} \int_A g(f(x)) J_m f(x) \, d\mathcal{L}^m(x) = \int_A \mathbf{1}_E(x) J_m f(x) \, d\mathcal{L}^m(x) = \int_E J_m f(x) \, d\mathcal{L}^m(x), \end{align*} where the last step uses $E \subseteq A$ to replace integration over $A$ against $\mathbf{1}_E$ with integration over $E$. We apply the [Area Formula](/theorems/3075) to the $\mathcal{L}^m$-measurable set $E$. The hypotheses of the area formula are satisfied: $f: \mathbb{R}^m \to \mathbb{R}^n$ is Lipschitz with $m \le n$ (the hypotheses of the present theorem), and $E \subseteq \mathbb{R}^m$ is $\mathcal{L}^m$-measurable. The area formula gives \begin{align*} \int_E J_m f(x) \, d\mathcal{L}^m(x) = \int_{\mathbb{R}^n} N(f, E, y) \, d\mathcal{H}^m(y), \end{align*} where $N(f, E, y) := \#\{x \in E : f(x) = y\} = \#(f^{-1}(y) \cap E)$. **Identification of $N(f, E, y)$**: since $f$ is injective on $A$ by hypothesis and $E \subseteq A$, $f$ is injective on $E$, so $\#(f^{-1}(y) \cap E) \in \{0, 1\}$ for every $y$. Specifically, \begin{align*} N(f, E, y) = \begin{cases} 1 & \text{if } y \in f(E), \\ 0 & \text{otherwise}. \end{cases} \end{align*} Hence $N(f, E, y) = \mathbf{1}_{f(E)}(y)$. We now identify $f(E)$. By definition of $E$, $f(E) = \{f(x) : x \in A, f(x) \in B\} = f(A) \cap B$ (using injectivity of $f$ on $A$ in the forward direction: every element of $f(A) \cap B$ has a unique preimage in $A$ which lies in $E$). Hence $\mathbf{1}_{f(E)}(y) = \mathbf{1}_{f(A) \cap B}(y) = \mathbf{1}_{f(A)}(y) \mathbf{1}_B(y)$. **Right-hand side**: combining, \begin{align*} \int_A g(f(x)) J_m f(x) \, d\mathcal{L}^m(x) = \int_{\mathbb{R}^n} \mathbf{1}_{f(A)}(y) \mathbf{1}_B(y) \, d\mathcal{H}^m(y) = \int_{f(A)} \mathbf{1}_B(y) \, d\mathcal{H}^m(y) = \int_{f(A)} g(y) \, d\mathcal{H}^m(y). \end{align*} This is the change of variables formula for $g = \mathbf{1}_B$. [/step]

[step:Extend to non-negative simple functions by linearity] A non-negative simple $\mathcal{H}^m$-measurable function on $\mathbb{R}^n$ has the form \begin{align*} g = \sum_{i=1}^N c_i \mathbf{1}_{B_i}, \end{align*} for finitely many constants $c_i \ge 0$ and Borel sets $B_i \subseteq \mathbb{R}^n$ (every $\mathcal{H}^m$-measurable simple function admits a representation in terms of Borel sets, since $\mathcal{H}^m$ is a Borel measure and one can replace any measurable representative set by a Borel set differing by an $\mathcal{H}^m$-null set without changing the integral). By linearity of the Lebesgue integral on the left-hand side and of the Hausdorff integral on the right-hand side, applying Step 1 to each $\mathbf{1}_{B_i}$ separately, \begin{align*} \int_A g(f(x)) J_m f(x) \, d\mathcal{L}^m(x) &= \sum_{i=1}^N c_i \int_A \mathbf{1}_{B_i}(f(x)) J_m f(x) \, d\mathcal{L}^m(x) \\ &= \sum_{i=1}^N c_i \int_{f(A)} \mathbf{1}_{B_i}(y) \, d\mathcal{H}^m(y) \\ &= \int_{f(A)} \sum_{i=1}^N c_i \mathbf{1}_{B_i}(y) \, d\mathcal{H}^m(y) \\ &= \int_{f(A)} g(y) \, d\mathcal{H}^m(y). \end{align*} The interchanges of finite sum and integral are justified because the sum is finite and each integrand is non-negative (or $L^1$ on each integration set, since simple functions with finitely many values are bounded). [/step]

[step:Extend to general non-negative measurable $g$ by monotone convergence] Let $g: \mathbb{R}^n \to [0, +\infty]$ be $\mathcal{H}^m$-measurable. By the standard approximation theorem for non-negative measurable functions, there exists an increasing sequence of non-negative simple $\mathcal{H}^m$-measurable functions $g_k: \mathbb{R}^n \to [0, +\infty)$ with $g_k(y) \uparrow g(y)$ for every $y \in \mathbb{R}^n$ as $k \to \infty$. For the **right-hand side**: applying the Monotone Convergence Theorem to the sequence $g_k \uparrow g$ on $f(A)$ with respect to $\mathcal{H}^m$, \begin{align*} \int_{f(A)} g_k(y) \, d\mathcal{H}^m(y) \uparrow \int_{f(A)} g(y) \, d\mathcal{H}^m(y) \qquad \text{as } k \to \infty. \end{align*} For the **left-hand side**: since $g_k \uparrow g$ pointwise on $\mathbb{R}^n$, the composition $g_k \circ f \uparrow g \circ f$ pointwise on $A$ (and on $\mathbb{R}^m$). Since $J_m f \ge 0$, the products satisfy $g_k(f(x)) J_m f(x) \uparrow g(f(x)) J_m f(x)$ pointwise on $A$. The functions $x \mapsto g_k(f(x)) J_m f(x)$ are $\mathcal{L}^m$-measurable (composition of measurable functions; $f$ is continuous hence Borel measurable, $g_k$ is $\mathcal{H}^m$-measurable, and $J_m f$ is $\mathcal{L}^m$-measurable as a function of the Jacobian matrix). Applying the Monotone Convergence Theorem, \begin{align*} \int_A g_k(f(x)) J_m f(x) \, d\mathcal{L}^m(x) \uparrow \int_A g(f(x)) J_m f(x) \, d\mathcal{L}^m(x) \qquad \text{as } k \to \infty. \end{align*} By Step 2, for each $k$, \begin{align*} \int_A g_k(f(x)) J_m f(x) \, d\mathcal{L}^m(x) = \int_{f(A)} g_k(y) \, d\mathcal{H}^m(y). \end{align*} Passing to the limit $k \to \infty$ in this equality, both sides converge by the two monotone convergence applications above, yielding \begin{align*} \int_A g(f(x)) J_m f(x) \, d\mathcal{L}^m(x) = \int_{f(A)} g(y) \, d\mathcal{H}^m(y). \end{align*} This is the change of variables formula for general non-negative measurable $g$, completing the proof. (Remark on subtlety: there is a small issue concerning whether $g \circ f$ is $\mathcal{L}^m$-measurable when $g$ is only $\mathcal{H}^m$-measurable, since $\mathcal{H}^m$-null sets in $\mathbb{R}^n$ may pull back to non-measurable sets in $\mathbb{R}^m$ under $f^{-1}$. The standard resolution is to redefine $g$ on an $\mathcal{H}^m$-null subset of $f(A)$ to obtain a Borel measurable representative; the corresponding pull-back is then Borel measurable in $\mathbb{R}^m$, and the alteration does not change either integral. We have implicitly performed this reduction by working with Borel representatives in Step 2.) [/step]