Control Theory

Motivation

Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping $H$, so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).

The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?

Setting

The abstract monotone model consists of a state space $S$, a control space $C$, nonempty constraint sets $U(x)\subseteq C$, a terminal function $J_0 : S\to(-\infty,\infty]$, and a mapping $H(x,u,J)\in[-\infty,\infty]$ defined for $x\in S$, $u\in C$ and $J : S\to[-\infty,\infty]$, which is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu : S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors, and it is stationary if all $\mu_k$ are equal. The operators are

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

the cost of a policy is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0)(x)$, $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$, and the optimal cost is $J^*(x)=\inf_\pi J_\pi(x)$. A policy is optimal if $J_\pi=J^*$.

Assumption I (uniform increase) is $J_0(x)\le H(x,u,J_0)$ for all $x$, $u\in U(x)$; under it the sequence defining $J_\pi$ is nondecreasing, so the limit exists in $[-\infty,\infty]$. Assumption I.1 says $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $J_0$, and I.2 says that for some $\alpha>0$, $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ and $J\ge J_0$. Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below $J_0$, and a lower shift bound).

The DP algorithm (value iteration) generates $T(J_0), T^2(J_0),\dots$; for $k\ge0$ and $\lambda\in\mathbb R$ the level sets

$$U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$$

collect the controls that keep the stage-$k$ cost below $\lambda$.

Formalization targets

Goal: Proposition 5.11

Let I, I.1 and I.2 hold, let $C$ be a Hausdorff space, and let $U_k(x,\lambda)$ be compact for all $x\in S$, $\lambda\in\mathbb R$ and $k\ge\bar k$. Then (a) some policy $\pi^*=(\mu_0^*,\mu_1^*,\dots)$ satisfies

$$(T_{\mu_k^*}T^k)(J_0)=T^{k+1}(J_0)\qquad\forall k\ge\bar k;$$

(b) for every such policy, $\{\mu_k^*(x)\}$ has an accumulation point whenever $J^*(x)<\infty$; and (c) any $\mu^*$ that picks such an accumulation point at those states, and any admissible control where $J^*(x)=\infty$, defines an optimal stationary policy:

$$J_{\mu^*}=J^*.$$

Milestones

In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation $J^*=T(J^*)$ under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff $T_{\mu^*}(J^*)=T(J^*)$), Proposition 5.10 (under the compactness hypothesis, $J_\infty=T(J_\infty)=T(J^*)=J^*$ and a stationary optimal policy exists), Proposition 5.6 ($\varepsilon$-optimal policies from approximate attainment, with explicit constants $\sum_k\alpha^k\varepsilon_k=\varepsilon$ and $\varepsilon(1-\alpha)$), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and $\varepsilon$-optimal policies under D, D.2 with finite $S$ and $J^*>-\infty$), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).

Significance

Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.

Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.

Difficulty

The obvious route to (c) is to pass to the limit in $H[x,\mu_k^*(x),T^k(J_0)]=T^{k+1}(J_0)(x)$. That fails twice. First, $\{\mu_k^*(x)\}$ need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, $H$ is not assumed continuous in $u$ at all: the only regularity in $u$ is compactness of the level sets $U_k(x,\lambda)$, and the only regularity in $J$ is I.1 along monotone sequences. States with $J^*(x)=\infty$ need separate treatment, because there the level sets give no control on $\mu_k^*(x)$.

For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of $S$ and $J^*>-\infty$ essentially, and both hypotheses are needed.

Formalization scope

Functions $J$ are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them $J_\pi$ is the limit (limUnder) of the policy compositions, which exists under I or D; $T^k$ is the iterate T^[k]; the composition $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first; the model requires $S$ nonempty and $J_0>-\infty$; "I.2 holds" is the existence of a scalar $\alpha$, and results that name the scalar take it as a parameter. An accumulation point of a sequence in $C$ is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that $\mu^*$ is admissible. $J^*+\varepsilon$ is computed pointwise in $[-\infty,\infty]$ and equals $+\infty$ where $J^*$ does.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$. Mathlib's EReal gives $\top+\bot=\bot$, so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable $W$ (expect, positive and negative parts summed in $[0,\infty]$, $+\infty$ when the positive part diverges) and the sum inside the minimax supremum (badd, $+\infty$ when either summand is $+\infty$), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose $H$ and $J_0$ are these mappings; such models exist because the mappings are monotone.

