The OR Formalization Drive

Motivation

This mission is the sixteenth and last of the Disjunctive Programming series, and its goal theorem is the book's own closing result. The chapter's arc closes a loop opened at the very start of the book: Theorem 2.1 (02a-convex-hull) gave the convex hull of a union of polyhedra in the same space via lifting; this chapter's Theorem 13.13 (not drafted in this mission — see below) gives the dominant of a union of polytopes in different spaces, and the chapter's final result specializes that machinery to the case where the two polytopes are polymatroids — obtaining a fully explicit, closed-form convex hull in the original variable space, with no lifting at all. Polymatroids are among the most heavily studied objects in combinatorial optimization, from Edmonds's foundational greedy-algorithm characterization onward (J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87), and a disjunction of two polymatroids — "satisfy one covering system or the other" — arises naturally whenever two competing combinatorial resource constraints interact.

Setting

Fix a ground set $N = \{1,\dots,n\}$. A set function $r : 2^N \to \mathbb{R}$ is a polymatroid rank function if $r(\emptyset)=0$, $r$ is nondecreasing, and $r$ is submodular: $r(A)+r(B) \ge r(A\cup B)+r(A\cap B)$ for all $A,B\subseteq N$. (A related but distinct condition, used earlier in the chapter for "Application 1," additionally requires $r(A)\le|A|$ on every proper subset — matroid rank functions satisfy both.) The associated polymatroid is

$$P(r) := \Big\{x \in \mathbb{R}^n_+ : \textstyle\sum_{j\in A} x_j \le r(A) \text{ for all } A \subseteq N\Big\}.$$

For two ground sets $M,N$ and set functions $r_1,r_2$, the disjoint-space union is $Z(r_1,r_2) := \{(x,y)\in[0,1]^m\times[0,1]^n : x\in P(r_1) \text{ or } y\in P(r_2)\}$. For polymatroid rank functions $r_1,r_2$ on the same ground set $N$, $\Pi := \{\pi \ge 0 : \pi x \le 1 \text{ for } x \in P(r_1)\cup P(r_2)\}$ and $U := \{u \ge 0 : \sum_A u_A r_i(A) \le 1,\ i=1,2\}$ (indexed by all subsets $A \subseteq N$) are the auxiliary polytopes the final proof reduces to.

Formalization targets

Proposition 13.16. For set functions $r_1,r_2$ satisfying the Application-1 conditions,

$$\mathrm{conv}(Z(r_1,r_2)) = \Big\{(x,y) : \frac{|A|-x(A)}{|A|-r_1(A)} + \frac{|B|-y(B)}{|B|-r_2(B)} \ge 1 \ \forall A\subseteq M, B\subseteq N \text{ with } r_1(A)<|A|,\ r_2(B)<|B|\Big\}.$$

Corollary 13.21. The same-space specialization: $\mathrm{conv}(P(r_1)\cup P(r_2)) = \{w\in[0,1]^n : w=x+y, \text{[the same displayed inequality, } A,B\subseteq N\text{]}\}$.

Proposition 13.22. $\Pi$ is exactly the projection, onto $\pi$, of $\{\pi_j \le \sum_{A\ni j} u_A\ (j\in N),\ \sum_A u_A r_i(A)\le1\ (i=1,2),\ \pi,u\ge0\}$.

Proposition 13.23. Every extreme point of $\Pi$ arises from an extreme point of $U$ via $\pi_j = \sum_{A\ni j} u_A$.

