All missions

Motivation

Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.

The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.

Setting

A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with $\sum_{s', r} p(s', r \mid s, a) = 1$. A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate $0 \le \gamma < 1$, the state value $v_\pi(s)$ is the expected discounted return $\mathbb E_\pi[\sum_{k \ge 0} \gamma^k R_{t+k+1} \mid S_t = s]$, and the action value is

$$q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)\,[r + \gamma v_\pi(s')].$$

For ε > 0, a policy is ε-soft if $\pi(a \mid s) \ge \varepsilon/|A|$ for all s and a. A policy π′ is ε-greedy with respect to $q_\pi$ if at each state some maximizer $A^*(s)$ of $q_\pi(s, \cdot)$ receives probability $1 - \varepsilon + \varepsilon/|A|$ and every other action receives $\varepsilon/|A|$; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and $v_{\pi''}(s) \le v_\pi(s)$ for every ε-soft π″ and every state s.

The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:

$$\tilde p(s', r \mid s, a) = (1 - \varepsilon)\, p(s', r \mid s, a) + \sum_{a'} \frac{\varepsilon}{|A|}\, p(s', r \mid s, a').$$

Its optimal value function is written $\tilde v_*$.

Formalization targets

Goal: ε-greedy improvement with the equality case

For $0 \le \gamma < 1$, $0 < \varepsilon \le 1$, an ε-soft policy π and any ε-greedy policy π′ with respect to $q_\pi$,

$$v_{\pi'}(s) \ge v_\pi(s) \quad \text{for all } s, \qquad \text{and} \qquad v_{\pi'} = v_\pi \;\Longrightarrow\; \pi, \pi' \text{ are optimal among the ε-soft policies}.$$

The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.

Milestones

1. Policy improvement theorem for stochastic policies (4.7)–(4.8), p. 78: $\sum_a \pi'(a \mid s) q_\pi(s, a) \ge v_\pi(s)$ for all s implies $v_{\pi'} \ge v_\pi$, strictly at every state where the hypothesis is strict.
2. Eq. (5.2), pp. 101–102: $\sum_a \pi'(a \mid s) q_\pi(s, a) = \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a) + (1-\varepsilon)\max_a q_\pi(s, a) \ge v_\pi(s)$.
3. Characterization, p. 102: an ε-soft π is optimal among ε-soft policies if and only if $v_\pi = \tilde v_*$.
4. Uniqueness, p. 102: $\tilde v_*$ is the unique solution of the Bellman optimality equation with the altered transition probabilities $\tilde p$, and that equation splits as $(1-\varepsilon)\max_a(\cdot) + \frac{\varepsilon}{|A|}\sum_a(\cdot)$.
5. Fixed-point equation, p. 102: if $v_{\pi'} = v_\pi$, then $v_\pi(s) = (1-\varepsilon)\max_a q_\pi(s, a) + \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a)$.

Significance

The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value $\tilde v_*$ of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.

The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.

Difficulty

The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity $v_\pi(s) = \sum_a \pi(a \mid s) q_\pi(s, a)$, which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.

Formalization scope

Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so $|A(s)| = |A|$, the book's footnote 3, p. 48), and a finite reward set. The conventions are:

• $v_\pi$ is defined from expected discounted returns as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ with $0 \le \gamma < 1$; Bellman equations are theorems, never definitions. $q_\pi$ is the one-step lookahead (4.6) on this $v_\pi$.
• $\tilde v_*$ is the supremum of the new environment's policy values over all stochastic policies, a bounded family for $\gamma < 1$.
• ε ranges over (0, 1]: the book requires ε > 0, and for ε > 1 no ε-soft policy exists. The equality in (5.2) is stated without the book's intermediate division by 1 − ε, so the case ε = 1 is included.
• "Any ε-greedy policy" is encoded by quantifying over every choice of maximizer at every state.
• "Optimal among ε-soft policies" means ε-soft and pointwise at least as good as every ε-soft policy.

Defining $v_\pi$ as the solution of the Bellman expectation equation, or $\tilde v_*$ as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "$v_{\pi'} \ge v_\pi$" alone: the equality case is part of the book's claim and part of the goal.

The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity $v_\pi = (I - \gamma P_\pi)^{-1} r_\pi$, the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §4.2 (pp. 76–79) and §5.4 (pp. 100–103). http://incompleteideas.net/book/the-book-2nd.html
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (policy iteration).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, doi:10.1002/9780470316887.

Motivation

The bullwhip effect is the observation that the variability of orders increases as one moves up a supply chain, from the retailer towards the manufacturer and its suppliers. It was documented in industry and in classroom experiments such as the Beer Game (Sterman 1989), and analysed by Lee, Padmanabhan and Whang (1997), who named demand forecasting, lead times, batch ordering, rationing and price variations as its main causes. A remedy often proposed is to centralize demand information: give every stage of the chain the customer demand data, so that no stage forecasts from the distorted orders of its downstream neighbour.

Chen, Drezner, Ryan and Simchi-Levi (2000) quantified the effect for a retailer that forecasts with a moving average and orders with an order-up-to policy. They gave an explicit lower bound on the ratio of the order variance to the demand variance in terms of the lead time, the forecasting window and the demand autocorrelation. They then showed that in a multistage chain with fully centralized demand information this ratio still grows with the total lead time upstream of each stage. This mission formalizes that result, Theorem 3.1 of the paper, together with the single-stage analysis it rests on.

Setting

Time is indexed by the integers. The customer demands $D_t$ seen by the retailer follow the AR(1) model

$$D_t = \mu + \rho D_{t-1} + \epsilon_t, \tag{1}$$

where $\mu \ge 0$, $|\rho| < 1$, and the errors $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2$. The demand is in steady state, so that $E(D_t) = \mu/(1-\rho)$ and $\mathrm{Var}(D) = \mathrm{Var}(D_t) = \sigma^2/(1-\rho^2)$ for every $t$.

The retailer does not know the demand process. With a window of $p \ge 1$ past observations it forms the moving-average estimates

$$\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad e_t = D_t - \hat D^1_t, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}},$$

where $L$ is the lead-time parameter ($L = 1$ means an order placed at the end of period $t$ arrives at the start of period $t+1$) and $C_{L,\rho}$ is a constant the paper leaves unspecified. The order-up-to point is $y_t = \hat D^L_t + z\,\hat\sigma^L_{et}$ for a safety factor $z$, and the order placed in period $t$ is $q_t = y_t - y_{t-1} + D_{t-1}$. It may be negative: excess inventory is returned without cost.

In the multistage chain with centralized information, stages $k = 1, 2, \dots$ (stage $1$ is the retailer) all observe $D_t$ and use the same estimate $\hat D_t = \sum_{i=1}^p D_{t-i}/p$. Stage $k$ has lead time $L_k$ and safety factor $z_k$ and uses the order-up-to point $y^k_t = L_k\hat D_t + z_k\hat\sigma^{L_k}_{et}$. Following the paper's sequence of events, stage $1$ orders $q^1_t = y^1_t - y^1_{t-1} + D_{t-1}$, and stage $k \ge 2$, receiving $q^{k-1}_t$, orders $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$.

Formalization targets

Goal: Theorem 3.1 (p. 441)

For every stage $k \ge 1$ and every period $t$,

$$\frac{\mathrm{Var}(q^k_t)}{\mathrm{Var}(D)} \ge 1 + \left(\frac{2\sum_{i=1}^k L_i}{p} + \frac{2\left(\sum_{i=1}^k L_i\right)^2}{p^2}\right)(1-\rho^p),$$

with equality when $z_1 = \dots = z_k = 0$. The bound holds for every choice of the constants $C_{L_k,\rho}$ and of the safety factors.

Milestones (p. 438)

1. The AR(1) moments $\mathrm{Var}(D_t) = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}(D_{t-1}, D_{t-p-1}) = \rho^p\sigma^2/(1-\rho^2)$.
2. Eq. (4): $q_t = (1 + L/p)D_{t-1} - (L/p)D_{t-p-1} + z(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$ for every outcome.
3. Lemma 2.1: $\mathrm{Cov}(D_{t-i}, \hat\sigma^L_{et}) = 0$ for $i = 1, \dots, p$.
4. The variance identity after Eq. (4):

$$\mathrm{Var}(q_t) = \left[1 + \left(\tfrac{2L}{p} + \tfrac{2L^2}{p^2}\right)(1-\rho^p)\right]\mathrm{Var}(D) + 2z\left(1+\tfrac{2L}{p}\right)\mathrm{Cov}(D_{t-1}, \hat\sigma^L_{et}) + z^2\,\mathrm{Var}(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1}).$$

