The OR Formalization Drive

Why restricted policy classes

Abstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping $H(x,u,J)$: the cost of using control $u$ at state $x$ when the future is valued by the function $J$. Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors $\mu:S\to C$ and $H$ is defined on all extended-real functions on $S$.

That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which $H$ acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class $\tilde M$ and $H$ is only defined on a prescribed class $\tilde F$ of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.

Setting

The data are a state space $S$, a control space $C$, nonempty constraint sets $U(x)\subseteq C$, and three restricted classes: sets of functions $F^*\subset\tilde F\subset F$, where $F$ is the set of all functions $S\to[-\infty,\infty]$, and a set $\tilde M$ of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$. The mapping $H:S\times C\times\tilde F\to[-\infty,\infty]$ is monotone: $J\le J'$ in $\tilde F$ implies $H(x,u,J)\le H(x,u,J')$. For $\mu\in\tilde M$ and $J\in\tilde F$,

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

A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ with every $\mu_k\in\tilde M$; their set is $\tilde\Pi$. Given $J_0\in F^*$ with $J_0>-\infty$, the $N$-stage and infinite-horizon costs are

$$J_{N,\pi}=(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0),\qquad J_\pi(x)=\lim_{N\to\infty}J_{N,\pi}(x),$$

and the optimal costs are $J^*_N=\inf_{\pi\in\tilde\Pi}J_{N,\pi}$ and $J^*=\inf_{\pi\in\tilde\Pi}J_\pi$. For a stationary policy $(\mu,\mu,\dots)$ write $J_\mu$.

Five standing conditions tie the classes together: A.1 (every control $u\in U(x)$ is the value $\mu(x)$ of some $\mu\in\tilde M$), A.2 ($F^*$ is closed under $T$ and under adding constants), A.3 ($\tilde F$ is closed under every $T_\mu$, $\mu\in\tilde M$, and under adding constants), A.4 ($\varepsilon$-minimizing selectors for $T(J)$, $J\in F^*$, exist in $\tilde M$), and A.5 ($\tilde F$ and $F^*$ are closed under pointwise limits). Assumption $\tilde C$ asks for a closed subset $\bar B$ of the space $B$ of bounded real functions with the sup norm $\|\cdot\|$, containing $J_0$ and invariant under $T$ on $\bar B\cap F^*$ and under $T_\mu$ on $\bar B\cap\tilde F$, such that every $J_\pi$ exists and is real, each $T_\mu$ is $\alpha$-Lipschitz on $B\cap\tilde F$, and every $m$-fold composition $T_{\mu_0}\cdots T_{\mu_{m-1}}$ is a $\rho$-contraction on $\bar B\cap\tilde F$ for some $\rho<1$.

Formalization targets

Goal: Proposition 6.4 (p. 97)