Theorem 13.24 (goal, the book's closing theorem). For polymatroid rank functions $r_1,r_2$,

$$\mathrm{conv}(P(r_1)\cup P(r_2)) = \Big\{x\ge0 : x(A)\le\max\{r_1(A),r_2(A)\}\ \forall A\subseteq N;\ \ \frac{r_2(B)-r_1(B)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(A) + \frac{r_1(A)-r_2(A)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(B) \le 1$$ $$\ \forall A,B\subseteq N \text{ with } (r_1(A)-r_2(A))(r_1(B)-r_2(B))<0\Big\}.$$

The targets trace the book's own tower: the disjoint-space specialization (13.16) and its same-space corollary (13.21) establish the lifted description; Propositions 13.22-13.23 build the blocker/projection machinery; Theorem 13.24 collapses everything into the unlifted, original-variable-space closed form that is the book's final word.

Significance

Theorem 13.24 is a genuinely rare achievement in polyhedral combinatorics: a complete, explicit, non-lifted facet description for the union of two polymatroids — objects whose individual facet structure is already exponential and only tractable via the greedy algorithm and submodular minimization. That the union of two such objects still admits a closed form, stated purely in terms of the two rank functions evaluated at pairs of subsets, is the payoff the entire chapter's machinery (dominants, blockers, upper monotonicity, disjoint-space unions) was built toward. The result strictly generalizes an earlier theorem restricted to matroid polyhedra, obtained there by different techniques specific to matroids; this proof works because polymatroid optimization (Edmonds's greedy algorithm) survives in the more general submodular, non-0/1-truncated setting.

Both directions are proved in the source (Balas's own chapter, building on Edmonds's polymatroid theory and the disjoint-union machinery developed earlier in the same chapter) but have no counterpart on this platform: nothing existing treats polymatroids, polymatroid rank functions, or a closed-form union of two polymatroids. Mathlib's Combinatorics/Matroid/* covers matroids and their rank functions but not this strictly more general polymatroid object (an integer- or real-valued submodular monotone set function, not a matroid's 0/1-truncated rank). This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.24 is to state only the "single active subset" family of inequalities ($x(A)\le\max\{r_1(A),r_2(A)\}$) and treat the two-subset family as a minor addendum — but the two-subset inequalities are not optional refinements, they are half of the facet system, arising from the genuinely two-dimensional case of the underlying linear program (a basic feasible solution of $U$ with two nonzero components). Dropping them, or stating them only for a special case of $A,B$, would produce a strictly weaker (and generally invalid, since it would omit real facets) description.

The condition $(r_1(A)-r_2(A))(r_1(B)-r_2(B))<0$ is easy to state but not to motivate without the underlying linear algebra: it is exactly the condition under which the $2\times2$ system $u_Ar_1(A)+u_Br_1(B)=1$, $u_Ar_2(A)+u_Br_2(B)=1$ has a solution with both $u_A,u_B>0$ — a fact the book verifies by direct computation (Cramer's rule) rather than a structural argument, which is why this mission states the condition exactly as derived rather than paraphrasing it into a more "intuitive" but unfaithful form.

Formalization scope

The ambient space is Fin n → ℝ throughout (or Fin m → ℝ / Fin n → ℝ separately for Proposition 13.16's disjoint spaces), matching the series default; subsets $A,B\subseteq N$ are Finset (Fin n), and the auxiliary variable $u$ of Propositions 13.22-13.23 is indexed by Finset (Fin n) itself (a genuine Fintype for fixed n), matching "$u_A$ for all $A\subseteq N$" directly. IsApp1SetFunction and IsPolymatroidRankFunction are kept as two distinct predicates — the goal theorem uses the latter, Proposition 13.16/Corollary 13.21 the former — matching BRIEF.md's explicit warning to locate and preserve the book's own exact numbered conditions rather than infer a single merged notion. A trivializing formalization to rule out explicitly: stating Theorem 13.24 with only the single-subset inequality family, which would omit the two-subset facets that are half of the theorem's actual content.

This mission depends on no other chunk's Lean definitions; it restates 13a-dominants's dominant/blocker/upper-monotone vocabulary only informally (the underlying object, not any specific Lean declaration), per the series convention, since no chunk in this series can import another's draft module. Theorem 13.13 (the general dominant of a disjoint-space union) and Theorem 13.18 (the general same-space reduction) — the two results whose specializations Proposition 13.16 and Corollary 13.21 respectively are — were not drafted this pass; see HARD.md. As the last mission of the whole book, this chunk's items.yaml closes the series begun in 01-intro-duality: sixteen missions, one book, spanning from the founding disjunctive Farkas lemma to this closed-form union of two polymatroids.

Selected references

• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87 (reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, Springer, 2003, 11–26, https://doi.org/10.1007/3-540-36478-1_2).
• E. Balas, A. Bockmayr, N. Pisaruk, and L. Wolsey, On unions and dominants of polytopes, Mathematical Programming A 99 (2004), 223–239. https://doi.org/10.1007/s10107-003-0432-4
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.2.1–13.8 (the book's final chapter). https://doi.org/10.1007/978-3-030-00148-3

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first $n$ rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret $O(d\sqrt n\log^{3/2} n)$ with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension $d \ge 1$ and an unknown parameter $\theta_* \in \mathbb R^d$. In round $t = 1, 2, \dots$ the learner is given a nonempty decision set $D_t \subseteq \mathbb R^d$, chooses $X_t \in D_t$, and observes the reward

$$Y_t = \langle X_t, \theta_* \rangle + \eta_t .$$

There is a filtration $\{F_t\}_{t \ge 0}$ such that $X_t$ is $F_{t-1}$-measurable and $\eta_t$ is $F_t$-measurable and conditionally $R$-sub-Gaussian: $\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)$ for all $\lambda \in \mathbb R$, with $R \ge 0$ fixed.

For a regularization parameter $\lambda > 0$ let $\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\top$ and let $\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_s$ be the regularized least-squares estimate. With $\|v\|_A = \sqrt{v^\top A v}$ and a known bound $\|\theta_*\|_2 \le S$, the confidence ellipsoid is

$$C_t = \Big\{\theta : \|\widehat\theta_t - \theta\|_{\overline V_t} \le R\sqrt{2\log\big(\det(\overline V_t)^{1/2}\det(\lambda I)^{-1/2}/\delta\big)} + \lambda^{1/2}S\Big\}.$$

The OFUL algorithm chooses, in round $t$, a pair $(X_t, \widetilde\theta_t)$ maximizing $\langle x, \theta \rangle$ over $D_t \times C_{t-1}$. The pseudo-regret is $R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangle$, where $\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle$.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If $\|X_t\|_2 \le L$, $\langle x, \theta_*\rangle \in [-1,1]$ for all $x \in D_t$, and $\lambda \ge \max(1, L^2)$, then for every $\delta > 0$, with probability at least $1 - \delta$,

$$\forall n \ge 0, \quad R_n \le 4\sqrt{nd\log(\lambda + nL^2/d)}\Big(\lambda^{1/2}S + R\sqrt{2\log(1/\delta) + d\log(1 + nL^2/(\lambda d))}\Big).$$

Milestone: Theorem 1, the self-normalized bound

For any positive definite $V$, $\overline V_t = V + \sum_{s\le t}X_sX_s^\top$ and $S_t = \sum_{s \le t}\eta_sX_s$: with probability at least $1-\delta$, for all $t \ge 0$,

$$\|S_t\|^2_{\overline V_t^{-1}} \le 2R^2\log\big(\det(\overline V_t)^{1/2}\det(V)^{-1/2}/\delta\big).$$

Milestones: Theorem 2, the confidence ellipsoids

With probability at least $1 - \delta$, $\theta_* \in C_t$ for all $t \ge 0$ (first claim). If $\|X_t\|_2 \le L$, then with probability at least $1-\delta$, for all $t$, $\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S$ (second claim, stated here for $d \ge 2$).

Significance

Theorem 3 bounds the regret of OFUL by $O(d\sqrt n\log n)$ with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases $V = \lambda I$, $R = 1$, $\delta < 1$ of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence $X_t$ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix $\overline V_t$, which is itself built from the adaptively chosen actions; a bound for each fixed $t$ does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $\|x\|_A$ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed $t+1$ for $t : ℕ$, so sums over $s \le t$ are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy $R^2$) requires; this is an added hypothesis. Every "with probability at least $1-\delta$, for all $t$" is stated as an outer-measure bound $\le \delta$ on the failure event, with the time quantifier inside the event. $\det(\cdot)^{1/2}$ is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes $\langle x,\theta\rangle$ over $D_t \times C_{t-1}$, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward $\langle x^*_t, \theta_*\rangle$ is the supremum over $D_t$, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed $nL/d$ is replaced by $nL^2/d$, which is what the determinant–trace bound $\det\overline V_n \le (\lambda + nL^2/d)^d$ gives; for $L \le 1$ the corrected bound implies the printed one. The hypothesis $\lambda \ge \max(1, L^2)$ is added: for $\lambda < 1$ the printed logarithm can be negative, and the printed bound would then assert $R_n \le 0$. In the second claim of Theorem 2, $d \ge 2$ is added, because at $d = 1$ the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if $\theta_* \in C_{t-1}$ for all $t$ then $R_n \le \dots$". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same $\delta$ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on $\mathbb R^d$, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general $V$ and $R$, and reusable determinant lemmas are all welcome.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of $d$ actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.

The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time $t$ (or with a horizon $n$ fixed in advance), and its guarantee is on the expected regret, which grows like $\log n$. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.

Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the $d$-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB($\delta$), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least $1-\delta$. This mission formalizes that section.

Setting

There are $d \ge 1$ arms with unknown means $\mu_1, \dots, \mu_d \in \mathbb R$. Write $\mu_* = \max_{1 \le i \le d} \mu_i$ for the best mean and $\Delta_i = \mu_* - \mu_i \ge 0$ for the gap of arm $i$.

Randomness lives on a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_t)_{t \ge 0}$. In round $t = 1, 2, \dots$ the learner plays an arm $I_t$ that is $\mathcal F_{t-1}$-measurable and receives the reward $\mu_{I_t} + \eta_t$. The noise $\eta_t$ is $\mathcal F_t$-measurable and conditionally 1-sub-Gaussian:

$$\mathbf E\left[e^{\lambda\eta_t} \mid \mathcal F_{t-1}\right] \le e^{\lambda^2/2} \qquad \text{for all } \lambda \in \mathbb R .$$

The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.

After $t$ rounds, $N_{i,t}$ is the number of plays of arm $i$ and $\overline X_{i,t}$ is the average reward received from it. For a confidence level $\delta > 0$ the confidence width is

$$c_{i,t} = \sqrt{\frac{1 + N_{i,t}}{N_{i,t}^2}\left(1 + 2\log\frac{d\,(1 + N_{i,t})^{1/2}}{\delta}\right)} \qquad (3)$$

with $c_{i,t} = +\infty$ when $N_{i,t} = 0$. UCB($\delta$) plays, in round $t$, an arm that maximizes $\overline X_{i,t-1} + c_{i,t-1}$; in particular every arm is played once before any comparison is made. The pseudo-regret after $n$ rounds is

$$R_n = \sum_{t=1}^n \left(\mu_* - \mu_{I_t}\right).$$

This is the linear bandit of the paper with the standard basis of $\mathbb R^d$ as decision set and $\theta_* = \mu$.

Formalization targets

Goal: Theorem 7 (constant regret of UCB($\delta$))

For every $\delta > 0$, with probability at least $1-\delta$, for all $n \ge 0$ simultaneously,

$$R_n \le \sum_{i : \Delta_i > 0}\left(3\Delta_i + \frac{16}{\Delta_i}\log\frac{2d}{\Delta_i\delta}\right).$$

The right-hand side depends only on the gaps, $d$ and $\delta$.

Milestone: Lemma 6 (confidence intervals)

For any adapted choice of arms (not only UCB($\delta$)) and every $\delta > 0$, with probability at least $1-\delta$,

$$|\overline X_{i,t} - \mu_i| \le c_{i,t} \qquad \text{for all arms } i \text{ and all } t \ge 0 .$$

Significance

The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability $1-\delta$ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability $\delta$ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.

Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for $V = \lambda I$ and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.

Difficulty

Two points separate this from textbook UCB analyses. First, the number of samples $N_{i,t}$ of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of $t$: a union bound over all $t$ costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale $\sum_s \eta_s \mathbf 1\{I_s = i\}$. Second, the regret statement is uniform in $n$ with constants depending on the gaps; converting a condition of the form "$c(N) \ge \Delta_i/2$" into an explicit bound on $N$ requires solving an inequality in which $N$ appears both polynomially and inside a logarithm, and the explicit constants $3$ and $16$ must come out of that step.

Formalization scope

The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.

• Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, $\mu_*$ is ⨆ i, μ i (the maximum over a nonempty finite type).
• Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index $0$ are unused.
• The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
• "With probability at least $1-\delta$, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most $\delta$. For $\delta \ge 1$ the statements are trivially true, as in the paper.
• The rule (4) is read with the statistics of rounds $1, \dots, t-1$, because the printed $\overline X_{i,t}$, $c_{i,t}$ already count round $t$. An unplayed arm, whose width is $+\infty$ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
• The printed Theorem 7 has no quantifier on $n$; it is formalized in the uniform-in-$n$ form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
• Lean's division by zero makes $\overline X_{i,t}$ and $c_{i,t}$ equal to $0$ when $N_{i,t} = 0$. Lemma 6 therefore excludes $N_{i,t} = 0$ explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with $\Delta_i > 0$, so its divisions are well defined.

A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.

Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case ($d = 1$, $\lambda = 1$, $A_s = \mathbf 1\{I_s = i\}$, $\overline V_t = 1 + N_{i,t}$), a union bound over arms, and elementary inequalities inverting $N \mapsto \frac{1+N}{N^2}(1 + 2\log(d\sqrt{1+N}/\delta))$. Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• T. L. Lai, H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation tradeoff using variance estimates in multi-armed bandits, Theoretical Computer Science 410, 2009. https://doi.org/10.1016/j.tcs.2009.01.016

Motivation

A Markov decision process (MDP) is controlled with transition probabilities estimated from data, and optimal policies computed for the estimated model can perform badly when the estimates are off. Robust MDPs replace the single transition model by a set of models and optimize the worst case over that set. Two readings of "the set" are possible. In the stationary uncertainty model, the unknown transition matrices are fixed but unknown; this is the reading that confidence regions from statistics support, but the resulting min–max problem is hard to solve. In the time-varying uncertainty model, an adversary ("nature") may pick different matrices at every stage; this relaxation is solved exactly by robust dynamic programming. Nilim and El Ghaoui (Oper. Res. 2005) solve the second problem in place of the first, and Theorem 4 of their paper justifies the substitution for discounted costs: in the infinite horizon the two readings, and the restriction to stationary controllers, all give the same value, and in the finite horizon the two readings differ by an amount that decays geometrically in the horizon.

Timeline:

• 1973: Satia and Lave study MDPs with uncertain transition probabilities (Oper. Res. 21).
• 1994: Puterman's monograph collects the nominal theory, including the optimality of stationary deterministic policies for discounted finite MDPs (Wiley).
• 2001: Bagnell, Ng and Schneider state a robust Bellman recursion for stationary games without proof (CMU-RI-TR-01-25).
• 2005: Iyengar (Math. Oper. Res. 30) and Nilim and El Ghaoui independently prove the robust Bellman recursion under rectangular uncertainty; Nilim and El Ghaoui add Theorem 4.
• 2013: Wiesemann, Kuhn and Rustem extend robust MDPs beyond rectangular sets (Math. Oper. Res. 38).

Setting

States form a finite set $\mathcal X = \{0,\dots,n-1\}$ and actions a finite nonempty set $\mathcal A$. A stage cost $c(i,a)\ge 0$ is given for every state and action, together with a discount factor $0<\nu<1$ and an initial state $i_0$. For every action $a$ and state $i$ a nonempty set $\mathcal P_i^a$ of probability vectors in the simplex $\Delta_n$ is given: the possible rows of the transition matrix $P^a$. Rectangularity means that every row is chosen independently: one stage of nature is a family $(P^a)_{a\in\mathcal A}$ with $i$-th row of $P^a$ in $\mathcal P_i^a$, and the set of such families is $\mathcal Q$.

A controller policy $\pi=(\mathbf a_0,\mathbf a_1,\dots)$ assigns an action $\mathbf a_t(i)$ to each state at each stage; the set of all of them is $\Pi$, and the stationary ones (the same map at every stage) form $\Pi_s$. A nature policy $\tau=(P_t^a)$ picks one element of $\mathcal Q$ per stage; the set is $\mathcal T$, and the stationary ones form $\mathcal T_s$. Starting from $\mu_0 = e_{i_0}$, the state law evolves by $\mu_{t+1}(j)=\sum_i \mu_t(i)P_t^{\mathbf a_t(i)}(i,j)$. The discounted costs over horizon $N$ and over the infinite horizon are

$$C_N(\pi,\tau)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)\,c(i,\mathbf a_t(i)),\qquad C_\infty(\pi,\tau)=\lim_{N\to\infty}C_N(\pi,\tau).$$

For a controller class $\mathcal C\in\{\Pi,\Pi_s\}$ and a nature class $\mathcal S\in\{\mathcal T,\mathcal T_s\}$ the robust values are $\phi_\infty(\mathcal C,\mathcal S)=\inf_{\pi\in\mathcal C}\sup_{\tau\in\mathcal S}C_\infty(\pi,\tau)$ and $\phi_N(\Pi,\mathcal S)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal S}C_N(\pi,\tau)$. Finally $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^Nc_{\max}/(1-\nu)$.

