Control Theory

Why delays in boundary feedback matter

Boundary feedback is the standard way to stabilize vibrating structures governed by wave equations: a sensor measures the velocity at the boundary and an actuator applies a force proportional to it. For the one-dimensional damped wave equation with such feedback, the closed loop is uniformly exponentially stable (Chen, 1979). In practice the measured velocity reaches the actuator only after a computation time, so the feedback acts with a time delay $\varepsilon > 0$. The question addressed by Datko, Lagnese and Polis (1986) is whether arbitrarily small delays can destroy the stability of a system that is stable without them.

Their note answers it with an explicit example and a sharp threshold on the feedback gain. It is the founding example of delay-induced instability in boundary stabilization, cited by most later work on robustness of boundary control to delays.

Timeline.

• Chen (1979, 1981): energy decay $E(u,t) \le Ce^{-\alpha t}E(u,0)$ for boundary-damped wave equations without delay.
• Datko (1978): delays in the velocity term of the equation itself can destabilize; a lemma on zeros of exponential polynomials in vertical strips (the source of Lemma 1 here).
• Datko, Lagnese, Polis (1986, DOI 10.1137/0324007): the delayed boundary feedback $u_x(1,t) = -ku_t(1,t-\varepsilon)$ for the damped string, with a trichotomy in the gain $k$.
• Nicaise and Pignotti (2006, DOI 10.1137/060648891): the multidimensional undamped problem with feedback $-\mu_1u_t(t) - \mu_2u_t(t-\tau)$; stability iff $\mu_2 < \mu_1$, instability for a sequence of delays otherwise.

Setting

Fix real numbers $a \ge 0$ (damping), $k \ge 0$ (feedback gain) and $\varepsilon > 0$ (delay), and put $K = e^{-2a} \in (0,1]$. The delayed system is

$$\begin{aligned} &(1)\quad u_{tt} - u_{xx} + 2au_t + a^2u = 0, && 0<x<1,\ t>0,\\ &(2)\quad u(0,t) = 0, && t>0,\\ &(8)\quad u_x(1,t) = -k\,u_t(1,t-\varepsilon), && t>\varepsilon . \end{aligned}$$

A classical solution is a $C^2$ function $u(x,t)$ with complex values satisfying (1), (2), (8).

Separated solutions $u = e^{\omega t}\varphi(x)$ lead to the eigenvalue problem

$$\varphi''(x) = (a+\omega)^2\varphi(x)\ (0<x<1),\qquad \varphi(0) = 0,\qquad \varphi'(1) + k\omega e^{-\varepsilon\omega}\varphi(1) = 0 .$$

The spectrum $\sigma(a,k,\varepsilon)$ is the set of $\omega \in \mathbb C$ for which this problem has a solution $\varphi$ not identically zero on $[0,1]$. The paper encodes it through the entire functions

$$f(\varepsilon,\omega) = 1 + Ke^{-2\omega} + ke^{-\varepsilon\omega}(1 - Ke^{-2\omega}),\qquad h(\varepsilon,\omega) = \omega f(\varepsilon,\omega) + a(1 + Ke^{-2\omega}),$$

and the critical gain $(1-K)/(1+K)$. In Lean these are K a, f a k ε ω, h a k ε ω, delaySpectrum a k ε, IsClassicalSolution a k ε u and IsExpUnstableSolution a k ε u in the namespace DatkoDelayWave.BoundaryDelay.

Formalization targets

Goal: the stability trichotomy (THEOREM, p. 153)

1. If $0 < k < \frac{1-K}{1+K}$: for each $\varepsilon > 0$ there is $\beta(\varepsilon) > 0$ with

$$\sigma(a,k,\varepsilon) \subseteq \{\operatorname{Re}\omega \le -\beta\}.$$

