Lemma 1 — under D, J* is the limit of the N-stage optimal values J_N

Consider the abstract dynamic programming model of Bertsekas (1977): monotone mapping $H$, terminal function $\bar J>-\infty$, policies $\pi=\{\mu_0,\mu_1,\dots\}$ with cost $J_\pi=\lim_N(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J)$, and optimal value $J^*=\inf_\pi J_\pi$. For $N\ge1$ let

be the optimal value function of the $N$-stage problem (36). If Assumption D ($\bar J\ge H(\cdot,u,\bar J)$) holds, then for every $x\in S$

This says that under uniform decrease the infinite-horizon optimal value is the limit of the finite-horizon optimal values; it is the first half of the proof that the dynamic programming algorithm converges under D.

Formalization Note The limit is taken pointwise in $[-\infty,\infty]$ with its order topology, as Tendsto (fun N => J_N x) atTop (𝓝 (J* x)).