Operations Research

Motivation

In stochastic optimization the law of a random return $r$ is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility $u$ by its worst case

Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which $u$ the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility $u'$ is decreasing and changes curvature once, with finite limits: log-logistic utilities $C+\log\frac{1}{1+e^{-ax}}$ used in statistics and classification, and catenary-type utilities $C-b\cosh(ax)$, each plus a concave quadratic.

The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.

Setting

Let $u:\mathbb R\to\mathbb R$.

• The family $\mathcal Q$ collects the coefficient triples of quadratics lying below $u$: $\mathcal Q=\{(A,B,C) \mid q(y)=Ay^2+By+C\le u(y)\ \forall y\in\mathbb R\}$.
• A two-point law with support $\{a,b\}$, $a<b$, puts mass $p\in(0,1)$ on $a$ and $1-p$ on $b$. It has mean $\mu$ and variance $\sigma^2$ when $pa+(1-p)b=\mu$ and $p(a-\mu)^2+(1-p)(b-\mu)^2=\sigma^2$.
• Two-point support property (Definition 1). $u$ has it with respect to $(\mu,\sigma^2)$ if some quadratic $q$ with coefficients in $\mathcal Q$ meets $u$ at two points $a<b$, i.e. $q(a)=u(a)$, $q(b)=u(b)$, and a two-point law with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$ exists. $u$ has the two-point support property if this holds for every $\mu\in\mathbb R$ and every $\sigma>0$.
• Shapes (Definition 2). $f:\mathbb R\to\mathbb R$ is convex-concave if for some $x_0$ it is convex on $(-\infty,x_0)$ and concave on $(x_0,\infty)$; concave-convex if $-f$ is convex-concave; S-shaped if increasing and convex-concave; inverse S-shaped if $-f$ is S-shaped. So an inverse S-shaped $f$ is decreasing, concave on $(-\infty,x_0)$ and convex on $(x_0,\infty)$.
• Lemma 1's quadratic. For $a<b$ and slopes $q_a,q_b$, set

and $q(y)=Ay^2+By+C$ (lemma1Quad).

• The function $g$. For $\mu\in\mathbb R$, $\sigma>0$ and $y<\mu$ let $z=\mu+\sigma^2/(\mu-y)$ (partnerPoint) and $g(y)=\frac{u(z)-u(y)}{z-y}-\frac{u'(y)+u'(z)}{2}$ (prop5Gap).

Formalization targets

Goal: Proposition 5 (p. 102)

If $u$ is differentiable, $u'$ is inverse S-shaped, and the limits $\lim_{y\to-\infty}u'(y)$ and $\lim_{y\to+\infty}u'(y)$ exist and are finite, then

Milestones

1. Proof of Lemma 1, first sentence. If $a<b$ and $\frac{u(b)-u(a)}{b-a}=\frac{q_a+q_b}{2}$, then $q(a)=u(a)$ and $q(b)=u(b)$.
2. Tangency (p. 110). $q'(a)=q_a$ and $q'(b)=q_b$.
3. Lemma 1. $u$ has two-point support if and only if for all $\mu$ and $\sigma>0$ there are $a<b$ and $q_a,q_b$ with

4. Limits of $g$ (p. 110). Under the goal's hypotheses, with $\ell_\pm=\lim_{y\to\pm\infty}u'(y)$,

5. A zero of $g$ (p. 110). There is $a<\mu$ with $g(a)=0$; with $b=\mu+\sigma^2/(\mu-a)$ one has $a<b$, $(b-\mu)(\mu-a)=\sigma^2$ and $\frac{u(b)-u(a)}{b-a}=\frac{u'(a)+u'(b)}{2}$.

Significance

The result. Through the paper's Proposition 4, two-point support turns the worst-case expected utility over all laws with mean $\mu$ and variance $\sigma^2$ into a minimization over a single parameter $p\in(0,1)$ of $pu(\mu+\sqrt{(1-p)/p}\,\sigma)+(1-p)u(\mu-\sqrt{p/(1-p)}\,\sigma)$. Combined with the projection property of the paper's Section 2, this gives tractable robust counterparts of multivariate stochastic programs whose objective depends on a linear combination $x'R$ of random returns. Proposition 5 is the paper's sufficient condition that places a concrete class of utilities in this regime; it is also closed under adding any quadratic.