2. If $k = \frac{1-K}{1+K} > 0$: for each $\varepsilon > 0$, $\sigma(a,k,\varepsilon) \subseteq \{\operatorname{Re}\omega < 0\}$, but there is a countable set $R \subseteq (0,\infty)$, dense in $(0,\infty)$, such that for each $\varepsilon \in R$ some sequence $\omega_n \in \sigma(a,k,\varepsilon)$ has $\operatorname{Re}\omega_n \to 0$.
3. If $k > \frac{1-K}{1+K}$: there is an open set $D \subseteq (0,\infty)$, dense in $(0,\infty)$, such that for each $\varepsilon \in D$ the system has a classical solution with $|u(x_0,t)| \ge ce^{\gamma t}$ for some $\gamma, c > 0$, $x_0 \in (0,1)$ and all $t \ge 0$.

Milestones

In attack order: the characteristic equation (16) ($\omega \in \sigma \iff h(\varepsilon,\omega) = 0$ for $\omega \ne -a$); separated solutions; Lemma 1 (one zero of $f$ forces infinitely many zeros of $f$ and $h$ in every vertical strip around it); (17)–(18) (no zeros of $h$ in the right half-plane below or at the critical gain); the half-plane bound below the critical gain; (19) (no purely imaginary zeros at the critical gain); the explicit zero $f\bigl(\tfrac{2(2m+1)}{2n+1}, \tfrac{(2n+1)\pi i}{2}\bigr) = 0$; density of the delays $\tfrac{2(2m+1)}{2n+1}$; the root family (12)–(15) above the critical gain; Lemma 2 (an open dense set of delays with zeros of $f$ in $\operatorname{Re}\omega > 0$); the three parts of the THEOREM separately; and, off the goal's path, the undelayed formula $\operatorname{Re}\omega = \tfrac12\log\bigl|\tfrac{k-1}{k+1}\bigr|$ for $a = 0$.

Significance

The result shows that exponential stability obtained by boundary velocity feedback is not robust to delays when the gain is above $(1-K)/(1+K)$: delays from a dense set of lengths, including arbitrarily small ones, produce exponentially growing modes. When $a = 0$ the critical gain is $0$, so every positive gain is fragile. Below the critical gain the spectral gap survives every delay. This identifies a quantitative robustness margin and motivated the later analysis of delayed boundary control, including the Nicaise–Pignotti theorems already posed on the platform for a different, multidimensional model (NicaiseDelayWave.*).

The result is proved in the paper, partly by citation: Lemma 1 is quoted from Datko (1978) without proof, and the open-mapping step of Lemma 2 is sketched. No machine-checked version exists. A formalization would check the threshold computations, supply the strip-zero lemma for this exponential polynomial, and give a rigorous version of the open-mapping step.

Difficulty

The algebraic parts, (16)–(19) and the explicit zeros, are calculations with complex exponentials. The difficulty is in Lemma 1 and Lemma 2. Lemma 1 needs the almost-periodic structure of exponential polynomials in vertical strips together with a Hurwitz or Rouché type argument, and neither is in Mathlib. Lemma 2 needs zeros of $f(\varepsilon,\cdot)$ to persist under small changes of the real parameter $\varepsilon$. The paper's route through the logarithmic map (11) does not work as printed, because it is stated with the principal branch exactly on the branch cut. In part (i), the delicate step is excluding accumulation of zeros at the imaginary axis as $|\operatorname{Im}\omega| \to \infty$, which the half-plane estimate alone does not give.

Formalization scope

Parameters $a, k, \varepsilon$ are real, $\omega \in \mathbb C$, eigenfunctions are maps $\mathbb R \to \mathbb C$ and solutions are maps $u : \mathbb R \to \mathbb R \to \mathbb C$ (space first). Partial derivatives are deriv of the sections. Solutions and eigenfunctions are required to be $C^2$ on all of $\mathbb R^2$, resp. $\mathbb R$; this loses no eigenvalue, since solutions of (5) are combinations of $e^{\pm(a+\omega)x}$. Committed readings of the paper's loose phrases:

• the spectrum is the eigenvalue set of the problem above, not the zero set of $h$; $h(\varepsilon,-a) = 0$ always, so (16) is stated for $\omega \neq -a$;
• "countably dense set $R$ in $(0,\infty)$": $R \subseteq (0,\infty)$, $R$ countable, $(0,\infty) \subseteq \overline R$;
• "dense open set $D$ in $(0,\infty)$": $D \subseteq (0,\infty)$ open, $(0,\infty) \subseteq \overline D$;
• "exponentially unstable solution": a classical solution with $|u(x_0,t)| \ge ce^{\gamma t}$ for all $t \ge 0$;
• "an infinite number of zeros" (Lemma 1): the zero set in the open strip is infinite, for $f$ and for $h$ separately;
• "there exists $\beta(\varepsilon) > 0$": $\forall \varepsilon > 0\ \exists \beta > 0$, so $\beta$ may depend on $\varepsilon$;
• part (ii) carries $k > 0$, the paper's standing assumption (p. 152); without it the part is false at $a = 0$;
• $m, n$ in $2(2m+1)/(2n+1)$ are positive integers in (12)–(15) and in the density of (15), as in the proof of Lemma 2; in the explicit threshold zero, where the page says "$m, n$ are arbitrary", they range over all natural numbers.

Trivializing encodings are ruled out: defining the spectrum as the zero set of $h$ would make $-a$ a spurious spectral point, and reading "exponentially unstable" as "the spectrum meets $\operatorname{Re}\omega > 0$" would delete the solution-level content of part (iii).

A complete development needs zero-counting tools for exponential polynomials in strips (almost periodicity, Hurwitz's theorem), which would be reusable for other delay equations. Contributions to any milestone, and to that general infrastructure, are welcome.

Selected references

• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24(1), 152–156, 1986. https://doi.org/10.1137/0324007
• R. Datko, A procedure for determination of the exponential stability of certain differential-difference equations, Quart. Appl. Math. 36, 279–292, 1978.
• G. Chen, Energy decay estimates and exact boundary value controllability for the wave equation in a bounded domain, J. Math. Pures Appl. 58, 249–274, 1979.
• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5), 1561–1585, 2006. https://doi.org/10.1137/060648891

Motivation

Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with $\rho\le1$. The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.

This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition $\rho<1$ and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.

Setting

The network has buffers $0,1,\dots,I$, where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}\in\{0,1\}$ records whether activity $j$ needs processor $k$, and $B_{ji}\in\{0,1\}$ whether activity $j$ processes buffer $i$.
• An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Every activity is one or the other. Every processor serves only input activities (an input processor) or only service activities (a service processor).
• $m_j>0$ is the mean processing requirement of activity $j$, $\mu_j=1/m_j$, and $P^j$ is its routing matrix.

The input-output matrix is $R_{ij}=\mu_j\big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\big)$. An allocation is $a\in\mathbb R^J_+$ with $\sum_jA_{kj}a_j\le1$ for every processor and $=1$ for every input processor; $\mathcal A$ is the set of allocations and $\mathcal E$ the set of its extreme points. The network pressure of $a$ at buffer level $z\in\mathbb R^I_+$ is $p(a,z)=z\cdot Ra$.

The static planning LP asks for $x\ge0$ and $\rho$ with $Rx=0$, $\sum_jA_{kj}x_j\le\rho$ for service processors and $=1$ for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every $z\in\mathbb R^I_+$ some maximizer of $p(\cdot,z)$ over $\mathcal E$ has $z_i>0$ on all its constituent buffers. Assumption 2 says there is $x\ge0$ with $Rx>0$ componentwise.

A fluid model solution is a pair of paths $(\bar Z,\bar T)$, buffer levels $\bar Z(t)\in\mathbb R^I$ and cumulative activity times $\bar T(t)\in\mathbb R^J$, satisfying (14)–(18): $\bar Z(t)=\bar Z(0)-R\bar T(t)$ (written out over buffers), $\bar Z\ge0$, input processors always busy, every processor's busy time at most elapsed time, and $\bar T$ nondecreasing with $\bar T(0)=0$. A time $t>0$ is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular $t$,

$$R\dot{\bar T}(t)\cdot\bar Z(t)=\max_{a\in\mathcal E}Ra\cdot\bar Z(t).$$

Formalization targets

Goal: Theorem 5

$$\text{Assumptions 1, 2 and an LP solution with } \rho<1\ \Longrightarrow\ \exists\,\delta>0:\ |\bar Z(0)|\le1\Rightarrow \bar Z(t)=0\ \ \forall t\ge\delta,$$

