Operations Research

Motivation

A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor $\beta<1$, Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem ($\beta=1$) is harder, because total income is typically infinite.

David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats $\beta=1$ as a limit of $\beta<1$. Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to $1$. Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).

Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of $V_\beta$ in $1-\beta$ and $n$-discount optimality.

Setting

There are finitely many states $s$ and a finite set $A$ of actions, every action available in every state. In state $s$, action $a$ yields income $i(s,a)\in\mathbb R$ (any sign) and moves the system to state $s'$ with probability $q(s'\mid s,a)$; each $q(\cdot\mid s,a)$ is a probability vector.

A decision rule is a function $f$ from states to actions; $F$ is the finite set of decision rules. A policy is a sequence $\pi=\{f_n,\ n=1,2,\dots\}$ in $F$: on day $n$, in state $s$, action $f_n(s)$ is used. Policies are deterministic and Markov but may change with time. The policy $(f,\pi)$ uses $f$ on day $1$ and then follows $\pi$; $f^{(\infty)}$ uses $f$ every day and is called stationary.

For $f\in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s'\mid s,f(s)))_{s,s'}$. With $Q_0(\pi)=I$ and $Q_n(\pi)=Q(f_1)\cdots Q(f_n)$, the return of $\pi$ at discount factor $0\le\beta<1$ is

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n\,Q_n(\pi)\,r(f_{n+1}),$$

a vector indexed by the initial state. Vectors are compared coordinatewise; $w_1>w_2$ means $w_1\ge w_2$ and $w_1\ne w_2$.

A policy $\pi^*$ is $\beta$-optimal if $V_\beta(\pi^*)\ge V_\beta(\pi)$ for every policy $\pi$. Following §4 of the paper, a policy is optimal if it is $\beta$-optimal for all $\beta$ sufficiently near $1$.

Formalization targets

Goal: Theorem 5

There exist a decision rule $f$ and $\beta_0<1$ such that

$$V_\beta(f^{(\infty)})\ \ge\ V_\beta(\pi)\qquad\text{for all }\beta\in(\beta_0,1)\text{ and all policies }\pi.$$

One $f$ and one $\beta_0$ serve every competing policy and every $\beta\in(\beta_0,1)$.

Milestones

1. The composition rule $V_\beta(f,\pi)=L(f)V_\beta(\pi)$, with $L(f)w=r(f)+\beta Q(f)w$, and its $N$-fold version (§2).
2. Theorem 1: if $V_\beta(f,\pi^*)\le V_\beta(\pi^*)$ for all $f\in F$, then $\pi^*$ is $\beta$-optimal.
3. Theorem 2: if $V_\beta(f,\pi)>V_\beta(\pi)$ then $V_\beta(f^{(\infty)})>V_\beta(\pi)$.
4. Theorem 3 (policy improvement): if no action improves $f^{(\infty)}$ by one step, $f^{(\infty)}$ is $\beta$-optimal; otherwise switching to improving actions gives $g^{(\infty)}>f^{(\infty)}$.
5. Corollary: for each fixed $\beta\in[0,1)$ some stationary policy is $\beta$-optimal.
6. Each coordinate of $V_\beta(f^{(\infty)})$ is a rational function of $\beta$ on $[0,1)$ with nonvanishing denominator.
7. Some $f^*$ is $\beta$-optimal for a set of $\beta$'s having $1$ as a limit point.
8. If $V_\beta(f^{*(\infty)})\ge V_\beta(g^{(\infty)})$ for a set of $\beta$'s accumulating at $1$, then it holds for all $\beta$ near $1$.

Significance

The result. Theorem 5 shows that the infinitely many discounted problems near $\beta=1$ share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.

Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in $\beta$, both reusable for any finite-state discounted model.

Difficulty

The Corollary gives, for each $\beta$, some optimal stationary policy, and $F$ is finite, so one $f^*$ is $\beta$-optimal for infinitely many $\beta$ accumulating at $1$. The obvious argument stops there: optimality on a sequence of $\beta$'s says nothing about the $\beta$'s in between, and a pointwise limit argument cannot produce a whole interval $(\beta_0,1)$. The step that fails is passing from "frequently" to "eventually", and it needs structural information about how $V_\beta$ depends on $\beta$, not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every $\beta$ near $1$.

Formalization scope