Formalization targets

Goal: Theorem 4 (p. 786)

$$\phi_\infty(\Pi,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi,\mathcal T_s),$$ $$0\le \phi_N(\Pi,\mathcal T)-\phi_N(\Pi,\mathcal T_s)\le \frac{\nu^N c_{\max}}{1-\nu}\quad\text{for every }N .$$

The second line is the paper's "the gap goes to zero at a geometric rate $\nu$", with the constant the paper's own argument produces.

Milestones (proof order of the paper)

1. Eq. (34): $C_N(\pi,\tau)\le C_\infty(\pi,\tau)\le C_N(\pi,\tau)+\varepsilon_N$ for all $\pi\in\Pi$, $\tau\in\mathcal T$, $N$.
2. Eq. (35): $\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi,\mathcal T)\le\phi_N(\Pi,\mathcal T)+\varepsilon_N$.
3. Step (e): the same sandwich for $\phi_N(\Pi,\mathcal T_s)$ and $\phi_\infty(\Pi,\mathcal T_s)$.
4. Eq. (33): for every $\varepsilon>0$ and all large $N$, $\phi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\le\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi_s,\mathcal T_s)$.
5. Step (c): for every stationary $\pi$, $\sup_{\tau\in\mathcal T}C_\infty(\pi,\tau)=\sup_{\tau\in\mathcal T_s}C_\infty(\pi,\tau)$, hence $\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$.
6. Step (d), nominal fact: for stationary $\tau$, $\inf_{\pi\in\Pi}C_N(\pi,\tau)\to\inf_{\pi\in\Pi_s}C_\infty(\pi,\tau)$.
7. Step (d): $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$.