for every solution of (14)–(18) and (20). The constant $\delta$ depends on the network only.

Milestones

1. For an input activity $j$, $R_{ij}=-\mu_jB_{j0}P^j_{0i}\le0$.
2. Assumption 2 yields $\hat x\ge0$ with $R\hat x>0$ that vanishes on input activities and loads no input processor.
3. After scaling $\hat x$, the vector $x^*=\tilde x+\hat x$ is an allocation and $Rx^*\ge\delta e$ for some $\delta>0$.
4. The maximum of $p(\cdot,z)$ over $\mathcal A$ is attained on $\mathcal E$ (p. 201).
5. The identities (22)–(23): $\dot f(t)=2\dot{\bar Z}(t)\cdot\bar Z(t)=-2R\dot{\bar T}(t)\cdot\bar Z(t)$ for $f=\sum_i\bar Z_i^2$.
6. $R\dot{\bar T}(t)\cdot\bar Z(t)\ge Rx^*\cdot\bar Z(t)\ge\delta\sum_i\bar Z_i(t)\ge\delta\|\bar Z(t)\|$.
7. $\dot f(t)\le-2\delta\sqrt{f(t)}$ at regular times.
8. The explicit emptying time: $\bar Z(t)=0$ for $t\ge\|\bar Z(0)\|/\delta$.

Significance

The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under $\rho\le1$, which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under $\rho<1$, the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem $Rx=\lambda$, no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has $Rx=0$ and the equality constraints (2). The definitions file (network, $\mathcal A$, $\mathcal E$, pressure, fluid model, (20)) is shared in content with the other missions of this series.

Difficulty

Each algebraic step is short; the work is in the analysis. The obvious route reads $\dot f\le-2\delta\sqrt f$ as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of $\bar T$ and $\bar Z$ on $[0,\infty)$ from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, $\sqrt f=\|\bar Z\|$, whose derivative bound holds only where $f>0$. The step "by (20)" also needs the maximum over $\mathcal E$ to dominate every allocation in $\mathcal A$. That is the vertex property of a bounded polyhedron, which in Lean means compactness of $\mathcal A$ plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to $\|\bar Z\|$.

Formalization scope

• Indices are 0-based: internal buffers Fin I, buffers $0..I$ as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.
• Paths are functions ℝ → (Fin n → ℝ) constrained only at $t\ge0$. Derivatives are deriv, used only at regular points.
• (20) is encoded as IsGreatest of the set of pressures over $\mathcal E$, so the maximum is attained and an empty $\mathcal E$ cannot pass through a junk supremum. $\mathcal E$ is Mathlib's Set.extremePoints.
• The fluid model of the theorem is the predicate "(14)–(18) and (20)". Solutions are not required to be fluid limits.
• The standing assumptions of §2 are one predicate, Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and $m_j>0$. The row sums of $P^j$ are not imposed.
• The theorem's text cites "the LP (9)–(12)". The proof needs $x\ge0$, so the LP used is (9)–(13), as in Theorems 1, 2 and 4.
• The norm in Definition 4 is Euclidean, as in the proof.
• Assumption 1 is a hypothesis of the goal because the page states it. The fluid-level argument does not use it.
• Ruled out: a vacuous goal. A sorry-free sanity file shows a one-buffer network (one input activity, one service activity) that satisfies every hypothesis of the goal and has a maximum pressure fluid solution. The milestone on the maximum over $\mathcal A$ carries the hypothesis $\mathcal A\neq\emptyset$, because the standing assumptions alone do not imply it.

Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on $[0,\infty)$, the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with $\dot g\le-\varepsilon$ on $\{g>0\}$.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Motivation

Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.

Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.

Setting

Fix a horizon $T$ and an initial state $x_1\in\mathbb R$. For each stage $k=1,\dots,T$ there are a per-unit control cost $c_k\ge0$, control bounds $L_k\le U_k$, disturbance bounds $\underline w_k\le\overline w_k$, and a state cost $h_k:\mathbb R\to\mathbb R$ that is convex and coercive. The state evolves as

$$x_{k+1}=x_k+u_k+w_k,\qquad u_k\in[L_k,U_k],\qquad w_k\in\mathcal W_k=[\underline w_k,\overline w_k].$$

