[proofplan] Fix a point $(t,x)$ with $t<T$ and compare the dynamic programming identity on the short interval $[t,t+h]$ with the first-order Taylor expansion of $V$ along controlled trajectories. Constant controls give one inequality against each fixed action $a\in U$, hence against the infimum over $U$. The assumed approximate minimizers for the short-time problem give the reverse inequality up to an $o(h)$ error. Dividing by $h$ and letting $h\downarrow 0$ identifies $-\partial_t V$ with the Hamiltonian, and the terminal condition follows from the value function at the degenerate terminal interval. [/proofplan]

[step:Fix a short time interval and define the Hamiltonian convention] Fix $(t,x)\in [0,T)\times\mathbb{R}^n$. Choose $h>0$ so small that $t+h\leq T$ and the dynamic programming principle is valid on $[t,t+h]$. For $a\in U$, define the constant control \begin{align*} u_a:[t,t+h]\to U,\qquad u_a(s)=a. \end{align*} By hypothesis, $u_a\in\mathcal{A}_{t,t+h}$ for all sufficiently small $h>0$. For $p\in\mathbb{R}^n$, the Hamiltonian convention used in this theorem is \begin{align*} H(x,p)=\inf_{a\in U}\{\ell(x,a)+p\cdot f(x,a)\}. \end{align*} Thus proving the Hamilton-Jacobi-Bellman equation is exactly proving \begin{align*} -\partial_t V(t,x)=H(x,\nabla_x V(t,x)). \end{align*} [/step]

[step:Use constant controls to obtain the lower bound for each action]Fix $a\in U$, and let $y_a:[t,t+h]\to\mathbb{R}^n$ denote the trajectory generated by $u_a$, so that $y_a(t)=x$ and \begin{align*} \dot y_a(s)=f(y_a(s),a). \end{align*} The dynamic programming principle gives, because the infimum is bounded above by the cost of the admissible control $u_a$, \begin{align*} V(t,x)\leq \int_t^{t+h}\ell(y_a(s),a)\,d\mathcal{L}^1(s)+V(t+h,y_a(t+h)). \end{align*} Since $y_a\in C^1([t,t+h];\mathbb{R}^n)$ and $\dot y_a(t)=f(x,a)$, the first-order expansion of a differentiable curve gives \begin{align*} y_a(t+h)=x+h f(x,a)+o(h) \end{align*} as $h\downarrow 0$. Since $\ell$ is continuous and $y_a(s)\to x$ as $s\downarrow t$, the elementary averaging property for continuous functions on shrinking intervals gives \begin{align*} \int_t^{t+h}\ell(y_a(s),a)\,d\mathcal{L}^1(s)=h\ell(x,a)+o(h). \end{align*} Since $V\in C^1([0,T]\times\mathbb{R}^n)$, Taylor expansion at $(t,x)$ gives \begin{align*} V(t+h,y_a(t+h))=V(t,x)+h\partial_t V(t,x)+h\nabla_x V(t,x)\cdot f(x,a)+o(h). \end{align*} Substituting these two expansions into the dynamic-programming inequality yields \begin{align*} 0\leq h\{\ell(x,a)+\partial_t V(t,x)+\nabla_x V(t,x)\cdot f(x,a)\}+o(h). \end{align*} Dividing by $h>0$ and letting $h\downarrow 0$ gives \begin{align*} -\partial_t V(t,x)\leq \ell(x,a)+\nabla_x V(t,x)\cdot f(x,a). \end{align*} Because $a\in U$ was arbitrary, \begin{align*} -\partial_t V(t,x)\leq \inf_{a\in U}\{\ell(x,a)+\nabla_x V(t,x)\cdot f(x,a)\}. \end{align*}[/step]

[guided]We first extract information from controls that we can name explicitly. Fix an action $a\in U$, and define the constant admissible control \begin{align*} u_a:[t,t+h]\to U,\qquad u_a(s)=a. \end{align*} Let $y_a:[t,t+h]\to\mathbb{R}^n$ be the corresponding trajectory, so $y_a(t)=x$ and \begin{align*} \dot y_a(s)=f(y_a(s),a). \end{align*} The dynamic programming principle says that $V(t,x)$ is the infimum of the short-time running cost plus the future value. Since an infimum is no larger than any particular admissible cost, applying it to $u_a$ gives \begin{align*} V(t,x)\leq \int_t^{t+h}\ell(y_a(s),a)\,d\mathcal{L}^1(s)+V(t+h,y_a(t+h)). \end{align*} Now we expand each term to first order in $h$. The theorem statement declares $y_a\in C^1([t,t+h];\mathbb{R}^n)$ and the ODE gives $\dot y_a(t)=f(y_a(t),a)=f(x,a)$. Therefore the first-order expansion of the differentiable curve $y_a$ at $t$ gives \begin{align*} y_a(t+h)=x+h f(x,a)+o(h) \end{align*} as $h\downarrow 0$. The running cost is also first-order in the interval length. The map $s\mapsto \ell(y_a(s),a)$ is continuous at $t$, so the elementary averaging property on shrinking intervals gives \begin{align*} \int_t^{t+h}\ell(y_a(s),a)\,d\mathcal{L}^1(s)=h\ell(x,a)+o(h). \end{align*} Finally, $V\in C^1([0,T]\times\mathbb{R}^n)$, so Taylor expansion in both the time and space variables at $(t,x)$ gives \begin{align*} V(t+h,y_a(t+h))=V(t,x)+h\partial_t V(t,x)+h\nabla_x V(t,x)\cdot f(x,a)+o(h). \end{align*} Substituting the two first-order expansions into the dynamic-programming inequality and cancelling $V(t,x)$ from both sides gives \begin{align*} 0\leq h\{\ell(x,a)+\partial_t V(t,x)+\nabla_x V(t,x)\cdot f(x,a)\}+o(h). \end{align*} After division by $h>0$ and passage to the limit $h\downarrow 0$, we obtain \begin{align*} -\partial_t V(t,x)\leq \ell(x,a)+\nabla_x V(t,x)\cdot f(x,a). \end{align*} This inequality holds for every fixed $a\in U$. Therefore the left-hand side is bounded above by the greatest lower bound of the right-hand side over all actions: \begin{align*} -\partial_t V(t,x)\leq \inf_{a\in U}\{\ell(x,a)+\nabla_x V(t,x)\cdot f(x,a)\}. \end{align*}[/guided]

[step:Use approximate minimizers to obtain the reverse bound for the infimum] By the assumed first-order approximate-minimizer consistency, there is a remainder $r_{t,x}(h)=o(h)$ as $h\downarrow 0$ such that \begin{align*} 0\geq h\left\{\partial_t V(t,x)+\inf_{a\in U}\bigl(\ell(x,a)+\nabla_x V(t,x)\cdot f(x,a)\bigr)\right\}+r_{t,x}(h). \end{align*} Dividing by $h>0$ and letting $h\downarrow 0$ gives \begin{align*} -\partial_t V(t,x)\geq \inf_{a\in U}\{\ell(x,a)+\nabla_x V(t,x)\cdot f(x,a)\}. \end{align*} This is precisely the reverse inequality to the one obtained from constant controls. [/step]

[step:Identify the Hamiltonian and write the differential equation] Combining the two inequalities gives \begin{align*} -\partial_t V(t,x)=\inf_{a\in U}\{\ell(x,a)+\nabla_x V(t,x)\cdot f(x,a)\}. \end{align*} By the definition of $H$, \begin{align*} -\partial_t V(t,x)=H(x,\nabla_x V(t,x)). \end{align*} Equivalently, \begin{align*} \partial_t V(t,x)+H(x,\nabla_x V(t,x))=0. \end{align*} Since $(t,x)\in [0,T)\times\mathbb{R}^n$ was arbitrary, the Hamilton-Jacobi-Bellman equation holds on $[0,T)\times\mathbb{R}^n$. [/step]

[step:Evaluate the value function at the terminal time] The terminal condition is part of the hypotheses: for every $x\in\mathbb{R}^n$, \begin{align*} V(T,x)=g(x). \end{align*} This holds for every $x\in\mathbb{R}^n$, completing the proof. [/step]