All missions

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

A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).

This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.

Setting

Let $\Gamma$ be a game with finitely many players $i$, a finite nonempty strategy set $S_i$ for each player, and payoffs $u_i(s)$ for strategy tuples $s \in \prod_j S_j$. Write $(x, s_{-i})$ for $s$ with player $i$'s strategy replaced by $x$.

• A play is a strategy tuple. Fix a memory $m$ and a sample size $k$ with $1 \le k \le m$. The state $h \in H = (\prod_j S_j)^m$ is the sequence of the last $m$ plays, oldest first.
• A successor of $h$ is obtained by deleting the oldest play and appending a new one.
• A sample is a set of $k$ positions of $h$. Player $i$'s best reply to a sample $K$ maximizes the total payoff $\sum_{t \in K} u_i(x, (h_t)_{-i})$ against the sampled plays.
• A best-reply distribution gives, for each $i$ and $h$, a probability distribution $p_i(\cdot \mid h)$ on $S_i$ that is positive exactly on the strategies that are best replies to some sample of size $k$. The sampling law itself is arbitrary.
• Adaptive play $P^0$ is the Markov chain on $H$ that moves from $h$ to the successor with new play $s$ with probability $\prod_i p_i(s_i \mid h)$.
• A strict Nash equilibrium is a tuple $s$ from which every unilateral deviation is strictly worse. A convention is a state $(s, s, \dots, s)$ with $s$ a strict Nash equilibrium.
• The best-reply graph has an edge $s \to (x, s_{-i})$ whenever $x \ne s_i$ is a best reply of $i$ to $s_{-i}$. $\Gamma$ is weakly acyclic if from every $s$ a directed path leads to a sink. $L(s)$ is the length of a shortest such path from $s$ to a strict Nash equilibrium, and $L_\Gamma = \max_s L(s)$.

Formalization targets

Goal: Theorem 1 (p. 64)

If $\Gamma$ is weakly acyclic and $k \le m/(L_\Gamma + 2)$, then for every best-reply distribution and every initial state $h$,

$$\lim_{t\to\infty} \sum_{h' \text{ a convention}} \big((P^0)^t\big)_{hh'} = 1 .$$

Milestones

1. Absorbing states (§4, p. 62): $P^0_{hh} = 1$ if and only if $h$ is a convention.
2. Sinks (§4, p. 64): the sinks of the best-reply graph are exactly the strict Nash equilibria. Hence weak acyclicity means that one-player-at-a-time best replies can reach a strict equilibrium from every tuple.
3. A run of best replies (proof of Theorem 1, p. 64): if $m \ge 2k-1$, then with positive probability $k$ consecutive identical best replies to the last $k$ plays are appended.
4. Uniform bound (proof of Theorem 1, p. 65): there is $q > 0$ such that from every state a convention is reached within $M = kL_\Gamma + m$ periods with probability at least $q$.
5. Geometric tail (proof of Theorem 1, p. 64): such a uniform bound makes the probability of no convention after $rM$ periods at most $(1-q)^r$.
6. Example 2 (pp. 65–66, off the goal's path): in a Battle-of-the-Sexes game with complete sampling $k = m$, a perfectly miscoordinated history stays miscoordinated forever.

Significance

Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio $k/m$ is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.

The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of $2k-1$, $3k-1$ and $kr + 2k - 1$ periods), which the text checks only in words.

Difficulty

Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound $k \le m/(L_\Gamma+2)$. A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.

Formalization scope

Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition $k \le m/(L_\Gamma+2)$ is $k(L_\Gamma+2) \le m$ in ℕ. $L(s)$ is an sInf on ℕ that is never empty under weak acyclicity.

The display (1) on p. 62 reads "the right-most element of $h$". The formalization uses the right-most element of the successor $h'$, the only reading under which the rule is meaningful.

The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to $1$ from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a $2\times2$ coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.

A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.

Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• D. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984. https://doi.org/10.1007/978-1-4684-0176-9
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988.
• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2002, 2265–2294. https://doi.org/10.1111/1468-0262.00376
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21, 1997, 40–55. https://doi.org/10.1006/game.1997.0595

Pricing and stocking a perishable good

A retailer of style goods — seasonal clothing, newspapers, anything that loses most of its value when the selling period ends — must decide before the season how many units to stock, knowing demand only as a probability distribution. Units left over are liquidated at a loss; units short are sales forgone. This single-period trade-off is the newsvendor problem, and its solution, the critical-fractile rule, is one of the first results of stochastic inventory theory.