States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from $0$ (π 0 is Blackwell's $f_1$). Incomes are real-valued with no sign restriction. The law of motion law s a s' $=q(s'\mid s,a)$ satisfies the published predicate IsTransitionKernel. $Q_n(\pi)$ is the ordered matrix product and $V_\beta(\pi)$ is the tsum of the series, which converges absolutely for $0\le\beta<1$; every statement at a fixed $\beta$ assumes $0\le\beta<1$, and nothing is stated for $\beta\ge1$. Vector inequalities are coordinatewise, and the strict order is "$\ge$ and $\ne$", not coordinatewise strict. "$\beta$ sufficiently near $1$" is "there is $\beta_0<1$ such that for every $\beta\in(\beta_0,1)$". The paper's §4 phrase $V_\beta(\pi)=U(\beta)$ is encoded as $\beta$-optimality, so no supremum over policies appears.

The word "optimal" has two meanings in the paper: at one fixed $\beta$ (§3, the Corollary) and for all $\beta$ near $1$ (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single $\beta$, with "there exists $\beta$", for a set of $\beta$'s accumulating at $1$, or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.

Needed infrastructure: summation and shifting of the discounted series, Neumann series $(I-\beta Q)^{-1}=\sum_n\beta^nQ^n$ for stochastic $Q$, Cramer's rule to express $(I-\beta Q)^{-1}r$ as a ratio of polynomials in $\beta$, and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, Technology Press and Wiley, 1960.
• A. F. Veinott Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999 (Proposition 6.2.3, Blackwell optimality for finite models). https://doi.org/10.1002/9780470317037

Motivation

Many problems in convex optimization, variational inequalities and equilibrium modelling reduce to finding a point $x$ with $0 \in A x + B x$, where $A$ and $B$ are maximal monotone operators on a real Hilbert space $\mathcal H$: for example, minimizing $f + g$ for closed proper convex $f, g$ is the case $A = \partial f$, $B = \partial g$. When the resolvent of $A + B$ is hard to evaluate but the resolvents of $A$ and $B$ separately are easy, one uses a splitting method. Douglas–Rachford splitting, introduced for monotone operators by Lions and Mercier (1979) after an alternating-direction scheme of Douglas and Rachford (1956) for the heat equation, is the most widely used one; through its dual form it underlies the alternating direction method of multipliers (ADMM) used throughout large-scale optimization and statistics.

Eckstein and Bertsekas (MIT report LIDS-P-1919, 1989; Mathematical Programming 55, 1992) showed that Douglas–Rachford splitting is a special case of the proximal point algorithm applied to a single derived operator, the splitting operator $S_{\lambda,A,B}$. This identification lets the convergence theory of the proximal point algorithm transfer to splitting, and yields a generalized method with inexact resolvent evaluations and relaxation.

Timeline.

• Minty (1962): a monotone $T$ is maximal iff $I + T$ is onto.
• Rockafellar (1976): the proximal point algorithm with variable stepsizes and summable errors converges weakly to a zero.
• Lions and Mercier (1979): Douglas–Rachford splitting for maximal monotone $A$, $B$; its map $G_{\lambda,A,B}$ is firmly nonexpansive.
• Gol'shtein and Tret'yakov (1979): relaxed proximal iterations with factors $\rho_k \in (0,2)$, in finite dimension, with a fixed stepsize.
• Eckstein and Bertsekas (1989/1992): the splitting operator; Douglas–Rachford as a proximal point method; the generalized proximal point algorithm and the generalized Douglas–Rachford method, including the case with no solution.

Setting

An operator on $\mathcal H$ is a subset $T \subseteq \mathcal H \times \mathcal H$, with $Tx = \{y \mid (x,y) \in T\}$; it may be multivalued and partially defined. Its domain is $\operatorname{dom} T = \{x \mid Tx \ne \emptyset\}$, its image $\operatorname{im} T$ the projection on the second coordinate, its inverse $T^{-1} = \{(y,x) \mid (x,y) \in T\}$. Scaling and sum are $cT = \{(x, cy)\}$ and $A + B = \{(x, y+z) \mid (x,y) \in A, (x,z) \in B\}$; $I$ is the identity. $T$ is monotone if $\langle x' - x, y' - y\rangle \ge 0$ for all $(x,y),(x',y') \in T$, and maximal monotone if no other monotone operator strictly contains it. The resolvent is $J_{cT} = (I + cT)^{-1}$, and $\operatorname{zer} T = \{x \mid 0 \in Tx\}$. An operator $J$ is firmly nonexpansive if $\|y'-y\|^2 \le \langle x'-x, y'-y\rangle$ for all $(x,y),(x',y') \in J$.

For $\lambda > 0$ the Douglas–Rachford map is $G_{\lambda,A,B} = J_{\lambda A} \circ (2J_{\lambda B} - I) + (I - J_{\lambda B})$, and the splitting operator is

$$S_{\lambda,A,B} = \{(v + \lambda b,\ u - v) \mid (u,b) \in B,\ (v,a) \in A,\ v + \lambda a = u - \lambda b\}.$$

Its zero set is $Z^*_\lambda = \{u + \lambda b \mid b \in Bu,\ -b \in Au\}$.

Formalization targets

Goal: Theorem 7 (generalized Douglas–Rachford splitting)

Let $A$, $B$ be maximal monotone, $\lambda > 0$, and let $\{z^k\}, \{u^k\}, \{v^k\} \subseteq \mathcal H$, $\alpha_k, \beta_k \ge 0$ and $\rho_k$ satisfy

$$\|u^k - J_{\lambda B}(z^k)\| \le \beta_k,\quad \|v^{k+1} - J_{\lambda A}(2u^k - z^k)\| \le \alpha_k,\quad z^{k+1} = z^k + \rho_k (v^{k+1} - u^k),$$

with $\sum \alpha_k < \infty$, $\sum \beta_k < \infty$ and $0 < \inf \rho_k \le \sup \rho_k < 2$. Then

$$\operatorname{zer}(A+B) \ne \emptyset \implies z^k \rightharpoonup z^* \text{ for some } z^* \in Z^*_\lambda,\qquad \operatorname{zer}(A+B) = \emptyset \implies \{z^k\} \text{ unbounded}.$$

Milestones

In the paper's order: Minty's theorem (Theorem 1); properties of firmly nonexpansive operators (Lemma 1); the monotone / firmly nonexpansive correspondence (Theorem 2, Corollaries 2.1–2.3); zeros as fixed points of resolvents (Lemma 2); the generalized proximal point algorithm (Theorem 3): weak convergence to a zero of $T$ under summable errors, relaxation in $(0,2)$ and stepsizes bounded away from $0$, unboundedness when $\operatorname{zer} T = \emptyset$; (maximal) monotonicity of $S_{\lambda,A,B}$ (Theorem 4) and firm nonexpansiveness of its resolvent (Corollary 4.1); $\operatorname{zer} S_{\lambda,A,B} = Z^*_\lambda$ (Theorem 5); and $(I + S_{\lambda,A,B})^{-1} = G_{\lambda,A,B}$ (Theorem 6).

Significance

Theorem 7 gives convergence of Douglas–Rachford splitting with both resolvents evaluated inexactly and with over- or under-relaxation, and it characterizes the case without a solution: the iterates are unbounded exactly when $A + B$ has no zero. The relaxed, inexact form is the one implementations actually run, and through Gabay's identification of ADMM with Douglas–Rachford on the dual it is the basis of the paper's Theorem 8, a convergence theorem for a generalized ADMM. Theorem 3, used to prove Theorem 7, is itself a standard reference form of the inexact relaxed proximal point algorithm.

All results here are proved in the paper (one step in the unbounded case of Theorem 3 rests on results of Rockafellar 1969 and 1970 on sums of maximal monotone operators). As of 2026, neither Douglas–Rachford splitting in this generality nor the generalized proximal point algorithm is formalized in Lean or Mathlib. Mathlib has Hilbert spaces, weak topologies and summability, but no theory of maximal monotone operators, Minty's theorem or resolvents. The mission builds that layer and machine-checks the paper's results on it.

Difficulty

The convergence argument cannot be strong: in infinite dimensions the proximal point algorithm need not converge in norm (Güler 1991), so the conclusion is weak convergence, and identifying the weak limit as a zero requires the weak–strong closedness of the graph of a maximal monotone operator. The maximality halves of Theorems 2 and 4 need Minty's theorem, whose proof requires a nontrivial existence argument (all known proofs use Zorn's lemma or an equivalent). The unbounded case of Theorem 3 is a contradiction argument that truncates $T$ by the subdifferential of the indicator of a ball and invokes two external facts: maximality of the sum of two maximal monotone operators under an interiority condition (Rockafellar 1970), and existence of zeros for maximal monotone operators with bounded domain (Rockafellar 1969). Neither is available in Lean. The natural first idea for Theorem 7, iterating the firm nonexpansiveness of $G_{\lambda,A,B}$, gives neither the error tolerance on both resolvents nor the unbounded case without the full machinery of Theorem 3.

Formalization scope

• $\mathcal H$ is a real inner product space that is complete ([CompleteSpace H]). An operator is a map H → Set H. Monotonicity, maximal monotonicity, $\operatorname{dom}$, $\operatorname{zer}$ and the function-level resolvent predicate IsResolvent are the published definitions ThreeOpSplitting_Convergence_MonotoneOperators; weak convergence is the published WeakTendsto ($\langle z^k, y\rangle \to \langle z^*, y\rangle$ for every $y$).
• §2 notions are graph notions (opResolvent, IsFirmlyNonexpansiveOp, ...), so Theorem 2 and Corollary 2.1 can speak of resolvents that are a priori partial or multivalued. In Theorems 3, 6 and 7 the resolvents are maps $J : \mathcal H \to \mathcal H$ with $\lambda^{-1}(x - J x) \in A(Jx)$ for all $x$, unique by Corollary 2.2.
• $S_{\lambda,A,B}$ is defined by its set formula, not as $G_{\lambda,A,B}^{-1} - I$; with the latter, Theorem 6 and Corollary 4.1 would be unfoldings. Taking free resolvent functions without the IsResolvent hypothesis would make the iteration unrelated to $A$ and $B$; the hypothesis is always present.
• $\inf \rho_k > 0$, $\sup \rho_k < 2$ are encoded as $\exists\, \rho_1, \rho_2$ with $0 < \rho_1 \le \rho_k \le \rho_2 < 2$; $\inf c_k > 0$ as $\exists\, c_0 > 0$, $c_0 \le c_k$. Summability is Summable with nonnegative terms. Sequences start at $k = 0$; $v^0$ is unused. Unboundedness is ¬ Bornology.IsBounded (Set.range z).
• Printed slips corrected and disclosed in the items: Theorem 7 states its sequences in $\mathbb R^n$ (read $\mathcal H$); Theorem 3 prints $(1 - \rho_k) w^k$ (read $\rho_k w^k$, as on p. 9 and in the proof) and $(I + cT)^{-1}$ (read $(I + c_k T)^{-1}$).
• Not included: Corollary 2.4, Corollaries 6.1–6.2 (special cases of Theorem 7), §5 (partial inverses, generalized ADMM). The second sentence of Corollary 6.1 (convergence of $J_{\lambda B}(z^k)$) is deliberately excluded: its argument does not transfer weak convergence (Svaiter 2011).
• Welcome contributions: Minty's theorem in Hilbert space, the resolvent calculus of §2, and weak-limit lemmas (Opial-type arguments) are reusable well beyond this mission.

Selected references

• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, MIT report LIDS-P-1919, 1989; Mathematical Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
• P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16 (1979) 964–979. https://doi.org/10.1137/0716071
• G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962) 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM J. Control Optim. 29 (1991) 403–419. https://doi.org/10.1137/0329022
• B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM J. Control Optim. 49 (2011) 280–287. https://doi.org/10.1137/100788100

Motivation

A manufacturer that makes one product to stock faces random demand, can produce at most $b$ units per period, and can store at most $U$ units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level $\bar y$ each period. With a production limit, the natural modification is to produce up to $\bar y$ when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.

Timeline.

• 1950s–60s: optimality of base-stock (critical-number) policies for uncapacitated periodic-review models; see Heyman and Sobel's Stochastic Models in Operations Research, Vol. II (1984).
• 1986: Federgruen and Zipkin, Part I (average cost, MOR 11(2):193–207) and Part II (discounted cost, MOR 11(2):208–215) establish the capacitated case. Part I handles the unbounded state space with a general average-cost theory for countable-state Markov decision processes by Federgruen, Schweitzer and Tijms (1983).

Setting

Time is divided into periods $t = 0, 1, \dots$. The demands $D_0, D_1, \dots$ are independent copies of a random variable $D$ with values in $\{0, 1, 2, \dots\}$ and probability mass function $p(j)$; write $\mu = E(D)$ and $P(j) = \Pr\{D \le j\}$. At the start of period $t$ the inventory is an integer $x_t$ (negative values are backorders). The decision maker raises it to

$$y_t \in Y(x_t) = \{y \in \mathbb Z : x_t \le y \le x_t + b,\ y \le U\},$$

pays the expected one-period cost $G(y_t)$, and demand is subtracted: $x_{t+1} = y_t - D_t$. The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.

The standing assumptions are: $G \ge 0$ is convex and $G(y) \to \infty$ as $|y| \to \infty$ (Assumption 1); the characteristic function of $D$ is analytic at the origin (Assumption 2), and $0 < \mu$; $G(y) \le A + B|y|^\rho$ for some positive integer $\rho$ (Assumption 3); $b > \mu$ and $P(b) < 1$ (Assumption 4). The smallest global minimizer of $G$ is $\bar y^\infty$, and $U \ge \bar y^\infty$.

A Markov policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of maps with $\pi_t(x) \in Y(x)$. The critical-number policy with critical number $\bar y$ is $\delta[\bar y](x) = \max(x, \min(\bar y, x + b))$. A stationary policy $\delta$ is strongly optimal with average cost $g$ if, from every initial state $x \le U$, its average cost $t^{-1}E\{\sum_{i<t} G(y_i)\}$ converges to $g$, while every Markov policy has lim-inf average cost at least $g$ from every initial state.

The analysis uses the operators $Rv(y) = G(y) + E\,v(y - D)$ and $Sv(x) = \min_{y \in Y(x)} Rv(y)$, and the optimality equation

$$g + v(x) = Sv(x),\qquad x \le U. \tag{6}$$

For an interval $\iota = [l, u]$, $H_\iota v(x)$ is the largest expected sum of $v(y_t)$, over policies forced to produce at capacity below $l$ and to produce nothing above $u$, until the inventory first returns to $\iota$.

Formalization targets

Goal: Theorem 1 (p. 202)

There exist $g^*$, $v^*$ and $y^* \ge \bar y^\infty$ such that $(g^*, v^*)$ solves (6), $v^*$ is convex with global minimizer $y^*$, and

$$\delta^* = \delta[y^*] \text{ is strongly optimal with average cost } g^*.$$

The $y^*$ in the optimality claim is the minimizer constructed in part (a).

Milestones

• Lemma 2(a)–(c) (pp. 196–197): a normal-tail inequality and two series estimates.
• Lemma 3 (p. 198): if $v(x) = O(|x|^q)$ then $H_\iota v(x) = O(|x|^{q+3})$.
• Corollary 1 (p. 200): $H_\iota 1 = O(|x|^3)$ and $H_\iota G = O(|x|^{\rho+3})$, both finite.
• Corollary 2 (p. 201): $(t+1)^{-1}P[\delta_{0t}]\cdots P[\delta_{tt}](H_\iota 1 + H_\iota G)(x) \to 0$.
• Lemma 4 (p. 201): reachability of every state in $[L, U - D_-]$ under some policy that produces at capacity below $L$.
• Lemma 5 (p. 202): $S$ and $Q$ preserve the class $V$ of convex functions of growth $O(|x|^{\rho+3})$ that are nonincreasing below $\bar y^\infty$.

Significance

The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of $\delta[\bar y]$ by a renewal formula, proves it convex in $\bar y$ (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.

Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.

Difficulty

The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth $O(|x|^{\rho+3})$ uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).

Formalization scope

All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States $x, y$ and the capacity $U$ are integers; demands are natural numbers with a real probability mass function p; $b$ is a positive natural number. Convexity on $\mathbb Z$ is the second-difference inequality. Expectations of a real function are series $\sum_j p(j)\,v(y-j)$; expected policy costs and hitting sums are $[0,\infty]$-valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states $x \le U$, which are the only states visited. Assumption 2 is stated literally, as real-analyticity of $\theta \mapsto \sum_j p(j)e^{i\theta j}$ at $0$. The order cost is zero, as in the paper. $\bar y^\infty$ is a parameter characterised as the least minimizer of $G$, not an infimum.

"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of $\delta^*$ to $g^*$ from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that $E\,v^*(y-D)$ converges, that $v^*$ has growth $O(|x|^{\rho+3})$, and that $g^* \ge 0$; all three follow from the paper's proof.

A trivializing reading is ruled out: the existence of $g$, $v$ and $y^*$ is one existential, so $y^*$ cannot be decoupled from the solution of (6), and strong optimality includes the convergence of $\delta^*$'s own average cost to $g^*$, so $g = 0$ does not satisfy it vacuously.

Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.

Selected references

• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands I. The Average-Cost Criterion, Mathematics of Operations Research 11(2):193–207, 1986. https://doi.org/10.1287/moor.11.2.193
• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands II. The Discounted-Cost Criterion, Mathematics of Operations Research 11(2):208–215, 1986. https://doi.org/10.1287/moor.11.2.208
• A. Federgruen, P. J. Schweitzer and H. C. Tijms, Denumerable Undiscounted Semi-Markov Decision Processes with Unbounded Rewards, Mathematics of Operations Research 8(2):298–314, 1983. https://doi.org/10.1287/moor.8.2.298
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$, right-hand sides $y_1,\ldots,y_n\in\mathbb R$, and an objective vector $z\in\mathbb R^d$:

$$\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).$$

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$-element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$: $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$. The first phase solves the relaxed program LP′ from the objective $A_I\alpha$.

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$. For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$, together with two artificial constraints at first coordinates $1$ and $-1$. LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$.