The controller chooses $u_k$ after seeing $x_k$; the adversary then chooses $w_k$. The min-max value $J_{mM}$ is the value of the nested problem $\min_{u_1}[c_1u_1+\max_{w_1}[h_1(x_2)+\min_{u_2}[\cdots]]]$, computed by the Bellman recursion with $J^*_{T+1}\equiv0$:

$$g_k(y)=\max_{w\in\mathcal W_k}\big[h_k(y+w)+J^*_{k+1}(y+w)\big],\qquad J^*_k(x)=\min_{L_k\le u\le U_k}\big[c_ku+g_k(x+u)\big],\qquad J_{mM}=J^*_1(x_1).$$

An affine control policy and an affine running cost at stage $k$ are

$$q_k(w)=q_{k,0}+\sum_{t=1}^{k-1}q_{k,t}w_t,\qquad z_k(w)=z_{k,0}+\sum_{t=1}^{k}z_{k,t}w_t,$$

so $q_k$ sees the disturbances before stage $k$ and $z_k$ those up to stage $k$. Under these policies the state after stage $k$ is $x_1+\sum_{t\le k}(q_t(w)+w_t)$.

Formalization targets

Goal: Theorem 3.1

There exist affine policies $q_k$ and affine costs $z_k$ such that, for every $k=1,\dots,T$,

$$L_k\le q_k(w)\le U_k\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_{k-1},$$ $$z_k(w)\ge h_k\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_k,$$ $$J_{mM}=\max_{w_1,\dots,w_k}\Big[\sum_{t=1}^k\big(c_tq_t(w)+z_t(w)\big)+J^*_{k+1}\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\Big].$$

At $k=T$ this says that affine policies are robustly feasible and attain the min-max value.

Milestones

1. Lemma 7.1 (with (8)–(9), P2): $J^*_k$ and $g_k$ are convex, and the optimal control is the clamp $\max(L_k,\min(U_k,y^*-x))$ for a minimizer $y^*$ of $c_ky+g_k(y)$.
2. P3: the clamp is non-increasing and 1-Lipschitz.
3. Lemma 4.1: the maximum of $\theta_1+f(\theta_2)$, $f$ convex, over a planar zonogon $\Theta=\pi([0,1]^k)$ is attained at one of the $k+1$ vertices on its right side.
4. Corollary 4.1: the maximum of $\theta_1+f(\theta_2)$ is unchanged when a polygon is replaced by its convex hull, its vertex set, its right side, or the zonogon hull of its vertices.
5. Lemma 4.2: after the optimal control is applied, the worst case is reached on the right side of $\operatorname{conv}\{\tilde v_0,\dots,\tilde v_k\}$.
6. Lemma 4.4: the matching-and-alignment system (37) defining the affine controller is feasible, and its solutions satisfy $-b_i\le q_i\le0$ and $L\le q(w)\le U$.
7. Lemma 4.8 and Lemma 4.9: the affine cost defined by system (51)–(53) dominates the convex cost, first at the hypercube vertices, then on the whole hypercube.

Significance

The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the $h_k$ are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most $k+1$ vertices, matching the $k+1$ coefficients of an affine policy.

The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of $c_ky+g_k(y)$, and Lemma 4.3 is proved in one sub-case only.

Difficulty

Dynamic programming gives the optimal control as a function of the current state, $u^*_k(x_k)$, which is piecewise affine in $x_k$ with up to three pieces. Since $x_k$ is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost $z_k$ that still dominates $h_k$. Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all $2^k$ vertices of the disturbance box is overdetermined.

Formalization scope

Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 ($c_k\ge0$, $h_k$ convex and coercive) plus two disclosed additions, $L_k\le U_k$ and $\underline w_k\le\overline w_k$: the page writes both as intervals but does not say they are nonempty. $J^*_k$ is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.

The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by $b_i$, the hypothesis $b_i>0$. Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.

Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true $J^*_{k+1}$. The policies read only past disturbances (sums over $t<k$, resp. $t\le k$). $J_{mM}$ is the Bellman value over all state-feedback controls, not the value of the affine problem.