A formalization in which $J_\pi$ or $J^*$ is introduced as an arbitrary fixed point of $T$, or in which (c) assumes that $\mu^*$ is a limit of $\mu_k^*$, would make the goal trivial or different; both are ruled out by the definitions above.

Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; reprinted Athena Scientific, 1996. Chapter 5, pp. 70–90. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• D. Blackwell, "Positive dynamic programming", Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• R. E. Strauch, "Negative dynamic programming", Ann. Math. Statist. 37 (1966) 871–890. https://doi.org/10.1214/aoms/1177699369

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.

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

Motivation

Pontryagin's principle as presented by Luenberger is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.

Setting

Fix t₀ < t₁, a finite-dimensional Euclidean state space OCState n, a Euclidean control space OCControl m, and a permitted-control set Omega. A state-control pair (x,u) is admissible when x t₀ = xInit, the state is absolutely continuous on the interval, the control is almost everywhere strongly measurable and lies in Omega almost everywhere, the differential equation x' = F(x,u) holds almost everywhere in the interior, and the running cost is interval integrable. An optimal pair globally minimizes the interval integral among all admissible pairs.

The dynamics F and running cost ell are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives Fx and ellx vary continuously. A global Lipschitz estimate controls changes of F in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths Fx (x₀ t) (u₀ t) and ellx (x₀ t) (u₀ t) are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,

$$H(x,u,\lambda)=\langle \lambda,F(x,u)\rangle+\ell(x,u).$$

Formalization targets

The root VectorSpaceOpt.pontryagin_minimum_principle asserts the existence of an absolutely continuous costate lambda with terminal value lambda t₁ = 0. Almost everywhere it satisfies the weak inner-product form of

$$-\dot\lambda(t)=D_xF(x₀(t),u₀(t))^*\lambda(t)+D_x\ell(x₀(t),u₀(t)),$$

and almost everywhere on the control interval it satisfies

$$H(x₀(t),u₀(t),\lambda(t)) \le H(x₀(t),v,\lambda(t)) \quad\text{for every }v\in\Omega.$$

Two milestones capture source dependencies. control_state_lipschitz_estimate is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. adjoint_lagrangian_comparison formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.

Significance

This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.

The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.

Difficulty

The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.

Formalization scope

The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on Icc t₀ t₁, restoring the compact-interval boundedness used by the source. The maps F, ell, Fx, and ellx are jointly continuous; state derivatives are supplied by HasFDerivAt; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.

There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every t, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on Icc t₀ t₁; an alternative source-faithful repair would assert the inequality at every continuity point of u₀. The mission does not claim existence of an optimal pair, compactness of Omega, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 9, §9.6, Proposition 1 and Theorem 1, pp. 262–264, including the printed all-times wording and its proof context. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (interval integration, absolute continuity, Euclidean spaces, Fréchet derivatives, ODE estimates, and a.e. measurability).

Motivation

Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).

Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part $G+G^T$ of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).

Setting

The network has $N$ vertices with states $x_i(t)\in\mathbb R^n$. A coupling matrix $G=(G_{ij})\in\mathbb R^{N\times N}$ has $G_{ij}\ge 0$ for $i\ne j$ ($G_{ij}>0$ means a connection from vertex $j$ to vertex $i$) and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. The network is strongly connected if any vertex can be reached from any other by a directed path; $G$ is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form $\begin{pmatrix}\tilde G_{11}&0\\\tilde G_{21}&\tilde G_{22}\end{pmatrix}$ with square diagonal blocks of sizes $m$ and $N-m$, $1\le m\le N-1$. The in-degree of vertex $i$ is $k_i^{\mathrm{in}}=\sum_{j\ne i}G_{ij}$.

Each vertex runs the dynamics $\dot x=f(x,t)$ for a continuously differentiable $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$. A reference trajectory $s$ solves $\dot s=f(s,t)$. With coupling strength $c$, inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and control gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\Gamma(x_i-s),\qquad i=1,\dots,N.$$

It is globally synchronized if $x_i(t)-s(t)\to0$ for every $i$, every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix $K$,

