Dynamic Programming

Motivation

A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.

Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.

Setting

The states form a finite set $\mathcal X=\{1,\dots,n\}$, the decision horizon is $T=\{0,1,\dots,N-1\}$, and the action set $\mathcal A$ is finite, nonempty and the same in every state. Costs are $c_t(i,a)\ge0$ for $t\in T$, and there is a terminal cost $c_N(i)$. The system starts in a given state $i_0$.

Write $\Delta_n=\{p\in\mathbb R^n_+ : p^{\mathsf T}\mathbf 1=1\}$ for the probability simplex. For every action $a$ and state $i$, a nonempty set $\mathcal P_i^a\subseteq\Delta_n$ describes the possible $i$-th rows of the transition matrix under $a$. No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix $P^a$ is the product $\mathcal P^a=\mathcal P_1^a\times\cdots\times\mathcal P_n^a$.

A controller policy $\pi=(\mathbf a_0,\dots,\mathbf a_{N-1})$ consists of maps $\mathbf a_t:\mathcal X\to\mathcal A$, and $\Pi=\mathcal A^{nN}$ is the set of such policies. A policy of nature $\tau=(P_t^a)_{a\in\mathcal A,t\in T}$ picks, for every stage, action and state, a row $p_i^a(t)\in\mathcal P_i^a$. The admissible set is $\mathcal T=(\bigotimes_a\mathcal P^a)^N$, so nature may change the matrices from stage to stage. The expected total cost is

$$C_N(\pi,\tau)=\mathbf E\Big(\sum_{t=0}^{N-1}c_t(i_t,\mathbf a_t(i_t))+c_N(i_N)\Big),$$

where the state $i_t$ evolves as a Markov chain with transition matrix $P_t^{\mathbf a_t(i)}$ from state $i$. The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v)=\sup\{p^{\mathsf T}v : p\in\mathcal P\}$. The robust recursion (7) starts from $v_N=c_N$ and sets

$$v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big),$$

and for a fixed $\pi$ the evaluation recursion (10) starts from $v_N^\pi=c_N$ and sets $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$.

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

$$\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau),$$

together with three further statements. First, $\sup_{\tau}C_N(\pi,\tau)=v_0^\pi(i_0)$ for every $\pi$. Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves $v_0(i_0)$ in the worst case. Third, every nature policy whose rows attain the suprema $\sigma_{\mathcal P_i^a}(v_{t+1})$ (rule (9)) forces the value $v_0(i_0)$ on every controller.

Milestones

1. Lemma 1: a problem $\max q^{\mathsf T}v_0$ subject to $v_t\le g_t(v_{t+1})$ with monotone $g_t$ and $q\ge0$ is solved by the recursion $v_t=g_t(v_{t+1})$.
2. Support functions of nonempty subsets of $\Delta_n$ are componentwise nondecreasing.
3. The constraint maps of problems (15) and (16) are componentwise nondecreasing.
4. Eq. (14): for fixed $\pi$ and fixed matrices, $C_N(\pi,\tau)$ is the value of a linear program.
5. Eq. (16): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$.
6. Eq. (15): $\sup_{\tau\in\mathcal T}\min_{\pi}C_N(\pi,\tau)=v_0(i_0)$.

Significance

Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost $p^{\mathsf T}v_{t+1}$ of nominal dynamic programming is replaced by the support function $\sigma_{\mathcal P_i^a}(v_{t+1})$. The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of $\sigma$ for likelihood and entropy models, which the other missions of this series formalize.

The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.

Difficulty

The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets $\mathcal P_i^a$ are neither closed nor convex, so the suprema in $\sigma$ need not be attained, and $\mathcal T$ is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.

Formalization scope

