Operations Research

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$. Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$, which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$, a finite nonempty action set $A$, transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ is, for each state $s$, a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$.

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$. The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$. The discounted future state distribution from $\mu$ is

$$d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu),\qquad s_0\sim\mu,$$

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$.

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$: the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$. For nonnegative $f,g$ on $S$, $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

$$\eta_{\tilde\mu}(\pi^*)-\eta_{\tilde\mu}(\pi)\le\frac{\varepsilon}{1-\gamma}\left\|\frac{d_{\pi^*,\tilde\mu}}{d_{\pi,\mu}}\right\|_\infty\le\frac{\varepsilon}{(1-\gamma)^2}\left\|\frac{d_{\pi^*,\tilde\mu}}{\mu}\right\|_\infty.$$

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$; taking $\tilde\mu=D$, the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$, $\pi$ and any starting distribution $\mu$,

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi)=\frac{1}{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}\big[A_\pi(s,a)\big].$$

The states are weighted by the future state distribution of the new policy $\tilde\pi$, the advantage is that of the old policy $\pi$.

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$, which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$) and P s a s' (the paper's $P(s';s,a)$), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: "$X\le K\|f/g\|_\infty$" is "$X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$; no full-support assumption is made on $\mu$ or $\tilde\mu$. The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$, which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$, and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
• J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

• 1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$, $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
• 1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$. It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$, $s^2_i + B_i \le s^3_i$. The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$.

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$. Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$, Johnson defines

$$K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,$$

the sums running over the items in the first $u$ (resp. $v$) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

$$\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}$$

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$, then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

$$\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .$$

Milestones

1. Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
2. Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$, so that

$$\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),$$

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$, so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$. 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$, and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$.

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$, and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$, so the empty instance has makespan $0$. An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$, $H_{v+1}$. Statements with maxima over positions assume $n \ge 1$.

Hypotheses made explicit or corrected:

• $\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$, as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
• Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
• Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
• Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
• The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$, would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Why algorithmic robustness

A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.

Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.

Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.

Setting

Throughout, $\mathcal Z$ is a measurable space of samples and $\mathcal H$ is an arbitrary set of hypotheses. A loss $l : \mathcal H \times \mathcal Z \to \mathbb R$ satisfies $0 \le l(h,z) \le M$ for a constant $M$. A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$, and a learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$, written $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

For a probability measure $\mu$ on $\mathcal Z$, the expected error and the training error of the learned hypothesis are

$$\mathcal L(\mathcal A_{\mathbf s}) = \mathbb E_{z\sim\mu}\, l(\mathcal A_{\mathbf s}, z), \qquad l_{\mathrm{emp}}(\mathcal A_{\mathbf s}) = \frac1n \sum_{i=1}^n l(\mathcal A_{\mathbf s}, s_i).$$

Definition 2 (p. 396). For $K \in \mathbb N$ and $\epsilon(\cdot) : \mathcal Z^n \to \mathbb R$, the algorithm $\mathcal A$ is $(K, \epsilon(\cdot))$-robust if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$ such that for every $\mathbf s \in \mathcal Z^n$,

$$\forall s \in \mathbf s,\ \forall z \in \mathcal Z,\ \forall i:\quad s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).$$

The partition is chosen once, before the training set. Only the tolerance $\epsilon(\mathbf s)$ may depend on $\mathbf s$.

For a partition $C_1,\dots,C_K$, the cell count $|N_i|$ is the number of training points in $C_i$. The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.

Formalization targets

Goal: Theorem 1 (p. 396)

Let $\mathcal A$ be $(K,\epsilon(\cdot))$-robust and let $\mathbf s$ consist of $n \ge 1$ i.i.d. draws from $\mu$. Then for every $\delta > 0$, with probability at least $1-\delta$,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

The constants are the paper's and are kept as printed. $K$, $\epsilon(\cdot)$, $M$, $n$, $\delta$, $\mu$ and the algorithm are all universally quantified.

Milestones (proof of Theorem 1, pp. 396–397)

1. Bretagnolle–Huber–Carol inequality for the multinomial vector of cell counts. For every $\lambda \ge 0$,