$$(x-y)^T\bigl(f(x,t)-f(y,t)\bigr)\le(x-y)^TK\Gamma(x-y)\qquad\forall x,y\in\mathbb R^n,\ t\ge0 .$$

For positive weights $\xi_1,\dots,\xi_N$ put $\Xi=\operatorname{diag}(\xi)$, $D=\operatorname{diag}(d)$ and $\widehat G=\tfrac12(\Xi G+G^T\Xi)$.

Formalization targets

Goal: Theorem 3.1 (p. 1402)

Let $f$ satisfy Assumption 1 with $\Gamma$ symmetric, let $G$ be a strongly connected coupling matrix, and let $\xi$ be positive with $\widehat G$ having zero row sums (the weights of Lemma 2.12). If

$$\Xi\otimes\frac{K\Gamma+\Gamma^TK^T}{2}+c\,\widehat G\otimes\frac{\Gamma+\Gamma^T}{2}-c\,(\Xi D)\otimes\frac{\Gamma+\Gamma^T}{2}<0,$$

then the controlled network is globally synchronized.

Milestones

The path to the goal follows the paper: Lemma 2.5 (irreducible $\iff$ strongly connected), Lemma 2.9 ($\rho(A)=\|A\|_\infty$ for nonnegative $A$ with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector $x$ with $G^Tx=0$), Lemma 2.12 (the weights $\Xi$), and the derivative estimate (3.4) for $V=\tfrac12\sum_i\xi_ie_i^Te_i$, $e_i=x_i-s$:

$$\dot V\le e^T\bigl[\Xi\otimes(K\Gamma)+c(\widehat G-\Xi D)\otimes\Gamma\bigr]e .$$

Companion results

Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions ($K\Gamma=\Gamma K$, $\theta=\lambda_{\max}(\tfrac{K+K^T}{2})\ge0$) with $\Gamma$ positive definite: Corollary 3.2 (the $N\times N$ condition $\theta\Xi+c(\widehat G-\Xi D)<0$ suffices), Corollary 3.3 (i) (an explicit coupling threshold $c>\lambda_{\max}(\theta\Xi)/|\lambda_{\max}(\widehat G-\Xi D)|$), and Corollary 3.4 (the necessary conditions $d_i>\theta/c-k_i^{\mathrm{in}}$ at pinned and $k_i^{\mathrm{in}}>\theta/c$ at unpinned vertices).

Significance

The criterion reduces global synchronization of an $nN$-dimensional nonlinear system to one linear matrix inequality in the data $(G,\Gamma,K,c,D)$, and the corollaries reduce it further to an $N\times N$ inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below $\theta/c$ must be controlled. Weighting by the left null vector of $G$ is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.

The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization $\widehat G$), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.

Difficulty

The obvious first idea, the unweighted Lyapunov function $\tfrac12\sum_ie_i^Te_i$, produces the symmetric part of $G$, which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of $G$, whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of $V$ along solutions on $[0,\infty)$, the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with $(A\otimes B)_{(i,a),(j,b)}=A_{ij}B_{ab}$; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of $0$ in $\mathbb R^n$, which does not depend on the norm. Derivatives are taken within $[0,\infty)$. Pinning is encoded by $d_i>0$ instead of the paper's reordering of the first $l$ vertices. "$M<0$" is positive definiteness of $-M$ (Mathlib PosDef, which includes symmetry); every matrix compared with $0$ is symmetric by construction. $\lambda_{\max}(A)$ of a symmetric matrix is the least $r$ with $v^TAv\le r\,v^Tv$ for all $v$; $\rho(A)$ is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.

Added hypotheses, each disclosed in the item: $\Gamma^T=\Gamma$ in Theorem 3.1 and (3.4), because the printed theorem allows any $\Gamma$ and is then false (a directed 3-cycle with $\Gamma=\begin{pmatrix}1&3\\-3&1\end{pmatrix}$ satisfies (3.2) but its error grows); $c>0$ in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); $N\ge1$ in Lemma 2.10. The weights $\Xi$ are not arbitrary: Theorem 3.1 and the corollaries require $\widehat G$ to have zero row sums, which for a coupling matrix is equivalent to $G^T\xi=0$. Assuming the derivative bound (3.4), negative definiteness of $\widehat G-\Xi D$ or decay of $V$ in the goal would trivialize it and is excluded.