• States are Fin n and stages Fin N. Values $v_0,\dots,v_N$ are indexed by natural numbers, and only $t\le N$ is meaningful. Vectors are Fin n → ℝ with the componentwise order.
• The model is a structure holding the costs ($c_t\ge0$), the terminal cost (no sign assumed), and the row sets. Every row set must be nonempty and contained in stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it $\mathcal T$ is empty, and a real supremum over an empty index is $0$.
• Rectangularity is built in: a nature policy is a function $\tau(t,a,i)$ with $\tau(t,a,i)\in\mathcal P_i^a$. Nature does not observe the realised trajectory, and stationary nature ($\mathcal T_s$) is not the set used here.
• $C_N$ is defined by the forward state distribution, not by a backward recursion. Defining it backward would make the evaluation statements hold by definition, which is the trivializing formalization this choice rules out.
• $\sigma_{\mathcal P}$ is the real sSup of $\{p^{\mathsf T}v\}$. This is the true supremum because the set is nonempty and bounded above by $\max_j v_j$.
• Maxima over nature are suprema: ⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty $\Pi$ and over $\mathcal A$ are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.
• The terminal value $v_N=c_N$ is not printed in Theorem 1. It is taken from the proof and from Step 1 of the paper's algorithm (p. 785). The composition $g_1\circ\cdots\circ g_N$ in Lemma 1 is read as $g_0\circ\cdots\circ g_{N-1}$.
• Not included: Corollary 1 (the sequential game) and the accuracy part of Theorem 2. Contributions of either as additional theorems on these definitions are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• C. C. White, H. K. Eldeib, Markov Decision Processes with Imprecise Transition Probabilities, Operations Research 42(4):739–749, 1994. https://doi.org/10.1287/opre.42.4.739
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Many firms learn part of future demand before it has to be served: customers place orders days or weeks ahead of the date they need the goods, or commit to delivery dates in contracts. Advance demand information of this kind reduces the uncertainty the inventory manager has to protect against, and the question is how replenishment decisions should use it. Gallego and Özer (Management Science 47(10), 2001) model orders placed up to $N$ periods ahead and a supply lead time $L$. They show that, with a fixed ordering cost, the classical $(s,S)$ structure survives with parameters that depend on the observed future demand, and they identify when that dependence disappears.

The classical theory this builds on is the finite-horizon inventory model with a set-up cost. Scarf (1960) introduced $K$-convexity to prove that $(s,S)$ policies are optimal there. Veinott (1966) and Iglehart (1963) bounded the optimal policy parameters by myopic quantities. Gallego and Özer extend both results to a state that carries a vector of observed demands.

Setting

Periods are $t = 1, \dots, T$. In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ for periods $t, \dots, t+N$; $D_t$ is a random vector with law $\mu_t$ and nonnegative components. The lead time $L$ and the information horizon $N$ satisfy $N > L+1$; write $M = N - L - 1 \ge 1$. The state at the start of period $t$ is a pair $(x_t, o_t)$: the modified inventory position $x_t \in \mathbb{R}$, and the vector

$$o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M$$

of demands already observed for the periods beyond the protection period $t, \dots, t+L$.

The manager raises $x_t$ to an order-up-to level $y \ge x_t$, paying a set-up cost $K_t > 0$ if $y > x_t$. After $D_t$ is observed, the state moves to

$$x_{t+1} = y - \sum_{s=t}^{t+L+1} D_{t,s} - o_{t,t+L+1},\qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ \ (s = t+L+2,\dots,t+N),$$

with $o_{t,t+N} = 0$. With a convex single-period cost $G_t$, discount factors $\alpha_t > 0$ and $\delta(z) = \mathbf 1\{z > 0\}$, the optimal cost satisfies $J_{T+1} \equiv 0$ and

$$J_t(x, o) = \min_{y \ge x}\{K_t\delta(y - x) + V_t(y, o)\},\qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb E\,J_{t+1}(x_{t+1}, o_{t+1}).$$

Let $H_t(x, o) = K_t + \min_{y\ge x}V_t(y,o) - V_t(x,o)$. The order-up-to level $S_t(o)$ is the least minimizer of $V_t(\cdot, o)$, and the reorder point is $s_t(o) = \max\{x : H_t(x,o) \le 0\}$.

A function $g$ is $(a,b)$-convex, $g \in C(a,b)$, if $g(\theta x_1 + (1-\theta)x_2) \le \theta(a + g(x_1)) + (1-\theta)(b + g(x_2))$ for all $x_1 \le x_2$ and $\theta \in [0,1]$; $C(0,K)$ is Scarf's $K$-convexity. In the stationary problem $G_t = G$, $K_t = K$, $\alpha_t = \alpha$ and $\mu_t = \nu$, and the myopic levels are

$$S^m = \min\{y : G(y) \le G(x)\ \forall x\},\quad s^m = \max\{y \le S^m : G(y) \ge K + G(S^m)\},\quad \overline S = \inf\{y > S^m : G(y) > G(S^m) + \alpha K\}.$$

Formalization targets

Goal: Theorem 2 (p. 1350)

For the stationary problem, every $1 \le t \le T$ and every observed-demand vector $o_t \ge 0$,

$$o_{t,t+L+1} \ge \overline S - s^m \implies S_t(o_t) = S^m.$$