The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.

Selected references

• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of Affine Policies in Multi-stage Robust Optimization, arXiv:0904.3986v1, 2009; Mathematics of Operations Research 35(2):363–394, 2010. https://arxiv.org/abs/0904.3986, https://doi.org/10.1287/moor.1100.0444
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2):491–531, 2012. https://doi.org/10.1007/s10107-011-0444-4
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995 (Chapter 7, zonotopes). https://doi.org/10.1007/978-1-4613-8431-1

Motivation

A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.

K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.

Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.

Setting

The hidden state $x_t$, $t = 1, \dots, N$, takes values in a finite set $S$. The controls $u = (u_1, \dots, u_r)$ range over a compact nonempty set $U \subset \mathbb R^r$. The state moves by the transition probabilities $p_{ij}(u, t) = P\{x_t = j \mid x_{t-1} = i\}$, which are continuous in $u$. The state is observed through outputs $y_t$ in a finite set $Y$, with $q_{ij} = P\{y_t = j \mid x_t = i\}$, conditionally independent given the states. The law of $x_1$ is $p^1$. An instantaneous cost $g(u, i, t)$, continuous in $u$, is paid at each time.

A control law chooses $u(t) = c(\eta_1, \dots, \eta_t, t) \in U$ from the outputs observed so far, $\eta(t) = (\eta_1, \dots, \eta_t)$. With $u(t)$ moving $x_t$ to $x_{t+1}$, a law determines the joint law of $(x_1, \dots, x_N, y_1, \dots, y_N)$ and the expected cost

$$EL = E \sum_{t=1}^N g(u(t), x_t, t). \tag{2.6}$$

Problem P.1 is to find an admissible law minimizing (2.6).

The conditional state distribution is $w_i(t) = P\{x_t = i \mid \eta(t)\}$. It is updated by Bayes' rule: with $z^j(u, w)_i = \sum_s q_{ij}\, p_{si}(u, t+1)\, w_s$ and $\|z\| = \sum_i |z_i|$, the output $\eta_{t+1} = j$ gives $w(t+1) = z^j(u(t), w(t)) / \|z^j(u(t), w(t))\|$, and $\|z^j\|$ is the probability of that output. The cost-to-go $V_k(w)$ is the minimal expected cost of the steps $k, \dots, N$ when $x_k$ has distribution $w$, with $V_{N+1} = 0$. Problem P.2 controls the process $w(t)$ directly: a law chooses $u(t)$ from $w(1), \dots, w(t)$ to minimize $E\sum_{t=1}^N \sum_i g(u(t), i, t)\, w_i(t)$.

Formalization targets

Goal: Theorem 3

P.1 has a solution if and only if P.2 has one. For every solution $(V, c^0)$ of the functional equation

$$V_k(w) = \min_{u \in U} \Big\{ \sum_i g(u, i, k)\, w_i + \sum_j V_{k+1}\Big(\frac{z^j(u, w)}{\|z^j(u, w)\|}\Big) \|z^j(u, w)\| \Big\}, \qquad V_{N+1} = 0, \tag{3.28}$$

with $c^0(w, k)$ attaining the minimum, the law

$$u(t) = c^0(w(t), t)$$

is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal $E_{\eta_1} V_1(w(1))$.

Milestones

1. (3.20)–(3.25): the conditional distributions obey the Bayes recursion, and $\|z^j\| = P[y_{t+1} = j \mid \eta(t)]$.
2. Theorem 1: the cost-to-go satisfies (3.28) with the minimum attained, and an optimal Markov law attains it.
3. Theorem 2: a solution of (3.28) gives an optimal law for P.1 with value (3.29).
4. Lemma 1: under $u(t) = c(w(t), t)$, $\{w(t)\}$ is a Markov process with transition probabilities $P(y, \Gamma, u) = \sum_{k \in K} \|z^k(u, y)\|$.
5. Proof of Theorem 3: the integral against this kernel is the sum in (3.28).

Significance

The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes $w(t)$ in real time, and the function $c^0$ can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.

Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.

Difficulty