Under A.1–A.5 and $\tilde C$: $J^*\in\bar B\cap F^*$ is the unique fixed point of $T$ in $\bar B\cap F^*$, with $T(J')\le J'\Rightarrow J^*\le J'$ and $J'\le T(J')\Rightarrow J'\le J^*$; each $J_\mu$, $\mu\in\tilde M$, is the unique fixed point of $T_\mu$ in $\bar B\cap\tilde F$;

$$\lim_{N\to\infty}\|T^N(J)-J^*\|=0\ \ (J\in\bar B\cap F^*),\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0\ \ (J\in\bar B\cap\tilde F);$$

a stationary $(\mu^*,\mu^*,\dots)\in\tilde\Pi$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$; and for every $\varepsilon>0$ some stationary policy in $\tilde\Pi$ satisfies $\|J^*-J_{\mu_\varepsilon}\|\le\varepsilon$.

Milestones

In attack order:

1. Proposition 6.3(a) (p. 96) — under A.1–A.4 and the exact selection assumption, a uniformly $N$-stage optimal policy exists iff the infimum in $T^{k+1}(J_0)(x)=\inf_{u\in U(x)}H[x,u,T^k(J_0)]$ is attained for each $x\in S$ and $k<N$.
2. Proposition 6.5(a) (p. 97) — under A.1–A.5, $\tilde C$ and exact selection: if for each $x$ some policy in $\tilde\Pi$ is optimal at $x$, then an optimal stationary policy exists in $\tilde\Pi$.

Further results of the chapter

The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:

• Proposition 6.2 — $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu_k^*}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$; such a policy forces $J^*_N=T^N(J_0)$.
• Proposition 6.1(a) — under Assumption $\tilde F.2$ and $J^*_k>-\infty$: $J^*_N=T^N(J_0)$ and $N$-stage $\varepsilon$-optimal policies exist in $\tilde\Pi$.
• Proposition 6.1(b) — under Assumption $\tilde F.3$ and $J_{k,\pi}<\infty$: $J^*_N=T^N(J_0)$ and $\{\varepsilon_n\}$-dominated convergence to optimality.
• Proposition 6.3(b) — compact level sets $U_k(x,\lambda)$ give both $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy.
• Proposition 6.5(b) — compact level sets of the iterates $T^k(J)$, $k\ge\bar k$, give an optimal stationary policy.

Significance

Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary $\varepsilon$-optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm $J^*_N=T^N(J_0)$, and their hypotheses ($\tilde F.3$, exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.

The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case ($F^*=\tilde F=F$, $\tilde M=M$) of Chapters 3 and 4.

Difficulty

The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to $T$ on $\bar B$. Here the obvious transcription fails at two points. First, $T$ maps $\bar B\cap F^*$ into itself but $T_\mu$ only maps $\bar B\cap\tilde F$ into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in $\tilde M$: pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.

Formalization scope

Functions on $S$ are S → EReal. $H$ is a total Lean function, but monotonicity is assumed only on $\tilde F$ and every statement evaluates $H$ only at functions of $\tilde F$. $J_\pi$ is limUnder; Assumption $\tilde C$ makes the limit exist. $B$ is Mathlib's $\ell^\infty(S,\mathbb R)$; a bound $\|G-G'\|\le c$ between extended-real functions means both are real everywhere and $|G(x)-G'(x)|\le c$, which is how the book's convention $\infty-\infty=\infty$ reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. $J^*_N$ and $J^*$ are infima over $\tilde\Pi$ only, the $\varepsilon$-optimality notions keep the book's two-case form at $-\infty$, and $N$ is a positive integer.

The chapter collapses to Chapters 3–4 if $F^*=\tilde F=F$ or $\tilde M=M$ is built in; here $F^*$, $\tilde F$ and $\tilde M$ are arbitrary and constrained only by A.1–A.5, and $J^*$ is never defined as a fixed point.

A complete development needs the $m$-step contraction mapping theorem on a closed subset of $\ell^\infty$, monotonicity lemmas for $T$ and $T_\mu$, and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption $\tilde C$ contraction, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 6. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control and Optimization 15(3), 1977, 438–464. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 1967, 165–177. https://doi.org/10.1137/1009030

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$. The state space $S$, control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$. Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$, the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ($\{g<c\}$ is analytic for every real $c$), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$.

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$-stage cost and optimal cost are

$$J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).$$

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$, and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$, for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$-th pair. The DP operators are

$$T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.$$

Formalization targets

Goal: Proposition 8.2

$$J^*_K=T^K(J_0),\qquad K=1,\dots,N,$$

under (F⁺) or (F⁻), where $J_0\equiv0$. The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$), Lemma 8.4 (monotone and bounded convergence for $T_\mu$). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ($J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$.

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$, choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$-optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

• Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
• Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$. Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
• The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
• The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
• Stages are indexed $0,\dots,N-1$, and a history is $k$ state–control pairs plus the current state.
• $g$ is stored on $S\times C$, but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$, not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

• the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
• extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.

Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).

Timeline:

• 1965: Blackwell, discounted dynamic programming on Borel spaces with Borel-measurable data, case (D).
• 1966: Strauch, negative dynamic programming, case (N), with Borel-measurable data.
• 1978: Bertsekas and Shreve, Chapter 9: lower semianalytic costs and universally measurable policies, in all three cases (P), (N), (D).
• 1979: Shreve and Bertsekas, the journal account of universally measurable policies.

Setting