Only the observed demand for the first period beyond the protection period is compared with the threshold; the other components of $o_t$ are free.

Milestones

• Lemma 1, Parts 1, 2, 4, 5 (p. 1349): inclusion, positive combinations, expectations, and $g(\max(x,s))$ for $(a,b)$-convex functions.
• Lemma 2 and Corollary 1 (p. 1350): for $V \in C(0,K)$ with a minimizer $S$, $H$ changes sign once from $-$ to $+$, and (for continuous $V$) $J(x) = V(\max(s,x))$.
• Theorem 1, Parts 1–3 (p. 1350): $V_t(\cdot, o_t) \in C(0, K_t)$ is coercive, a state-dependent $(s_t(o_t), S_t(o_t))$ policy is optimal, and $J_t(\cdot, o_t) \in C(0, K_t)$ with its limits at $\pm\infty$.
• Lemma 3 (p. 1351): $S^m \le S_t(o_t) \le \overline S$ and $s^m \le s_t(o_t)$.

Significance

Theorem 1 says that advance demand information does not destroy the $(s,S)$ structure: the optimal policy is still a reorder point and an order-up-to level, now functions of $o_t$. Theorem 2 is a horizon result. Once enough demand is already booked for period $t+L+1$, the order-up-to level is the myopic one, computed from $G$ alone, and the rest of the information vector can be ignored. The threshold $\overline S - s^m$ grows with the set-up cost. In practice the manager then orders only to cover demand up to period $t+L$, knowing another order will be placed in period $t+1$, and the search for state-dependent policies is confined to states with little booked demand.

The results are proved in the paper, with some steps argued informally (the unit forward difference in Lemma 3, a minimum over an open set in the definition of $\overline S$). As far as the platform's catalog shows, no $(s,S)$ optimality theorem of this form has a machine-checked proof: the platform has $K$-convexity lemmas for a single constant, not for $(a,b)$-convexity or a dynamic program with a vector state. A formal proof would check the infinite-state induction and the conditions under which the expectation in (9) is finite. The $(a,b)$-convexity layer and the one-period results (Lemma 2, Corollary 1) are reusable for any set-up cost model.

Difficulty

The obvious induction proves $K$-convexity of $V_t$ and then applies Scarf's argument. The vector state makes each step conditional on facts the scalar case gets for free. The expectation in (9) mixes a random shift of $x$ with a random update of $o$, so preserving $K$-convexity needs Lemma 1, Part 4 rather than the scalar version. Coercivity and continuity of $V_t(\cdot, o)$, and measurability and integrability of $D \mapsto J_{t+1}(x_{t+1}, o_{t+1})$, must be carried through the induction jointly in $(x, o)$. They cannot be assumed.

For Theorem 2, $V_t$ is not a function of $G$ alone, and a comparison of $S_t(o_t)$ with $S^m$ has to control $\mathbb E J_{t+1}$. That requires the lower bound $s^m \le s_{t+1}(o_{t+1})$ at the next period, which holds only on the nonnegative state space.

Formalization scope

Everything is stated about the functional equation (8)–(9). The paper derives it in Appendix A from a control problem over history-dependent policies, citing Özer (2000); that reduction is out of scope. The demand vector is Fin (L + M + 2) → ℝ and $o$ is Fin M → ℝ, with component $j$ equal to $o_{t,t+L+1+j}$. $J$ is defined by backward recursion, minima over $y \ge x$ are infima over $\{y : x \le y\}$, and expectations are Bochner integrals. $G_t$ is an abstract primitive, not built from holding and penalty costs.

The paper's hypotheses are $G_t$ convex with $G_t(y) \to \infty$ as $|y| \to \infty$ (stated for $\widetilde G_t$, used for $G_t$), $K_t > 0$ (Section 4), and $\alpha_{t+1}K_{t+1} \le K_t$. The formalization adds hypotheses the paper uses without stating:

• positive discount factors;
• demands nonnegative almost surely;
• every demand component has a finite mean, and $|G_t(y)| \le a_t + b_t|y|$ (so the expectation in (9) is finite);
• continuity of $V$ in the abstract Corollary 1;
• nonnegative observed demands $o_t$ in Lemma 3 and Theorem 2, where the lower bound fails for negative $o_{t,t+L+1}$.

All hypotheses are placed on the primitives; nothing is assumed about the derived $V_t$ or $J_t$. A Solutions/verification instance ($G(y) = |y|$, $K = 1$, $\alpha = 1/2$, zero demand) shows these hypotheses can be met together.

