Dynamic Programming and Optimal Control VI: Lookahead and RolloutTextbook
## Motivation
When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout β the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1β6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1β6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
## Setting
Two frameworks. For the stochastic bounds (Β§6.2β6.3): the basic finite-horizon model of Mission I of this series (`BertsekasDPModel`), its policy cost recursion, and the open-loop cost of a fixed control sequence (`BertsekasDPOpenLoopCost`). For rollout (Β§6.4.1): a **graph search problem** β a finite digraph with destination set and terminal costs $g(i)$ on destinations (`BertsekasGraphSearch`); a **base heuristic** $\mathcal{H}$ producing from every node a path to a destination (`BertsekasBaseHeuristic`), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$; the **rollout algorithm** $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (`BertsekasIsRolloutRun`). $\mathcal{H}$ is *sequentially consistent* if its paths have the tail property (Def. 6.4.1), *sequentially improving* if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).
## Target
For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$:
$$g(i_{\bar m}) \;\le\; H(i_1), \qquad g(i_{\bar m}) \;=\; \min\Big\{ H(i_1),\ \min_{j \in N(i_1)} H(j),\ \dots,\ \min_{j \in N(i_{\bar m - 1})} H(j) \Big\},$$
β `BertsekasDP.rollout_sequential_improvement` (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
## Significance
Prop. 6.4.2 is the "rollout never hurts" theorem β the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
## Difficulty
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the `IsLeast` membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one β it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
## Formalization scope
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs β the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in Β§6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Β§6.2β6.4.) http://www.athenasc.com/dpbook.html
- G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, *NIPS* 1996. https://papers.nips.cc/paper/1302
- D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, *J. Heuristics* 3 (1997), 245β262. https://doi.org/10.1023/A:1009635226865
9 thms2 active usersReviewed
πCompleted
Captain: Shuze Chen
Dynamic Programming and Optimal Control IV: LQR and the Riccati EquationTextbook
## Motivation
The discrete-time Riccati equation is the central object of linear-quadratic optimal control β the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005, Β§4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of Β§4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies β a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
## Setting
Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (`BertsekasRiccatiMap`)
$$F(P) = A^\top\big(P - P B (B^\top P B + R)^{-1} B^\top P\big) A + Q.$$
$(A,B)$ is **controllable** if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (`BertsekasControllablePair`); $(A,C)$ is **observable** if $(A^\top, C^\top)$ is controllable (`BertsekasObservablePair`). Separately, $g : \mathbb{R} \to \mathbb{R}$ is **$K$-convex** (`BertsekasKConvex`, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.
## Target
$$\exists\, P \succ 0:\quad F(P) = P,\quad P \text{ unique among } P' \succeq 0,\quad F^{k}(P_0) \to P \ \ \forall P_0 \succeq 0,\quad \rho\big(A + BL\big) < 1,$$
with $L = -(B^\top P B + R)^{-1} B^\top P A$ β `BertsekasDP.riccati_convergence_stability` (goal). Milestones: Lemma 4.2.1(a)β(d) (`kconvex_of_convex`, `kconvex_combination`, `kconvex_expectation`, `kconvex_sS_structure`), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.
## Significance
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.
## Difficulty
The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument β several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
## Formalization scope
Real matrices over `Fin n`; `Matrix.PosSemidef`/`PosDef`; matrix inverse is Mathlib's total inverse (zero on singular input β harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via `spectrum β` of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, Β§4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
- R. E. Kalman, Contributions to the theory of optimal control, *Bol. Soc. Mat. Mexicana* 5 (1960), 102β119.
- H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in *Mathematical Methods in the Social Sciences*, Stanford Univ. Press, 1960.
9 thms5 active usersReviewed
πCompleted
Captain: Shuze Chen
Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook
## Motivation
Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality β stochastic shortest path (SSP) problems first (Prop. 7.2.1β7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1β7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.
## Setting
States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (`BertsekasSSPModel`). Operators
$$(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]$$
(`BertsekasSSPPolicyOp`, `BertsekasSSPBellmanOp`), $N$-stage costs by backward recursion with policy shift (`BertsekasSSPNCost`), and the survival mass $P\{x_m \ne t\}$ (`BertsekasSSPSurvival`). **Assumption 7.2.1**: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (`BertsekasDiscounted*`); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (`BertsekasSSPAvoidProb`).
## Target
Under Assumption 7.2.1, there is a vector $J^*$ with
$$T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},$$
and a stationary policy attaining $J^*$ β `BertsekasDP.ssp_main_theorem` (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.
## Significance
These are the convergence guarantees behind value iteration and policy iteration β the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.
## Difficulty
$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 β only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for *nonstationary* policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the CesΓ ro limit need not exist.
## Formalization scope
Finite states `Fin n`, finite control type, constraint sets as `Finset`s with attained minima; no termination state in the carrier β termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is `Tendsto` in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real `liminf` and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)β(e) in one statement mirroring Prop. 7.3.1.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Β§7.1β7.4.) http://www.athenasc.com/dpbook.html
- D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, *Math. Oper. Res.* 16 (1991), 580β595. https://doi.org/10.1287/moor.16.3.580
- M. L. Puterman, *Markov Decision Processes*, Wiley, 1994. https://doi.org/10.1002/9780470316887
8 thms3 active usersReviewed
πCompleted
Captain: Shuze Chen
Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook
## 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
5 thms4 active usersReviewed
πCompleted
Captain: Shuze Chen
Dynamic Programming and Optimal Control III: The Minimum PrincipleTextbook
## Motivation
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero β no HJB equation, no adjoint equations, no maximum principle β which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
## Setting
Minimize, over admissible pairs, the cost
$$h(x(T)) + \int_0^T g(x(t), u(t))\,dt \quad\text{s.t.}\quad \dot x(t) = f(x(t), u(t)),\; x(0) = x_0,\; u(t) \in U \subseteq \mathbb{R}^m,$$
with $f, g, h$ continuously differentiable (`BertsekasCTModel`). Admissible controls are piecewise continuous on $[0,T]$ β formalized as: bounded image and continuous off a finite set (`BertsekasPiecewiseContinuousOn`) β and state trajectories are continuous, satisfying the ODE off a finite set (`BertsekasCTAdmissibleFrom`, parametrized by an arbitrary start $(t_0, \xi)$). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (`BertsekasHamiltonian`).
## Target
For an optimal admissible pair $(u^*, x^*)$: there exist an adjoint $p$ and a constant $c$ with
$$\dot p(t) = -\nabla_x H(x^*(t), u^*(t), p(t)), \quad p(T) = \nabla h(x^*(T)),$$
$$u^*(t) \in \arg\min_{u \in U} H(x^*(t), u, p(t)), \qquad H(x^*(t), u^*(t), p(t)) = c,$$
away from finitely many times β `BertsekasDP.pontryagin_minimum_principle` (goal). Milestones: Prop. 3.2.1 (`hjb_sufficiency_of_continuous`), Lemma 3.3.1 (`envelope_gradient_lemma`), Prop. 3.3.2 (`discrete_minimum_principle`).
The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous β the consequence of the Β§3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$.
## Significance
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem β the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument β the book's own HJB-based derivation is explicitly informal.
## Difficulty
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function β neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is *not* a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.
## Formalization scope
States and controls in `EuclideanSpace β (Fin n)` / `(Fin m)`; gradients in Mathlib's `gradient`; the ODE and adjoint via `HasDerivAt` off a finite exceptional set; costs via `intervalIntegral`. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable β the junk-value escape (non-integrable integrand β integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set β no compactness or convexity is assumed in the goal.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
- L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, *The Mathematical Theory of Optimal Processes*, Interscience, 1962.
- W. H. Fleming, R. W. Rishel, *Deterministic and Stochastic Optimal Control*, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7