Let $\Omega \subset \mathbb{R}^{n}$ be open, $f: \Omega \to \mathbb{R}$ be smooth and satisfy $\nabla f(x) \neq 0$ for evert $x$. I am trying to derive the following identity: $$\int_{\Omega} \delta(f(x))h(x)dx = \int_{f(x) = 0}\frac{h(x)}{|\nabla f(x)|}dS(x).$$
I know the right hand side of the above formula is defined to be the pullback of $\delta$ with $f$. Let $u \in \mathcal{D}'(\mathbb{R})$ be a given distribution and $\varphi$ a given test function. The pullback $f^{*}u$ of $u$ with (the smooth function) $f$ is, by definition, the distribution defined by the equality: $$\langle f^{*}u,\varphi \rangle = \langle u, \varphi_{f}\rangle$$ with: $$\varphi_{f}(t) = \frac{d}{dt}\int_{\{x \in \Omega: f(x)<t\}}\varphi(x)dx.$$
I know the standard argument to start the proof of the desired formula. Let $x_{0} \in \Omega$ be fixed. Because $\nabla f(x_{0}) \neq 0$, there exists some $j=1,...,n$, which without loss of generality we assume to be $j=1$, such that $\frac{\partial f(x_{0})}{\partial x_{1}} \neq 0$. In this case, by the inverse function theorem, there exists some neighborhood $U_{x_{0}}$ of $x_{0}$ and a neighborhood $V_{x_{0}}$ of $f(x_{0})$ such that $f: U_{x_{0}}\to V_{x_{0}}$ is a diffeomorphism. Hence, the function $\rho: U_{x_{0}} \to V_{x_{0}}$ given by: $$\rho^{-1}: (x_{1},...,x_{n}) \mapsto (f(x),x_{2},...,x_{n}) = (y_{1},...,y_{n})$$ is a diffeomorphism.
Let $\varphi$ be a test function which we can assume to be such that $\text{supp}\varphi \subset U_{x_{0}}$. We can then change coordinates to obtain: $$\varphi_{f}(t) = \int_{\mathbb{R}^{n-1}}\varphi(\rho(t,y'))|\det D\rho(t,y')|dy'$$ If the underlying distributin $u$ is taken to be $u = \delta$, then: $$\langle f^{*}\delta,\varphi\rangle = \varphi_{f}(0) = \int_{\mathbb{R}^{n-1}}\varphi(\rho(0,y'))|\det D\rho(0,y')|dy'$$
Could someone help me complete the proof? I was trying to follow the proof in these notes, but I was a little confused with their argument at each step that $y' \mapsto F(0,y')$ parametrizes $M = \{x \in \Omega: f(x) = 0\}$ so it is given by $F(0,y') = (g(y'),y')$ for some function $g$ given by the implicit function theorem. Could you guys help me?
Preliminary Implicit Function Theorem Result
Let $M = \{x \in \Omega : f(x)=0 \} $ and $x_0 \in M$. For simplicity assume that $\partial_1 f (x_0) \neq 0$. Then the implicit function theorem asserts that there exist an open neighborhood $V \times U \subset \mathbb{R} \times \mathbb{R}^{n-1}$ of $x_0$ and a smooth function $g: U \to V $ so that $$(x,y) \in (V \times U) \cap M \Leftrightarrow (x,y) = (g(y),y).$$
As a consequence the function $F : U \to (V \times U) \cap M$ defined by $F(y) = (g(y),y)$ is bijective (the inverse is just $(x,y) \mapsto y)$.
From this we see that $M$ is a smooth Riemannian manifold with the subspace topology from $\mathbb{R}^{n}$, the smooth atlas build from the functions of the type $F^{-1}$ and the metric tensor inherited from $\mathbb{R}^{n}$. It can be oriented by the gradient of $f$.
In a coordinate system of the form $F^{-1}$ (as above) the area form $dS$ of $M$ is given by $$dS = \sqrt{1+ |\nabla g|^2} dy_1 \wedge \cdots \wedge dy_{n-1}$$ as derived here. Throughout i use $\nabla$ for the gradient (in cartesian coordinates) and not for the covariant derivative.
Deriving The Formula
Let $x_0\in M$ with $\partial_1 f(x_0) \neq 0$. Throughout $(x,y) \in \mathbb{R} \times \mathbb{R}^{n-1}$, possibly restricted to open subsets so that expressions make sense.
Define a map $s$ by $s(x,y) = (f(x,y), y)$ (this is your $\rho^{-1}$). Then by the inverse function theorem $s$ is a local diffeomorphisms in some neighborhood of $x_0$ with inverse $h$. Let $g$ be as above then we know that (possibly restricting the diffeo) $h(0,y) = (g(y),y)$. This follows, becauses $$(x,y) = h \circ s (x,y) = h (f(x,y),y)$$ and $f(x,y)=0$ if and only if $(x,y) = (g(y),y)$.
Note that your application of the inverse function theorem to $f$ is invalid after all $\nabla f (x_0)$ can never be an invertible linear map (its not even a square matrix). Also how can $\rho$ be defined on $U_{x_0}$ and $V_{x_0}$ when $V_{x_0}$ is a subset of $\mathbb{R}$?
You have already shown that (with the support of $\varphi$ contained in some small neighborhood of $x_0$): $$ \langle f^{*}\delta,\varphi\rangle = \varphi_{f}(0) = \int_{\mathbb{R}^{n-1}}\varphi(h(0,y))|\det Dh(0,y)|dy$$ Using the fact that $\det Dh(0,y) = 1/ \det Dh^{-1}(h(0,y)) = 1/ \det Ds (h(0,y))$ and $\det Ds = \partial_1 f$ as well as $h(0,y) = (g(y),y)$ this becomes $$ \langle f^{*}\delta,\varphi\rangle= \int_{\mathbb{R}^{n-1}}\varphi/| \partial_1 f| ( g(y), y) dy.$$ In the document it is shown from $f(g(y),y)=0$ and the chain rule, that $$ | 1/ \partial_1 f |(g(y),y) = \frac{\sqrt{1+ |\nabla g (y)|^2}} {| \nabla f ( g(y),y) |}. $$ Inserting: $$ \langle f^{*}\delta,\varphi\rangle= \int_{\mathbb{R}^{n-1}}\varphi (g(y),y) \frac{\sqrt{1+ |\nabla g (y)|^2}} {| \nabla f ( g(y),y) |}dy = \int_M \varphi(x) \frac{dS(x)}{| \nabla f(x)|},$$ which concludes the proof (locally).