The obvious argument is backward induction on the conditional distributions. The difficulty is that $w(t)$ depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than $w(t)$ must gain nothing. Restricting the comparison class to laws of the form $c(w(t), t)$ assumes this conclusion.

A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over $U$ are attained, which needs continuity of $V_{k+1}$ on the simplex. The weights $\|z^j(u, w)\|$ can vanish, and then the update $z^j/\|z^j\|$ is undefined.

Formalization scope

States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and $U$ is compact and nonempty. The law $p^1$ of $x_1$ is the datum in place of the paper's law of $x_0$, since no control $u(0)$ exists. The transition from $x_t$ to $x_{t+1}$ uses $u(t)$ and the matrix $p(u(t), t+1)$. Times $1, \dots, N$ are indexed by Fin N as $0, \dots, N-1$.

The norm $\|\cdot\|$ is the $\ell^1$ norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When $\|z^j\| = 0$ the update is the zero vector and is always multiplied by $0$.

The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights $\|z^j\|$. "Given by Theorem 1" is read as "$c^0(w, k) \in U$ attains the minimum in (3.28)" (IsSolution328).

The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law $c^0(w(t), t)$ to be optimal in both problems, against every admissible law, with equal minimal values.

Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of $V_k$ on the simplex, and existence of solutions of (3.28).

Selected references

• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9
• P. D. Joseph and J. T. Tou, On linear control theory, Transactions of the AIEE, Part II 80(4):193–196, 1961. https://doi.org/10.1109/TAI.1961.6371743

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$-stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$, ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$, $u\in U(x)$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$. A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

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

and let $T^k$ be the $k$-fold composition of $T$. A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$-stage cost of $\pi$ and the $N$-stage optimal cost are

$$J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).$$

A policy is uniformly $N$-stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$-stage optimal, and $N$-stage $\varepsilon$-optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$.

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$), and F.3 (a quantitative selection property with a constant $\beta>0$).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$:

$$J^*_N=T^N(J_0),$$

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$.

Milestones

• Proposition 3.3: $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$. Needs monotonicity only.
• Corollary 3.3.1: a uniformly $N$-stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$.
• Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy exists.
• Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$.
• Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$.
• Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$, $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$, policies with $\{\varepsilon_n\}$-dominated convergence to optimality exist.
• Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$, the DP algorithm gives $J^*_N$ and $N$-stage $\varepsilon$-optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$. Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$. The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$-optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$, which is why F.3 and the definition of $\varepsilon$-optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$. Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$.

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$, so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of $N$ states, or the stocks of $N$ commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation

$$x_i(n+1) = \max_q \sum_{j=1}^N a_{ij}(q)\, x_j(n), \qquad x_i(0) = c_i,$$

and, in the limit of small time steps, to differential equations of the form $dx/dt = \max_q [A(q,t)x + b(q,t)]$ and, when two opposing controllers act, $dx/dt = \max_p \min_q[\dots]$.

These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).

Setting

Fix $N \ge 1$. Row $i$ of the matrix carries its own control $q_i$, ranging over a set $S_i$; the joint control is $q = (q_1, \dots, q_N)$ in $S = S_1 \times \dots \times S_N$, and $A(q) = (a_{ij}(q_i))$. Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over $q$ is then taken row by row.

The Perron root $\varphi(q)$ is the characteristic root of $A(q)$ of largest absolute value, the spectral radius of $A(q)$ as a complex matrix. The conditions (10.3) of the chapter are:

1. for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
2. $0 < a_{ij}(q) \le m < \infty$ on $S$;
3. $\varphi$ attains its maximum on $S$.

For the continuous processes, $\|x\| = \sum_i |x_i|$ and $\|A\| = \sum_{i,j}|a_{ij}|$, and a solution of $dx/dt = F(t,x)$, $x(0)=c$, on $[0,T]$ is a continuous $x$ with $x(t) = c + \int_0^t F(s, x(s))\,ds$, which is the book's "satisfying the equation almost everywhere". The successive approximations are $x_0 = c$, $x_{n+1}(t) = c + \int_0^t F(s, x_n(s))\,ds$.

Formalization targets

Goal: Chapter XI, Theorem 2

Under (10.3) there is exactly one $\lambda > 0$ for which