5. Theorem 2.2, the single-stage case:

$$\frac{\mathrm{Var}(q)}{\mathrm{Var}(D)} \ge 1 + \left(\frac{2L}{p} + \frac{2L^2}{p^2}\right)(1-\rho^p), \tag{5}$$

with equality when $z = 0$.

Significance

Theorem 2.2 shows that forecasting with a positive lead time is enough to make orders more variable than demand, even for independent demands ($\rho = 0$). It also says how the effect depends on each parameter: the bound decreases in the window $p$ and increases in the lead time $L$. Theorem 3.1 is the paper's answer to the centralization remedy. When every stage sees the true customer demand and uses the same forecast and the same policy, the variability of orders at stage $k$ is still bounded below by the single-stage expression with the cumulative lead time $\sum_{i\le k}L_i$. Centralization reduces the bullwhip effect but does not remove it. The decentralized comparison (Theorem 3.2, where the bound becomes multiplicative across stages) is a separate mission in this series.

On the formalization side, the Gaussian special case of the single-stage results is on the platform. Snyder and Shen's Fundamentals of Supply Chain Theory states Theorem 2.2, Lemma 2.1, Eq. (4) and the AR(1) moments for normally distributed errors, as the items SupplyChainTheory.bullwhip_signal_processing, bullwhip_lemma_13_1, bullwhip_order_identity and ar1_moments. This mission states them under the paper's weaker hypothesis of a symmetric error distribution. The multistage Theorem 3.1 has no machine-checked counterpart. The paper proves only Theorem 2.2 in print. For the proofs of Lemma 2.1 and Theorem 3.1 it refers to Ryan (1997) and to a working paper, so a formalization supplies arguments the published article does not contain.