Formalizing it. The result is proved on paper; no machine-checked version is known. The formalization produces a checked characterization of two-point support (Lemma 1), a reusable encoding of convex-concave and S-shaped functions, and a proof of Proposition 5. The printed final step of the paper's proof is incomplete (see Difficulty), so a complete formal proof requires an argument the paper does not spell out.

Difficulty

Conditions (a) and (b) of Lemma 1 come from a sign change of $g$ on $(-\infty,\mu)$: the two limits in milestone 4 need a l'Hôpital-type argument and the continuity of a monotone derivative. The central difficulty is condition (c): showing that the quadratic built from a pair $(a,b)$ lies below $u$ on the whole line. The obvious argument takes any zero $a$ of $g$ and counts the intersections of the linear $q'$ with the inverse S-shaped $u'$. This fails when $u'$ is affine on an interval: a zero of $g$ can then produce a quadratic that coincides with $u$ on $[a,b]$ but crosses above $u$ just left of $a$. A proof must therefore choose the zero of $g$, or the pair $(a,b)$, with care, and the curvature hypotheses are not strict.

Formalization scope

• Functions are ℝ → ℝ; $u'$ is deriv u, and the goal assumes Differentiable ℝ u. Finite limits are Tendsto (deriv u) atBot (𝓝 l) and Tendsto (deriv u) atTop (𝓝 l) for some real l; the one-sided limit at $\mu$ is along 𝓝[<] μ.
• "Increasing" in Definition 2 is strict (StrictMono); the paper writes "nondecreasing" for the weak notion. Convexity and concavity are ConvexOn/ConcaveOn on the open half-lines Set.Iio x₀, Set.Ioi x₀, as printed.
• A two-point law is encoded by its mass $p\in(0,1)$ on $a$, with $a<b$; this is equivalent to a probability measure on $\mathbb R$ with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$.
• "Intersects it at two points $a,b$" is read as $q(a)=u(a)$ and $q(b)=u(b)$ for some $a<b$ (at least two contact points). This is the reading under which Lemma 1 is an equivalence.
• The two-point support property quantifies over $\sigma>0$: no two-point law has variance $0$, so including $\sigma=0$ would make the property false for every $u$.
• The two-point support property is defined from Definition 1 (supporting quadratic plus feasible law), not from Lemma 1's conditions, so Lemma 1 is not a tautology. Every division by $b-a$, $z-y$ or $\mu-y$ occurs under $a<b$ or $y<\mu$.

Useful infrastructure: l'Hôpital's rule at infinity (Analysis/Calculus/LHopital), Darboux's theorem for derivatives, the intermediate value theorem, and one-sided limits of monotone functions. The shape definitions of Definition 2 are reusable for S-shaped value functions elsewhere (prospect theory, sigmoidal utilities). Proofs of the milestones, of the goal, and alternative arguments for condition (c) are all welcome. Related platform work: Wasserstein Distributionally Robust Optimization II.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30:277–298, 1991 (cited in Popescu 2007, reference list)

Motivation

Online convex optimization is a repeated game between a learner and an adversary. In each round $t=1,\dots,T$ the learner commits to a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$; only then is a convex cost function $f_t$ revealed, and the learner pays $f_t(x_t)$. The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.

Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order $1/\sqrt t$ has regret $O(GD\sqrt T)$ for any convex costs with gradients bounded by $G$ on a set of diameter $D$, and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes $1/(Ht)$ has regret only logarithmic in $T$ once every cost function is $H$-strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.

Setting

Fix $n\in\mathbb N$ and a nonempty, closed, bounded, convex set $\mathcal P\subseteq\mathbb R^n$, with the Euclidean norm $\|\cdot\|_2$ (§2.1, p. 171).