For positive right-hand sides, an optimal polar simplex is a $d$-subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$. The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$. Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$, where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$. The algorithm has separate random choices of $\mathcal I$ and $\alpha$.

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$. Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$, there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

$$\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.$$

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$, the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$, not standard deviation $\sigma$. The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$.

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$, computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$, so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$. The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$. Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

• Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

Motivation

A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set $\mathcal U$ (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over $\mathcal U$ at every Bellman update, which is expensive and does not scale to learning settings.

A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite sets of states and actions, $\mathcal A$ nonempty, and $\mathcal X := \mathcal S\times\mathcal A$. Fix a discount factor $\gamma\in(0,1)$ and a strictly positive initial distribution $\mu_0\in\Delta_{\mathcal S}$. A transition kernel $P$ assigns to every pair $(s,a)$ a probability distribution $P(\cdot\mid s,a)$ on $\mathcal S$; a reward is $r\in\mathbb R^{\mathcal X}$. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to every state an action distribution $\pi_s$.

For $v\in\mathbb R^{\mathcal S}$ write $r^\pi(s) = \sum_a\pi_s(a)r(s,a)$, $P^\pi(s'\mid s) = \sum_a\pi_s(a)P(s'\mid s,a)$, and define the evaluation Bellman operator

$$T^\pi_{(P,r)}v := r^\pi + \gamma P^\pi v .$$

The inner product on $\mathbb R^{\mathcal S}$ is $\langle v,\mu\rangle = \sum_s v(s)\mu(s)$, and the support function of a set $C\subseteq\mathbb R^{\iota}$ is $\sigma_C(y) = \max_{a\in C}\langle a,y\rangle$.

Given a set $\mathcal U$ of models $(P,r)$, the robust Bellman operator is

$$[T^{\pi,\mathcal U}v](s) := \min_{(P,r)\in\mathcal U}T^\pi_{(P,r)}v(s),$$

and the robust value function $v^{\pi,\mathcal U}$ is its fixed point. Around a nominal model $(P_0,r_0)$, an s-rectangular uncertainty set $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ is given by sets $\mathcal P_s\subseteq\mathbb R^{\mathcal X}$ and $\mathcal R_s\subseteq\mathbb R^{\mathcal A}$, one per state: its models are $P(s'\mid s,a) = P_0(s'\mid s,a)+P_s(s',a)$ and $r(s,a) = r_0(s,a)+r_s(a)$, with $P_s\in\mathcal P_s$ and $r_s\in\mathcal R_s$ chosen independently for each $s$. Finally $[v\cdot\pi_s](s',a) := v(s')\pi_s(a)$.

Formalization targets

Goal: Theorem 4.1 (general robust MDP)

For $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ and every policy $\pi$, $T^{\pi,\mathcal U}$ has a unique fixed point $v^{\pi,\mathcal U}$, and it is the optimal solution of

$$\max_{v\in\mathbb R^{\mathcal S}}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)-\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)\quad\forall s\in\mathcal S. \tag{2}$$