$$\Pr\Big\{\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \ge \lambda\Big\} \le 2^K \exp\Big(\frac{-n\lambda^2}{2}\Big).$$

2. Eq. (3). With probability at least $1-\delta$,

$$\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \le \sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

3. Eq. (4). For a partition witnessing robustness and for every training set $\mathbf s$, deterministically,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big|.$$

Significance

Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:

• Corollary 1: an adaptive number of cells;
• Corollaries 2 and 3: covering-number instances;
• Theorem 4: a pseudo-robust version;
• the Markovian case.

Its complexity term depends only on the number of cells $K$, not on any capacity measure of $\mathcal H$. This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, $K$ is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.

Theorem 1 is a published result with a short proof. What a formalization adds:

• a machine-checked statement of the robustness notion, pinning down which quantifier comes first;
• a formal proof of the multinomial concentration step, which the paper takes from van der Vaart and Wellner rather than proving;
• a reusable interface for the covering-number examples.

A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.

Difficulty

The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of $\mu$-measure zero, where the conditional expectation in the paper's chain is undefined.

The main obstacle is the probabilistic step. The quantity $\sum_i ||N_i|/n - \mu(C_i)|$ is an $\ell_1$ deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the $K$ coordinates gives a bound whose deviation level grows linearly in $K$. That is not $2^K e^{-n\lambda^2/2}$, and it does not give the constant $\sqrt{2K\ln 2}$ of Theorem 1. The difficulty is to obtain the exact exponential rate $2^K e^{-n\lambda^2/2}$ for the $\ell_1$ deviation as a whole, with no loss in the constant.

Formalization scope

Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and $\mu(C_i)$ enters as a real number.

"With probability at least $1-\delta$" is encoded as an upper bound $\delta$ on the outer measure, under $\mu^n$, of the set of training sets where the inequality fails. This needs no measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

The paper ignores measurability. The formalization restores it: every $l(h,\cdot)$ is measurable and every cell is a measurable set. Together with $0 \le l \le M$ this makes the expected error a genuine expectation.

The theorems assume $n \ge 1$. The Bretagnolle–Huber–Carol step assumes $\lambda \ge 0$, because the printed inequality is false for $\lambda < 0$. No upper bound on $\delta$ is imposed: for $\delta > 2^K$ the radicand is negative, the square root evaluates to $0$, and the statements remain true.

Two trivializing readings of Definition 2 are ruled out:

• The partition may not depend on the training set. In IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a $\{0,1\}$-valued loss would be $(2,0)$-robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.
• The tolerance may not depend on the test point, and the condition is required for every $z \in \mathcal Z$, not only for $z$ equal to a training point.

Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• H. Xu, C. Caramanis and S. Mannor, Robustness and Regularization of Support Vector Machines, Journal of Machine Learning Research 10 (2009) 1485–1510. https://www.jmlr.org/papers/v10/xu09b.html
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A two-stage stochastic linear program with fixed recourse chooses a first-stage decision $x$ before a random vector $\xi$ is observed, and then pays for a cheapest corrective action $y$ once $\xi$ is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.

Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of $x$ (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.

Setting

The data are a random element $\xi=(c,q,p,T)$ with $c\in\mathbb R^n$, $q\in\mathbb R^{\bar n}$, $p\in\mathbb R^{\bar m}$ and $T$ an $\bar m\times n$ matrix, distributed according to a probability measure $\mu$. The recourse matrix $W$ ($\bar m\times\bar n$), the first-stage matrix $A$ ($m\times n$) and $b\in\mathbb R^m$ are fixed. The recourse function is

$$Q(x,\xi)=\min\{q(\xi)y \mid Wy=p(\xi)-T(\xi)x,\ y\ge0\},$$

equal to $+\infty$ if the second-stage program is infeasible and $-\infty$ if it is unbounded.

The weak covariance condition (Definition 2.2) requires $c_j$, $q_jp_i$ and $q_jt_{ik}$ to be integrable for all indices; it does not require $q$, $p$ or $T$ themselves to be integrable. The paper also assumes throughout that $W$ has full row rank (p. 312).

Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and $(+\infty)+(-\infty)=+\infty$. The expected recourse is $\mathcal Q(x)=E_\xi\{Q(x,\xi)\}$ and the objective is

$$Z(x)=\bar c\,x+\mathcal Q(x),\qquad \bar c=E_\xi\{c(\xi)\}.$$

The induced constraints are $K_2=\bigcap_{\zeta\in\tilde\Xi_{p,T}}\{x : p-Tx\in\operatorname{pos}W\}$, where $\operatorname{pos}W=\{Wy:y\ge0\}$ and $\tilde\Xi_{p,T}$ is the support of the distribution of $(p,T)$. The fixed constraints are $K_1=\{x: Ax=b,\ x\ge0\}$, and $K=K_1\cap K_2$. The deterministic equivalent program (8.2) is to minimize $Z$ over $K$.

A convex program of the form $\min\{f(x) : Ax=b,\ x\ge0,\ x\in D\}$ with finite value $v$ is stable (Definition 8.1(iv)) if there is $\pi\in\mathbb R^m$ with $v\le f(x)+\pi(b-Ax)$ for all $x\in D$, $x\ge0$. Equivalently, the dual obtained by perturbing $b$ is solvable and has no duality gap.

Formalization targets

Goal: Theorem 8.11 (p. 337)

If the weak covariance condition holds, $W$ has full row rank, $K_2$ is a polyhedron and the program is finite, $v=\inf_K Z\in\mathbb R$, then

$$\exists\,\pi\in\mathbb R^m:\quad v\le Z(x)+\pi\,(b-Ax)\quad\text{for all }x\in K_2,\ x\ge0 .$$

Milestones

1. Corollary 7.3 (p. 328). The value $t\mapsto\min\{cx\mid Ax=t,\ x\ge0\}$ is a finite maximum of affine functions on $\operatorname{pos}A$, or $-\infty$ on all of $\operatorname{pos}A$.
2. Proposition 7.5 (p. 329). $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ for each $\xi$ in the support, concave polyhedral in $q$, and convex polyhedral in $(p,T)$.
3. Theorem 7.6 (p. 329). $Z$ is convex on $K$, and it is either finite on $K$ or identically $-\infty$ on $K$.
4. Theorem 7.7 (pp. 329–330). If $Z>-\infty$ on $K$, then $|Z(x)-Z(x^0)|\le\bar B\|x-x^0\|$ on $K$ (Euclidean norm).
5. Lemma 8.9 (p. 337). A finite program $\min\{f(x): Ax=b,\ x\ge0\}$ whose objective is convex and Lipschitz on a polyhedral domain is stable.

Significance

Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function $\phi(u)=\inf\{Z(x) : Ax=b-u,\ x\in K_2\cap\mathbb R^n_+\}$ at $u=0$, and hence a bounded rate of change of the optimal value under perturbations of $b$. The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically $-\infty$ on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.

The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on $K_2$ for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.

Difficulty

The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of $Q(\cdot,\xi)$. It fails unless that constant is integrable, and the weak covariance condition, not integrability of $\xi$, is what has to deliver this, uniformly over the finitely many second-stage bases.

For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of $Z$ has curved boundary, the perturbation function can have infinite slope at $0$; the polyhedral hypothesis on $K_2$ is what excludes this.

Formalization scope

• Types. Vectors are Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper ($c$, $q$, $\pi$) enter through dotProduct. The law $\mu$ is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). $Q$ is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.
• The integral. $\mathcal Q$ is written as lintegral of the positive part minus lintegral of the negative part, with $+\infty$ whenever the positive part is $+\infty$. This is the paper's $(+\infty)+(-\infty)=+\infty$; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be $0$ for non-integrable integrands and make every expected-cost statement trivial, and it is not used. $\bar c$ is a Bochner integral, legitimate because Definition 2.2 makes each $c_j$ integrable.
• Readings of informal words.
  • "Has first moments" is Integrable.
  • "Convex polyhedron" means finitely many weak linear inequalities; $\emptyset$ and $\mathbb R^n$ are included.
  • "Finite convex (concave) polyhedral function on $S$" means equal on $S$ to the maximum (minimum) of finitely many affine functions. The $x$ and $(p,T)$ parts of Proposition 7.5 are stated as a dichotomy with the identically $-\infty$ case; the $q$ part is stated, as Corollary 7.4 gives it, as finite concave polyhedral on $\operatorname{pos}(W^T,-W^T,I)$ when the recourse problem is feasible.
  • "Convex" for the extended-real $Z$ (Theorem 7.6) is ConvexOn of toReal on the finite branch.
  • "Bounded on $K$" (Theorem 7.7) is read as $Z>-\infty$ on $K$, the proof's own reading. Finiteness on $K$ is part of the conclusion.
  • "Convex and Lipschitz on a polyhedron" (Lemma 8.9) means the objective's domain is the polyhedron.
  • "The program is finite" means the infimum over $K$ is a real number.
  • "Stable" is the Kuhn–Tucker form above: a multiplier compared against the primal value, not merely a solvable dual. The latter would allow a duality gap.