• Cost functions. A sequence $f_1,f_2,\dots:\mathbb R^n\to\mathbb R$. Write $\nabla f_t(x)$ for the gradient and $\nabla^2 f_t(x)$ for the Hessian.
• Gradient bound. A number $G$ with $\|\nabla f_t(x)\|_2\le G$ for all $x\in\mathcal P$ and all rounds $t$ (p. 172).
• $H$-strong convexity (p. 172). For $H>0$, $f$ is $H$-strongly convex on $\mathcal P$ when it is twice differentiable and $\nabla^2 f(x)\succeq H I_n$ for every $x\in\mathcal P$, i.e. $v^\top\nabla^2 f(x)v\ge H\|v\|_2^2$ for all $v$.
• Euclidean projection. $\Pi_{\mathcal P}(y)$ is the point of $\mathcal P$ nearest to $y$, $\Pi_{\mathcal P}(y)=\arg\min_{x\in\mathcal P}\|x-y\|_2$ (IsProj P y z).
• Online Gradient Descent (Fig. 1, p. 174), with step sizes $\eta_1,\eta_2,\dots$: $x_1\in\mathcal P$ is arbitrary, and in iteration $t>1$

(IsOGDRun P η f x).

• Regret (p. 171): $\mathrm{Regret}_T=\sum_{t=1}^T f_t(x_t)-\min_{x\in\mathcal P}\sum_{t=1}^T f_t(x)$, and $\mathrm{Regret}_T(\mathrm{OGD})$ is its supremum over all cost sequences.

Formalization targets

Goal: Theorem 1 (p. 175)

For $H>0$, cost functions that are $H$-strongly convex on $\mathcal P$ with gradients bounded by $G$ on $\mathcal P$, and any run of Online Gradient Descent whose step after round $t$ is $\eta_{t+1}=1/(Ht)$, for every $T\ge1$ and every $u\in\mathcal P$:

This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at $T=1$ the bound reads $G^2/(2H)$.

Milestones

1. Eq. (1), the strong-convexity inequality: for $x,y\in\mathcal P$, $2(f(x)-f(y))\le 2\nabla f(x)^\top(x-y)-H\|y-x\|_2^2$.
2. Lemma 8 with $A=I_n$: for a convex $\mathcal P$, $z=\Pi_{\mathcal P}(y)$ and $a\in\mathcal P$, $\|y-a\|_2^2\ge\|z-a\|_2^2$. This is already on the platform, proved, as UnderstandingML.projection_lemma, and is reused as a reference item.
3. Eq. (2), the one-step inequality: for $z=\Pi_{\mathcal P}(x-\eta g)$, $\eta>0$, $\|g\|_2\le G$ and $u\in\mathcal P$, $2g^\top(x-u)\le(\|x-u\|_2^2-\|z-u\|_2^2)/\eta+\eta G^2$.

The last step of the argument is the harmonic-sum bound $\sum_{t=1}^T 1/t\le 1+\log T$, which Mathlib already provides (harmonic_le_one_add_log).

Significance

The result. Theorem 1 separates two regimes of online convex optimization: $\Theta(\sqrt T)$ regret for general convex costs and $O(\log T)$ for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the $O(\log T/T)$ rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain $O(n\log T)$ regret.

Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.

Difficulty

The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round $t$ must be $1/(Ht)$. Reading Fig. 1 literally with $\eta_t=1/(Ht)$ makes the step after round $t$ equal to $1/(H(t+1))$, and the sum then leaves an uncancelled term $\frac H2\|x_1-x^*\|_2^2$ that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of $\mathcal P$; convexity of $\mathcal P$ keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.

Formalization scope

Points are EuclideanSpace ℝ (Fin n), so $\|\cdot\|$ is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of $\mathbb R^n$, as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to $(v,v)$. Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of $\mathcal P$), which is unique for nonempty closed convex $\mathcal P$.

Choices and corrections relative to the printed text:

• Step-size index. Theorem 1 prints "step sizes $\eta_t=\frac1{Ht}$", while its proof sets $\eta_{t+1}=1/(Ht)$ for the step after round $t$. The goal uses the proof's indexing, as a hypothesis η (t + 1) = 1 / (H * t) for $t\ge1$ on the step sizes of Fig. 1.
• Eq. (2). The paper prints "$5\nabla_t^\top(x_t-x^*)$"; the $5$ is a typo for $2$, and the milestone states $2$. The verbatim milestone text keeps the printed $5$.
• Regret. Regret is stated against every comparator $u\in\mathcal P$; the minimum over the compact set $\mathcal P$ is attained, so this is the paper's statement. The expectation in the paper's regret is vacuous for this deterministic algorithm, and the supremum over cost sequences is the universal quantifier over $f$.
• Hypotheses. Strong convexity and the gradient bound are required for the rounds $1,\dots,T$ only. Convexity of each $f_t$, a standing assumption of §2.2, follows from $H$-strong convexity on the convex set $\mathcal P$ and is not added. No diameter bound enters Theorem 1.

