Coarea identity for smooth scalar functions

Put $G:=\{x\in \mathrm{\Omega }:\mathrm{\nabla }u(x)\mathrm{\ne }0\}$. The balls with rational centers and radii whose closures lie in $\mathrm{\Omega }$ and on which some ${\mathrm{\partial }}_{i}u$ never vanishes form a countable open cover of $G$ by density and countability [F5]; assign each ball the least such coordinate $i$. Each ball is convex. The map $T_i(x)=(x_1,\dots ,x_{i-1},u(x),x_{i+1},\dots ,x_n)$ has nonzero Jacobian there; it is injective because along each line parallel to the $i$th axis, $u$ is strictly monotone. Thus [F2] makes it a $C^1$ diffeomorphism onto its open image. By [F6], choose a locally finite smooth partition of unity $({\eta }_j)$ on $G$ subordinate to these chart balls. On a ball assigned coordinate $i$, write $y=x_{\widehat{i}}$ and $t=u(x)$; the inverse chart has graph form $x_i=h(y,t)$, with $\mathrm{\mid }\det D{T}_i\mathrm{\mid }=\mathrm{\mid }{\mathrm{\partial }}_{i}u\mathrm{\mid }$ and $\sqrt{1+\mathrm{\mid }{D}_{y}h{\mathrm{\mid }}^2}=\frac{\mathrm{\mid }\mathrm{\nabla }u\mathrm{\mid }}{\mathrm{\mid }{\mathrm{\partial }}_{i}u\mathrm{\mid }}$ by implicit differentiation. Change of variables [F2] and the surface density [F3], applied to the compactly supported nonnegative weight ${\eta }_j$, give ${\int }_G{\eta }_j\mathrm{\mid }\mathrm{\nabla }u\mathrm{\mid }dx={\int }_{\mathbb{R}}{\int }_{G\cap \{u=t\}}{\eta }_{j}d{\mathcal{H}}^{n-1}dt\mathrm{.}$

Sum the chart identities of step 1.1 over $j$. Since ${\sum }_j{\eta }_j=1$ on $G$, Tonelli [F8] gives ${\int }_{\mathrm{\Omega }}\mathrm{\mid }\mathrm{\nabla }u\mathrm{\mid }dx={\int }_{\mathbb{R}}{\mathcal{H}}^{n-1}(G\cap \{u=t\})dt,$ because $\mathrm{\nabla }u=0$ on $\mathrm{\Omega }\setminus G$. Sard's theorem [F1] says that outside a null set every point of a level is regular, so the integrand agrees almost everywhere in $t$ with ${\mathcal{H}}^{n-1}(\mathrm{\Omega }\cap \{u=t\})$. This also establishes measurability of the level-area function as a countable sum of the chart integrals in step 1.1.

Fix a nonzero regular value $t$ for which the area in step 2.1 is finite; throughout the proof ${\mathcal{H}}^{n-1}$ denotes the normalized graph measure from [F3], with counting measure if $n=1$. In that case every graph chart is a single point at fixed level, its empty-coordinate Jacobian is one, and the same substitution identity in step 1.1 is the ordinary one-dimensional substitution formula. Then ${\mathrm{\Gamma }}_t:=\mathrm{\Omega }\cap \{u=t\}$ is a smooth hypersurface. For a compactly supported smooth test field $\varphi$, its intersection with ${\mathrm{\Gamma }}_t$ is compact; local finiteness gives a neighborhood meeting only finitely many chart supports, whose partition sum is one there. Decompose $\varphi$ into the finite chart-supported sum and a remainder vanishing near ${\mathrm{\Gamma }}_t$. The remainder has zero divergence integral over either level set because its restriction to that open set extends as a compactly supported smooth field. Each chart term obeys the graph flux formula [F4]. Summing shows that $D{\chi }_{E_t^{+}}=+(\mathrm{\nabla }u\mathrm{/}\mathrm{\mid }\mathrm{\nabla }u\mathrm{\mid }){\mathcal{H}}^{n-1}{\mathrm{\mid }}_{{\mathrm{\Gamma }}_t}$ and $D{\chi }_{E_t^{-}}=-(\mathrm{\nabla }u\mathrm{/}\mathrm{\mid }\mathrm{\nabla }u\mathrm{\mid }){\mathcal{H}}^{n-1}{\mathrm{\mid }}_{{\mathrm{\Gamma }}_t}$. The level ${\mathrm{\Gamma }}_t$ is relatively closed in $\mathrm{\Omega }$; hence this measure is finite and Radon by the graph area construction [F3], and [F7] gives its partition variation as exactly ${\mathcal{H}}^{n-1}{\mathrm{\mid }}_{{\mathrm{\Gamma }}_t}$. Hence the indicator is BV and its perimeter equals that area. For $t>0$ and $t<0$, respectively, Markov's inequality gives $\mathrm{\mid }{E}_t^{+}\mathrm{\mid }\le t^{-1}\mathrm{\parallel }u{\mathrm{\parallel }}_1$ and $\mathrm{\mid }{E}_t^{-}\mathrm{\mid }\le \mathrm{\mid }t{\mathrm{\mid }}^{-1}\mathrm{\parallel }u{\mathrm{\parallel }}_1$, so the indicators are in $L^1$. The area integral is finite, so almost every applicable nonzero level is regular and has finite area by step 2.1; the required perimeter equality and almost-everywhere finiteness follow.