Significance

The first half of Theorem 4 says that, for discounted robust MDPs with rectangular uncertainty, nothing is gained by either player from non-stationary behaviour: the controller may restrict itself to stationary deterministic policies and nature's time variation buys it nothing. This is what makes the stationary game (6), solved by the robust Bellman recursion of Theorem 3, the right infinite-horizon object. The second half is a quantitative guarantee for practitioners: solving the tractable time-varying problem (4) instead of the statistically motivated but hard stationary problem (3) costs at most $\nu^Nc_{\max}/(1-\nu)$ in value.

The result is proved on paper. As far as a search of the platform shows (September 2026), no robust MDP result has a machine-checked proof here; the nominal counterpart, optimality of stationary policies for discounted finite MDPs, is on the platform as BertsekasDP.discounted_main_theorem in a different model encoding (state-dependent control sets). A complete development contributes a reusable encoding of robust MDPs with time-varying and stationary adversaries, the truncation estimates for discounted costs, and a formal record of one step whose printed argument is incomplete (Step (d), see Difficulty).

Difficulty

The truncation estimates (34), (35) and Step (e) are elementary. The equalities in (31) are not: they compare values of games whose players have infinite-dimensional strategy sets, and the paper writes "min" and "max" where the infima and suprema need not be attained, since the row sets are neither closed nor convex. Two steps of the printed proof rely on results the mission does not import. Step (a) identifies $\phi_N(\Pi,\mathcal T)$ with iterates of the robust Bellman recursion, which is Theorems 1 and 3 of the paper (formalized in sibling missions of this series). Step (c) says only "following similar steps as in Step (a)". Step (d) is incomplete as printed: it shows that for each fixed stationary nature the controller's best time-varying and best stationary responses agree, which is a statement about a max–min value, whereas $\phi_\infty(\Pi,\mathcal T_s)$ is a min–max value. The obvious attempt to exchange the infimum over $\Pi$ with the supremum over $\mathcal T_s$ from that per-nature fact alone fails; the exchange requires a duality statement for the stationary game.

Formalization scope