A regret bound written with a real ⨅/sInf over $\mathcal P$, or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in $\mathcal P$ and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, $f_t(x)=\frac H2\|x\|_2^2$ with $G=H$ meets all of them.

Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite $A$ (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022 (Theorem 3.3). https://arxiv.org/abs/1909.05207
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014 (Lemma 14.9, the projection lemma). https://doi.org/10.1017/CBO9781107298019

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit $\gamma \downarrow 0$; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are $n$ jobs with service times $s_i > 0$ and weights $c_i$, and $m$ identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time $C_i$ of a job is the total service time of the jobs on its machine up to and including it; the flow time is $\sum_i C_i$ and the weighted flow time $\sum_i c_i C_i$. The load of a machine is the total service time assigned to it, and $\delta_j$ is its excess over the average $S/m$. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of $n$ boxes, in box $i$ with probability $p_i$. A search of box $i$ costs $c_i$ and finds the object with probability $q_i$ if it is there. A search policy is a sequence of boxes; after $N_i$ unsuccessful searches of box $i$ the posterior probability that the object is there is proportional to $p_i(1-q_i)^{N_i}$, and the search index of the box is $p'_i q_i/c_i$, the current probability of finding the object per unit cost. The expected cost of a policy is $\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]$.

Two discount factors. Bandit process $A$ (state space $S_A$, kernel $P_A$, reward $r_A$) discounts at rate $a$ and $B$ at rate $b$; a reward obtained at time $t$ is worth $a^t$ or $b^t$ times its face value according to which process produced it. The cross indices are $\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]$ and $\nu_{BA}(y)$ with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as $\mathbb{E}\int_0^\tau b^t\,dt$ and compares $\nu_{AB}(x)$ with $\nu_{BA}(y)$ at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union $S_A \oplus S_B$.

Formalization targets

Goal: Theorem 3.6

For prior probabilities $p_i \ge 0$ summing to one, detection probabilities $0 < q_i \le 1$ and costs $c_i > 0$, a search policy is optimal if and only if at every step it searches a box of maximal current index $p'_i q_i / c_i$:

Milestones

Theorem 3.3, as the identity $\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)$ when $c_i = \kappa s_i$; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time $t$, $A$ when $a^t \nu_{AB}(x) > b^t \nu_{BA}(y)$ and $B$ when $a^t \nu_{AB}(x) < b^t \nu_{BA}(y)$ attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on $m$ machines and that the optimal schedules are exactly those placing the $r$-th block of $m$ longest jobs at level $r$ from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time $t$ weighs the indices by $a^t$ and $b^t$, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying $0.18$ ($a = 0.9$) and $1$ ($b = 0.5$) are best played $B, B, B$ and then $A$ forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as $\sum_i \ell_i s_i$ with $\ell_i$ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in $[0, \infty]$ of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, $p_i(1-q_i)^{N_i} q_i/c_i$, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an $A$-state by $P_A$ and a $B$-state by $P_B$; the payoff is the round-by-round series $\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])$, absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: $m \ge 1$, service times positive; $p_i \ge 0$, $\sum p_i = 1$, $0 < q_i \le 1$, $c_i > 0$; countable state spaces, bounded rewards, $a, b \in (0,1)$.

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by $a^t$, $b^t$. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
• D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
• J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
• K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
• P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x

Motivation

The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.

Setting

Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (BertsekasRiccatiMap)