Difficulty

Most of the algebra is routine. The difficulty is Lemma 2.1 and the covariances like it. The estimate $\hat\sigma^L_{et}$ is a square root of a quadratic form in past demands, so its covariance with a demand cannot be computed from second moments. Under Gaussian errors one can appeal to properties of Gaussian vectors. With only a symmetric error law, every distributional fact has to come from the symmetry of the errors and from the representation of the steady-state demand as an infinite series in past errors.

The printed derivation also moves faster than a proof. Expanding $\mathrm{Var}(q_t)$ from Eq. (4) produces the cross terms $\mathrm{Cov}(D_{t-1}, \hat\sigma^L_{e,t-1})$ and $\mathrm{Cov}(D_{t-p-1}, \hat\sigma^L_{et})$, which lie outside the lags $1, \dots, p$ of Lemma 2.1. The display after Eq. (4) does not account for them. A complete proof of milestone 4 must show that these terms vanish too. For the chain, the stage orders are defined by a recursion across stages, and the variance of $q^k_t$ involves the estimates $\hat\sigma^{L_i}_{et}$ of all stages $i \le k$.

Formalization scope

Random variables are real functions on a probability space $(\Omega, P)$, and time is $\mathbb Z$, so that $D_{t-p-1}$ exists for every $t$. Variance and covariance are Mathlib's ProbabilityTheory.variance and ProbabilityTheory.covariance. The demand structure ChenBullwhip.Centralized.AR1Demand records (1) for every outcome and the paper's error hypotheses: independence, identical distribution, symmetry, mean $0$ and variance $\sigma^2$. It adds four disclosed conditions:

1. $\sigma > 0$, since the results divide by $\mathrm{Var}(D)$;
2. square integrability of errors and demands, since Mathlib's variance of a non-square-integrable function is $0$;
3. a steady-state condition: every $D_t$ is square integrable with the law of $D_0$, which is the stationary solution the paper's moment formulas presuppose;
4. $p \ge 1$ in every result.

The published Gaussian structure SupplyChainTheory.AR1Demand satisfies these conditions, so this mission generalizes the Snyder–Shen items rather than referencing them. The constants $C_{L,\rho}$ are free real parameters, and in the chain $C_{L_k,\rho}$ is $C(L_k)$ for an arbitrary function $C$. Lead times are natural numbers, $L = 0$ included. Sums $\sum_{i=1}^p$ and $\sum_{i=1}^k$ run over $\{1,\dots,p\}$ and $\{1,\dots,k\}$, and stages are numbered from $1$. The order recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is read from the paper's sequence of events, because the paper prints no formula for $q^k_t$.