Milestones

1. Proposition 3.1. For any uncertainty set $\mathcal U = \mathcal P\times\mathcal R$ with $\mathcal P$ a nonempty compact set of kernels and $\mathcal R$ a nonempty compact set of rewards, $v^{\pi,\mathcal U}$ is the optimal solution of the robust program \max_{v}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v\le T^\pi_{(P,r)}v\ \ \forall(P,r)\in\mathcal U. \tag{$P_{\mathcal U}$}
2. Theorem 3.1. For $\mathcal U=\{P_0\}\times(r_0+\mathcal R)$, $v^{\pi,\mathcal U}$ is the optimal solution of $\max_v\langle v,\mu_0\rangle$ s.t. $v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)$ for all $s$.
3. Robust counterpart (proof of Theorem 4.1, App. B.1). For every $v$ and $s$,

$$\max_{(P,r)\in\mathcal U}\{v(s)-r^\pi(s)-\gamma P^\pi v(s)\} = \sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)+\sigma_{\mathcal R_s}(-\pi_s)+v(s)-T^\pi_{(P_0,r_0)}v(s).$$

Theorem 3.1 is the special case $\mathcal P_s=\{0\}$ of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.

Significance

The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer $\sigma_{\mathcal R_s}(-\pi_s)$ coming from reward uncertainty, and a regularizer $\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)$ coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ($\alpha^r_s\|\pi_s\|$ and $\alpha^P_s\gamma\|v\|\|\pi_s\|$, Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.

The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats $T^{\pi,\mathcal U}$ as linear in one step; a formal proof settles the statement independently of that step.

Difficulty

The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: $T^{\pi,\mathcal U}$ is a minimum of affine maps, hence concave and not affine, and the feasible set of $(P_{\mathcal U})$ is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of $T^{\pi,\mathcal U}$, which in turn requires every model in $\mathcal U$ to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set $\mathcal U$ into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation $P_s(s',a)$ against the kernel $P(s'\mid s,a)$.

Formalization scope

• States and actions are finite types, A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$, and the kernel property is the published IsTransitionKernel; $P^\pi(s'\mid s)$ is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.
• Perturbations $P_s$ are functions S × A → ℝ indexed $(s',a)$, as in the paper's $\mathbb R^{\mathcal X}$; rewards perturbations are A → ℝ.
• Minima and maxima (in $T^{\pi,\mathcal U}$ and in $\sigma$) are real sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.
• The robust value function is encoded as the fixed point of $T^{\pi,\mathcal U}$, and each theorem asserts its existence and uniqueness. The paper's definition $v^{\pi,\mathcal U}(s)=\min_{(P,r)\in\mathcal U}v^\pi_{(P,r)}(s)$ (p. 4) coincides with it for rectangular sets by a cited result; the proofs use only the fixed-point property. For the non-rectangular sets of Proposition 3.1 the pointwise minimum can be strictly larger than the fixed point and is then not the optimum of $(P_{\mathcal U})$, so the fixed point is the object the proposition is true for.
• "The optimal solution" means: feasible, objective-maximal, and the unique maximizer (uniqueness uses $\mu_0>0$).
• Disclosed hypotheses: $\mathcal U=\mathcal P\times\mathcal R$ with $\mathcal P$, $\mathcal R$ nonempty and compact and every transition in $\mathcal P$ a kernel (Prop. 3.1); $\mathcal P_s$, $\mathcal R_s$ nonempty and compact and every perturbed row $P_0(\cdot\mid s,a)+P_s(\cdot,a)$ in $\Delta_{\mathcal S}$ (Thm 4.1); reward sets rectangular in Thm 3.1, as its proof uses. These are the robust-MDP standing assumptions of p. 4 ($\mathcal P\subseteq\Delta^{\mathcal X}_{\mathcal S}$) and what makes "min" and "max" well defined.
• Not drafted: Corollary 4.1, whose ℓ²-ball $\mathcal P_s$ contains perturbations that leave the simplex, so $P_0+\mathcal P$ is not a set of kernels; Corollary 3.1 and Proposition 3.2 (consequences after the goal; Prop. 3.2 depends on an unspecified policy parametrization).
• A formalization that asserts only that the feasible sets of $(P_{\mathcal U})$ and (2) coincide, or that drops the kernel condition or the existence of the fixed point, does not count: the goal names the robust value function and its optimality.
• "Convex" in the statement of Theorem 4.1 is descriptive and is not part of the formal goal.

Contributions welcome: the monotone-contraction fixed-point lemma for $T^{\pi,\mathcal U}$ and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. PMLR 97
• S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and variance approximation in value function estimates, Management Science 53(2), 2007. doi:10.1287/mnsc.1060.0614

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).