In practice the retailer also sets the price, and the price moves the demand distribution. T. M. Whitin's 1955 paper Inventory Control and Price Theory (DOI 10.1287/mnsc.2.1.61) is one of the first to put the two decisions into one model. Its Section 3 restates the critical fractile for a given price, then lets the demand distribution depend on the unit profit and asks for the unit profit and stock that jointly maximize expected profit. For one explicit family of demand laws it solves the problem in closed form. This joint price-setting newsvendor problem later grew into a large literature (Mills 1959, Karlin and Carr 1962, and the survey of Petruzzi and Dada 1999), which cites Whitin's model as its starting point.

Setting

There is one selling period. Stock $x \ge 0$ is on hand at its start. Each unit sold earns the unit profit $P$; each unit left over at the close is liquidated at the unit liquidation loss $L > 0$.

Demand depends on the unit profit through its mean. The mean demand is the linear function

$$\mu(P) = k\,(P - P_0),$$

where $P_0 > 0$ is the unit profit at which demand falls to zero and $k$ is the reciprocal of the slope of the line relating unit profit and amount demanded. Demand decreases in $P$, so $k < 0$, and the admissible unit profits are $0 < P < P_0$. At unit profit $P$, demand $X$ has the rectangular (uniform) distribution on $[0, 2\mu(P)]$.

The expected marginal profit of the $x$-th unit is $f(x) = P\,\Pr(X \ge x)$, the probability that it sells weighted by the unit profit, and the expected marginal loss is $g(x) = L\,\Pr(X < x)$, the probability that it does not sell weighted by the liquidation loss. The expected profit of stocking $x$ units at unit profit $P$ is the area between them,

$$E(P, x) = \int_0^x \big[f(t) - g(t)\big]\,dt,$$

which is the expected profit on sales minus the expected liquidation loss. The equilibrium stock is

$$x_M(P) = -\frac{2kP(P_0 - P)}{P + L}.$$

Formalization targets

Goal: the optimal unit profit (Eq. (16))

With

$$P^* = \frac{(P_0 - 3L) + \sqrt{(3L - P_0)^2 + 16P_0L}}{4},$$

one has $0 < P^* < P_0$, and for all $0 < P < P_0$ and all $x \ge 0$

$$E(P, x) \le E\big(P^*, x_M(P^*)\big),$$

with equality only at $(P, x) = (P^*, x_M(P^*))$. The formula for $P^*$ involves only $P_0$ and $L$: the optimal unit profit is independent of the demand slope $k$.

Milestones, in the order of the paper

1. Eq. (8) — for a general demand law, profit is maximized at the stock whose probability of being sold is $L/(G + P + L)$ ($G$ a goodwill loss per unit short). This is already proved on the platform as SupplyChainTheory.chain_optimal_fractile and enters as a reference.
2. Eq. (11) — on $0 \le x \le 2\mu(P)$, $f(x) = \frac{P}{2k(P_0 - P)}x + P$ and $g(x) = \frac{-L}{2k(P_0 - P)}x$.
3. Eqs. (10), (13) — on the same range, $E(P, x) = \frac{P + L}{4k(P_0 - P)}x^2 + Px$.
4. Eqs. (9), (12) — $x_M(P)$ lies in $(0, 2\mu(P))$, is the only stock with $f = g$, and is the unique maximizer of $E(P, \cdot)$ over $x \ge 0$.
5. Eq. (14) — $E(P, x_M(P)) = -kP^2(P_0 - P)/(P + L)$.
6. Eq. (15) — the derivative of $P \mapsto E(P, x_M(P))$ vanishes exactly when $2P^2 + (3L - P_0)P - 2P_0L = 0$.
7. Footnote 7 — the elasticity of mean demand at $P^*$ equals $P^*/(P_0 - P^*)$, and it tends to $1$ as $P_0 \to \infty$ with $L$ fixed.

Significance

The goal is a complete closed-form solution of a joint pricing-and-stocking problem under uncertainty: one price and one stock level, explicitly, with a proof that no other pair does as well. The independence of the optimal unit profit from $k$ says that, in this family, the scale of the market does not affect the optimal margin; only the ratio of the zero-demand margin to the liquidation loss does. Footnote 7 relates the optimum to the classical monopoly rule (unit elasticity) in the limit of a negligible liquidation loss.

Whitin's derivation is calculus on closed forms and was never stated as a theorem with hypotheses. He calls the stationary point of (15) "the optimal $P$" without checking that it is a maximum, that it is global, or that the stock beyond the support of demand cannot do better. The formalization fixes all three: the goal is a statement of global, unique optimality over the whole admissible region. No machine-checked proof of this result, of the price-setting newsvendor, or of the uniform-demand newsvendor exists on the platform; the general critical-fractile rule (8) is the only part of Section 3 already proved there.

