Theorem: Leibniz's Integral Rule

Let $\map f {x, t}$, $\map a t$, $\map b t$ be continuously differentiable real functions on some region $R$ of the $\tuple {x, t}$ plane.
Then for all $\tuple {x, t} \in R$:
:$\ds \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x = \map f {\map b t, t} \frac {\d b} {\d t} - \map f {\map a t, t} \frac {\d a} {\d t} + \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x
      | r = \lim_{h \mathop \to 0} \frac 1 h \paren {\int_{\map a {t + h} }^{\map b {t + h} } \map f {x, t + h} \rd x - \int_{\map a t}^{\map b t} \map f {x, t} \rd x }
      | c = {{Defof|Derivative of Real Function}}
}}
{{eqn | r = <nowiki>\lim_{h \mathop \to 0} \frac 1 h \paren {\int_{\map a {t + h} }^{\map a t} \map f {x, t + h} \rd x + \int_{\map a t}^{\map b t} \map f {x, t + h} \rd x
            + \int_{\map b t}^{\map b {t + h} } \map f {x, t + h} \rd x - \int_{\map a t}^{\map b t} \map f {x, t} \rd x }</nowiki>
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = <nowiki>\lim_{h \mathop \to 0} \frac 1 h \paren {\int_{\map b t}^{\map b {t + h} } \map f {x, t + h} \rd x - \int_{\map a t}^{\map a {t + h} } \map f {x, t + h} \rd x
            + \int_{\map a t}^{\map b t} \paren {\map f {x, t + h} - \map f {x, t} } \rd x}</nowiki>
      | c = Linear Combination of Integrals
}}
{{end-eqn}}
By the Mean Value Theorem for Integrals, there exist $\xi_a \in \closedint {\map a t} {\map a {t + h} }$ and $\xi_b \in \closedint {\map b t} {\map b {t + h} }$ such that:
{{begin-eqn}}
{{eqn | l = \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x
      | r = <nowiki>\lim_{h \mathop \to 0} \frac 1 h \paren {\paren {\map b {t + h} - \map b t} \map f {\xi_b, t + h} - \paren {\map a {t + h} - \map a t} \map f {\xi_a, t + h}
            + \int_{\map a t}^{\map b t} \paren {\map f {x, t + h} - \map f {x, t} } \rd x}</nowiki>
}}
{{eqn | r = <nowiki>\lim_{h \mathop \to 0} \frac {\map b {t + h} - \map b t} h \cdot \lim_{h \mathop \to 0} \map f {\xi_b, t + h}
            - \lim_{h \mathop \to 0} \frac{\map a {t + h} - \map a t} h \cdot \lim_{h \mathop \to 0} \map f {\xi_a, t + h}
            + \lim_{h \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h} - \map f {x, t} } h \rd x</nowiki>
      | c = Combination Theorem for Limits of Real Functions, Linear Combination of Integrals
}}
{{eqn | r = \frac {\d b} {\d t} \map f {\map b t, t} - \frac {\d a} {\d t} \map f {\map a t, t} + \lim_{h \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h} - \map f {x, t} } h \rd x
      | c = {{Defof|Derivative of Real Function}}, as well as $\xi_a \to \map a t$ and $\xi_b \to \map b t$ as $h \to 0$
}}
{{end-eqn}}
Now, consider the last term:
:$\ds \lim_{h \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h} - \map f {x, t} } h \rd x$
By Limit of Function by Convergent Sequences, it suffices to find the following for an arbitrary sequence $\sequence {h_n}_{n \mathop \in \N}$ such that $\ds \lim_{n \mathop \to \infty} h_n = 0$:
:$\ds \lim_{n \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n} \rd x$
Fix such as sequence, as well as a value for $t$.
For each $n \in \N$, define a function $\map {f_n} x$ as:
:$\map {f_n} x = \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n}$
when $\tuple {x, t}$ and $\tuple {x, t + h_n}$ are in $R$.
By the Extreme Value Theorem:
:$M = \sup_{\tuple x \in R_t} \size {\frac \partial {\partial t} \map f {x, t} }$
is well-defined, where $R_t$ is the subset of $R$ where $t$ matches our chosen value.
Then, from the Mean Value Theorem, it follows that:
:$\size {\map {f_n} x} \le M$
for all values of $n$ and $x$.
By Limit of Function by Convergent Sequences, as $n \to \infty$:
:$\ds \map {f_n} x \to \lim_{h \mathop \to 0} \frac {\map f {x, t + h} - \map f {x, t} } h = \frac \partial {\partial t} \map f {x, t}$
by definition of Partial Derivative.
Therefore, by Lebesgue's Dominated Convergence Theorem:
:$\ds \lim_{n \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n} \rd x = \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$
Combining with the result from before:
:$\ds \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x = \frac {\d b} {\d t} \map f {\map b t, t} - \frac {\d a} {\d t} \map f {\map a t, t} + \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$
{{qed}}