An infinite horizon stochastic optimal control model (SM) is an eight-tuple $(S, C, U, W, p, f, \alpha, g)$. The state space $S$, the control space $C$ and the disturbance space $W$ are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint $U$ assigns to each state $x$ a nonempty set $U(x) \subseteq C$, and the set $\Gamma = \{(x,u) \mid u \in U(x)\}$ is analytic. The disturbance kernel $p(dw \mid x, u)$ is a Borel stochastic kernel and the system function $f : SCW \to S$ is Borel. The discount factor is $\alpha > 0$, and the one-stage cost $g : \Gamma \to [-\infty, \infty]$ is lower semianalytic: each sublevel set $\{g < c\}$ is analytic. The state moves by $x_{k+1} = f(x_k, u_k, w_k)$, with transition kernel $t(B \mid x, u) = p(\{w \mid f(x,u,w) \in B\} \mid x, u)$.

A policy $\pi = (\mu_0, \mu_1, \dots)$ chooses $u_k$ at random from a universally measurable stochastic kernel $\mu_k(du_k \mid x_0, u_0, \dots, x_k)$ concentrated on $U(x_k)$; $\Pi'$ is the set of all policies. A policy is Markov if each $\mu_k$ depends only on $x_k$, and it is stationary if, moreover, $\mu_k = \mu$ for all $k$. Writing $q_k(\pi, p_x)$ for the law of $(x_k, u_k)$ started from $x_0 = x$, the cost of $\pi$ and the optimal cost are

$$J_\pi(x) = \sum_{k=0}^\infty \alpha^k \int g\, dq_k(\pi, p_x), \qquad J^*(x) = \inf_{\pi \in \Pi'} J_\pi(x).$$

For $J : S \to [-\infty, \infty]$, the dynamic programming operators are

$$T(J)(x) = \inf_{u \in U(x)} \Big\{ g(x,u) + \alpha \int_S J(x')\, t(dx' \mid x, u) \Big\}, \qquad T_\mu(J)(x) = \int_C \Big[ g(x,u) + \alpha \int_S J\, dt \Big] \mu(du \mid x).$$

The three cases are (P) $g \ge 0$ on $\Gamma$; (N) $g \le 0$ on $\Gamma$; (D) $\alpha < 1$ and $|g| \le b$ on $\Gamma$ for some real $b$.

Formalization targets

Goal: the optimality equation (Proposition 9.8, Eq. (22))

Under each of (P), (N) and (D),

$$J^* = T(J^*).$$

Milestones

• $J^*$ is lower semianalytic (Corollary 9.4.1).
• For a stationary policy, $J_\mu = T_\mu(J_\mu)$ (Proposition 9.9).
• Optimality tests for stationary policies: under (P) or (D), $(\mu, \mu, \dots)$ is optimal iff $J^* = T_\mu(J^*)$ (Proposition 9.12); under (N) or (D), iff $J_\mu = T(J_\mu)$ (Proposition 9.13).
• Under (N) or (D), value iteration from $0$ converges to $J^*$, and under (D) it converges uniformly from every bounded lower semianalytic start (Proposition 9.14).

Further statements of the mission

• Markov policies suffice: at each state some Markov policy matches any policy's cost (Proposition 9.1), so $J^* = \inf_{\pi \in \Pi} J_\pi$ (Corollary 9.1.1).
• Partial converses of the optimality equation: $J \ge T(J)$, $J \ge 0$ gives $J \ge J^*$ under (P); $J \le T(J)$, $J \le 0$ gives $J \le J^*$ under (N); a bounded solution of $J = T(J)$ equals $J^*$ under (D) (Proposition 9.10). The analogous statements for $T_\mu$ and $J_\mu$ (Proposition 9.11).

Significance

The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for $\varepsilon$-optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.

All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.

Difficulty

Under (D), $T$ is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals $J^*$ requires knowing that $J^*$ belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: $\lim_k J_k(0) = 0$ while $J^*(0) = \infty$). Even when each $J_k$ is Borel, $J^*$ may fail to be (Example 2). So $J^* = T(J^*)$ cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines $T$.

The book's route lifts (SM) to a deterministic model on the space of probability measures $P(S)$, where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.

Formalization scope

The draft fixes the following conventions.