The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54 (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• J. Zhou, J. Lu, J. Lü, Pinning adaptive synchronization of a general complex dynamical network, Automatica 44 (2008), 996–1003. https://doi.org/10.1016/j.automatica.2007.08.016
• W. Yu, G. Chen, J. Lü, On pinning synchronization of complex dynamical networks, Automatica 45 (2009), 429–435. https://doi.org/10.1016/j.automatica.2008.07.016
• Q. Song, J. Cao, On pinning synchronization of directed and undirected complex dynamical networks, IEEE Trans. Circuits Syst. I 57 (2010), 672–680. https://doi.org/10.1109/TCSI.2009.2024971
• R. Olfati-Saber, R. M. Murray, Consensus problems in networks of agents with switching topology and time-delays, IEEE Trans. Automat. Control 49 (2004), 1520–1533. https://doi.org/10.1109/TAC.2004.834113
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

• Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
• Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
• Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$, and costs are discounted by a factor $\nu \in [0,1)$: the cost at stage $t$ is $\nu^t c(i,a)$.

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$. No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$, so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$, the state distribution evolves as $\mu_0 = e_{i_0}$, $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$. The discounted cost is

$$C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).$$

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$. The robust Bellman operator $g$ and, for a stationary policy $\pi$, the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

$$g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).$$

The two values of the game are

$$\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).$$

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$, i.e.

$$v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}$$

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

$$\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).$$

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$, where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

1. Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$, the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$, every feasible $v$ satisfies $v \le v_\infty$, and $v_\infty$ is the unique optimizer when $q > 0$.
2. The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$-Lipschitz in $\|\cdot\|_\infty$.
3. (26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$.
4. (28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$.
5. (27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$.

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$-contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

• $C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
• Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
• The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$.
• The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
• $\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
• $C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$, so the series is summable and the tsum is the limit of the $N$-stage costs, the paper's definition.
• $\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$.
• Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$, whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
• Corrected statements:
  • Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$.
  • In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$.
  • The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
• Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
• Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$). Both are needed by the other missions of this series.

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. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A closed set $F\subseteq\mathbb R^n$ is flow-invariant for a dynamical system when every trajectory that starts in $F$ stays in $F$. Invariance of sets underlies state constraints in optimal control, safety certificates for controlled systems, comparison and maximum principles for differential equations, and the positivity of solutions of kinetic and population models. The question is always the same: which infinitesimal condition at the points of $F$ is equivalent to the global statement that trajectories cannot leave $F$?

For a smooth vector field and a smooth boundary the answer is that the field must not point strictly outward. For a nonsmooth set, such as a polyhedron, the positive orthant or a set with inward cusps, "pointing inward" must be made precise through a notion of tangent vector that works at corners. Frank H. Clarke's 1975 paper introduces the generalized gradient of a Lipschitz function and derives from it a normal cone and a tangent cone for arbitrary closed sets. Its Theorem (4.4) shows that this tangent cone is exactly the right notion: for a Lipschitz differential inclusion $\dot x\in X(x)$, a closed set is flow-invariant if and only if $X(x)$ is contained in the tangent cone at each point of the set.

Timeline:

• 1942. Nagumo characterizes invariance for continuous ODEs with unique solutions by a condition on the distance function (Proc. Phys.-Math. Soc. Japan 24).
• 1969. Bony proves an invariance theorem for Lipschitz vector fields, stated through exterior normals, in the course of a maximum principle for degenerate elliptic operators (Bony 1969).
• 1970. Brezis characterizes flow-invariant closed sets of a locally Lipschitz vector field by $\lim_{\delta\downarrow0} d_F(y+\delta X(y))/\delta=0$ (Brezis 1970).
• 1972. Redheffer gives simplified proofs of the Bony and Brezis theorems under weaker "uniqueness function" hypotheses (Amer. Math. Monthly 79, 740–747).
• 1975. Clarke extends the characterization to Lipschitz multifunctions with nonempty compact values, with tangency in the sense of his new tangent cone, and recovers Bony and Brezis as corollaries (Clarke 1975, Theorem (4.4), Corollaries (4.10), (4.12)).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $\zeta\cdot v$ and norm $|\cdot|$.

Generalized gradient. For $f:\mathbb R^n\to\mathbb R$ Lipschitz on bounded sets, $\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$ (Definition (1.1)). The generalized directional derivative is $f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}[f(x+h+\delta v)-f(x+h)]/\delta$ (Definition (1.3)).

Distance function. For a nonempty closed $E\subseteq\mathbb R^n$, $d_E(x)=\min\{|x-e|:e\in E\}$. It is Lipschitz with constant $1$. A point $e\in E$ with $|x-e|=d_E(x)$ is a closest point to $x$; it exists but need not be unique.

Normal and tangent cones. For $e\in E$, the cone of normals is

$$N_E(e)=\operatorname{cl}\{p:\ s\,p\in\partial d_E(e)\text{ for some }s>0\}\qquad\text{(Definition (3.1))},$$

and the tangent cone is its dual,

$$T_E(e)=\{\zeta:\ \zeta\cdot v\le0\text{ for all }v\in N_E(e)\}\qquad\text{(Definition (3.6))}.$$

Differential inclusions. A multifunction $X$ assigns to each $x\in\mathbb R^n$ a set $X(x)\subseteq\mathbb R^n$; standing assumption of §4: every $X(x)$ is nonempty and compact. A trajectory is an absolutely continuous $x:[0,1]\to\mathbb R^n$ with $\dot x(t)\in X(x(t))$ for almost every $t$ ((4.1)). $X$ is Lipschitz if there is $K$ such that for all $x_1,x_2$ and $v_1\in X(x_1)$ some $v_2\in X(x_2)$ has $|v_1-v_2|\le K|x_1-x_2|$ ((4.2)). A closed set $F$ is flow-invariant for $X$ if every trajectory with $x(0)\in F$ has $x(t)\in F$ for all $t\in[0,1]$ ((4.3)).

Formalization targets

Goal: Theorem (4.4)

Let $X$ be a Lipschitz multifunction with nonempty compact values and $F$ a nonempty closed subset of $\mathbb R^n$. Then

$$F\text{ is flow-invariant for }X\iff X(x)\subseteq T_F(x)\ \text{ for every }x\in F.$$

Milestones, in the order the proof uses them

1. Proposition (1.4). $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$.
2. Proposition (2.4). If $\nabla d_E(x)$ exists and is nonzero, then $x\notin E$, $x$ has a unique closest point $e$, and $\nabla d_E(x)=(x-e)/|x-e|$.
3. Corollary (2.5). For $e\in E$, $\partial d_E(e)=\operatorname{co}\{0,\lim (x_i-e_i)/|x_i-e_i|\}$ over $x_i\notin E$, $x_i\to e$, $e_i$ closest to $x_i$.
4. Proposition (3.2). $N_E(e)=\operatorname{cl}\operatorname{co}\{\lim s_i(x_i-e_i)\}$ over $s_i\ge0$, $x_i\to e$, $e_i$ closest to $x_i$.
5. Inequality (4.8). If $X(y)\subseteq T_F(y)$ on $F$ and $x$ is a trajectory, then $f(t)=d_F(x(t))$ satisfies $f'(t)\le Kf(t)$ almost everywhere.
6. Limit (4.9). If $F$ is flow-invariant, then $d_F(y+\delta v)/\delta\to0$ as $\delta\downarrow0$ for every $y\in F$ and $v\in X(y)$.
7. Proposition (3.7). $v\in T_E(e_0)$ iff $\lim_{e\to e_0,\,e\in E}\liminf_{\delta\downarrow0} d_E(e+\delta v)/\delta=0$.

Significance

The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on $F$ that can be checked without solving anything. It is the prototype of the strong invariance theorems of nonsmooth control theory, later developed in viability theory and in the monograph of Clarke, Ledyaev, Stern and Wolenski, and it is the tool behind state-constrained optimal control and Lyapunov-type arguments for nonsmooth systems. Its corollaries recover the Bony and Brezis theorems for Lipschitz vector fields. The companion milestones (2.5), (3.2) and (3.7) are standalone facts of nonsmooth geometry: the Clarke normal cone is generated by limits of proximal normals, and Clarke tangency can be tested along rays from nearby points of the set.

Formalizing it. The result is proved in the paper and has been reproved in textbooks; to the best of our knowledge it has no machine-checked proof. Mathlib contains Rademacher's theorem, absolutely continuous functions on intervals and the Bouligand tangent cone, but no Clarke generalized gradient, no Clarke normal or tangent cone, and no theory of differential inclusions. A complete development supplies a first nonsmooth-analysis layer on top of Mathlib and a first existence theorem for Lipschitz differential inclusions.

Difficulty

The direction (2) $\Rightarrow$ (1) looks like a Gronwall argument for $f(t)=d_F(x(t))$, but $d_F$ is not differentiable, $x$ is only absolutely continuous, and the closest point to $x(t)$ can jump. The step that must be controlled is the comparison between $\dot x(t)$, a nearby admissible velocity at the closest point, and the normal $x(t)-y$; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.

The direction (1) $\Rightarrow$ (2) needs a trajectory through an arbitrary $y\in F$ whose initial velocity is a prescribed $v\in X(y)$. For a nonconvex multifunction this is Filippov's theorem [7, Theorem 5], which the paper cites and does not prove. A solver must prove it, or an equivalent existence result for Lipschitz inclusions with compact values, from scratch in Lean. The Clarke tangent cone and the more familiar Bouligand (contingent) cone differ pointwise at nonconvex corners, so a statement written with Mathlib's tangentConeAt is a different theorem from (4.4). That the two universal conditions "$X(x)\subseteq T_F(x)$ for all $x\in F$" are equivalent for Lipschitz $X$ is a later, separate result and cannot be assumed.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $d_E$ is Metric.infDist · E; "$e$ is a closest point to $x$" is e ∈ E ∧ dist x e = infDist x E.
• $\partial f$ and $f^\circ$ follow Definitions (1.1) and (1.3). The gradient limits carry DifferentiableAt, because Mathlib's gradient is $0$ off the differentiability set. $f^\circ$ is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.
• $N_E$ and $T_E$ are defined from $\partial d_E$ as in (3.1) and (3.6). The tangent cone is not Mathlib's tangentConeAt.
• A trajectory is x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every $t\in[0,1]$, ∃ w ∈ X (x t), HasDerivAt x w t. Values outside $[0,1]$ are irrelevant.
• Standing assumptions made explicit: $X(x)$ nonempty and compact for every $x$ (§4, p. 259); $E$, $F$ nonempty and closed and $e\in E$ (§3, p. 254); $f$ Lipschitz on bounded sets (§1, p. 247). The Lipschitz constant of (4.2) is global.
• Ruled out: dropping absolute continuity (Cantor-type curves would leave $F$), using deriv in (4.1), using a punctured filter in (3.7), which would make (3.7)(2) hold at isolated points, and assuming Filippov's theorem as a hypothesis of (4.9) or of the goal.
• Needed infrastructure: the Clarke calculus for $d_E$, a chain-rule-type estimate for $d_F\circ x$ along absolutely continuous curves, a Gronwall lemma for absolutely continuous functions (Mathlib has norm_le_gronwallBound_of_norm_deriv_right_le for the differentiable case), and Filippov's existence theorem. The generalized gradient, cones and trajectory notions are reusable by any nonsmooth-optimization or control mission. Contributions of any of these as separate lemmas are welcome.
• The §1 definitions duplicate those of the companion mission Generalized Gradients and Applications I; the two missions were drafted at the same time.

Selected references

• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
• A. F. Filippov, Classical solutions of differential equations with multivalued right-hand side, SIAM J. Control 5 (1967), 609–621. https://doi.org/10.1137/0305040
• H. Brezis, On a characterization of flow-invariant sets, Comm. Pure Appl. Math. 23 (1970), 261–263. https://doi.org/10.1002/cpa.3160230211
• J. M. Bony, Principe du maximum, inégalité de Harnack et unicité du problème de Cauchy pour les opérateurs elliptiques dégénérés, Ann. Inst. Fourier 19 (1969), 277–304. https://doi.org/10.5802/aif.319
• R. M. Redheffer, The theorems of Bony and Brezis on flow-invariant sets, Amer. Math. Monthly 79 (1972), 740–747. MR 46 #2166.
• F. H. Clarke, Yu. S. Ledyaev, R. J. Stern, P. R. Wolenski, Nonsmooth Analysis and Control Theory, Graduate Texts in Mathematics 178, Springer, 1998. https://doi.org/10.1007/b97650

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