The definition of $\overline S$ is read as an infimum: the paper prints a minimum over an open set. $S_t(o_t)$ and $s_t(o_t)$ appear through IsLeast and IsGreatest, never as sInf/sSup values. A default value therefore cannot satisfy a conclusion, and vacuous readings (an empty minimizer set, an unbounded reorder set) are excluded. The infinite-horizon results (Lemma 4, Theorem 3, Corollary 2) and the zero set-up cost case are not part of this mission. Contributions are welcome at every level, and most of all a reusable library for $(a,b)$-convex functions.

Selected references

• G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott, On the Optimality of (s,S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

Motivation

Infinite-horizon optimal control problems with nonnegative costs (Strauch's negative dynamic programming, the positive-cost counterpart of Blackwell's positive model) are among the settings where the standard tools of discounted dynamic programming fail: there is no contraction, costs may be infinite, and the value-iteration algorithm started from zero may converge to the wrong limit. Strauch showed in 1966 that under these assumptions the limit of value iteration can lie strictly below the optimal cost (Strauch 1966). Bertsekas (1977) recast the deterministic, stochastic and minimax versions of these problems as one abstract problem about a monotone mapping $H$, and proved Bellman's equation, optimality criteria for stationary policies, and conditions for convergence of the dynamic programming algorithm at that level of generality (Bertsekas 1977). This framework became the basis of the "abstract dynamic programming" theory developed later in Bertsekas and Shreve (1978) and Bertsekas (2013, 2022).

This mission formalizes the part of the paper that works under the uniform increase assumption, culminating in the paper's compactness condition for convergence of value iteration.

Setting

A model consists of a nonempty state space $S$, a control space $C$, for each $x\in S$ a nonempty constraint set $U(x)\subseteq C$, a mapping $H:S\times C\times F\to[-\infty,+\infty]$, where $F$ is the set of functions $J:S\to[-\infty,\infty]$ ordered pointwise, and a terminal function $\bar J\in F$ with $\bar J(x)>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for $u\in U(x)$.

A selector is $\mu:S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors, and $\{\mu,\mu,\dots\}$ is stationary. Define

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$ $$J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J)(x),\qquad J^*(x)=\inf_\pi J_\pi(x),\qquad J_\infty(x)=\lim_{N\to\infty}T^N(\bar J)(x).$$

$J^*$ is the optimal value function and $J_\infty$ the limit of the dynamic programming algorithm. A policy is optimal if $J_\pi=J^*$.

Assumption I is $\bar J(x)\le H(x,u,\bar J)$ for all $x$ and $u\in U(x)$. Assumption I.1 says that $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $\bar J$. Assumption I.2 says there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+re)\le H(x,u,J)+\alpha r$ for $r>0$ and $J\ge\bar J$, where $e\equiv1$. For the convergence analysis the paper introduces, for $k\ge1$, the sets $C_k=\{(x,u,\lambda)\mid u\in U(x),\ H[x,u,T^{k-1}(\bar J)]\le\lambda\}$ with $\lambda$ real, their projections $P(C_k)$ on $(x,\lambda)$ through admissible $u$, and the closure $\overline{P(C_k)}$ obtained by adding limits of real sequences $\lambda_n$ at fixed $x$.

Formalization targets

Goal: Proposition 12

Let I, I.1, I.2 hold, let $C$ be a Hausdorff topological space, and suppose there is $\bar k$ such that $U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ is compact for every $x$, real $\lambda$ and $k\ge\bar k$. Then

$$P\Bigl(\bigcap_{k\ge1}C_k\Bigr)=\bigcap_{k\ge1}\overline{P(C_k)},\qquad J_\infty=T(J_\infty)=T(J^*)=J^*,$$

and there exists an optimal stationary policy.

Milestones