• Standing assumptions. Full row rank of $W$ appears in Theorems 7.7 and 8.11, where the proof uses square nonsingular submatrices of $W$. It is omitted from Theorem 7.6 and Corollary 7.3 (Theorem 7.2's rank assumption), where it is not needed; this makes those statements stronger.
• Corrections to the page. Theorem 8.11 is printed with "$K$ is polyhedral", $K=K_1\cap K_2$, and read literally it is false. Take $T(\xi)$ uniform on the unit circle, $p\equiv1$, $W=(1)$, $q\equiv0$, $c\equiv(-1,0)$ and $K_1=\{x_2=1,\ x\ge0\}$. Then $K_2$ is the unit disk and $K=\{(0,1)\}$ is polyhedral with finite value $0$, but no multiplier exists. The goal therefore assumes "$K_2$ is polyhedral", as the sentence before Lemma 8.9 and the proof require. In the dual (8.3) the page writes $c$ for $\bar c$.
• Ruled out. A statement of stability as "the dual supremum is attained" without equality to the primal value is not the goal, and neither is a hypothesis making $K$ empty or $Z$ identically $-\infty$: the finiteness hypothesis excludes both.
• Infrastructure. The needed pieces are Minkowski–Weyl for polyhedra (PointedCone.FG/DualFG in Mathlib), LP duality with $\pm\infty$ values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.

Selected references

• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• R. M. Van Slyke and R. J.-B. Wets, A duality theory for abstract mathematical programs with applications to optimal control theory, J. Math. Anal. Appl. 22(3):679–706, 1968 (cited by Wets for Definition 8.1 and the dual (8.3)).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 3. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A two-stage stochastic program with recourse is a linear program in which a decision $x$ is taken before a random vector $\xi$ is observed, and a corrective (recourse) decision $y$ is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in $x$ alone, and the first question is which $x$ are admissible at all: the random second-stage constraints induce constraints on $x$ that are not written down anywhere in the data.

Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix $W$ is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix $T$ is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.

Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every $x$ feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random $W$. The 1974 survey collects these results in the form formalized here.

Setting

The data are a fixed real $\bar m \times \bar n$ matrix $W$ and a random vector $\xi = (c, q, p, T)$ with $c \in \mathbb{R}^n$, $q \in \mathbb{R}^{\bar n}$, $p \in \mathbb{R}^{\bar m}$ and $T$ an $\bar m \times n$ matrix. The law of $\xi$ is a probability measure $\mu$ on the product space, and its support $\tilde\Xi$ is the smallest closed set of measure one. The recourse function is

$$Q(x,\xi) = \min\{\, q(\xi)y \mid Wy = p(\xi) - T(\xi)x,\ y \ge 0 \,\},$$

equal to $+\infty$ when the program is infeasible and $-\infty$ when it is unbounded below. The expected recourse $\mathcal Q(x) = E_\xi\{Q(x,\xi)\}$ uses the paper's integral: the sum of the positive part $\int Q^+ d\mu \in [0,+\infty]$ and the negative part $-\int Q^- d\mu \in [-\infty,0]$, with $(+\infty) + (-\infty) = +\infty$.

The weak covariance condition (Definition 2.2) asks that $c_j$, $q_j p_i$ and $q_j t_{ik}$ be integrable for all $i, j, k$. Write $\operatorname{pos} W = \{Wy \mid y \ge 0\}$. The candidate feasibility sets for the induced constraints are

• $K_2^\mu$: the $x$ for which, with probability one, some $y \ge 0$ solves $Wy = p(\xi) - T(\xi)x$;
• $K_2^p$: the $x$ for which such a $y$ exists for every $\xi \in \tilde\Xi$;
• $K_2^s = \{x \mid \mathcal Q(x) < +\infty\}$;
• $K_2 = \bigcap_{\zeta \in \tilde\Xi_{p,T}} K_2(\zeta)$, where $\tilde\Xi_{p,T}$ is the support of the law of $(p,T)$ and $K_2(\zeta) = \{x \mid p - Tx \in \operatorname{pos} W\}$ for $\zeta = (p,T)$.

A convex polyhedron is a set $\{x \mid Gx \ge \alpha\}$ given by finitely many linear inequalities; $\emptyset$ and $\mathbb{R}^n$ are polyhedra.

Formalization targets

Goal: Theorem 4.10

If $T$ is fixed and $\xi$ satisfies the weak covariance condition, then

$$K_2 = \{x \in \mathbb{R}^n \mid Gx \ge \alpha\} \quad \text{for some finite system } G, \alpha,$$

so $K_2$ is a closed convex polyhedron. The number of inequalities is not fixed in advance, and $K_2$ may be empty.

Milestones

1. Theorem 4.1. Under weak covariance, $K_2^\mu = K_2^p = K_2^s$.
2. Corollary 4.5. Under weak covariance, $K_2 = K_2^p = K_2^\mu = K_2^s$.
3. Theorem 4.6. For every set $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$, $K_2 = \bigcap_{\zeta \in \Sigma} K_2(\zeta)$.
4. Theorem 4.7. $K_2$ is closed and convex; if the closed positive hull $\operatorname{pos}(\tilde\Xi_{p,T})$ is a convex polyhedral cone, $K_2$ is a convex polyhedron.

Significance

Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of $(p, T)$. This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when $p(\xi)$ has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.

The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).

Difficulty

Two steps resist the obvious approach. First, $K_2^p \subseteq K_2^s$ needs an integrable upper bound for the positive part of $Q(x,\cdot)$ on the whole support. $Q$ is only piecewise linear in $\xi$, can equal $-\infty$, and $q$, $p$, $T$ are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra $K_2(\zeta)$, and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of $p$ is the content of the goal, and the resulting system may be inconsistent, in which case $K_2 = \emptyset$.

Formalization scope

Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is $\mathbb{R}^n \times \mathbb{R}^{\bar n} \times \mathbb{R}^{\bar m} \times \mathbb{R}^{\bar m \times n}$ with its Borel structure, and $\mu$ is a probability measure on the whole space (the paper's sample space $\Xi$ only carries $\mu$). Readings fixed by the formalization:

• "has first moments" (Def. 2.2) is Integrable with respect to $\mu$.
• The integral is the paper's: two lower Lebesgue integrals, returning $+\infty$ whenever the positive part diverges. Mathlib's EReal subtraction ($\top - \top = \bot$) and the Bochner integral of toReal (zero for non-integrable functions) would both make $K_2^s$ wrong and are not used.
• "support" is Mathlib's Measure.support; $\tilde\Xi_{p,T}$ is the support of the pushforward under the (continuous, hence measurable) projection onto $(p,T)$.
• "$T$ is fixed" means $T(\xi) = T_0$ with probability one, a weaker hypothesis than pointwise constancy.
• "convex polyhedron" is the solution set of finitely many weak linear inequalities, the number of them existentially quantified; "convex polyhedral cone" is the conic hull of finitely many vectors; "closed positive hull" is the closure of the conic hull.
• Full row rank of $W$ is the paper's standing assumption (p. 312) and is carried as a hypothesis of Theorem 4.1, Corollary 4.5 and Theorem 4.10; it is inessential for them.
• Theorem 4.6 is stated as "for every $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$". The literal statement fails: a closed half-plane has no extreme points, so the "inverse of convex closure" would give $\Sigma = \emptyset$ and an intersection equal to $\mathbb{R}^n$.
• The set on p. 314 (iii) is printed $K_2^p$.

A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral $\mathcal Q$ would make $K_2^s = \mathbb{R}^n$. Neither is used.

A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of $\operatorname{pos} W$ (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.

Selected references

• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• R. M. Van Slyke and R. J.-B. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
• D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Ch. 3. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost $K$ per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an $(s, S)$ policy is optimal: order up to $S$ whenever the stock falls below $s$, and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair $(s, S)$ to use.

Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary $(s, S)$ policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an $(s, S)$ policy used throughout inventory theory textbooks.

Timeline:

• 1958: Arrow, Karlin and Scarf collect the early dynamic inventory models.
• 1960: Scarf proves optimality of $(s, S)$ policies in the finite-horizon model via $K$-convexity.
• 1963: Iglehart extends optimality to the infinite-horizon model.
• 1965: Veinott and Wagner derive the renewal closed form (10)–(11) and the bounds and search procedure built on it.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent random variables on $\{0, 1, 2, \dots\}$ with common distribution $\varphi$, $\varphi(k) = \Pr(\xi_t = k)$. Write $\varphi^i$ for the $i$-fold convolution of $\varphi$ ($\varphi^0$ is the point mass at $0$) and $\Phi^i(k) = \sum_{t=0}^{k}\varphi^i(t)$ for its distribution function, so $\Phi^0 \equiv 1$.

In period $t$ the stock before ordering is $X_t \in \mathbb Z$ and the stock after ordering is $Y_t \ge X_t$; then $X_{t+1} = Y_t - \xi_t$. With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period $t$ is $K\delta(Y_t - X_t) + G_\alpha(Y_t)$, where $K \ge 0$ is the set-up cost, $\delta(0) = 0$, $\delta(z) = 1$ for $z > 0$, and $G_\alpha : \mathbb Z \to \mathbb R$ is the one-period cost. Period $t$ is discounted by $\alpha^{t-1}$ with $0 \le \alpha < 1$.

A stationary $(s, S)$ policy, for integers $s \le S$, sets $Y_t = S$ if $X_t < s$ and $Y_t = X_t$ otherwise. Its total expected discounted cost from $X_1 = x$ is

$$f(x \mid s, S) = \sum_{t=1}^{\infty} \alpha^{t-1} E\bigl[K\delta(Y_t - X_t) + G_\alpha(Y_t)\bigr],$$

and its equivalent cost per period is $a_\alpha(x \mid s, S) = (1 - \alpha) f(x \mid s, S)$.

The renewal quantities are

$$m_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\varphi^i(k), \qquad M_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\Phi^i(k),$$

the latter being the discount renewal function,

$$L_\alpha(x, d) = G_\alpha(x) + \sum_{i=1}^{\infty}\sum_{k=0}^{d}\alpha^i G_\alpha(x - k)\varphi^i(k), \qquad r_\alpha(d) = \sum_{i=1}^{\infty}\alpha^i\bigl[\Phi^{i-1}(d) - \Phi^i(d)\bigr].$$

If $T(d)$ is the first period in which cumulative demand exceeds $d$, then $L_\alpha(x, d)$ is the expected discounted one-period cost over periods $1, \dots, T(d)$ from stock $x$ without ordering, and $r_\alpha(d) = E[\alpha^{T(d)}]$.

Formalization targets

Goal: Eq. (11)

With $D = S - s$,

$$a_\alpha(x \mid s, S) = \begin{cases} \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)} & x < s, \\[2ex] (1 - \alpha)L_\alpha(x, x - s) + \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)}\, r_\alpha(x - s) & x \ge s. \end{cases}$$

Milestones

1. Appendix §1: $M_\alpha(k) < \infty$ for $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$.
2. Eq. (8): $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)m_\alpha(j)$.
3. Eq. (9): $r_\alpha(d) = \alpha - (1 - \alpha)M_\alpha(d)$.
4. The renewal equation $f(S) = L_\alpha(S, D) + Kr_\alpha(D) + f(S)r_\alpha(D)$.
5. $f(x) = K + f(S)$ for $x < s$.
6. $f(x) = L_\alpha(x, x - s) + Kr_\alpha(x - s) + f(S)r_\alpha(x - s)$ for $x \ge s$.
7. Eq. (10): the closed form of $f$ with denominator $1 - r_\alpha(D)$.

Significance

Eq. (11) turns the cost of an $(s, S)$ policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in $G_\alpha$, $K$ and the renewal sequence $m_\alpha$, which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes $a_\alpha(\cdot \mid s, S)$ over a finite box, and the undiscounted limit $\alpha \to 1$ gives the long-run average cost $(L_1(S, D) + K)/(1 + M_1(D))$.

The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an $(s, S)$-controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.

Difficulty

The paper's argument conditions on the random time $T(D)$ at which the process renews and uses the strong Markov property at that time. In the formalization, $f$ is defined as a sum over periods of expectations under the law of $X_t$. Relating that sum to one that splits at the random time $T(D)$ requires either a stopping-time decomposition of the chain or an explicit accounting of the law of $X_t$ before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states $y \in \mathbb Z$, which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine $f(S)$ without the fact that $r_\alpha(D) < 1$ for $\alpha < 1$, which comes from (9).