• Spaces. Borel spaces are topological spaces homeomorphic to Borel subsets of complete separable metric spaces, carrying their Borel $\sigma$-algebras. Analytic sets are Mathlib's AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.
• Extended reals. Values lie in EReal. The book's convention $\infty - \infty = -\infty + \infty = \infty$ is implemented explicitly, because Mathlib's EReal sets $\bot + \top = \bot$. The integral of an extended-real function is $\int f^+ - \int f^-$ with the same convention.
• Policies. These are sequences of universally measurable stochastic kernels on the history spaces $S_0C_0 \cdots S_k$, charging $U(x_k)$ with mass one. The laws of $(x_0, u_0, \dots, x_k, u_k)$ are built recursively from the kernels.
• Costs. $J_\pi$ is the series $\sum_k \alpha^k \int g\, dq_k$, computed as the difference of the series of positive and negative parts. Under each of (P), (N), (D) it coincides with the integral of the total discounted cost. $J^*$ is the infimum over all policies.
• Case labels. Each statement carries the case labels the book attaches to it, as hypotheses on the model.
• Scope. Only the (SM) statements are formalized. The deterministic model (DM) on $P(S)$ is the book's proof device and enters no statement.

The goal admits a trivializing formalization that this draft rules out. $J^*$ is not defined as a fixed point of $T$, nor as the limit of $T^k(0)$; it is the infimum of the costs of all policies, which under (P) can differ from that limit.

A complete development needs universally measurable kernels and their compositions on product spaces, measurability of $x \mapsto \int f(x, y)\, q(dy \mid x)$ for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996. Chapter 9. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Why partial balance

Equilibrium distributions of Markov models of networks are rarely computed by solving the full equilibrium equations directly. In the classical product-form results (migration processes, Jackson and Kelly networks, loss networks, clustering processes) the equilibrium distribution satisfies a stronger, local family of equations, and that is what makes it computable. The strongest such family is detailed balance, which characterizes reversibility. Many models that are not reversible still satisfy an intermediate family, partial balance: the probability flux balances not pair by pair but across a chosen set of transitions. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) uses partial balance throughout: quasi-reversibility in Chapter 3 is a form of it, and the models that display it tend to be insensitive, meaning their equilibrium distribution does not change when exponential holding times are replaced by general ones with the same mean.

Section 9.4 of the book collects what partial balance means in a single statement. Theorem 9.5 summarizes Exercises 1.6.2–1.6.4 and 1.7.7–1.7.8 and gives five operational characterizations of partial balance. Corollaries 9.6–9.8 translate them into the language of spatial processes, and Theorem 9.9 turns partial balance of a coarse description into a product-form equilibrium for a finer one. This last step is the mechanism behind insensitivity.

Setting

A Markov process on a state space $\mathcal S$ has transition rates $q(j,k)\ge0$ for $j\ne k$, with $q(j,j)=0$. It is irreducible: every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers $\pi(j)$ summing to one that satisfies the equilibrium equations

$$\pi(j)\sum_{k\in\mathcal S}q(j,k)=\sum_{k\in\mathcal S}\pi(k)q(k,j),\qquad j\in\mathcal S.$$

For an irreducible process on a finite state space it exists and is unique.

Given a set $\mathcal A\subseteq\mathcal S$, $\pi$ satisfies partial balance with respect to $\mathcal A$ if

$$\pi(j)\sum_{k\in\mathcal A}q(j,k)=\sum_{k\in\mathcal A}\pi(k)q(k,j),\qquad j\in\mathcal A.$$

Truncating the process to $\mathcal A$ deletes every transition out of $\mathcal A$, and the result is required to be irreducible within $\mathcal A$. The time-reversed process of a process with equilibrium distribution $\pi$ has rates $\pi(k)q(k,j)/\pi(j)$.

A spatial process has $J$ sites, the vertices of a graph $G$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and the state space is $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. Write $T_j^m\mathbf n$ for the state $\mathbf n$ with the attribute of site $j$ changed to $m$. The process must satisfy three conditions: only one site changes at a time; the rate $q(\mathbf n,T_j^m\mathbf n)$ depends on the other sites only through the neighbours of $j$; and any $T_j^m\mathbf n$ can be reached from $\mathbf n$ without changing the other sites. The conditional distribution of site $j$ given the rest is $P(n_j\mid\mathbf n_{G-j})=\pi(\mathbf n)/\sum_m\pi(T_j^m\mathbf n)$. A Markov field is a positive distribution whose conditional distributions depend only on the neighbours of $j$.

Formalization targets

Goal: Theorem 9.5

For an irreducible process on a finite $\mathcal S$ with equilibrium distribution $\pi$, a nonempty $\mathcal A$ within which the truncated process is irreducible, and a constant $c>0$, $c\ne1$, the following are equivalent:

1. partial balance with respect to $\mathcal A$;
2. the equilibrium distribution of the truncated process is $\pi(j)/\sum_{k\in\mathcal A}\pi(k)$;
3. multiplying the rates $q(j,k)$, $j,k\in\mathcal A$, by $c$ leaves the equilibrium distribution unchanged;
4. multiplying the rates $q(j,k)$, $j\in\mathcal A$, $k\notin\mathcal A$, by $c$ changes the equilibrium distribution to

$$B\pi(j)\ (j\in\mathcal A),\qquad Bc\pi(j)\ (j\notin\mathcal A),\qquad B^{-1}=\sum_{j\in\mathcal A}\pi(j)+c\sum_{j\notin\mathcal A}\pi(j);$$

5. time reversal and truncation to $\mathcal A$ commute.

When $\mathcal S-\mathcal A$ is nonempty, these are also equivalent to:

6. the chain observed just before each exit from $\mathcal A$ and the chain observed just after each entry into $\mathcal A$ have the same equilibrium distribution.

Milestones

• Corollary 9.6: the equivalences for the sets on which all sites but $j$ are frozen, i.e. partial balance (9.26) at a site.
• Corollary 9.7: on a state space with at least two states, partial balance at every site makes $\pi$ a Markov field, with $0<\pi(\mathbf n)<1$ as in the book's definition.
• Corollary 9.8: the equivalences for the set on which site $j$ is frozen at one attribute (9.27).
• Theorem 9.9: if a reduced description $\mathbf n=f(\mathbf x)$ has a distribution $\pi(\mathbf n)$ in partial balance for the rates (9.31), then the finer process has equilibrium distribution $\pi(\mathbf x)=\pi(\mathbf n)\prod_jP_j(x_j\mid n_j)$.

What the results give

Theorem 9.5 makes partial balance testable by operations on the process itself: truncation, speeding up or slowing down transitions, and time reversal. The book points to close relationships between statement (iv) and the product form of Section 2.3, and between statement (ii) and part (iii) of Theorem 3.12. Corollary 9.6 (iv) explains why the reversed migration process has such a simple form. Corollary 9.7 strengthens Theorem 9.3 by replacing reversibility with partial balance at each site. Theorem 9.9 is the step from partial balance to insensitivity: it is what the book uses to show that a spatial process keeps its equilibrium distribution when the lifetimes of attributes are mixtures of gamma distributions.

All of these results were proved in 1979. None has a machine-checked proof. The platform has the reversible special case of statement (ii) (KellyStochasticNetworks.truncated_reversible) and the rate-level objects for time reversal and truncation, which this mission reuses. Formalizing Theorem 9.5 also produces a reusable account of embedded exit and entry chains of a finite Markov process.

Difficulty

Most of the equivalences (i)–(v) are short manipulations of the equilibrium equations, but each direction from a property of an altered process back to partial balance needs uniqueness of equilibrium distributions for irreducible finite processes, and (v) ⇒ (i) also needs their existence. Mathlib has neither in the form needed here. Statement (vi) is a different kind of claim. The equilibrium distribution of the exit chain is proportional to the exit flux $\pi(j)\sum_{k\notin\mathcal A}q(j,k)$, and that of the entry chain to the entry flux. Proving this requires the hitting distributions and the Green's function of the jump chain killed on leaving a set, and the convergence of the series that define them. Corollary 9.8 (v) inherits that work. Theorem 9.9 requires uniqueness for the reduced frozen processes and careful bookkeeping of the fibres $\{x_j:f_j(x_j)=n_j\}$.

Formalization scope

State spaces are finite types, and every sum is an unconditional sum over a finite type. Because the state space is finite, the book's extra condition for (vi), a finite flux out of $\mathcal A$, holds automatically. Rates are real functions with $q(j,j)=0$ built into the hypotheses; the reduced rates of (9.31) also have zero self-rates. "The equilibrium distribution of a process is $X$" means: $X$ is positive, sums to one, satisfies the equilibrium equations, and every distribution with these properties equals $X$. The book's "$c\ne0$ or $1$" is read as $c>0$, $c\ne1$, so that altered rates remain rates. Truncation to $\mathcal A$ is the published truncatedRates, a process on the subtype $\mathcal A$, and the reversed rates are the published reversedRates. The exit and entry chains are defined from the jump chain through series of restricted matrix powers. Spatial processes live on $\prod_j\mathcal N_j$ with $T_j^m$ given by Function.update. In Theorem 9.9 the graph is complete, as the book assumes from p. 202 on.