Difficulty

The expected profit is defined from the demand law, so the closed forms (11) and (13) must be derived from the uniform distribution — probabilities of half-lines under a conditioned Lebesgue measure, and an interval integral of the resulting piecewise-linear functions. They hold only on the support of demand; beyond $2\mu(P)$ the marginal profit is $0$ and the marginal loss is $L$, and the global statement must cover that region too.

The pricing step is where the paper is loose. Setting the derivative of (14) to zero gives a quadratic with two real roots, and a stationary point of a function on an open interval need not be its maximum. The goal asks for the global maximum over $0 < P < P_0$ and its uniqueness, and asks that it be the global maximum of the joint problem, not only of the reduced function $P \mapsto E(P, x_M(P))$.

Formalization scope

All quantities are real numbers; stock is continuous, as in the paper's calculus. Mean demand is meanDemand k P₀ P = k * (P - P₀) and the paper's sign convention is kept: $k < 0$ is a hypothesis of every statement, as are $L > 0$ and $0 < P < P_0$ (or $P_0 > 0$ where $P$ is not fixed). The demand law is ProbabilityTheory.cond volume (Set.Icc 0 (2 * μ)); $f$ and $g$ use $\Pr(X \ge x)$ and $\Pr(X < x)$; $E$ is an interval integral defined for every $x$.

The paper's loose phrases are read as follows. "Equation (9) may be solved for $x$" becomes uniqueness of the root of $f - g$ on $x \ge 0$; "the equilibrium value of $x$" becomes the unique maximizer of $E(P, \cdot)$ over $x \ge 0$; "differentiating (14)" becomes a HasDerivAt statement with the explicit derivative for $P \mapsto E(P, x_M(P))$, together with the equivalence with (15); "solving (15) gives the optimal $P$" becomes the goal's joint global maximum with equality case; "independent of $k$" is the shape of the formula for $P^*$; "as $P_0$ becomes large relative to $L$, the optimal elasticity approaches unity" becomes a limit as $P_0 \to \infty$ with $L$ fixed.

Defining $E$ by the closed form (13) instead of from the demand law would make milestones (11) and (13) tautologies and would change the model beyond the support of demand; this formalization rules that out. The paper's goodwill loss $G$ belongs to the fixed-price model of (8) and does not appear in $E$.

A complete development needs the uniform distribution's tail probabilities, interval integrals of piecewise-linear functions, and one-variable calculus for the quadratic and the cubic $P^2(P_0 - P)/(P + L)$; the uniform-law lemmas are reusable for any newsvendor problem with uniform demand. Proofs of the milestones, and alternative arguments for the goal, are welcome.

Selected references

• T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 61–68, 1955. https://doi.org/10.1287/mnsc.2.1.61
• E. S. Mills, Uncertainty and Price Theory, Quarterly Journal of Economics 73(1), 116–130, 1959. https://doi.org/10.2307/1883828
• S. Karlin and C. R. Carr, Prices and Optimal Inventory Policy, in Arrow, Karlin and Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 159–172, 1962.
• N. C. Petruzzi and M. Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Eq. (14.8) (the critical fractile, formalized on the platform as SupplyChainTheory.chain_optimal_fractile).

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

Inventory calculations often take the selling price as fixed, while price calculations often treat the cost of supplying demand as independent of the order policy. Whitin's 1955 model connects the two decisions in one annual-profit calculation. A merchant chooses both the price charged to customers and the size of each replenishment order. Changing the price changes annual demand; changing demand changes the number of orders, inventory carrying cost, and therefore the economic lot size. This makes the selling price and the inventory decision parts of the same optimization problem. Whitin's paper gives a compact example in which the connection can be written down explicitly.

The mission concentrates on Section 2, the stationary-demand model for a stable item. Section 3 of the paper studies style goods under uncertain sales and belongs to a separate mission. The result here concerns a deterministic annual demand curve and continuous order quantities, so a solver can focus on the interaction between a classical economic order quantity calculation and a price first-order condition.

Setting

The price is a real number $p$. Annual demand is the linear function $D(p)=ap+b$, where $a$ and $b$ are given real constants. A feasible price has $D(p)>0$. The paper does not require $a<0$ in its displayed model, so the formal statements leave the slope unrestricted. Negative $a$ is the economically usual decreasing-demand case; in other regimes a joint maximum may simply fail to exist.