$(A,B)$ is controllable if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (BertsekasControllablePair); $(A,C)$ is observable if $(A^\top, C^\top)$ is controllable (BertsekasObservablePair). Separately, $g : \mathbb{R} \to \mathbb{R}$ is $K$-convex (BertsekasKConvex, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.

Target

with $L = -(B^\top P B + R)^{-1} B^\top P A$ — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.

Significance

The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.

Difficulty

The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.

Formalization scope

Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5 (1960), 102–119.
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford Univ. Press, 1960.

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

Why airlines protect seats

An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.

Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.

Setting

A single flight leg has capacity $C \in \mathbb N$. Class 1 has fare $f_1$, class 2 has fare $f_2$, with $0 \le f_2 \le f_1$. The numbers of requests for the two classes are random variables $r_1, r_2$ with values in $\mathbb N$, defined on a probability space $(\Omega, \mu)$ and independent. There are no cancellations, no no-shows, and a refused request is lost.

The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level $S \in \{0, \dots, C\}$ is the number of seats reserved for class 1; it sets the class-2 booking limit $BL_2 = C - S$. All class-2 requests arrive before any class-1 request. Class 2 therefore books $\min(r_2, C - S)$ seats and class 1 books $\min(r_1, C - \min(r_2, C-S))$, and the realised revenue is

The expected revenue is $\bar R(S) = \mathbb E[R_S]$.

The tail probability of class 1 is $\bar P_1(S) = P[r_1 \ge S]$, the probability of receiving $S$ or more class-1 requests, and the expected marginal seat revenue of the $S$-th class-1 seat is

For a single class with $S$ seats the expected revenue is $f_1\,\mathbb E[\min(r_1, S)]$, and $\mathrm{EMSR}_1(S)$ is its increment from $S-1$ to $S$ seats. The EMSR protection level $S_2^1$ is the largest integer $S \in \{0, \dots, C\}$ with

In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.

Formalization targets

Goal: Eqs. (5.15)–(5.16), optimality of the EMSR protection level

The goal fixes no distribution: it holds for every pair of independent $\mathbb N$-valued demands, and $S_2^1$ depends only on $f_2/f_1$ and the law of $r_1$.

Milestones

1. Eq. (5.11). $f_1\mathbb E[\min(r_1,S)] - f_1\mathbb E[\min(r_1,S-1)] = f_1 P[r_1 \ge S]$ for $S \ge 1$.
2. Eqs. (6.1)–(6.2). $\bar P_1$ and, for $f_1 \ge 0$, $\mathrm{EMSR}_1$ are non-increasing in $S$.
3. Eq. (4.8), Littlewood's rule, already on the platform as RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).
4. Sect. 5.2, p. 112. $\bar R(S) \le \bar R(S_2^1)$ for $S_2^1 \le S \le C$: a smaller booking limit for class 2 cannot raise expected revenue.
5. Sect. 5.2, p. 114. With the same class-2 limit $C - S$, the expected nested revenue is at least the expected revenue of two distinct inventories with $S$ and $C - S$ seats, strictly if $f_1 > 0$ and $P[r_2 < C - S,\ r_1 > S] > 0$.

Significance

The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.

The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of $f_1 P[r_1 \ge S]$ against $f_2$ and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.

Difficulty

The expected revenue couples the two demands through the capacity left by class 2, so $\bar R$ is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment $\bar R(S) - \bar R(S-1)$: it is not $\mathrm{EMSR}_1(S) - f_2$, as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of $r_1$ and $r_2$ is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with $P[r_1 > S]$ in place of $P[r_1 \ge S]$ the rule is off by one seat and the claim fails.

Formalization scope

Conventions the Lean statements commit to:

• Demands are $\mathbb N$-valued measurable random variables r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.
• $\bar P_1(S) = P[r_1 \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11), not $P[r_1 > S]$ as in Eq. (5.2).
• The EMSR protection level is the largest $S \in \{0,\dots,C\}$ with $f_1 P[r_1 \ge S] \ge f_2$ (Eq. (5.15)); Eq. (5.16)'s equality is the continuous idealisation and is not stated.
• Booking order: all class-2 requests precede all class-1 requests (pp. 108, 112). This order is built into the revenue formula, not assumed separately.
• Fares satisfy $0 \le f_2 \le f_1$; the thesis has $f_1 > f_2$, and the statements also cover equality.
• Expectations are Bochner integrals of bounded revenues, probabilities are μ.real; seat counts use truncated subtraction only where $S \le C$.

A trivializing formalization is ruled out: $S_2^1$ is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.

The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity $\mathbb E[\min(r,S)] - \mathbb E[\min(r,S-1)] = P[r \ge S]$ and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41, 1993. https://doi.org/10.1287/opre.41.1.127
• R. E. Curry, Optimal airline seat allocation with fare classes nested by origins and destinations, Transportation Science 24, 1990. https://doi.org/10.1287/trsc.24.3.193
• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).