States are Fin n; the action type is finite and nonempty. The row sets are an arbitrary family rows a i ⊆ stdSimplex ℝ (Fin n) with each set nonempty; nonemptiness is implicit in the paper and explicit here, and no convexity or closedness is assumed. A stage of nature is the subtype of families A → Fin n → (Fin n → ℝ) whose rows lie in the given sets, so rectangularity is built in. Controller policies are sequences ℕ → Fin n → A, nature policies sequences of stage choices; stationary policies of either player are the constant sequences. $C_N$ is defined from the forward state distribution (not from a Bellman recursion) and reads only stages $<N$, so the finite-horizon values over infinite sequences are exactly the paper's values (3) and (4) with stage costs $\nu^tc$ and zero terminal cost. $C_\infty$ is the sum of the series of nonnegative stage costs, which converges for $0\le\nu<1$ and equals $\lim_N C_N$. Every min and max of the paper is a real infimum ⨅ or supremum ⨆; all families are nonempty and lie in $[0,c_{\max}/(1-\nu)]$, and attainment is not assumed anywhere. The discount factor satisfies $0<\nu<1$, as in §4 of the paper.

The rate in the goal is the explicit bound $\nu^Nc_{\max}/(1-\nu)$; a formalization stating only that the gap tends to zero, or stating (31) with the infinite-horizon cost replaced by a Bellman fixed point, proves a different theorem and is not accepted.

A complete development needs: the stochastic-matrix facts for the forward distribution, geometric-series bounds, robust value iteration for the time-varying and the stationary adversary, and nominal stationarity of discounted MDPs. The model and truncation estimates are reusable for any discounted robust MDP result. Contributions of any milestone, and of proofs of Step (c) and Step (d) by any route, are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001.
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566

Motivation

The eigenvalues of the Laplacian of a graph carry metric information about the graph. The second-smallest one, $\lambda_1(G)$, was named the algebraic connectivity by Fiedler (Fiedler 1973), who showed it is positive exactly for connected graphs. N. Alon and V. D. Milman (J. Combin. Theory Ser. B 38 (1985) 73–88) showed that a large $\lambda_1$ also forces two further properties: small diameter and a concentration of measure phenomenon, in which almost every vertex is close to any set containing half the vertices. They used these facts to build explicit expanders and superconcentrators, which are sparse networks with strong connectivity guarantees used in the theory of computation and in communication network design.

This mission covers Section 2 of that paper, "The Main Tools": the edge-count inequality (Lemma 2.1), the isoperimetric inequalities (Theorems 2.5 and 2.6), and the resulting diameter bound (Theorem 2.7).

Timeline:

• 1973: Fiedler introduces $\lambda_1(G)$ as algebraic connectivity and proves $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
• 1985: Alon and Milman prove the isoperimetric and diameter bounds of Section 2.
• 1986: Alon proves the converse direction, that edge expansion implies a spectral gap (Alon 1986).
• Later work sharpened the constant in the diameter bound, e.g. Chung 1989.

Setting

Let $G = (V, E)$ be a finite, connected, simple graph on $n = |V| \ge 2$ vertices. Write $d(v)$ for the degree of a vertex $v$, $d = \max_v d(v)$ for the maximum degree, and $A_G$ for the adjacency matrix. The Laplacian is the $V \times V$ matrix

$$Q = Q_G = \operatorname{diag}(d(v))_{v \in V} - A_G .$$

For real functions $f$ on $V$ with scalar product $(f, g) = \sum_v f(v)g(v)$, the quadratic form of $Q$ is $(Qf, f) = \sum_{\{u,v\} \in E} (f(u) - f(v))^2 \ge 0$. The eigenvalues of $Q$, counted with multiplicity, are real and are written $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$. The algebraic connectivity $\lambda_1 = \lambda_1(G)$ is the second-smallest of them.

For vertices $u, v$, $\operatorname{dist}(u, v)$ is the number of edges of a shortest path from $u$ to $v$. For disjoint vertex sets $A, B$ the paper writes $\rho$ for the distance between them, $a = |A|/n$ and $b = |B|/n$ for their relative sizes, and $E_A$ ($E_B$) for the set of edges with both endpoints in $A$ (in $B$). $[x]$ denotes the integer part of $x \ge 0$.

Formalization targets

Goal: Theorem 2.7 (p. 79)

$$\operatorname{dist}(u, v) \;\le\; 2\left[\sqrt{2d/\lambda_1}\,\log_2 n\right] \qquad\text{for all } u, v \in V.$$

Milestones, in the order the proof uses them

1. Section 2, p. 76: $0 = \lambda_0 < \lambda_1$ for connected $G$.
2. Eq. (2.1), Rayleigh's principle: if $\sum_v f(v) = 0$ then $(Qf, f) \ge \lambda_1 \|f\|^2$.
3. Lemma 2.1: for nonempty $A, B$ at distance $\rho \ge 1$,

$$\lambda_1 n \le \frac{1}{\rho^2}\Big(\frac1a + \frac1b\Big)\big(|E| - |E_A| - |E_B|\big).$$

4. Remark 2.3: $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
5. Theorem 2.5: if $\rho > 1$ then

$$b \le \frac{1-a}{1 + (\lambda_1/d)\,a\rho^2}.$$

6. Theorem 2.6: if every $A$–$B$ distance exceeds a real $\rho \ge 1$, then

$$b \le (1-a)\exp\!\Big(-\ln(1+2a)\Big[\sqrt{\lambda_1/(2d)}\,\rho\Big]\Big).$$

Each statement keeps the paper's explicit constants. The goal is the endpoint of this chain and the paper's headline graph-theoretic bound.

Significance

Theorem 2.7 gives, for any family of graphs of bounded maximum degree whose algebraic connectivity stays bounded away from zero, a diameter of order $\log n$. By the paper's Remark 2.8, the 4-regular graphs constructed in its Section 4 show that this order cannot be improved. Theorem 2.6 is a discrete concentration of measure inequality: the proportion of vertices at distance more than $\rho$ from a set of relative size $a$ decays exponentially in $\rho\sqrt{\lambda_1/(2d)}$. It is the graph analogue of the Gromov–Milman concentration for manifolds, and Section 3 of the paper applies it to cubes and other product graphs. Theorem 2.5 is the input for the construction of expanders from graphs with a spectral gap (Theorem 4.3 of the paper).

All results are proved in the paper, and the formal work here is a machine-checked version of known proofs. As far as could be determined, none of the four inequalities (Lemma 2.1, Theorems 2.5–2.7) has been formalized in Lean or elsewhere. Mathlib has the Laplacian matrix, its positive semidefiniteness, and the relation between its kernel and connected components, but no statement about its second eigenvalue. The spectral facts (milestones 1–2), stated for Mathlib's Matrix.IsHermitian.eigenvalues₀, are reusable for any future work on algebraic connectivity.

Difficulty

The combinatorial steps are short. The work is at the interface between the spectral definition and the quadratic form. Mathlib defines eigenvalues through the spectral theorem for a Hermitian matrix, sorted into a list. Obtaining Rayleigh's principle for the second eigenvalue from that list, with the constant functions as the eigenvector of $\lambda_0 = 0$, takes a Courant–Fischer-type argument over an orthonormal eigenbasis. It does not follow from positive semidefiniteness alone. Strict positivity of $\lambda_1$ additionally needs that the kernel of $Q$ is one-dimensional for a connected graph.

Theorem 2.6 iterates Theorem 2.5 over a sequence of neighbourhoods $\{v : \operatorname{dist}(v, A) \le j\mu\}$ with a real step length $\mu$, so it needs bookkeeping of integer parts and of real-valued distance thresholds. Theorem 2.7 then combines Theorem 2.6 with Remark 2.3 and needs the estimate $\tfrac12\, 2^{-[\log_2 n]} < 1/n$ with the integer part kept. Replacing $[\cdot]$ by the real number inside it changes the statement.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a Fintype vertex type with decidable adjacency. Every item assumes G.Connected and $2 \le |V|$ (the goal writes $1 < |V|$, as the paper does).
• $Q$ is G.lapMatrix ℝ. $\lambda_1$ is the mission definition AlonMilman.Diameter.lambda1: the eigenvalue at index $n-2$ of eigenvalues₀, which lists the eigenvalues in decreasing order. It is $0$ by convention when $n < 2$, a case no theorem uses.
• $\lambda_1$ is defined spectrally. Defining it as the best constant in Eq. (2.1) would make Rayleigh's principle definitional and remove the spectral content of the mission, so that formalization is excluded. Likewise the goal quantifies over all pairs of vertices of a connected graph and does not use SimpleGraph.diam without connectivity, since that is $0$ for a disconnected graph.
• Distances are SimpleGraph.dist (a natural number). "The distance between $A$ and $B$ is $\rho$" is encoded as $\rho \le \operatorname{dist}(u, v)$ for all $u \in A$, $v \in B$. Because the bounds weaken as $\rho$ decreases, this is equivalent to the paper's exact distance. In Theorem 2.6 $\rho$ is real and the hypothesis is strict.
• $E_A$ is AlonMilman.Diameter.edgesWithin G A. All counts are cast to $\mathbb R$ before subtraction, $a = |A|/n$ is a real quotient, $[x]$ is Nat.floor, $\log_2$ is Real.logb 2, and $\ln$ is Real.log.
• Lemma 2.1 requires $A, B$ nonempty (so $a, b > 0$). Theorems 2.5 and 2.6 hold as stated for empty sets and carry no such hypothesis.

Contributions welcome: proofs of any milestone, and in particular general Mathlib-style lemmas for Rayleigh quotients and eigenvalues₀, which have uses beyond this mission.

Selected references

• N. Alon, V. D. Milman, λ1, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• M. Fiedler, Algebraic connectivity of graphs, Czechoslovak Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• F. R. K. Chung, Diameters and eigenvalues, J. Amer. Math. Soc. 2 (1989) 187–196. https://doi.org/10.1090/S0894-0347-1989-0965008-X

Motivation

Before a queueing network's stability can be studied in any depth, a much cruder question has to be settled: is stability even possible for the given arrival rates and service capacities, under any control policy at all? For a single M/M/1 queue the answer is the familiar $\lambda < \mu$, but a general stochastic processing network (SPN) — many buffers, many activities, servers that can be pooled or shared across job classes — has no single scalar "utilization" to compare against a threshold. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this with a linear program: the static planning problem, first formulated by Harrison (2000). This mission formalizes the theorem that answers the crude question in one direction — no control policy can stabilize a network outside the region that program identifies — which is why, as the book puts it, "throughout the remainder of this book, attention is essentially restricted to subcritical networks."

Setting

An SPN has $I$ buffers, indexed by $i \in \mathcal{I}$, and $J$ activities, indexed by $j \in \mathcal{J}$. Its first-order data — the quantities that matter for a capacity calculation, as opposed to full stochastic detail — are: the $I \times J$ material requirement matrix $B$ ($B_{ij}$ = number of class-$i$ items one type-$j$ service consumes), the $I \times J$ mean output matrix $\Gamma$ (its $j$th column is the expected output vector of a type-$j$ service), the mean service times $m_j > 0$, the $K \times J$ capacity consumption matrix $A$ (server pool $k$ against activity $j$), and the server-pool capacities $b \in \mathbb{R}_+^K$. From these,

$$R := (B - \Gamma)M^{-1}, \qquad M := \operatorname{diag}(m_1, \dots, m_J),$$

so that $R_{ij}$ is the long-run average rate at which activity $j$ depletes buffer $i$'s content.

Given an arrival-rate vector $\lambda \in \mathbb{R}_+^I$, the static planning problem (SPP) is the linear program

$$\gamma^\ast(\lambda) := \min_{x \ge 0,\, \gamma} \ \gamma \quad \text{s.t.} \quad Rx = \lambda, \quad Ax \le \gamma b,$$

whose decision variable $x_j$ is a long-run average activity rate and whose objective $\gamma$ upper-bounds every server pool's utilization. The network is subcritical at $\lambda$ if $\gamma^\ast(\lambda) < 1$, and the subcritical region is $\Lambda := \{\lambda : \gamma^\ast(\lambda) < 1\}$.

An SPN is stable (Definition 3.6, mission I) when its ambient Markov chain is positive recurrent, equivalently has a unique stationary distribution, equivalently its buffer contents converge in distribution to a non-defective limit. This mission's chapter portion (Chapters 4-5) also treats three extensions used elsewhere in the book: a Markovian arrival process replacing independent Poisson arrivals; alternate routing with immediate commitment, where arrivals must be routed into an eligible buffer at the instant they arrive, with routing rates constrained by an augmented version of the SPP; and processor sharing (PS) networks, whose service discipline falls outside the book's ordinary relaxed-control framework and is instead analyzed through an equivalent head-of-line (EHL) model built to have the same generator.

Formalization targets

