Operations Research

Motivation

Many decisions are made before their objective coefficients are known. A planner may know the feasible decisions and the form of a linear optimization problem, but must predict its cost vector from available features. Squared prediction error measures how close a forecast is to the eventual coefficients; it need not measure the quality of the decision chosen with that forecast. Elmachtoub and Grigas define a loss based on the excess realized cost of the resulting decision, then introduce a convex surrogate, SPO+, for training prediction rules Elmachtoub and Grigas, 2020, §§2–3.

The central population question is whether minimizing the surrogate still selects predictions that minimize the decision loss when the full data distribution is available. Their Theorem 1 answers this under conditions on the feasible region and the conditional distribution of costs Elmachtoub and Grigas, 2020, p. 21. The result concerns the loss itself, before sample size, model capacity, or an algorithm for fitting a predictor enter the picture.

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact, and convex. Given a cost vector $c\in\mathbb R^d$, a decision $w\in S$ incurs cost $c^\top w$. The nominal value, optimal-decision set, and support function are

$$z^*(c)=\min_{w\in S}c^\top w,\qquad W^*(c)=\arg\min_{w\in S}c^\top w,\qquad \xi_S(c)=\max_{w\in S}c^\top w.$$

An optimization oracle $w^*$ returns one element of $W^*(c)$ for each $c$, without a tie-breaking rule. For a predicted cost $\hat c$ and realized cost $c$, the unambiguous SPO loss uses the worst realized decision among all decisions optimal for the prediction:

$$\ell_{\mathrm{SPO}}(\hat c,c) =\max_{w\in W^*(\hat c)}c^\top w-z^*(c).$$

This is Definition 2 of the paper. Its SPO+ loss, Definition 3, is

$$\ell_{\mathrm{SPO+}}(\hat c,c) =\xi_S(c-2\hat c)+2\hat c^\top w^*(c)-z^*(c).$$

The factor $2$ is fixed by the paper's surrogate. Proposition 3 states that SPO+ upper-bounds SPO, is convex in $\hat c$, and has the explicit subgradient $2(w^*(c)-w^*(2\hat c-c))$ Elmachtoub and Grigas, 2020, pp. 17–18.

Let $x$ denote an observed feature, $\nu$ its probability law, and $\kappa_x$ the conditional law of $c$ given $x$. Their joint law is $D=\nu\otimes\kappa$. A measurable predictor $f$ maps each $x$ to a cost prediction $f(x)$. The population risks $R_{\mathrm{SPO}}(f)$ and $R_{\mathrm{SPO+}}(f)$ are expectations over $(x,c)\sim D$ of the corresponding losses at $(f(x),c)$, as in displays (11) and (12) Elmachtoub and Grigas, 2020, p. 20. There is no prescribed parametric predictor class.

Formalization targets

Theorem 1: Fisher consistency of SPO+

Write $m(x)=\mathbb E[c\mid x]$. Under Assumption 1, the optimal-decision set $W^*(m(x))$ is a singleton for almost every $x$; each conditional law is centrally symmetric about $m(x)$ and continuous on all of $\mathbb R^d$; and $S$ has nonempty interior. The goal says that every measurable minimizer $f$ of SPO+ population risk satisfies

$$f(x)=m(x)\quad\text{for }\nu\text{-almost every }x, \qquad R_{\mathrm{SPO}}(f)\le R_{\mathrm{SPO}}(g) \quad\text{for every measurable }g.$$

This is the paper's Fisher-consistency statement, including its stronger identification of every SPO+ minimizer with the conditional mean Elmachtoub and Grigas, 2020, Theorem 1. The goal does not assert that a minimizer exists.

Supporting propositions

The milestone list follows the paper's numbered results: Proposition 3's pointwise upper bound, convexity, and subgradient; Proposition 6's mean minimizer and uniqueness claims for a single cost law; and both directions of Proposition 5, which relate SPO risk minimizers to decisions optimal at the mean Elmachtoub and Grigas, 2020, pp. 18, 22–23. The single-law propositions have no feature variable.

Significance

Theorem 1 identifies a condition under which a convex training objective preserves the population target of the decision loss. Its identification statement is stronger than merely saying that one selected SPO+ minimizer is SPO-optimal: all SPO+ minimizers agree almost surely with conditional mean cost. The propositions isolate what this depends on. Proposition 6 concerns the surrogate risk, while Proposition 5 connects a prediction's optimal-decision set to the true risk.

The result was proved in the cited preprint and published in Management Science in 2022; this mission asks for a Lean proof of that known result, not a new consistency theorem. A completed development would provide reusable definitions for cost-based decision losses and a checked account of the distributional assumptions needed for uniqueness. The published oracle predicate is already available on the platform; the two losses, risks, and distributional predicates are introduced here.

Difficulty

The SPO loss may jump when a predicted cost admits more than one optimal decision. Its definition takes the maximum realized cost over that whole decision set. Consequently, showing that a prediction selects one mean-optimal decision does not by itself control the SPO loss; Proposition 5's converse requires a singleton set. The surrogate is convex but generally not differentiable, because the support function of $S$ need not be differentiable. Establishing the unique population minimizer also depends on how the cost law covers the space: absolute continuity by itself permits a bounded-support law for which nearby predictions tie. These are substantive issues in moving from the single-cost-law statements to an almost-sure claim about measurable predictors Elmachtoub and Grigas, 2020, §4 and Appendix B.

Formalization scope

The code represents $\mathbb R^d$ by EuclideanSpace ℝ (Fin d) and $c^\top w$ by its standard inner product. Every theorem assumes the paper's nonempty compact convex $S$. Real infima and suprema encode the attained minima and maxima on $S$. An oracle is an explicit parameter satisfying the published SPOBounds.Natarajan.IsOracle predicate; it is not given an extra measurability or tie-breaking assumption. The SPO loss is the paper's unambiguous Definition 2, which differs from the oracle-dependent loss in the published module.

Expected losses are extended nonnegative integrals, so an infinite risk remains infinite. Conditional costs are represented by a Markov kernel $\kappa$, and the joint law by $\nu\otimes\kappa$. Integrability of costs makes the conditional and joint means finite. Central symmetry means equality of the conditional law with its reflection $c\mapsto 2m(x)-c$. Assumption 1.3, “continuous on all of $\mathbb R^d$,” is pinned to absolute continuity with respect to Lebesgue measure and full support, meaning every nonempty open set has positive probability. This full-support condition is needed for Proposition 6(b)'s uniqueness claim: a continuous law confined to a small ball supplies a counterexample to the weaker reading.

The risks range over all measurable predictors, as display (12) requires. A Bochner integral for an arbitrary nonintegrable loss, a restricted hypothesis class, the oracle-dependent SPO loss of Definition 1, or absolute continuity without full support would change or trivialize the target. Contributions to the support-function, measurable-risk, and conditional-law infrastructure are useful beyond this mission; the seven numbered proposition parts provide its immediate formalization targets.

Selected references

• A. N. Elmachtoub and P. Grigas, Smart “Predict, then Optimize”, arXiv:1710.08005v5, 2020; published in Management Science 68(1), 2022. Preprint

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ($\mathrm{UDP}_{\min}$). There are items $[n]$ and consumers $[m]$, $m\ge 1$. Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$. Given a price assignment $p:[n]\to\mathbb R_{>0}$, consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$, and nothing otherwise. The seller's revenue is

$$\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),$$

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$, and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$. Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$, $S\subseteq\mathcal C$, with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$. With revenues $r:\mathcal C\to\mathbb R_{>0}$, an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$. If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$, revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$.

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$, $r((x,v))=m\,v$, and $\mathcal P=\frac1m\sum_i\mathcal P_i$, where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$, $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$.

Formalization targets

Goal: Corollary 4.7

$$\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.$$

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$, $\rho:=v_m/v_1$", stated in product form.

Milestones

1. Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
2. Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
3. Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
4. Prices to assortments: for valuation-valued $p$, $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
5. Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
6. Theorem 3.2 for an arbitrary regular model:

$$\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.$$

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$. More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$. The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$, which receive the paper's "$+\infty$" price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$; the reduction to a regular model is what supplies it.

Formalization scope

• Items and consumers are finite types X and M, with Nonempty M ($m\ge1$). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ($r=m\,v>0$) and its ratio $v_m/v_1$ need positivity.
• A consumer with $B_i=\emptyset$ pays $0$. Ties among cheapest items do not affect payments, so payments are defined directly.
• $\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$. Uniform pricing ranges over all $q>0$, not only valuations.
• The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$, and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
• The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$, which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
• Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$; $\ln$ is Real.log applied to ratios $\ge1$.
• Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
• Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
• G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
• V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
• P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
• A. Aouad, V. Farias, R. Levi and D. Segev, The approximability of assortment optimization under ranking preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1754

Motivation

A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.

The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order $\sqrt{NT\log NT}$ (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most $K$ products be displayed, no policy can have regret smaller than order $\sqrt{NT/K}$ on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.

Timeline. The square-root lower bound for $N$-armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining $O(N^2\log^2T)$ and $O(N\log T)$ bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent $\Omega(\sqrt{NT/K})$ lower bound formalized here; Chen and Wang (2017) later obtained $\Omega(\sqrt{NT})$ when $K<N/4$.

Setting

There are $n$ products. An instance consists of a no-purchase weight $v_0>0$, attraction parameters $v_1,\dots,v_n$ with $0\le v_i\le v_0$, and revenues $r_i\in[0,1]$. At each period $t=1,\dots,T$ the seller offers an assortment $S_t\subseteq\{1,\dots,n\}$ and observes a choice $c_t\in S_t\cup\{0\}$, where $0$ means no purchase. Under the multinomial logit (MNL) model,

$$p_i(S)=\frac{v_i}{v_0+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

and choices are independent across periods given the offered sets. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i/(v_0+\sum_{j\in S}v_j)$.

A policy chooses $S_t$ from the past assortments and choices, possibly at random. It satisfies the $K$-cardinality constraint if $|S_t|\le K$ always. Its regret over $T$ periods is

$$\mathrm{Reg}_\pi(T,v)=\mathbb E_\pi\Big(\sum_{t=1}^{T}R(S^*,v)-R(S_t,v)\Big),$$

where $S^*$ maximizes $R(\cdot,v)$ over assortments of at most $K$ products.

A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.

Formalization targets

Goal: Theorem 2 (p. 14)

There is an absolute constant $C>0$ such that for all $n\ge2$, $1\le K\le n$ and $T\ge n$ there is a finitely supported randomized instance, chosen before the policy, such that every policy $\pi$ respecting the $K$-cardinality constraint satisfies

$$\mathbb E_{v}\big[\mathrm{Reg}_\pi(T,v)\big]\ge C\sqrt{\frac{nT}{K}} .$$

The constant is not fixed; any positive value suffices.

Milestones

The paper proves Theorem 2 in two cases.

1. Lemma E.1 (p. 57): the Bernoulli divergence bound $\mathrm{kl}(\alpha,\alpha+\epsilon)\le 4\epsilon^2/\alpha$ in the direction used by Lemma E.2.
2. Lemma E.2 (p. 57): for a guessing algorithm on $N\ge12$ coins and $t\le N\alpha/(60\epsilon^2)$, at least $N/3$ hiding places $j$ of the biased coin have $\mathcal P_j(a_t=j)\le 1/2$.
3. Lemma 5.1 (p. 15): on the Bernoulli instance $I_{\mathrm{MAB}}$ with $\epsilon=\frac1{100}\sqrt{N\alpha/T}$, every online algorithm has expected regret at least $\epsilon T/6$.
4. Lemma E.4 (p. 60): one period of MNL feedback on the instance $\hat I_{\mathrm{MNL}}$, where $\epsilon=\sqrt{1/(32T)}$, has divergence at most $4\epsilon^2$.
5. Lemma E.5 (p. 61): over $T$ periods the two choice laws of that instance have divergence at most $4T\epsilon^2$.

Items 1–3 serve the case $K<n$, which the paper reduces to a multi-armed bandit through the instance $I_{\mathrm{MNL}}$ of Definition 5.2 ($NK$ products in $N$ groups of $K$, one hidden group with larger attraction). Items 4–5 serve the case $K=n$ through the two-point instance $\hat I_{\mathrm{MNL}}$ of Definition E.1.

Significance

The theorem shows that the $\sqrt{T}$ growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size $K$ is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.

The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude $\alpha$ close to $1$, where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the $K=N$ case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.

Difficulty

The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers $K$ products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over $T$ pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.

A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.

Formalization scope

Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length $T$, laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight $v_0$ is explicit (Definition 5.2 has $v_0=K$). $R(S^*,v)$ is a maximum over the finite, nonempty family $\{S:|S|\le K\}$.

Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then $n,K,T$, then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with $C=0$ allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.

Hypotheses added to the printed statements: $n\ge2$ and $K\ge1$ in Theorem 2 (the claim fails for $n=1$ and $K=0$); $0<\alpha$, $0<\epsilon$, $\alpha+\epsilon\le3/4$ in Lemma E.1; $0<\alpha$, $0<\epsilon$, $2\alpha+\epsilon\le1$ in Lemma E.2; $0<\alpha$, $2\alpha+\epsilon\le1$, $T\ge1$ in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's $\epsilon=\sqrt{1/(32T)}$, with $T\ge1$ and $n\ge2$ so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.

The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in $[0,\infty]$). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound $d(p,q)\le(q-p)^2/(p(2-p-q))$ (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880 — DOI https://doi.org/10.1287/opre.2018.1832
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
• X. Chen, Y. Wang, A Note on a Tight Lower Bound for MNL-Bandit Assortment Selection Models, arXiv:1709.06109, 2017. https://arxiv.org/abs/1709.06109

Motivation

Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).

The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.

Setting

There are periods $1,\ldots,n$. Demand $d_t$ and setup cost $f_i$ are nonnegative for the periods in the horizon. The marginal production cost $c_i$ is any real number. Write $d_{i,j}=\sum_{t=i}^j d_t$ for cumulative demand from $i$ through $j$. Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods $1,\ldots,n$.

The forward lot-sizing cost $F(j)$ describes the least cost of serving periods $1,\ldots,j$ under the zero-inventory property cited by the paper. Its recursion starts with $F(0)=0$. If $d_j=0$, no new production is needed and $F(j)=F(j-1)$. If $d_j>0$, the last production setup may occur at some $i\le j$, giving

$$F(j)=\min_{1\le i\le j}\bigl(f_i+c_i d_{i,j}+F(i-1)\bigr).$$

This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at $d_j=0$ would charge a setup that need not occur.

Program D′ chooses free real values $v_1,\ldots,v_n$ to maximize $\sum_{t=1}^n d_tv_t$, subject to

$$\sum_{t=i}^n d_t\max\{0,v_t-c_i\}\le f_i \qquad(1\le i\le n).$$

“Free” means there is no nonnegativity constraint on $v_t$. The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.

The greedy forward rule visits periods in increasing order. At a period with $d_j>0$, the chosen value is the minimum of the upper bounds left by the constraints indexed $i\le j$:

$$v_j=\min_{1\le i\le j} \left(c_i+\frac{f_i-\sum_{t=i}^{j-1}d_t\max\{0,v_t-c_i\}}{d_j}\right).$$

When $d_j=0$, the rule places no restriction on $v_j$. This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.

Formalization targets

The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:

$$\sum_{t=1}^j d_tv_t=F(j)\quad(1\le j\le n), \qquad \sum_{t=1}^n d_tu_t\le\sum_{t=1}^n d_tv_t \quad\text{for every feasible }u.$$

The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.

Significance

The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost $F(n)$, and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to $F$ Wagelmans et al., p. S153.

A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.

Difficulty

A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with $F(j)$ also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.

Formalization scope

Lean represents the horizon by natural-number indices $1,\ldots,n$ and the demand, setup, marginal-cost and dual sequences by functions $\mathbb N\to\mathbb R$. Finite sums use closed intervals; the sum before period $j$ uses $[i,j)$, so it is empty when $i=j$. Minima are over the nonempty finite set $\{1,\ldots,j\}$, only when $j\ge1$. The horizon $n=0$ has empty sums and no constraints. The cost and dual values are real, with no sign condition on $c_i$ or $v_i$.

Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through $n$ holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.

The identification of $F$ with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including $O(n^2)$ for the greedy forward algorithm and $O(n\log n)$ for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of $F$ as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.

Selected references

• A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1, 1992, S145–S156. DOI

Motivation

Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)

The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145

Setting

A planning horizon consists of periods $1,\dots,n$, with $n\ge1$, and an extra terminal period $n+1$. In period $i$, a known demand $d_i\ge0$ must be met without backlogging. The final demand is positive, $d_n>0$; a trailing zero-demand period could otherwise be deleted. A production setup costs $f_i\ge0$, and every unit produced in that period has a marginal cost $c_i\in\mathbb R$. The sign of $c_i$ is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand $D(t)=\sum_{j=t}^{n}d_j$, with $D(n+1)=0$. If production at $i$ covers demand until the next production period $t$, then $D(i)-D(t)$ units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147

The backward value $G(t)$ starts at $G(n+1)=0$ and follows Equation (1). At positive demand, it minimizes $f_i+c_i[D(i)-D(t)]+G(t)$ over $i<t\le n+1$. When $d_i=0$, skipping setup and using $G(i+1)$ is an additional choice. The paper identifies $G(t)$ with the optimal cost from $t$ onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of $G$; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147

For a fixed $i$, plot the finite points $(D(t),G(t))$ for $i<t\le n+1$. Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set $E_i$. Write $\operatorname{succ}_i(t)$ for the next larger index in $E_i$. The consecutive-point ratio is $r_i(t)=[G(t)-G(\operatorname{succ}_i(t))]/[D(t)-D(\operatorname{succ}_i(t))]$. These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization targets

Efficient candidates

Proposition 1 says every candidate outside $E_i$ can be removed without changing the minimum:

$$\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=\min_{t\in E_i}\{c_i[D(i)-D(t)]+G(t)\}.$$

The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using $r_i(t)$ and $c_i$. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149

Threshold rule and backward value

The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:

$$q(i)=\min\bigl(\{n+1\}\cup\{t\in E_i:t<n+1,\ r_i(t)<c_i\}\bigr).$$

The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals $G(i)$:

$$\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=c_i[D(i)-D(q(i))]+G(q(i)),$$ $$G(i)=\begin{cases}f_i+c_i[D(i)-D(q(i))]+G(q(i)),&d_i>0,\\ \min\{G(i+1),f_i+c_i[D(i)-D(q(i))]+G(q(i))\},&d_i=0.\end{cases}$$

This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150

Significance

The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150

The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.

Difficulty

A candidate point can have a smaller value $G(t)$ than a neighboring point yet still fail to minimize $c_i[D(i)-D(t)]+G(t)$ for a given $c_i$. Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope $c_i$, and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization scope

Periods are natural numbers starting at $1$; $n+1$ is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost $f_i$. No sign restriction is imposed on $c_i$. The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

The algorithm's printed Iterations use $d_{1n}$ where $d_{in}$ is required; the Lean statement uses $D(i)-D(q(i))=d_{i,q(i)-1}$, matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's $O(n\log n)$ bound, the binary-search implementation, the amortized list updates, the $O(n)$ Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152

Selected references

• A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1 (1992), S145–S156. DOI: 10.1287/opre.40.1.S145

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$, order enough to bring it up to the order-up-to level $S$. Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$, $j\ge0$, and $p_0<1$. An order costs $K>0$. $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$. The paper assumes only:

• $-G$ is unimodal: for some integer $m$, $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$;
• $\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$.

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$. The renewal density $m$ and renewal function $M$ are

$$m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).$$

For integers $s<S$, the long-run average cost of the (s, S) policy is

$$c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.$$

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$. The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$, $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$.

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$.

• Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$. Set $S^0:=y^*$, $c^0:=c(s,S^0)$ and $S:=y^*+1$.
• Step 1. While $G(S)\le c^0$: if $c(s,S)<c^0$, set $S^0:=S$, increase $s$ while $c(s,S^0)\le G(s+1)$, and set $c^0:=c(s,S^0)$. In either case, $S:=S+1$.

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$, every $K>0$, every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$, the algorithm terminates. On termination, with final values $s,S^0,c^0$,

$$c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.$$

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

1. the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$, and Lemma 0 on the comparisons it implies;
2. Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$;
3. Corollary 1, the stopping rule of Step 0;
4. Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$, which give the stopping rule of Step 1;
5. Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$, an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$, the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$. Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

• Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$. All costs are real.
• The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$, and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$, so every quantifier over reorder levels carries $s<S$.
• $m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$.
• The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$. Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$.
• Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$, $c^*(S)$, $y_i^*$, $\bar S^*$, $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$-statements, or binders characterised as least or greatest elements.
• The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
• Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$; leaving $c(s,S)$ unguarded for $s\ge S$.
• Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$, $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$, $K=1$, $G(0)=5$, $G(y)=10-0.1\cdot2^{-|y|}$ ($y\neq0$), $S=1$, where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
• Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$.
• Welcome contributions: general facts about the discrete renewal density ($m\ge0$, $M>0$), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

• Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
• 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
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.