The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.

Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).

Setting

A linear program in standard form has $m$ constraints and $n$ decision variables:

A solution $x$ is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.

The slack variables $w_i = b_i - \sum_j a_{ij}x_j$ are appended to the list of variables as $x_{n+i} = w_i$, so that the constraints become the linear system $[A\ I]\,x = b$ with $x \ge 0$ in $\mathbb{R}^{n+m}$. A dictionary is given by a set $\mathcal B$ of $m$ basic indices whose columns of $[A\ I]$ are linearly independent; the remaining indices $\mathcal N$ are nonbasic. Solving for the basic variables gives

The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if $\bar b_i \ge 0$ for every $i\in\mathcal B$, and degenerate if $\bar b_i = 0$ for some $i\in\mathcal B$.

The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable $x_k$ is chosen among the nonbasic variables with $\bar c_k > 0$, and a leaving variable $x_l$ among the basic variables with $\bar a_{lk} > 0$ that minimize the ratio $\bar b_l/\bar a_{lk}$; then $x_k$ becomes basic and $x_l$ nonbasic. The method stops when no $\bar c_j$ is positive (the dictionary is optimal) or when the entering column has no positive $\bar a_{ik}$ (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols $0<\epsilon_m\ll\dots\ll\epsilon_1\ll$ all data and chooses the leaving variable by the perturbed ratio test.

Formalization targets

Goal: Theorem 3.3 (termination under Bland's rule, p. 31)

From every feasible dictionary $D_0$, there is no infinite sequence of pivots

in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary $D_T$ at which the method stops, optimal or exhibiting unboundedness.

Milestones

• Theorem 3.1 (p. 27): if the simplex method fails to terminate, it must cycle, i.e. an infinite run visits some dictionary twice.
• Theorem 3.2 (p. 30): the simplex method always terminates when the leaving variable is selected by the lexicographic rule.
• Theorem 3.4 (p. 33), the fundamental theorem: (1) with no optimal solution the problem is infeasible or unbounded; (2) if a feasible solution exists, a basic feasible solution exists; (3) if an optimal solution exists, a basic optimal solution exists.

Significance

The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.

Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form $Ax=b$, $x\ge 0$, full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over $[A\ I]$. This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.

Difficulty

The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length $\bar b_l/\bar a_{lk}$ is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.

For Theorem 3.2, the symbols $\epsilon_i$ cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.

Formalization scope

Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The $n+m$ variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order $x_1,\dots,x_n,x_{n+1}=w_1,\dots,x_{n+m}=w_m$ that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has $m$ elements and a proof that its columns of $[A\ I]$ are linearly independent; the coefficients $\bar b,\bar a,\bar c,\bar\zeta$ are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.

Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors $(\bar b_i, r_{i1},\dots,r_{im})/\bar a_{ik}$ of the perturbed ratios; the symbol $\epsilon_p$ is attached in the starting dictionary to its $p$-th basic variable in increasing index order, which for the initial dictionary is the $p$-th constraint. Unboundedness in Theorem 3.4 is "for every $M$ a feasible solution with objective $>M$", as defined on p. 7. The statements carry no explicit constants.

A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.

A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 3. https://doi.org/10.1007/978-1-4614-7630-6
• R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
• G. B. Dantzig, A. Orden, P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2):183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
• E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020406
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.4 (lexicographic rule and Bland's rule in tableau form).

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC($\alpha$), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$. How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; nonnegative finite costs $C(i,a)$; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$. A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$. A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$. Fix a discount factor $\alpha\in(0,1)$. The discounted cost of $\theta$ and the discounted value function are

both in $[0,\infty]$, the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$, probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$. The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation