The [Leibniz integral rule](https://en.wikipedia.org/wiki/Leibniz_integral_rule), in its multivariate form, deals with differentiation of the following sort:
$$ \frac{\partial}{\partial t} \int\_{D(t)} F({\bf x}, t) \, d{\bf x} \, , \qquad D(t)\in \mathbb{R}^d \, .$$


I am looking for a fully rigorous formulation of this theorem, as well as a proper proof. So far, I could only find:


1. The one-dimensional case (see e.g., Courant calculus book).
2. Physics-flavored proofs, where the normal speed $v\_n ({\bf x})$ is not well defined (see e.g., [here](http://sgpwe.izt.uam.mx/files/users/uami/jdf/proyectos/Derivar_inetegral.pdf)). While insightful, this is not what I need.
3. Differential-geometry and form-based proofs (see the above paper). While these are valid, they are far more general than what I need.


**My question:** Are you familiar with a multivariate-calculus version and proof of this theorem?


I searched most of the textbooks mentioned [here](https://math.stackexchange.com/questions/44522/theoretical-multivariable-calculus-textbooks?rq=1) and [here](https://math.stackexchange.com/questions/43290/references-for-multivariable-calculus), but still no luck. Any ideas? I believe it is not usually covered in graduate curses of advanced multivariate analysis, and so it is pretty difficult to find it in the textbooks.


(This is [cross posted](https://math.stackexchange.com/q/2773708/161591) from math.se, since a week has passed and it recieved little-to-no-answer. Also, this is not to be confused with the Leibniz rule $(fg)'=f'g +fg'$, as in [this](https://mathoverflow.net/q/173636/42864) post.)



Rigorous multivariate differentiation of integral with moving boundaries (Leibniz integral rule)
This is probably just a more streamlined version of the proof in the article you linked to, mentioning somewhat less differential forms. I don't know a more elementary proof, but hope this is of use anyway.


I'll write $D\_t \subset \mathbb{R}^d$ for the domain of integration and I'll assume that the map $t\mapsto D\_t$ is sufficiently regular in the sense that for sufficiently short times, the motion of the domain can be described by the flow of an ambient vector field $X$ on $\mathbb{R}^d$. I.e. for each $t\in \mathbb{R}$ there should exist a vector field $X$ on $\mathbb{R}^d$ with flow $\Phi\_h:\mathbb{R}^d \to \mathbb{R}^d$ such that 
$$
D\_{t+h}=\Phi\_{h}(D\_{t}) \qquad \forall h \in (-\epsilon,\epsilon).
$$


(The field $X$ is not unique, one may add any vector field that's tangent to the boundary of $D\_t$.)


With such a vector field $X$ given we compute
\begin{align}
\frac{d}{dt} \int\_{D\_t}F(\mathbf{x},t)d\mathbf{x}
&= \lim\_{h\to 0}\frac{1}{h}\left( \int\_{D\_{t+h}}F(\mathbf{x},t+h)d\mathbf{x} - \int\_{D\_{t}}F(\mathbf{x},t)d\mathbf{x}\right)\\
&=\lim\_{h\to 0}\frac{1}{h}\left( \int\_{\Phi\_h(D\_{t})}F(\mathbf{x},t+h)d\mathbf{x} - \int\_{D\_{t}}F(\mathbf{x},t)d\mathbf{x}\right)\\
&=\lim\_{h\to 0}\frac{1}{h}\left( \int\_{D\_{t}}\Phi^\*\_h(F(\mathbf{x},t+h)d\mathbf{x}) - \int\_{D\_{t}}F(\mathbf{x},t)d\mathbf{x}\right)\\
\end{align}


(The previous equality is just the substitution rule for integrals in several variables. So $\Phi^\*\_h\left(F(\mathbf{x},t+h)d\mathbf{x}\right)$ denotes the pullback of the differential form $F(\mathbf{x},t+h)d\mathbf{x}$ along $\Phi\_h$. It's what you get by replacing every $\mathbf{x}$ with $\Phi\_h(\mathbf{x})$ in the expression $F(\mathbf{x},t+h)d\mathbf{x}$. We continue by swapping limit and integral)


\begin{align}
&=\int\_{D\_{t}}\lim\_{h\to 0} \frac{\Phi^\*\_h(F(\mathbf{x},t+h)d\mathbf{x}) - F(\mathbf{x},t)d\mathbf{x}}{h}
\end{align}


(To go on use Taylor $F(\mathbf{x},t+h)=F(\mathbf{x},t)+\frac{\partial F(\mathbf{x},t)}{\partial t}\cdot h+O(h^2)$ as well as linearity of $\Phi^\*$ and $\Phi^\*\_0=\text{id}\_{\mathbb{R}^n}$.)
$$
=\int\_{D\_{t}} \left(\frac{\partial F(\mathbf{x},t)}{\partial t}d\mathbf{x} 
+\lim\_{h\to 0}\frac{\Phi^\*\_h(F(\mathbf{x},t)d\mathbf{x}) - F(\mathbf{x},t)d\mathbf{x}}{h}\right).
$$
Now that limit in the integral is per definition $L\_X(F(\mathbf{x},t)d\mathbf{x})$, the [Lie derivative](https://en.wikipedia.org/wiki/Lie_derivative) of the form 
$\omega=F(\mathbf{x},t)d\mathbf{x}$ with respect to $X$. Using Cartan's magic formula $L\_x \omega = d(i\_X \omega)+i\_X(d\omega)$, which in our case simplifies to $L\_x \omega = d(i\_X \omega)$ since $F(\mathbf{x},t)d\mathbf{x}$ is of top degree, we get
$$
=\int\_{D\_{t}}\frac{\partial F(\mathbf{x},t)}{\partial t}d\mathbf{x} 
+\int\_{D\_{t}} d \left(i\_X(F(\mathbf{x},t)d\mathbf{x})\right)
$$
Applying [Stokes theorem](https://en.wikipedia.org/wiki/Stokes%27_theorem#Formulation_for_smooth_manifolds_with_boundary) to the second integral we finally arrive at
$$
\frac{d}{dt} \int\_{D\_t}F(\mathbf{x},t)d\mathbf{x}
=
\int\_{D\_{t}}\frac{\partial F(\mathbf{x},t)}{\partial t}d\mathbf{x} 
+\int\_{\partial D\_{t}} i\_X(F(\mathbf{x},t)d\mathbf{x}).
$$
For those who want to get rid of that insertion in the second integral, a direct computation shows that $\int\_\Gamma i\_X( f(\mathbf{x})d\mathbf{x})=\int\_\Gamma f(\mathbf{x}) X\cdot d\vec{A}$ where $d\vec{A}$ denotes the usual "surface element" with respect to the standard metric. So you can write the Leibniz integral rule as 
$$
\frac{d}{dt} \int\_{D\_t}F(\mathbf{x},t)d\mathbf{x}
=
\int\_{D\_{t}}\frac{\partial F(\mathbf{x},t)}{\partial t}d\mathbf{x} 
+\int\_{\partial D\_{t}} F(\mathbf{x},t)\, X\cdot d\vec{A}.
$$