The orders are computed from the demands through the definitions above. They are never arbitrary random variables with assumed moments. "Tight" is formalized as equality, and orders are never truncated at zero. Without the steady-state condition, a process started from an arbitrary $D_0$ satisfies (1) but has time-dependent moments, and the results fail; with $\sigma = 0$ the ratio form would be false. Both cases are excluded by the structure, not by vacuous hypotheses. The structure is satisfiable: i.i.d. standard Gaussian demands on $\mathbb Z \to \mathbb R$ form an instance.

A complete development needs: the $L^2$ series representation of a stationary AR(1) process; distributional symmetry facts for i.i.d. sequences with a symmetric law; and covariance bookkeeping for finite linear combinations. The first two are reusable for any linear time-series model with symmetric innovations. Contributions to any milestone, and to general lemmas about stationary AR(1) processes, are welcome.

Selected references

• F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
• J. D. Sterman, Modeling Managerial Behavior: Misperceptions of Feedback in a Dynamic Decision Making Experiment, Management Science 35(3):321–339, 1989. https://doi.org/10.1287/mnsc.35.3.321
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
• J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Northwestern University, 1997 (cited by the paper for the proofs of Lemma 2.1 and Theorem 3.1).

Motivation

Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.

In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has $2^{\Omega(\sqrt n)}$ inequalities.

Timeline.

• 1990: De Simone shows that the correlation polytope is linearly isomorphic to the cut polytope.
• 1991: Yannakakis proves the factorization theorem (extension complexity equals the nonnegative rank of a slack matrix) and the exponential lower bound for symmetric formulations of the TSP and perfect matching polytopes.
• 1992: Razborov proves the distributional lower bound for set disjointness.
• 2003: de Wolf shows that the support of $M(n)_{ab}=(1-a^\top b)^2$ needs $2^{\Omega(n)}$ rectangles to cover.
• 2012/2015: Fiorini et al. prove $\mathrm{xc}(\mathrm{CUT}(n))=2^{\Omega(n)}$, $\mathrm{xc}(\mathrm{TSP}(n))=2^{\Omega(\sqrt n)}$, and a $2^{\Omega(\sqrt n)}$ bound for stable set polytopes of some graphs on $n$ vertices.
• 2013: Kaibel and Weltge give a short combinatorial proof of the correlation-polytope bound, with constant $C=\log_2(3/2)$.
• 2014: Rothvoss proves $2^{\Omega(n)}$ for the perfect matching polytope.

Setting

Let $\iota$ be a finite index set. An extended formulation (EF) of a set $P\subseteq\mathbb R^{\iota}$ is a linear system $E^{=}x+F^{=}y=g^{=}$, $E^{\le}x+F^{\le}y\le g^{\le}$ in variables $(x,y)\in\mathbb R^{\iota}\times\mathbb R^{k}$ such that $x\in P$ exactly when some $y$ satisfies it. Its size is the number of inequalities. The extension complexity $\mathrm{xc}(P)$ is the least size of an EF of $P$.

A polytope is the convex hull of finitely many points. A face of $P$ is $P$ itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope $Q$ is an extension of $P$ if $\pi(Q)=P$ for some linear map $\pi$. Given $P=\{x : Ax\le b\}=\mathrm{conv}(V)$, the slack matrix has entries $S_{ij}=b_i-A_iv_j$. The nonnegative rank $\mathrm{rank}_+(M)$ is the least $r$ with $M=TU$, where $T\ge 0$ has $r$ columns and $U\ge 0$ has $r$ rows.

For $n$-bit strings $a,b$, $a^\top b$ is the number of common ones, and $M(n)$ is the $2^n\times 2^n$ matrix $M_{ab}=(1-a^\top b)^2$. A 1-monochromatic rectangle cover of its support is a family of products $R_1\times R_2$, each containing only entries with $M_{ab}\ne 0$, that together contain all of them.

On the complete graph $K_n=(V_n,E_n)$, $\chi^F\in\mathbb R^{E_n}$ is the characteristic vector of an edge set $F$ and $\delta(X)$ is the cut of $X\subseteq V_n$. The polytopes are

$$\mathrm{CUT}(n)=\mathrm{conv}\{\chi^{\delta(X)}\},\qquad \mathrm{COR}(n)=\mathrm{conv}\{bb^\top : b\in\{0,1\}^n\}\subseteq\mathbb R^{n\times n},$$ $$\mathrm{TSP}(n)=\mathrm{conv}\{\chi^F : F\subseteq E_n \text{ is a tour (Hamiltonian cycle) of } K_n\}.$$

Formalization targets

Goal: Theorem 12

$$\exists\,C>0\ \exists\,N\ \forall n\ge N:\qquad \mathrm{xc}(\mathrm{TSP}(n))\ \ge\ 2^{C\sqrt n}.$$

The constant is left unfixed, so the goal survives any improvement of it.

Milestones, in attack order

• Razborov's distributional bound (displayed in the proof of Theorem 1) and Theorem 1: every 1-rectangle cover of the support of $M(n)$ has $2^{\Omega(n)}$ rectangles.
• Lemma 2 and Theorem 3 (Yannakakis): $\mathrm{rank}_+(S)\le r$ $\iff$ an extension with at most $r$ facets $\iff$ an EF with at most $r$ inequalities.
• Theorem 4: $\mathrm{rank}_+(M)$ is at least the rectangle covering bound of its support (already proved on the platform, referenced).
• Theorem 5: $\mathrm{COR}(n)$ is linearly isomorphic to $\mathrm{CUT}(n+1)$. Lemma 6: $\langle 2\,\mathrm{diag}(a)-aa^\top,x\rangle\le 1$ is valid for $\mathrm{COR}(n)$, with slack $M_{ab}$ at $bb^\top$.
• Theorem 7: $\mathrm{xc}(\mathrm{CUT}(n+1))=\mathrm{xc}(\mathrm{COR}(n))\ge 2^{Cn}$.
• Lemma 9: $\mathrm{xc}$ does not increase under taking faces or linear images. Lemma 11: $\mathrm{TSP}(q)$ with $q=O(n^2)$ has a face that is an extension of $\mathrm{COR}(n)$.
• Stable sets: Lemma 8 and Theorem 10, $\mathrm{xc}(\mathrm{STAB}(G_n))=2^{\Omega(\sqrt n)}$ for some graph $G_n$ on $n$ vertices.

Significance

The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.

Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.

Difficulty

The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because $M(n)$ has rank $O(n^2)$. The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of $\mathrm{TSP}(q)$ with $q=O(n^2)$. Theorem 12 also needs a monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ that the paper only indicates.

Formalization scope

• Everything is over $\mathbb R$. Points of $\mathbb R^d$ are functions $\iota\to\mathbb R$ on a finite type. $\mathbb R^{E_n}$ has one coordinate per unordered edge of $K_n$ (non-diagonal elements of Sym2 (Fin n)). $\mathbb R^{n\times n}$ is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.
• $\mathrm{xc}$ and $\mathrm{rank}_+$ are natural numbers (sInf of the attainable sizes), never $\infty$, so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.
• Every $2^{\Omega(f(n))}$ is $\exists C>0\,\exists N\,\forall n\ge N$, $2^{Cf(n)}\le\cdot$ (real power). Every $O(n^2)$ is a constant $c$ with $\le c\,n^2$, uniform in $n$.
• Theorem 7 and Lemma 11 carry an added $n\ge 1$: at $n=0$ the printed statements fail, since $\mathrm{COR}(0)$ is a point with $\mathrm{xc}=0$ and no positive $q\le c\cdot 0$ exists.
• "Linearly isomorphic" in Theorem 5 is an injective linear map carrying $\mathrm{CUT}(n+1)$ onto $\mathrm{COR}(n)$, because the two ambient spaces have different dimensions.
• In Theorem 3, $\dim P\ge 1$ is "$P$ has two distinct points". Faces include $\emptyset$ and $P$, facets are maximal proper faces, and facets are counted with an explicit finite family.
• Ruled out: a TSP polytope over ordered pairs, all cycles or directed tours, a weakened isomorphism in Theorem 5, and an extension complexity valued in $\mathbb N\cup\{\infty\}$ that is infinite on a broken EF definition.
• Welcome contributions: proofs of any milestone, in particular Lemma 2 and the factorization theorem (reusable for every later extension-complexity result), Theorem 5, and the face construction of Lemma 11; a proof of the monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ as a supporting lemma.