Formalization scope

• Namespace VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; $x - s$ and $D = S - s$ enter $L_\alpha$, $M_\alpha$, $r_\alpha$ through Int.toNat, which is exact because the statements assume $s \le x$ or $s \le S$.
• Reduced model. The primitives are $G_\alpha$, $K$, $\alpha$ and $\varphi$, as in the paper's Eq. (2): the unit purchase cost is set to $0$ and the holding–penalty cost is replaced by $G_\alpha$.
• Demand is a real function $\varphi : \mathbb N \to \mathbb R$, non-negative and summing to $1$.
• The cost $f$ is the expected discounted cost of the controlled chain: the law of $X_t$ is built recursively from $X_1 = x$ and the transition $\Pr(X_{t+1} = z \mid X_t = y) = \varphi(Y(y) - z)$. It is not defined by (10) or by the renewal equations, and not as the solution of a fixed-point equation. A formalization in which any of milestones 4–7 or the goal holds by definition is ruled out.
• Series are real tsums. $L_\alpha$ is defined by the series (7) and $r_\alpha$ by the first line of (9), i.e. through the law $\Pr[T(d) = i] = \Phi^{i-1}(d) - \Phi^i(d)$; the paper's derivations of these series from $T(d)$ are not formalized. For $\alpha < 1$ all series converge for every $G_\alpha$, because after period $1$ the stock after ordering lies in the finite set $\{S\} \cup [s, \max(x, S)]$.
• Hypotheses. Milestones 1–3 assume $0 \le \alpha \le 1$ and $\alpha\varphi(0) < 1$, the paper's standing assumption on p. 533. Milestones 4–7 and the goal assume $0 \le \alpha < 1$, $K \ge 0$ and $s \le S$. The paper's standing assumptions that $G_\alpha$ is convex and tends to $+\infty$ as $|y| \to \infty$ are not imposed: the statements hold for every $G_\alpha$ when $\alpha < 1$, and the paper's derivation does not use them. This is a disclosed generalization.
• Printed slips. None found in the formalized statements.
• Not formalized: the recursion (A1) for $m_\alpha$, the limit (12) as $\alpha \to 1$, and the stationary analysis (13)–(20).

Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.

Selected references

• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• K. J. Arrow, S. Karlin and H. Scarf, Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.