In attack order: Proposition 2 ($J_N=T^N(\bar J)$ for the $N$-stage problem); Proposition 4 ($\varepsilon$-optimal policies, stationary when $\alpha<1$); Proposition 5 (Bellman's equation $J^*=T(J^*)$ and minimality of $J^*$ among $T$-excessive functions above $\bar J$); Corollary 5.1 (the same for $J_\mu$); Proposition 7 ($\{\mu^*,\mu^*,\dots\}$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$); Proposition 10 ($J_\infty\le T(J_\infty)\le T(J^*)=J^*$, with equality throughout iff $J_\infty=T(J_\infty)$); Lemma 2 ($\overline{P(C_k)}=E[T^k(\bar J)]$, the epigraph); Proposition 11 (convergence of value iteration is equivalent to interchanging projection and intersection); Lemma 3 (a function with compact real sublevel sets attains its minimum).

Significance

The result. Proposition 12 gives a checkable condition, compactness of sublevel sets of the one-stage costs, under which value iteration started at $\bar J$ converges to the optimal cost and an optimal stationary policy exists, in any model covered by the abstract framework: deterministic and stochastic control with nonnegative costs, minimax control, and problems with state constraints encoded by infinite costs. Without such a condition the algorithm can stall below $J^*$ even in one-dimensional deterministic problems. Propositions 5 and 7 are the abstract form of the classical Bellman equation and optimality criterion for positive-cost problems.

Formalizing it. The results are proved in the paper. The platform's existing dynamic programming results are finite-state, real-valued and contraction-based; none covers extended-real costs, general state spaces, or the uniform increase regime. This mission would produce a machine-checked abstract DP layer over EReal in which the Bellman equation, the stationary-policy criterion and the convergence conditions are proved once for every model satisfying the assumptions. No machine-checked proof of these results is known.

Difficulty

The obvious argument for $J_\infty=J^*$ interchanges a limit in $N$ with an infimum over policies. Under Assumption I the iterates increase, and a limit of infima of an increasing family can be strictly smaller than the infimum of the limits; the paper's own example in Section 1 shows it. Monotone convergence arguments therefore do not apply. The paper converts the interchange into a statement about projections of the sets $C_k$ and closes the gap with a compactness argument, which requires handling infinite values carefully: epigraphs are taken over real $\lambda$ only, and states where the value is $+\infty$ are treated separately. Proposition 4, on which Bellman's equation rests, needs a selection of nearly optimal policies state by state and a geometric control of the errors through I.2.

Formalization scope

Functions in $F$ are S → EReal. Policies are sequences ℕ → Selector, where a selector is a function with $\mu(x)\in U(x)$ for all $x$. The composition $T_{\mu_0}\cdots T_{\mu_{N-1}}$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ and $J_\infty$ are limUnder atTop of their defining sequences. Every statement assumes Assumption I, under which these sequences are nondecreasing and the limits exist. $T$ takes the infimum over $U(x)$ only and $J^*$ over admissible policies only. Both $S$ and each $U(x)$ are nonempty. $\lambda$ ranges over $\mathbb R$, and the closure $\overline{\,\cdot\,}$ is the sequential closure in $\lambda$ at fixed $x$, not a topological closure on $S\times\mathbb R$. The sets $C_k$ are used only for $k\ge1$. I.2 is parameterized by its scalar $\alpha$. Proposition 4's second part refers to the $\alpha$ for which I.2 is assumed.

Repairs of the page. Lemma 3 is false as printed. On $\mathbb N$ with the cofinite topology every subset is compact, yet $f(n)=-n$ has no minimum. It also fails for $U=\emptyset$. The mission states Lemma 3 for a Hausdorff space $C$ and nonempty $U$, and Proposition 12 for a Hausdorff control space. Proposition 12 is also false as printed: with $S=\{0\}$, $C=U(0)=\mathbb N$ cofinite, $\bar J(0)=0$ and $H(0,u,J)=J(0)+1/(u+1)$, all hypotheses hold but no stationary policy is optimal and (70) fails. Proposition 11(b)'s parenthetical "(equivalently there exists an optimal stationary policy)" holds only together with $J_\infty=J^*$ (the paper cites an example with an optimal stationary policy and $J_\infty\neq J^*$). It is stated in that joint form, never as an equivalence between condition (68) and the bare existence of an optimal stationary policy.

Trivializing readings ruled out. An empty constraint set would make $T\equiv+\infty$ and the policy set empty, so every Bellman identity would hold trivially. The model therefore requires $U(x)\neq\emptyset$. The goal's three conclusions, (70), the chain of equalities and the optimal stationary policy, are all required, so a formalization that states only one of them is not the goal.

Needed infrastructure: monotone limits in EReal, infima over sets, and compactness in Hausdorff spaces (Mathlib's Cantor intersection theorem). The definitions (model, assumptions, epigraph sets) can be reused for the companion mission under Assumption D and for later abstract DP developments. Proofs of any milestone are welcome, as are reusable lemmas on monotone EReal sequences.

Selected references

• D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. http://web.mit.edu/dimitrib/www/abstractdp.html

Motivation

Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.

Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).

Timeline:

• 1953: Shapley introduces stochastic games (PNAS 39).
• 1960: Howard, Dynamic Programming and Markov Processes, policy iteration for known transitions.
• 1973: Satia and Lave, max-min and max-max policy iteration for uncertain transitions (dynamic-programming equations and optimality of pure stationary policies cited from Satia's 1968 Stanford thesis).
• 2005: Iyengar; Nilim and El Ghaoui, robust dynamic programming under rectangular uncertainty.

Setting

There are finitely many states $i$ and, in state $i$, a finite nonempty set $D_i$ of decisions $k$. A transition $i\to j$ under decision $k$ earns reward $r^k_{ij}$; rewards are discounted by $\beta$ with $0\le\beta<1$. For every pair $(i,k)$ there is a nonempty, closed, convex set $S_i^k$ of probability rows $p=(p_1,\dots,p_N)$, $p_j\ge0$, $\sum_j p_j=1$. Nature's choice is a matrix $P\in S$: one row $p_i^k\in S_i^k$ for every pair.

A pure stationary policy $A=(A_1,\dots,A_N)$ selects $A_i\in D_i$. Under $P$ its present value $v^A(P)$ is the unique solution of equations (5),

$$v_i^A=\sum_j p^{A_i}_{ij}\big(r^{A_i}_{ij}+\beta v_j^A\big).$$

Nature's minimum is $\underline v_i(A)=\inf_{P\in S}v_i^A(P)$, and the max-min return of criterion (2) is $\bar v_i=\max_A\underline v_i(A)$. A policy is max-min optimal if $\underline v(A)=\bar v$ in every state.

The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes $A$, computes $v^A$ from the current rows, replaces each row at $A_i$ by a minimizer of $\sum_j p_j(r^{A_i}_{ij}+\beta v^A_j)$ over $S_i^{A_i}$ (6), and stops when the minima reproduce $v^A$. Phase 2 (policy improvement) chooses in each state a decision $B_i$ maximizing the test quantity (7),

$$t_i^k(v)=\min_{p\in S_i^k}\sum_j p_j\big(r^k_{ij}+\beta v_j\big),$$

at $v=\underline v(A)$, keeping $A_i$ on ties; if $B=A$ the algorithm terminates.

Formalization targets

Goal: Proposition 5 with Proposition 3

Along every run $A^0,A^1,\dots$ of Phase 2 steps,

$$\underline v(A^n)\le\underline v(A^{n+1})\ \ \forall n,\qquad \exists\,n<\#\{\text{policies}\}:\ A^{n+1}=A^n,\ \ \underline v(A^n)=\bar v,$$

and the terminal policy attains the solution of the equations (4) and is $\varepsilon$-optimal for every $\varepsilon>0$.

Milestones

• Eq. (5): the present-value equations have a unique solution.
• $[I-\beta P]^{-1}$ is nonnegative with diagonal at least 1 for stochastic $P$ (proof of Proposition 5).
• Proposition 1: equations (4), with randomized decisions and mixed choices of nature, have a unique solution, and it is the max-min return.
• Proposition 2: a pure stationary policy attains it.
• A non-final Phase 1 iteration lowers nature's value weakly everywhere and strictly somewhere (proof of Proposition 4).
• Proposition 4: Phase 1 comes within $\varepsilon$ of nature's optimum after finitely many iterations.
• Proposition 3: at termination no pure stationary policy is better.
• Each policy change strictly improves the max-min return (proof of Proposition 5).

Significance

The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every $S_i^k$ a single row) recovers Howard's policy iteration.

On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.

Difficulty

The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix $P^{*B}$ minimizing against $B$ is not the one minimizing against $A$. Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.

Formalization scope

States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at $N=1$ and trivially true at $N=0$), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:

• $0\le\beta<1$ (not printed; every return is an infinite discounted sum) and nonempty $S_i^k$ (not printed; Phase 1 presupposes a feasible row) are added standing hypotheses; closedness and convexity are the paper's.
• The present value is $[I-\beta P^A]^{-1}$ applied to the one-step rewards; the Eq. (5) milestone proves it is the unique solution of (5).
• "min over $p_i^k\in S_i^k$" in (2) is an infimum over the nonempty type of admissible choices $P\in S$, bounded below; "max over all policies" is a maximum over pure stationary policies, with randomization handled in (4).
• In (4), $\tau$ ranges over probability vectors on $D_j$ and $\alpha$ over probability measures on row vectors with $\alpha(S_j^k)=1$; the missing integral sign and unmatched brace of the printed display are corrected.
• "Optimal" = equal to the max-min return in every state; "$\varepsilon$-optimal" = within $\pm\varepsilon$ in every state (p. 731); "$\varepsilon$-optimal for nature" = within $\varepsilon$ of nature's minimum.
• "Terminates" = Phase 2 returns the same policy; "a finite number of iterations" is stated with the explicit bound "fewer than the number of policies".
• Phase 1 is taken exact in Phase 2 (the proofs of Propositions 3 and 5 use exact minimizers); the Phase 1 stopping test is printed without $\Sigma$ and the sum is formalized.
• Retention rule: Phase 2 keeps $A_i$ when it is already a maximizer. It is not printed, but it is Howard's rule and Proposition 5 is false without it.
• Proposition 5's "$\varepsilon$-optimal … in a finite number of iterations" is formalized as exact termination at an optimal policy, which implies the printed claim for every $\varepsilon$.

Equation (4) must not be collapsed to $\max_k\min_{p\in S_j^k}$ in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.

Needed infrastructure: Neumann series for $I-\beta P$ with stochastic $P$, monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• L. S. Shapley, Stochastic Games, PNAS 39(10), 1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5), 780–798, 2005. https://doi.org/10.1287/opre.1050.0216

Motivation

Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).

Setting

A finite-horizon episodic Markov Decision Process $M = (S, A, \{P^M_h\}_{h=1}^H, \{R^M_h\}_{h=1}^H, d_1)$ consists of a finite state space $S$, a finite action space $A$, a horizon $H$, per-layer transition kernels $P^M_h : S\times A \to \Delta(S)$ and reward distributions $R^M_h : S\times A \to \Delta(\mathbb R)$, and an initial state distribution $d_1 \in \Delta(S)$. An episode unrolls for $h=1,\dots,H$: the learner selects an action $a_h \sim \pi_h(s_h)$ under a randomized non-stationary policy $\pi = (\pi_1,\dots,\pi_H) \in \Pi^{\mathrm{rns}}$ (each $\pi_h : S \to \Delta(A)$), receives reward $r_h \sim R^M_h(s_h,a_h)$, and transitions to $s_{h+1}\sim P^M_h(s_h,a_h)$. The value of $\pi$ is $f^M(\pi) := \mathbb E^{M,\pi}[\sum_h r_h]$, and the state-action and state value functions $Q^{M,\pi}_h(s,a)$, $V^{M,\pi}_h(s)$ are the analogous reward-to-go quantities from layer $h$ onward. In the online RL problem, $M^\star$ is unknown, the learner interacts with it for $T$ episodes, and the goal is to minimize the regret $\mathrm{Reg} = \sum_{t=1}^T \big(f^{M^\star} (\pi^{M^\star}) - f^{M^\star}(\pi^t)\big)$ against the best policy $\pi^{M^\star} \in \arg\max_{\pi\in\Pi^{\mathrm{rns}}} f^{M^\star}(\pi)$.

Formalization targets

Goal — Theorem 1 (UCB-VI regret)

$$\exists\, C>0,\ \forall\, \delta\in(0,1],\quad \Pr\Big[\mathrm{Reg} \le C\cdot H\cdot S\cdot\sqrt{A\,T}\cdot\sqrt{\log(SAHT/\delta)}\Big] \ge 1-\delta,$$

for the UCB-VI algorithm run with the explicit bonus $b^t_{h,\delta}(s,a) = 2\sqrt{\log(2SAHT/\delta)/n^t_h(s,a)}$, under Assumption 6 (deterministic, known, $[0,1]$-bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in $S,A,H,T$, logarithmic in $1/\delta$), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.

Reaching it rests on three structural facts, each formalized as a milestone in attack order:

• Proposition 25 (Bellman optimality): existence of a single deterministic policy simultaneously optimal at every state, computable by backward induction — the reason dynamic programming solves planning at all.
• Lemma 13 (Performance difference) and Lemma 14 (Bellman residual decomposition): two "credit assignment" identities decomposing a value gap (between two policies, or one policy under two models) into a sum of per-layer, on-roll-in terms.
• Lemma 15 (Error decomposition for optimistic policies): the fact that a greedy policy driven by any optimistic value estimate suffers sub-optimality controlled additively — not exponentially — by that estimate's own Bellman residuals, evaluated on-policy.

Significance

The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as $\sqrt T$ in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as $\varepsilon$-greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as $H+2$ states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.

Formalizing it. No part of this chapter's mathematical content already has a faithful counterpart on the platform (see Difficulty, below, and Formalization scope). This mission contributes: (i) a from-scratch Lean formalization of the finite-horizon episodic MDP model and its value functions, faithful to the book's $0$/$1$-indexing and reward-distribution conventions; (ii) faithful statements (drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a faithful statement of Theorem 1 itself, including a from-scratch construction of the finite $T$-episode adaptive interaction process needed to make sense of a high-probability regret guarantee. Proving these — Proposition 25 by backward induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's optimism bound with a concentration argument bounding the estimation-error and martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work for solvers.

Difficulty

The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that $Q^t$ is close to $Q^{M^\star,\star}$ in some fixed sense — fails because $Q^t$'s error is itself random (it depends on the transitions observed so far) and compounds across $H$ layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided $Q^t$ is optimistic. Making $Q^t$ optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates $\widehat P^t_h$ (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all $(s,a,h,t)$ — accounting for the $SAHT$ inside the bonus's logarithm. The final regret sum further requires bounding $\sum_t \sum_h 1/\sqrt{n^t_h(s^t_h,a^t_h)}$ by a pigeonhole/potential-function argument over the visitation counts, which is where the $S\sqrt{AT}$ scaling — rather than a naive $SA\sqrt{T}$ — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.

Formalization scope

MDP and value functions. States and actions are finite types (Fintype); layers are represented $0$-indexed throughout the Lean development (the book's layer $h$ is h - 1), with the terminal convention V _ _ H _ = 0 matching $V_{H+1}\equiv 0$. Since every value/expectation formula in this chapter uses the reward distribution $R_h(s,a)\in\Delta(\mathbb R)$ only through its mean, EpisodicMDP.R records that mean directly — equivalent, by linearity of expectation, to carrying the full distribution, and changing no theorem's content. Transition kernels and policies are represented as plain real-valued functions (S → A → ℝ-style) rather than as Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields asserting the probability-distribution properties (nonnegativity, summing to $1$) where the book requires membership in $\Pi^{\mathrm{rns}}$ or a well-formed kernel; this keeps every expectation a finite Finset.sum, needing no measure theory. The optimal value functions Qstar/Vstar are defined as literal suprema over the entire (uncountable, since $|A|\ge2$) policy type — not via a recursive shortcut — which is what rules out the trivializing formalization of Proposition 25: defining Vstar by the very recursion the proposition asserts would make the proposition a tautology, whereas here it is a genuine claim about a supremum over an enormous space of competitor policies.

UCB-VI and Theorem 1. Because $S$, $A$, $H$, and $T$ are all finite, the $T$-episode adaptive interaction (in which round $t$'s policy is a function of the realized history of the first $t-1$ episodes) is modeled as a finite probability space: the outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum over it, and "with probability $\ge 1-\delta$" is a plain inequality between two real numbers — no MeasureTheory is used anywhere in this mission. The universal constant $C$ in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a literal numeral, since its value is not pinned down by the book on this page and this mission does not carry out the (non-milestoned) concentration argument that would derive it; this is the convention adopted throughout for the book's own "$\lesssim$" notation. The empirical-transition estimator inside $Q^t_h$ is defined to be $0$ when $n^t_h(s,a)=0$ (no data yet collected for that pair) — a boundary case Eq. (5.25) does not address, resolved here by convention rather than proof.

Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a diameter parameter, and its Bellman-optimality statement is the average-cost optimality equation — genuinely different from this chapter's finite-horizon episodic Bellman recursion, even though both go by the name "Bellman optimality." No reference item was reused; every definition and theorem in this mission is drafted from scratch. Both missions bound regret via optimism over a confidence set of models, but for different objectives (average reward vs. finite-horizon cumulative reward) and different MDP classes.

Reusable infrastructure and open contributions. EpisodicMDP, Policy, V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission on finite-horizon episodic RL in this book's later chapters. Contributions welcome: proofs of the four milestone lemmas (by backward induction and telescoping, respectively); the concentration lemmas underlying Theorem 1's optimism guarantee (Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof combining them.

Selected references

• Foster, D. J. and Rakhlin, A., Foundations of Reinforcement Learning and Interactive Decision Making, 2023. arXiv:2312.16730v1
• Azar, M. G., Osband, I., and Munos, R., Minimax Regret Bounds for Reinforcement Learning, ICML 2017. arXiv:1703.05449
• Jaksch, T., Ortner, R., and Auer, P., Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010).

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

$$x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,$$

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

$$\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,$$

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
• P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
• T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559