Selected references

• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, J. ACM 62(2), Art. 17, 2015. https://doi.org/10.1145/2716307
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. Syst. Sci. 43(3), 441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• A. A. Razborov, On the distributional complexity of disjointness, Theoret. Comput. Sci. 106(2), 385–390, 1992. https://doi.org/10.1016/0304-3975(92)90260-M
• R. de Wolf, Nondeterministic quantum query and communication complexities, SIAM J. Comput. 32(3), 681–699, 2003. https://doi.org/10.1137/S0097539702407345
• C. De Simone, The cut polytope and the Boolean quadric polytope, Discrete Math. 79(1), 71–75, 1990. https://doi.org/10.1016/0012-365X(90)90056-N
• V. Kaibel, S. Weltge, A short proof that the extension complexity of the correlation polytope grows exponentially, Discrete Comput. Geom. 53, 397–401, 2015. https://doi.org/10.1007/s00454-014-9655-9
• T. Rothvoss, The matching polytope has exponential extension complexity, J. ACM 64(6), Art. 41, 2017. https://doi.org/10.1145/3127497

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$. Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$, so $D(0) = H(0) = 0$. For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$, let $\tilde C(i) = c_i - H(i-1)$, and let

$$S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)$$

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$.

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$,

$$F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).$$

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$.

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$, with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$. Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$.

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$. The $j$th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$, for every potential cumulative demand in some open interval above $D(j)$.

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$, ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$, with equal $\tilde C$-values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$. Then

$$S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}$$

Milestones

In attack order:

• identity (1a) for the carrying costs;
• Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$;
• the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$;
• the strict chains (7)–(8) of the Appendix;
• Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$;
• Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$, $g(k+1) \le g(k)$ removes $i_k$, and $g(r) = \infty$ removes $i_r$.

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$, up to a term that does not depend on $l$.

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$, and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

• equal slopes, where $G = \pm\infty$;
• several lines meeting at one point;
• the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$, read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

• Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$. Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
• Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final "$< \infty$" of (6) is part of the condition.
• Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
• Disclosed change 1, $\Omega(j)$. The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$. This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$".
• Disclosed change 2, Lemma 2(d). The printed hypothesis "$c_{k,l} < c_l$" duplicates part (c) and is read as "$c_{k,l} = c_l$". The equivalence "$\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$" is stated under $A(k,l) \ne 0$, since $A(k,l) = 0$ gives $G = +\infty$ by (5).
• Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$: rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$, never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
• Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
• Reusable infrastructure. The model, the recursion (2), $A$, $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
• H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
• 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(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
• A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$. It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$. In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$, has the form

$$C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}$$

The paper's standing assumptions on $G$ are:

1. $-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
2. $\lim_{|y|\to\infty}G(y)=\infty$.

The sequence $y_Q$. Let $y_1$ be an integer minimizing $G$. Given $y_1,\dots,y_Q$, let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$, and set

$$y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}$$

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$, and

$$C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .$$

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$, $Q=1$, $C^*=S$, $r=y_1-1$, $R=y_1+1$. Each pass compares $G(r)$ and $G(R)$; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$. The output is the final $(r,Q)$.

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$, stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

$$C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .$$

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