Goal: Theorem 5.2 — only subcritical networks can be stable

$$\text{(baseline stochastic assumptions)} \ \wedge \ \text{(Markov representation)} \ \wedge \ \text{(SPN stable)} \implies \lambda \in \Lambda.$$

This is the weakest target that captures the chapter's content: it asserts nothing about which policy achieves stability, or whether subcriticality is sufficient (Chapters 6 onward answer that, case by case, and Chapter 5 itself gives two counterexamples where it is not) — only that subcriticality is unconditionally necessary.

Further results (milestones)

Proposition 4.1 (a strong law of large numbers for class-level arrivals under randomized routing), Proposition 4.4 (PS-network stability reduces to EHL-model stability), Proposition 5.1 (for a unitary network, subcriticality reduces to the classical load condition $\rho < b$), and Corollaries 5.4-5.6 (the same necessity conclusion under a Markovian arrival process, under alternate routing, and its consequence for maximally stable policies).

Significance

The result itself. Theorem 5.2 converts "can this network be stabilized at all?" from an open-ended search over control policies into a single linear-program feasibility check on first-order data alone. Corollary 5.6 turns this into the standard proof template every later chapter uses: exhibit a policy whose implementation does not reference $\lambda$, show it is stable throughout the subcritical region, and conclude maximal stability — without having to separately characterize the true stability region $\Lambda^\ast$, which the book calls "a deep mathematical problem" in general.

Formalizing it. A search of the platform for "processing network," "static planning problem," and "linear program" returned no hits: the SPN-specific static planning problem — its decision variables $x$ tied to a network's material-balance matrix $R$ and capacity matrix $A$ — has no existing counterpart, though the platform's linear-optimization field (16 missions) has general LP duality substrate a future proof of Proposition 5.1 or Theorem 5.2 could draw on. This mission is a from-scratch formalization of the SPP, the subcritical region, and the necessity theorem.

Difficulty

The natural first attempt states Theorem 5.2 as a claim about the buffer-contents process $Z(t)$ directly. This fails to separate cleanly from the proof, because the actual argument passes through an auxiliary quantity — the stationary mean $x := \mathbb{E}_\pi[N(0)]$ under the chain's (unique, by stability) stationary distribution $\pi$ — that has no meaning outside a specific proof strategy. The formalization instead states the goal purely in terms of the data $(R, A, b)$ and the hypothesis of stability, exactly as the book's own statement does, leaving $x$'s construction to the (currently sorry) proof. A second difficulty is Corollary 5.4's Markovian arrival process: naively reusing BaselineAssumptions with a non-Poisson arrival process is impossible, since Poisson-ness is a mandatory structural field of that definition, not an optional hypothesis — the corollary needs its own hypothesis structure that changes exactly the one clause Assumption 2.1(a) contributes and nothing else.

Formalization scope

Buffers and activities are Fin I, Fin J; matrices are Matrix over ℝ. The subcritical region is defined via the optimal SPP value $\gamma^\ast$, formalized with Mathlib's IsLeast (attained infimum, matching the book's own "$\gamma^\ast \le 1$ iff $x$ exists" phrasing, which presupposes attainment) rather than a bare existential — a formalization using, say, sInf would silently commit to junk values on an infeasible or unbounded LP and would not obviously match the book's own usage of $\gamma^\ast$ as literally attained. The basic SPN model's full state-process construction (Sections 2.3-2.4) is not re-derived from scratch here; Theorem 5.2 instead takes the structural facts its own proof invokes — the capacity constraint $AN(t) \le b$ (Eq. 2.11) and the material-requirement matrix $B$ — as explicit data, reusing mission I's BaselineAssumptions and MarkovRepresentation for the stochastic and Markov-chain apparatus. Proposition 4.4's shared- generator fact between a PS network and its EHL model (the actual content the book's construction of Section 4.4 establishes) is likewise taken as an explicit hypothesis rather than rebuilt from the refined-class/phase-type machinery of Eqs. (4.19)-(4.29); reconstructing that machinery from scratch, or reproving Proposition 4.1's SLLN from the chain's strong Markov property at regeneration times, are both welcome future contributions. A formalization that stated Theorem 5.2 with $\Lambda$ replaced by an unconstrained existential (dropping the LP structure entirely) would trivialize the chapter's actual content — the LP-feasibility characterization is what makes $\Lambda$ checkable, and is preserved here in full.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. M. Harrison, "Brownian models of open processing networks: canonical representation of workload," Annals of Applied Probability 10 (2000), 75-103.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197-218.

Motivation

A robust Markov decision process replaces the unknown transition probabilities of an MDP by sets of plausible values and optimises against the worst case. Nilim and El Ghaoui (Oper. Res. 53 (2005)) showed that, when the uncertainty is rectangular (each row of each transition matrix varies independently in its own set), the robust problem is solved by a Bellman-type recursion. Each step of that recursion needs, for every state and action, the value of an inner problem: the largest expectation of the next-stage value vector over the uncertainty set of one transition row. The recursion is only as tractable as this inner problem.

The paper studies several uncertainty models built from statistical estimates of the transition rows. In the entropy model the uncertain row is any distribution within a prescribed Kullback–Leibler divergence of a nominal distribution. For this model the paper reduces the inner problem to the minimisation of a scalar convex function, which is then solved by bisection. Iyengar (Math. Oper. Res. 30 (2005)) obtained the same robust recursion independently, and the same scalar reduction is the basic computation in later KL-constrained distributionally robust optimisation. This mission formalizes that reduction and the properties of the scalar function that the paper derives from it.

Setting

Let $n\ge 1$ and let $\Delta_n=\{p\in\mathbb R^n : p\ge 0,\ \sum_j p(j)=1\}$ be the probability simplex. For $p,q\in\mathbb R^n$ the Kullback–Leibler divergence is

$$D(p\|q)=\sum_j p(j)\log\frac{p(j)}{q(j)},$$

with $0\log 0=0$. Fix a nominal distribution $q\in\Delta_n$ with $q(j)>0$ for every $j$, and a level $\beta>0$. The entropy uncertainty set is

$$\mathcal P=\{p\in\Delta_n : D(p\|q)\le\beta\}.$$

For a vector $v\in\mathbb R^n$ (in the MDP, the value function of the next stage), the inner problem (17) is

$$\sigma_{\mathcal P}(v)=\max_{p\in\mathcal P} p^{\mathsf T}v .$$

The paper's scalar dual function (47) is, for $\lambda>0$,

$$\sigma(\lambda)=\lambda\log\Big(\sum_j q(j)\,e^{v(j)/\lambda}\Big)+\beta\lambda .$$

Write $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$, the $q$-mass of the maximisers of $v$. The tilted distribution at $\lambda>0$ is $p^*(j)=q(j)e^{v(j)/\lambda}/\sum_i q(i)e^{v(i)/\lambda}$.

In Lean, vectors are Fin n → ℝ, $\Delta_n$ is stdSimplex ℝ (Fin n), and $D$, $\mathcal P$, $\sigma$, $p^*$, $v_{\max}$, $Q(v)$ are klDiv, klBall, dualFn, tiltedDist, vmax, maxMass in the namespace RobustMDP.EntropyInner.

Formalization targets

Goal: the dual of the inner problem (§6.2, Eq. (47), p. 791)

$$\max_{p\in\mathcal P} p^{\mathsf T}v=\inf_{\lambda>0}\sigma(\lambda),$$

with the maximum attained. This is kl_ball_inner_problem_dual. It holds for every $n$, every $v$, every $q>0$ in $\Delta_n$ and every $\beta>0$.

Milestones

1. §6.1: $\max_{p\in\Delta_n}D(p\|q)=\max_i(-\log q_i)$, and for $\beta\ge\max_i(-\log q_i)$ the set $\mathcal P$ is all of $\Delta_n$ and the inner value is $v_{\max}$.
2. Eq. (48): $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$ for $\lambda>0$.
3. §6.2, the optimal distribution: $p^{\mathsf T}v-\lambda D(p\|q)\le\lambda\log\sum_j q(j)e^{v(j)/\lambda}$ on $\Delta_n$, with equality at $p^*$.
4. §6.2, elimination of $\mu$: $\min_{\mu}\big[\mu+\beta\lambda+\lambda\sum_j q(j)e^{(v(j)-\mu)/\lambda-1}\big]=\sigma(\lambda)$.
5. Eq. (49): $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$.
6. Eq. (50): $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$.
7. §6.3: if $\beta\ge-\log Q(v)$, then $\inf_{\lambda>0}\sigma=v_{\max}$ and the inner value is $v_{\max}$.

Significance

The goal turns an $n$-dimensional optimisation over a nonpolyhedral convex set into a one-dimensional convex minimisation whose objective costs $O(n)$ to evaluate. Combined with the bisection bracket from (48) and the behaviour at $0$ from (49), it gives the paper's $O(n\log(v_{\max}/\delta))$ cost per inner problem (§6.4), and hence the per-step cost of the robust Bellman recursion under entropy uncertainty. Milestone 7 identifies exactly when the uncertainty set is large enough that the robust step ignores the nominal model; unlike the cruder threshold of milestone 1, it depends on $v$.

The result is proved in the paper modulo "standard duality arguments". The paper gives no proof of the duality step itself, and its expansions (49)–(50) are proved only in outline in Appendix C. No formal proof of any of these statements is known to exist; Mathlib has the measure-theoretic Donsker–Varadhan ingredients but not the finite, constrained dual stated here. The mission produces a machine-checked version of the whole chain, with the attainment questions (which side is a max, which is only an infimum) settled explicitly.

Difficulty

The inequality $\max_{\mathcal P}p^{\mathsf T}v\le\sigma(\lambda)$ for every $\lambda>0$ is the routine half. The obstacle is the reverse inequality. The paper appeals to Lagrangian strong duality under a Slater condition, but the Lagrangian dual function equals $\sigma(\lambda)$ only for $\lambda>0$; at $\lambda=0$ it is $v_{\max}$, and the dual infimum may be approached only as $\lambda\to0^+$. A proof that looks for a minimiser $\lambda^*>0$ and a matching primal point $p^*$ fails in precisely the regime $\beta\ge-\log Q(v)$ of milestone 7, where no such $\lambda^*$ exists and the primal optimum sits on the face of the simplex spanned by the maximisers of $v$. The strong-duality argument must also handle the boundary of $\Delta_n$, where $D(\cdot\|q)$ is not differentiable.

Formalization scope

• Vectors are Fin n → ℝ; $\Delta_n$ is stdSimplex ℝ (Fin n). $D(p\|q)$ is a local finite sum with Lean's $\log 0=0$, which gives $0\log0=0$; Mathlib's measure-valued InformationTheory.klDiv is not used.
• Standing hypotheses in every theorem: $q\in\Delta_n$, $q(j)>0$ for all $j$, and $\beta>0$, as in §6.1. No restriction on $v$ is imposed; the "without loss of generality $v\ge0$" of the paper's §5 is not assumed here.
• The primal "max" is stated with IsGreatest (attained, since the KL ball is compact). The paper's "$\min_{\lambda>0}\sigma(\lambda)$" is an infimum, stated with IsGLB over $\{\sigma(\lambda):\lambda>0\}$: it is not attained when $\beta\ge-\log Q(v)$.
• dualFn is total in $\lambda$ and equals $0$ at $\lambda=0$ (division by zero), not the paper's $\sigma(0)=v_{\max}$. Every statement uses $\lambda>0$; the value at $0$ appears as the one-sided limit of (49). Accordingly (48) is stated for $\lambda>0$.
• $v_{\max}$ is ⨆ j, v j, the attained maximum over the finite nonempty index set; $\max_i(-\log q_i)$ likewise.
• (49) is stated as a limit along 𝓝[>] 0 together with a little-o remainder; (50) as a limit along atTop.
• Milestone 7 uses the non-strict condition $\beta\ge-\log Q(v)$ of the paper's first sentence, which contains the strict version of its second.
• Trivializing formalizations are excluded: the statements quantify over all $n$, $v$ and $q$, so a constant $v$, $n=1$, or the whole-simplex case of milestone 1 does not discharge the goal.

Useful infrastructure: a finite Gibbs variational inequality, compactness of the KL ball, and convexity and one-sided asymptotics of the log-sum-exp function in the temperature parameter. These are reusable for any KL-constrained robust optimisation mission. Proofs of the milestones, alternative proofs of the goal that avoid a general strong-duality theorem, and the sharper $O(\lambda e^{-t/\lambda})$ remainder of Appendix C are all welcome.

Selected references

• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. D. Donsker and S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102