$$\lambda y_i = \max_q \sum_{j=1}^N a_{ij}(q)\, y_j, \qquad i = 1,\dots,N,$$

has a solution with all $y_i > 0$. That solution is unique up to a positive factor, and

$$\lambda = \max_{q \in S} \varphi(q).$$

Milestones

1. § 4, Lemma. For row-wise maximized operators $T_1(x) = \max_q[b_1(q,t) + \int_0^t A(q,s)x\,ds]$ and $T_2(y)$ likewise, $\|T_1(x) - T_2(y)\| \le \max_q[\|b_1 - b_2\| + \int_0^t \|A(q,s)\|\,\|x-y\|\,ds]$.
2. Theorem 1. If $\|A(q,t)\|, \|b(q,t)\| \le f(t)$ with $f$ locally integrable and the maximum is attained, then $dx/dt = \max_q[A(q,t)x + b(q,t)]$, $x(0) = c$, has a unique solution, the uniform limit of the successive approximations.
3. Theorem 3 (corrected). If moreover $\varphi$ has a unique maximizer on $S$ and $c \ge 0$, $c \ne 0$, then the recurrence satisfies $x_i(n) \sim a\,y_i\,\lambda^n$ with $a = a(c) > 0$.
4. Theorem 4. The same well-posedness for $dx/dt = \max_p\min_q[A(p,q,t)x + b(p,q,t)] = \min_q\max_p[\dots]$ on $[0,T]$.
5. Theorem 5. If $(Bp,q) \ge d > 0$ on probability vectors, the solution of $du/dt = \max_p\min_q[(Ap,q) - (Bp,q)u]$ satisfies

$$\lim_{t\to\infty} u(t) = \max_p \min_q \frac{(Ap,q)}{(Bp,q)} = \min_q \max_p \frac{(Ap,q)}{(Bp,q)} .$$

Significance

Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration $x(n+1) = \max_q A(q)x(n)$: after normalization by $\lambda^n$ the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.

The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.

Difficulty

The map $y \mapsto \max_q A(q)y$ is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification $\lambda = \max_q \varphi(q)$ must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each $A(q)$, including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when $S$ is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in $t$ and Lipschitz in $x$ with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.

Formalization scope

Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row $i$'s control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume $N \ge 1$; for $N = 0$ every $\lambda$ would qualify.

Conventions and repairs:

• Theorem 3 prints "a unique q for which the maximum value of q is assumed". A control has no maximum value; the proof uses "$q^*$ ... the value of $q$ for which $\lambda = \varphi(q^*)$", so the hypothesis is uniqueness of the maximizer of $\varphi$. For $c = 0$ the iterates vanish and $x_i(n) \sim a y_i\lambda^n$ fails, so $c \ne 0$ is assumed (the proof takes $c > 0$ "without loss of generality"). The asymptotic is stated as $x_i(n)/\lambda^n \to a y_i$ with $a > 0$.
• Theorems 1 and 4: the book's controls are functions of $t$ with the maximum outside the integral; since the maximization is pointwise (§ 4), the statements use pointwise sets and the integral of the pointwise maximum. Measurability of $t \mapsto F(t,x)$ is not stated in the book and is assumed. In Theorem 4 the max-min is taken row by row, and (2a) is encoded as the existence of a saddle point in each row.
• § 4 Lemma: "$\le \max_q[\dots]$" is stated as "$\le [\dots]$ at some admissible joint $q$".
• Theorem 5: the right-hand side is the max-min form; the equality of the two ratio values is part of the conclusion.

Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for $dx/dt = F(t,x)$ with an integrable Lipschitz constant, each reusable well beyond this mission.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter XI. https://doi.org/10.2307/j.ctv1nxcw0f
• R. Bellman, "A Markovian decision process", Journal of Mathematics and Mechanics 6 (1957), 679–684.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• O. Perron, "Zur Theorie der Matrices", Mathematische Annalen 64 (1907), 248–263. https://doi.org/10.1007/BF01449896
• B. Lemmens and R. Nussbaum, Nonlinear Perron–Frobenius Theory, Cambridge University Press, 2012. https://doi.org/10.1017/CBO9781139026079