[proofplan]
The strategy bootstraps the change-of-variables form of the coarea formula from the basic [Coarea Formula](/theorems/3078) by approximating $g$ with simple functions and applying the basic formula to each level set in turn. Step 1 establishes the formula for $g = \mathbf{1}_E$ where $E \subseteq \mathbb{R}^n$ is $\mathcal{L}^n$-measurable, by recognising the basic coarea formula applied to the set $A \cap E$. Step 2 extends to non-negative simple functions by linearity. Step 3 extends to general non-negative measurable $g$ via monotone approximation by simple functions and the Monotone Convergence Theorem on both sides. The slicing measurability of $t \mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k}$ — needed to even state the right-hand side — emerges as part of the construction.
[/proofplan]
[step:Establish the formula for $g = \mathbf{1}_E$ with $E \subseteq \mathbb{R}^n$ measurable]
Let $E \subseteq \mathbb{R}^n$ be $\mathcal{L}^n$-measurable, and set $g := \mathbf{1}_E$.
**Left-hand side**: for $x \in A$, $g(x) = 1$ if $x \in E$ and $0$ otherwise, so
\begin{align*}
\int_A \mathbf{1}_E(x) \, J_k f(x) \, d\mathcal{L}^n(x) = \int_{A \cap E} J_k f(x) \, d\mathcal{L}^n(x).
\end{align*}
The set $A \cap E$ is $\mathcal{L}^n$-measurable as the intersection of two $\mathcal{L}^n$-measurable sets. Apply the [Coarea Formula](/theorems/3078) to $A \cap E$. The hypotheses of Theorem 3078 are satisfied: $f: \mathbb{R}^n \to \mathbb{R}^k$ is Lipschitz with $n \ge k \ge 1$, and $A \cap E \subseteq \mathbb{R}^n$ is $\mathcal{L}^n$-measurable. The coarea formula gives
\begin{align*}
\int_{A \cap E} J_k f(x) \, d\mathcal{L}^n(x) = \int_{\mathbb{R}^k} \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E) \, d\mathcal{L}^k(t).
\end{align*}
**Right-hand side**: for each $t \in \mathbb{R}^k$, the inner integral is
\begin{align*}
\int_{f^{-1}(t) \cap A} \mathbf{1}_E(x) \, d\mathcal{H}^{n-k}(x) = \mathcal{H}^{n-k}(\{x \in f^{-1}(t) \cap A : x \in E\}) = \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E).
\end{align*}
Hence
\begin{align*}
\int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \mathbf{1}_E \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) = \int_{\mathbb{R}^k} \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E) \, d\mathcal{L}^k(t).
\end{align*}
The two sides agree (both equal the right-hand side of Theorem 3078 applied to $A \cap E$). The $\mathcal{L}^k$-measurability of $t \mapsto \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E)$, needed to interpret the integral, is part of the conclusion of Theorem 3078 (the basic coarea formula implicitly uses this measurability).
[/step]
[step:Extend to non-negative simple functions by linearity]
A non-negative simple $\mathcal{L}^n$-measurable function on $\mathbb{R}^n$ has the form
\begin{align*}
g = \sum_{i=1}^N c_i \mathbf{1}_{E_i}
\end{align*}
for finitely many constants $c_i \ge 0$ and $\mathcal{L}^n$-measurable sets $E_i \subseteq \mathbb{R}^n$.
By linearity of the Lebesgue integral on the left side (a finite linear combination), Step 1 applied to each $\mathbf{1}_{E_i}$:
\begin{align*}
\int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) &= \sum_{i=1}^N c_i \int_A \mathbf{1}_{E_i}(x) J_k f(x) \, d\mathcal{L}^n(x) \\
&= \sum_{i=1}^N c_i \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \mathbf{1}_{E_i} \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) \\
&= \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \sum_{i=1}^N c_i \mathbf{1}_{E_i} \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) \\
&= \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t).
\end{align*}
The interchange of finite sum and integral (on both the inner $\mathcal{H}^{n-k}$-integral and the outer $\mathcal{L}^k$-integral) is justified because the sum has finitely many terms and each integrand is non-negative.
The $\mathcal{L}^k$-measurability of $t \mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} = \sum_i c_i \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E_i)$ follows from the measurability obtained in Step 1 for each $E_i$, combined with finite linear combinations preserving measurability.
[/step]
[step:Extend to general non-negative measurable $g$ by monotone convergence]
Let $g: \mathbb{R}^n \to [0, +\infty]$ be $\mathcal{L}^n$-measurable. By the standard approximation theorem for non-negative measurable functions, there exists an increasing sequence $(g_j)_{j=1}^\infty$ of non-negative simple $\mathcal{L}^n$-measurable functions $g_j: \mathbb{R}^n \to [0, +\infty)$ with $g_j(x) \uparrow g(x)$ for every $x \in \mathbb{R}^n$ as $j \to \infty$.
**Left-hand side limit**: since $g_j \uparrow g$ pointwise and $J_k f \ge 0$, we have $g_j J_k f \uparrow g J_k f$ pointwise on $A$. Applying the Monotone Convergence Theorem on $(A, \mathcal{L}^n \lfloor A)$,
\begin{align*}
\int_A g_j(x) J_k f(x) \, d\mathcal{L}^n(x) \uparrow \int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) \qquad (j \to \infty).
\end{align*}
**Right-hand side limit**: for each fixed $t \in \mathbb{R}^k$, $g_j \uparrow g$ pointwise on $f^{-1}(t) \cap A$. Applying the Monotone Convergence Theorem on $(f^{-1}(t) \cap A, \mathcal{H}^{n-k})$:
\begin{align*}
\int_{f^{-1}(t) \cap A} g_j \, d\mathcal{H}^{n-k} \uparrow \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} \qquad (j \to \infty).
\end{align*}
Define
\begin{align*}
\Psi_j: \mathbb{R}^k &\to [0, \infty] \\
t &\mapsto \int_{f^{-1}(t) \cap A} g_j \, d\mathcal{H}^{n-k}, \\
\Psi: \mathbb{R}^k &\to [0, \infty] \\
t &\mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k}.
\end{align*}
Each $\Psi_j$ is $\mathcal{L}^k$-measurable by Step 2. The pointwise monotone limit $\Psi_j \uparrow \Psi$ ensures $\Psi$ is $\mathcal{L}^k$-measurable as the pointwise limit of measurable functions. Applying the Monotone Convergence Theorem to $(\Psi_j)$ on $(\mathbb{R}^k, \mathcal{L}^k)$:
\begin{align*}
\int_{\mathbb{R}^k} \Psi_j(t) \, d\mathcal{L}^k(t) \uparrow \int_{\mathbb{R}^k} \Psi(t) \, d\mathcal{L}^k(t) \qquad (j \to \infty).
\end{align*}
**Combining**: by Step 2, for each $j$,
\begin{align*}
\int_A g_j J_k f \, d\mathcal{L}^n = \int_{\mathbb{R}^k} \Psi_j(t) \, d\mathcal{L}^k(t).
\end{align*}
Passing $j \to \infty$ in this equality and using the two monotone convergence statements:
\begin{align*}
\int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) = \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} g(x) \, d\mathcal{H}^{n-k}(x) \, d\mathcal{L}^k(t).
\end{align*}
This is the coarea change of variables formula for general non-negative measurable $g$, completing the proof.
[/step]