The equilibrium distribution of the truncated process must be the unique positive normalized solution of the truncated equilibrium equations. It must not be defined as the conditional distribution, which would make (ii) a tautology. For the same reason (iii) and (iv) are stated through the equilibrium equations of the altered rates, not by assumption.

Theorem 9.10 (p. 207) is not a target. Its hypothesis, that a nominal lifetime "can have any distribution with unit mean", is not defined on the page, and the point-process and lifetime description it needs lies outside this rate-level development.

Contributions are welcome at every level: uniqueness and existence of equilibrium distributions for irreducible finite rate matrices (reusable across the series), convergence of the killed Green's function, and proofs of the corollaries from the goal.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979; reissued Cambridge University Press, 2011. https://doi.org/10.1017/CBO9781139171724 (§9.4, pp. 200–208; §1.6, pp. 25–27)
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$, the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$, by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$. For a state $j$, $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$, transient if $f_{jj} < 1$ for every $j$, and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$: $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$,

$$[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},$$

that is $p_{i0} = \alpha_i$, $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ for $j > i+1$. In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

$$\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],$$

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

$$\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .$$

Together: ergodic for $\rho < 1$, recurrent-null for $\rho = 1$, transient for $\rho > 1$. The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

1. Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$, the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$.
2. Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
3. Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$.
4. Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ($i \ne 0$) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$, and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

• The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
• States are indexed from $0$, as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$), so the statement is not vacuous.
• $\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$: an infinite mean gives $\rho = 0$, and that chain is ergodic.
• The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$. Milestones 2–4 carry them, as the paper's standing assumptions (§1).
• Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$.
• Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
• Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$, and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
• D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

Motivation

A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.

A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.

Setting

Fix $c, f \in \mathbb R^n$ and write a linear program in the homogeneous form (6)

$$(P)\qquad \min\{c^{T}x \mid Ax \ge 0,\ f^{T}x = 1\},$$

where $A$ is a real $m\times n$ matrix and $Ax\ge0$ is componentwise. Every linear program can be put in this form. The matrix $A$ is uncertain: it is only known to lie in an uncertainty set $\mathcal U$ of $m\times n$ matrices. Each $A\in\mathcal U$ gives an instance $(P)$ with feasible set $\{x\mid Ax\ge0,\ f^{T}x = 1\}$ and optimal value $c^*(P)$; the family of instances is $\mathcal P$. The robust counterpart (7) is

$$(P_{\mathcal U})\qquad \min\{c^{T}x \mid x \in G_{\mathcal U}\},\qquad G_{\mathcal U} = \{x\mid Ax\ge0\ \ \forall A\in\mathcal U;\ f^{T}x = 1\},$$

and its optimal value is $c^*$. Since $G_{\mathcal U}$ does not change when $\mathcal U$ is replaced by its closed convex hull, the paper assumes throughout that $\mathcal U$ is convex and closed.

Let $\mathcal U_i\subseteq\mathbb R^n$ be the set of all realizations of the $i$-th row, the projection of $\mathcal U$ onto the data of the $i$-th constraint. The uncertainty is constraint-wise if $\mathcal U = \mathcal U_1\times\dots\times\mathcal U_m$: the rows vary independently. The Boundedness Assumption asks for a convex compact set $Q\subseteq\mathbb R^n$ that contains the feasible set of every instance.

Formalization targets

Goal: Proposition 2.1 (p. 5)

If the uncertainty is constraint-wise and the Boundedness Assumption holds, then

1. $(P_{\mathcal U})$ is infeasible if and only if some instance is infeasible:

$$G_{\mathcal U} = \emptyset \iff \exists A\in\mathcal U:\ \{x\mid Ax\ge0,\ f^{T}x=1\}=\emptyset;$$

2. if $(P_{\mathcal U})$ is feasible with optimal value $c^*$, then

$$c^* = \sup\{c^*(P)\mid (P)\in\mathcal P\}. \tag{9}$$

Milestones

The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of $G_{\mathcal U}$ in every instance's feasible set; the reduction of the semi-infinite system (8) on $Q$ to a finite subsystem; the statement that the finite system (10) $A_1x\ge0,\dots,A_Nx\ge0,\ f^{T}x=1$ then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.