• §2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$.
• Figure 1 (p. 809): $y_{Q+1}$ has the least $G$-value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$.
• Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$.
• Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$.
• Display before (6): $\min_r C(r,Q)=C^*(Q)$.
• (6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$, and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$.
• Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
• Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$.

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$, an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$. Because it uses only the form (1) and the unimodality of $-G$, it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$.

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$.

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$, and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$: "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$, not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$, and fails for constant $G$.

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$, $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

• Types. $G:\mathbb Z\to\mathbb R$, $\kappa\in\mathbb R$ with $\kappa>0$, reorder points in $\mathbb Z$, order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$, so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$.
• Assumptions. "$-G$ unimodal" is NegUnimodal G: $\exists m$, $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$. "$\lim_{|y|\to\infty}G=\infty$" is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$-weights it holds for every function.
• The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$, as the paper defines them, is the first milestone.
• The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$, $C^*\le G(R)$; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
• Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$, under the paper's simplification $y_1>0$; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$, which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
• Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
• Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$. Lemma 2's "$Q^*$" is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise "$r^*(Q)=L(Q)-1$" means $L(Q)-1$ is an optimal reorder point.
• Ruled out. Defining the algorithm's output as an argmin of $C$, or by searching for Lemma 2's $q$, would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

• 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
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
• H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
• I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

Motivation

Myerson's optimal auction (Myerson 1981) maximizes a seller's expected revenue when buyers have independent private values, but it is a sealed-bid mechanism: every buyer reports a value, and the allocation and payments are computed from all reports at once. Real sellers more often post prices: buyers arrive, each sees a take-it-or-leave-it price, and buys or leaves. Chawla, Hartline, Malec and Sivan (arXiv:0907.2435) ask how much revenue such simple mechanisms lose. Their strongest notion is the order-oblivious posted-price mechanism (OPM): the prices are fixed in advance, and the guarantee must hold whatever order the buyers arrive in, even an adversarial one.

The tool behind the guarantee for sellers of $k$ identical units is a prophet inequality. In the single-choice version, a gambler inspects independent random rewards one at a time and must accept or reject each on the spot; Krengel and Sucheston, and Samuel-Cahn (Ann. Probab. 1984), showed that a single fixed threshold earns at least half of what a prophet who sees all rewards earns. The paper extends Samuel-Cahn's threshold rule to $k$ choices (Appendix D.2) and turns it into a revenue guarantee (Theorem 10).

Setting

There are $n$ agents $[n]$. Agent $i$'s value $v_i$ for being served is drawn independently from a distribution $F_i$ with density $f_i$; the virtual valuation is $\phi_i(v) = v - (1 - F_i(v))/f_i(v)$ (Definition 1), and $F_i$ is regular if $\phi_i$ is non-decreasing (Definition 2). The seller may serve any set of agents in a downward-closed set system $\mathcal J$; this mission uses the $k$-uniform matroid, where a set is feasible exactly when it has at most $k$ members.

A mechanism $M$ maps reported values $\mathbf v$ to an allocation $M(\mathbf v) \in \mathcal J$ and payments $\pi_i(\mathbf v)$. It is truthful if reporting the true value is a dominant strategy and no agent ever gets negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_{\mathbf v}[\sum_i \pi_i(\mathbf v)]$, and $\mathcal R^{\mathcal M}$ denotes the revenue of Myerson's mechanism, the largest over truthful mechanisms (Theorem 19).

Given prices $\mathbf p$ and values $\mathbf v$, agent $i$ desires service if $v_i \ge p_i$. Let $\mathcal S_{\mathbf v}$ be the class of maximal feasible sets of desiring agents. When agents arrive in an arbitrary order and each buys if it desires service and can still be feasibly served, the set of buyers lies in $\mathcal S_{\mathbf v}$. The paper's pessimistic revenue estimate is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{\mathbf v \sim \mathbf F}\ \min_{S \in \mathcal S_{\mathbf v}} \sum_{i \in S} p_i .$$

For the prophet inequality, $X_1, \dots, X_n$ are independent nonnegative random variables with order statistics $X_{(1)} \ge \dots \ge X_{(n)}$, and $(x)^+ = \max(0, x)$. The threshold rule with threshold $c$ picks indices $t_1(c), \dots, t_k(c)$, where $t_i(c)$ is the lesser of $n-k+i$ and the $i$-th smallest index $j$ with $X_j \ge c$ (or $n - k + i$ if there is none). The numbers $a^*$ and $b^*$ are the unique solutions of

$$a = \sum_{i=1}^k \mathbb E\big(X_{(i)} - a/k\big)^+, \qquad b = \sum_{i=1}^n \mathbb E\big(X_i - b/k\big)^+ .$$

Formalization targets

Goal: Theorem 10 (p. 9)

$$\exists\, \mathbf p\ \ \forall M \text{ truthful}:\qquad \mathcal R^M \le 2\, \mathcal R^{\mathrm{obl}}_{\mathbf p}$$

for every instance with regular distributions and a $k$-uniform matroid constraint. The prices are chosen once, before the mechanism it is compared with; this is the paper's "$\mathcal R^{\mathrm{obl}}_{\mathbf p}$ 2-approximates $\mathcal R^{\mathcal M}$".

Milestones

1. Proposition 1 (p. 5): under regularity, the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$ (with the lowest type receiving zero utility).
2. $a^*$ and $b^*$ exist and are unique (App. D.2, p. 18).
3. The claim $a^* \le b^*$ (App. D.2, p. 18).
4. Theorem 24 (p. 18), the $k$-choice prophet inequality: for $a^* \le k c \le b^*$,

$$\sum_{i=1}^k \mathbb E\big[X_{(i)}\big] \le 2 \sum_{i=1}^k \mathbb E\big[X_{t_i(c)}\big].$$

Significance

The theorem says that a seller of $k$ identical units can fix one price per buyer, ignore the arrival order entirely, and still collect half of the optimal revenue. The factor 2 is tight: Appendix D.2 gives a single-item example with two buyers where no order-oblivious pricing does better. Corollary 11 extends the result to partition matroids, and Theorem 24 is reused for the graphical-matroid result (Theorem 12, App. D.3). Theorem 24 is a statement in optimal stopping independent of mechanism design, and $k$-choice prophet inequalities are now a standard tool for online allocation.

The results are proved in the paper (preprint arXiv:0907.2435v2; a conference version appeared at STOC 2010). To our knowledge none of them, nor any prophet inequality, has a machine-checked proof; Mathlib has independence of random variables but no order statistics, stopping-rule prophet inequalities, or Myerson's revenue characterization in this multi-agent dominant-strategy form. A related single-unit, Bayesian-incentive-compatible form of Proposition 1 exists on the platform (MechanismDesign.Auctions.revenue_eq_virtual_surplus), in a different model.

Difficulty

The threshold rule picks the first values above $c$, not the largest, and its picks are dependent random indices; the expectation $\mathbb E[X_{t_i(c)}]$ does not factor. The obvious comparison of the gambler with the prophet term by term fails, because the gambler can exhaust its $k$ picks on early, small values. The bound has to balance two events: either at least $k$ values reach $c$, or a value is picked whenever it exceeds $c$; independence enters exactly in the second. The rule also has forced picks at the end of the sequence, which must be handled as stated.

On the mechanism side, $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a minimum over an adversarially chosen family, not the revenue of one run, so it cannot be read off from a single sequential mechanism. Proposition 1 needs the full revenue-equivalence argument: monotone allocations, the payment identity, and an integration by parts against the density.

Formalization scope

• Distributions: each $F_i$ has a bounded support $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i$, and a measurable density positive on it (a pinned convention; the paper says only "with density $f_i$"). Regularity is required on the support. The prior is the product of the marginals.
• Mechanisms: deterministic, dominant-strategy incentive compatible and ex-post individually rational on the type space, with measurable allocation events and measurable, integrable payments. Payments of unserved agents are not forced to be zero.
• $\mathcal R^{\mathcal M}$ is not constructed. The goal is stated against every truthful mechanism, which by Theorem 19 is equivalent. Quantifier order matters: "for every mechanism there are prices" is a weaker statement and is not the goal.
• Proposition 1 carries the normalization that an agent of the lowest type gets zero utility, which the paper presupposes on p. 12.
• $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over the finite, nonempty family $\mathcal S_{\mathbf v}$; maximality is essential, since without it the empty set makes the estimate $0$ and the goal false. Prices are arbitrary reals.
• $a^*$ and $b^*$ are characterised by their equations as hypotheses, not defined by an infimum. Order statistics count multiplicity. Lean indices are 0-based. The threshold rule includes the page's forced picks $t_i(c) = n - k + i$; it is not replaced by a pure threshold rule. Theorem 24 and the claims about $a^*, b^*$ assume $1 \le k \le n$; the goal assumes nothing about $k$.
• Out of scope: non-regular distributions (ironing), Corollary 11, and the p. 19 identity rewriting $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ as a sum of virtual values (a proof step, not a milestone).

Useful reusable infrastructure: order statistics and their measurability, Samuel-Cahn-type threshold rules, and Myerson's payment identity for dominant-strategy mechanisms. Proofs of any milestone, and supporting lemmas on these objects, are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010 (STOC 2010). https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150