The merchant pays a fixed setup cost $S$ whenever an order is placed. The purchase cost per unit is $C$, and the annual carrying charge for one unit kept in stock is $IC$, where $I$ is a carrying-rate factor. If $Q>0$ units are ordered each time, average stock is $Q/2$ and the annual number of orders is $D/Q$. A per-unit operating cost $k$ is incurred on annual demand, and $f$ is an annual fixed cost. The resulting total variable cost and two-variable annual profit are

$$\operatorname{TVC}(D,Q)=\frac Q2 IC+\frac DQ S+kD, \qquad \Pi(p,Q)=D(p)p-\operatorname{TVC}(D(p),Q)-f.$$

Only pairs with $D(p)>0$ and $Q>0$ are feasible. For a fixed demand level, the economic lot size is $Q^*(D)=\sqrt{2DS/(IC)}$. Substituting it into profit gives Whitin's reduced profit

$$P(p)=ap^2+bp-\sqrt{2SIC(ap+b)}-k(ap+b)-f.$$

The paper uses $P$ for annual profit in this section. The Lean development calls the two-variable function profit and the function after optimizing $Q$ reducedProfit.

Formalization targets

The first target is the unique lot-size minimum in Eq. (3), followed by its value in Eq. (4):

$$\operatorname{TVC}(D,Q^*(D))\leq\operatorname{TVC}(D,Q) \quad(Q>0),\qquad \operatorname{TVC}(D,Q^*(D))=\sqrt{2DSIC}+kD.$$

Equality in the inequality holds only at $Q=Q^*(D)$. The next target is the necessary stationarity condition in Eqs. (6)–(7): when $D(p)>0$ and the derivative of $P$ at $p$ is zero,

$$8a^3p^3+(16a^2b-8ka^3)p^2 +(10ab^2-12ka^2b+2k^2a^3)p +2b^3-4kab^2+2k^2a^2b-SICa^2=0.$$

The goal joins these steps at a global joint maximum. If a feasible pair $(p,Q)$ maximizes $\Pi$ over all feasible price and lot-size pairs, then $Q=Q^*(D(p))$ and $p$ satisfies the cubic. The goal is an implication about any joint maximizer; it does not assert that one exists for every demand curve. The cubic is a necessary condition only. Its algebraic roots may include prices that fail the original first-order equation or fail to maximize profit.

Significance

The result gives a concrete relation between a price chosen to maximize annual profit and the ordering cost and carrying charge of the inventory system. The lot-size formula alone optimizes cost at a fixed demand rate. The cubic makes the demand response to price and the resulting inventory cost visible in the price condition. It also specifies what can be inferred from the calculation: an optimal price must satisfy the equation, while selecting an optimum from candidate roots remains a separate question.

The paper already supplies the mathematical result. The formalization task is to represent the joint optimization and verify its necessary conditions in Lean, together with the cost identity on which the reduced-profit expression rests. The published Prove2Me definition InventoryControl_eoq already provides the classical EOQ cost and square-root quantity; this mission uses its cost function and adds Whitin's demand curve and profit. Related inventory results for backorders and multilevel systems describe different models and do not replace the targets here.

Difficulty

At a fixed price, choosing the lot size involves both a term proportional to $Q$ and one proportional to $1/Q$. The optimality statement needs a global inequality and a unique equality case, not merely the observation that a derivative vanishes. After substituting that quantity, the reduced profit contains a square root of the demand curve. Its derivative is meaningful on positive demand, and turning its stationarity equation into the displayed cubic loses information when an equation is squared. A proof therefore has to preserve the implication from optimality to the cubic without promoting all cubic roots to optima.

Formalization scope

The model uses real prices, real demands, and real lot sizes; it does not round order quantities to integers. The hypotheses $S,I,C>0$ make explicit the positive cost and carrying-charge conventions of Section 2. Neither $k$ nor $f$ is assigned a sign, and no sign is imposed on $a$ or $b$. The conditions $Q>0$ and $D(p)>0$ apply to every cost or profit comparison. They exclude Lean's total value for division by zero and the zero value assigned by Real.sqrt to a negative argument. The goal quantifies over every feasible pair in a joint maximum of the original profit, so optimizing $Q$ is part of its content. Defining profit only by the reduced formula would erase that claim.

The definitions comprise linear demand, total variable cost, two-variable profit, and reduced profit. The classical EOQ cost comes from the existing InventoryControl_eoq definition; the model-specific layer is small and can be reused in further work on pricing with inventory costs. The theorem targets welcome proofs of the global lot-size inequality, the minimized-cost identity, the stationary cubic, and their combination at a joint maximizer. The paper's quantity-discount footnote is outside this scope because it leaves the revised purchase and carrying-cost model unspecified.

Selected references

• T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 1955, pp. 61–68. DOI: 10.1287/mnsc.2.1.61.

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