Companions

The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: $G_{\mathcal U}$ is unchanged under passing to the closed convex hull of $\mathcal U$ (§2.1) or to the product $\mathcal U_1\times\dots\times\mathcal U_m$ of its projections (§2.2).

Significance

Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of $G_{\mathcal U}$ under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.

The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of $\mathcal U$.

Difficulty

The robust counterpart has a continuum of constraints, one for each $A\in\mathcal U$, so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in $Q$; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in $\mathcal U$, which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and $Ax\ge0$ is 0 ≤ A *ᵥ x in the componentwise order. The $i$-th row of $A$ is A i and $a^{T}x$ is a ⬝ᵥ x. The projections $\mathcal U_i$ are the images of $\mathcal U$ under $A\mapsto A_i$, not free sets, and constraint-wise uncertainty is the inclusion $\mathcal U_1\times\dots\times\mathcal U_m\subseteq\mathcal U$ (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of $Q$, as on the page.

Optimal values are infima: $c^*$ is the greatest lower bound (IsGLB) of $c^{T}x$ over $G_{\mathcal U}$, and (9) states that $c^*$ is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.

The goal carries the paper's standing assumption that $\mathcal U$ is convex and closed, and one disclosed addition: $\mathcal U$ is nonempty. The paper takes this for granted; without it part (i) fails for $f = 0$ and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets $\mathcal U_i$ are arbitrary sets with $\mathcal U = \prod_i\mathcal U_i$, or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.

A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/s0167-6377(99)00016-4 (cited here by the pages of the authors' manuscript).
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154

Motivation

The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders $q$ units before demand $D$ is observed, and pays a unit backordering cost $b$ for each unit of unmet demand and a unit holding cost $h$ for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.

Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features $p$ is comparable to the sample size $n$ ("big data"), a bound that grows with $p$ says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on $p$.

This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.

Setting

Cost. For an order $q$ and a demand $d$, the newsvendor cost is

$$C(q;d)=b\,(d-q)^+ + h\,(q-d)^+ ,\qquad b,h>0 .$$

Write $b\vee h=\max(b,h)$.

Data. A data point is a pair $z=(x,d)$ of a feature vector $x\in\mathbb R^p$ and a demand $d\in\mathbb R$. Features lie in a domain $\mathcal X$ inside the ball $\|x\|_2^2\le X_{\max}^2$, and demands lie in $\mathcal D=[0,\bar D]$. A sample $S_n=\{(x_i,d_i)\}_{i=1}^n$ consists of $n$ independent draws from an unknown probability distribution $\mu$ concentrated on $\mathcal X\times\mathcal D$.

Rules and risks. A vector $q\in\mathbb R^p$ defines the linear decision rule $q(x)=q^\top x$. Its true risk and empirical risk are

$$R_{true}(q)=\mathbb E_{(x,d)\sim\mu}\bigl[C(q^\top x;d)\bigr],\qquad \hat R(q;S_n)=\frac1n\sum_{i=1}^n C(q^\top x_i;d_i).$$

The regularized algorithm (NV-reg). For a parameter $\lambda>0$, the rule $\hat q=\hat q(S_n)$ minimizes

$$\hat R(q;S_n)+\lambda\|q\|_2^2\qquad\text{over } q\in\mathbb R^p .$$

The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from $\mathcal X\times\mathcal D$ are assumed to map $\mathcal X$ into $\mathcal D$ (the paper's $\mathcal Q\subset\mathcal D^{\mathcal X}$): the learned order quantity is never negative and never exceeds the demand cap.

Uniform stability. An algorithm is uniformly stable with parameter $\alpha_n$ if removing one observation from any sample changes the loss of its output at any test point by at most $\alpha_n$ (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).

Formalization targets

Goal: Theorem 2 (p. 9)

For every $\delta\in(0,1)$ and $n\ge1$, with probability at least $1-\delta$ over $S_n$,

$$|R_{true}(\hat q)-\hat R(\hat q;S_n)|\le\frac{(b\vee h)^2X_{\max}^2}{n\lambda}+\Bigl(\frac{2(b\vee h)^2X_{\max}^2}{\lambda}+(b\vee h)\bar D\Bigr)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

The dimension $p$ appears nowhere in the bound.

Milestones, in the order of the proof (p. 32)

1. Lemma 5 (p. 28). For $q,d\in[0,\bar D]$, $|C(q;d)|\le(b\vee h)\bar D$, and the bound is attained.
2. Display (31) (p. 31). $C$ is convex in its first argument and $(b\vee h)$-Lipschitz in it, i.e. $(b\vee h)$-admissible in the sense of Definition 2.
3. Theorem 5 (p. 31), Bousquet and Elisseeff's Theorem 22: regularization in a reproducing kernel Hilbert space with a $\sigma$-admissible loss and kernel bound $\kappa^2$ has uniform stability $\sigma^2\kappa^2/(2\lambda n)$. This is an existing platform statement, referenced rather than restated.
4. Theorem 4 (p. 30). (NV-reg) is uniformly stable with parameter $\alpha_n^r=(b\vee h)^2X_{\max}^2/(2n\lambda)$.
5. Theorem 6 (p. 31). Any algorithm with uniform stability $\alpha_n$ and loss in $[0,M]$ satisfies, with probability at least $1-\delta$,

$$|R_{true}(A,S_n)-\hat R(A,S_n)|\le2\alpha_n+(4n\alpha_n+M)\sqrt{\frac{\ln(2/\delta)}{2n}} .$$

Significance

The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate $O(1/\sqrt n)$ with constants that depend on the costs, the demand cap, the feature radius and $\lambda$, but not on the number of features. It gives a theoretical basis for regularizing when $p/n$ is not small, and it indicates how to scale $\lambda$ with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in $p$.

Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.

Difficulty

The bound is not a uniform-convergence argument: the class of linear rules on $\mathbb R^p$ has complexity growing with $p$, so any bound that holds simultaneously for all rules in the class depends on $p$. The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.

The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on $n-1$ points it carries the weight $1/(n-1)$, and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight $1/n$, which is the form of Theorem 5.

Formalization scope

Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost $h$ and underage cost $b$; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its $1/n$-weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is $\lambda\|q\|_2^2$ (the display prints both $\lambda\|q\|_2^2$ and $\lambda\|q\|_2$; the text calls the problem a quadratic program). "With probability at least $1-\delta$" is stated as: the event on which the gap exceeds the bound has measure at most $\delta$ under the product measure $\mu^n$.

Standing assumptions and pinned hypotheses.

1. $b,h,\lambda>0$, $X_{\max},\bar D\ge0$, $n\ge1$, $\delta\in(0,1)$.
2. $\mu$ is a probability measure giving full mass to $\mathcal X\times[0,\bar D]$, with $\|x\|_2^2\le X_{\max}^2$ on $\mathcal X$ (§3, p. 9; the page writes the ball as $\|x\|_2^2\le X_{\max}$, while Theorem 2's "$X_{\max}^2$ as the largest possible value of $\|x\|_2^2$" and Theorem 5's note fix the reading).
3. The algorithm is any map $S_n\mapsto\hat q(S_n)$ whose value minimizes the (NV-reg) objective, measurable in $S_n$ (Appendix B: "all functions are measurable").
4. The range assumption of Appendix B: for samples from $\mathcal X\times\mathcal D$, $\hat q^\top x\in[0,\bar D]$ for $x\in\mathcal X$.
5. The last constant is $(b\vee h)\bar D$, the loss bound $M$ from Lemma 5 that the proof feeds into Theorem 6; display (6) prints $\bar D$ there.
6. The convention that all sets are countable, and the intercept convention $x^1=1$, are not imposed.

Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in $\mathcal X$ and over samples drawn from $\mathcal X\times\mathcal D$; stated over the whole ball $\|x\|_2\le X_{\max}$, it would force $\hat q=0$ (both $\hat q^\top x$ and $\hat q^\top(-x)$ would lie in $[0,\bar D]$) and the goal would be nearly empty.

What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on $\mathbb R^p$; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.

Selected references

• C. Rudin and G.-Y. Vahn, The Big Data Newsvendor: Practical Insights from Machine Learning, MIT Sloan School Working Paper 5036-13, version of February 6, 2014 (MIT DSpace). The version formalized here.
• G.-Y. Ban and C. Rudin, The Big Data Newsvendor: Practical Insights from Machine Learning, Operations Research 67(1):90–108, 2019. https://doi.org/10.1287/opre.2018.1757
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2:499–526, 2002. https://jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008