Operations Research

Motivation

A retailer that carries several substitutable products, such as brands of the same item or sizes of the same garment, must choose stock levels before demand is known. When a product runs out, some of its customers buy another product instead. Inventory models with this demand substitution go back to McGillivray and Silver (1978, INFOR 16(1)) and Parlar and Goyal (1984). When the products are run by different firms, each firm's stock affects the demand its competitors see, and stocking becomes a game. Parlar (1988) proved existence and uniqueness of the equilibrium for two products; Lippman and McCardle (1997) treated a symmetric version of the game with an arbitrary number of firms.

Netessine and Rudi (SSRN 303779, working paper 2002; journal version in Operations Research 51(2), 2003) treat $n$ products with a general joint demand distribution and general prices and costs, under both centralized and competitive management. This mission formalizes their analysis of the competitive game (§2.2): the first-order characterization of its Nash equilibria (Proposition 3) and the existence, uniqueness and global stability of the equilibrium (Proposition 4).

Setting

There are $n$ products, indexed $i=1,\dots,n$, sold in a single period. Product $i$ is stocked at $Q_i\ge0$ units at unit cost $c_i$, sold at unit price $r_i$, and leftovers are salvaged at $s_i$, with $r_i>c_i>s_i>0$. Write $u_i=r_i-c_i$ (underage cost) and $o_i=c_i-s_i$ (overage cost).

The first-choice demand $D=(D_1,\dots,D_n)$ is a random vector with a known continuous joint distribution with positive support. A fraction $a_{ij}\in[0,1]$ of the customers who want product $i$ and find it out of stock buy product $j$ instead, with $a_{ii}=0$ and $\sum_{j}a_{ij}<1$ for every $i$; a customer whose second choice is also out of stock is lost. The effective demand for product $i$ is

$$D^s_i = D_i + \sum_{j\neq i} a_{ji}\,(D_j-Q_j)^+ ,$$

which depends on the other products' stocks $Q_{-i}$ but not on $Q_i$.

In the competitive model, firm $i$ chooses $Q_i$ and earns the expected profit

$$\pi_i(Q_i,Q_{-i}) = E\big[u_iD^s_i - u_i(D^s_i-Q_i)^+ - o_i(Q_i-D^s_i)^+\big]. \tag{9}$$

A best response of firm $i$ to $Q_{-i}$ is a stock $Q_i\ge0$ maximizing $\pi_i(\cdot,Q_{-i})$, and a Nash equilibrium is a stock vector from which no firm gains by deviating.

Formalization targets

Goal: Proposition 4

A Nash equilibrium exists, the equilibria are exactly the nonnegative solutions of the first-order conditions

$$\Pr(D_i<Q_i) - \Pr(D_i<Q_i<D^s_i) = \frac{u_i}{u_i+o_i},\qquad i=1,\dots,n, \tag{10}$$

and if either $\sum_{i}a_{ij}<1$ for all $j$ or $\sum_{j}a_{ij}<1$ for all $i$, the equilibrium $Q^d$ is unique and globally stable: every sequence of simultaneous best responses started at any nonnegative stock vector converges to $Q^d$.

Milestones

1. The derivative $\partial\pi_i/\partial Q_i = u_i-(u_i+o_i)\Pr(D^s_i<Q_i)$ (p. 8).
2. Concavity of $\pi_i$ in $Q_i$ (p. 8).
3. Proposition 3: a nonnegative stock vector is a Nash equilibrium if and only if it satisfies (10) (p. 8).
4. Each best response is unique and is characterized by (10) (proof of Proposition 4, p. 9).
5. The best response of firm $i$ is nonincreasing in the rivals' stocks, with slope in $Q_j$ at most $a_{ji}$ in absolute value (p. 9).
6. The simultaneous best-response map is Lipschitz with constant $\max_j\sum_i a_{ji}$ in the one-norm and $\max_i\sum_j a_{ji}$ in the infinity-norm (p. 9).

Significance

Proposition 4 makes the competitive equilibrium a well-defined object: a single stock vector, characterized by (10), which can be compared with the centralized optimum (the paper's Proposition 6) and which best-response adjustment reaches from any starting point. Without uniqueness, comparative statements about "the" competitive stocking level would be about an arbitrary selection.

The paper's argument has two gaps that this mission makes explicit. The proof asserts that best responses are single-valued because each profit is concave, and differentiates the best response using a density of $D^s_i$; the bound on the Jacobian is then stated in derivative form. The formal statements replace the derivative bounds by difference (Lipschitz) bounds, which need no differentiability, and state the positivity of the density on which single-valuedness rests. The paper also proves existence by citation to Lippman and McCardle; here existence is part of the goal. No machine-checked proof of these results is known.

Difficulty

The obvious route differentiates the best response implicitly, as the paper does. That requires $D^s_i$ to have a continuous, positive density at the equilibrium quantile, which is not a consequence of a continuous joint law: $D^s_i$ is a piecewise-linear function of $D$, and its distribution function may have kinks. A second point is that concavity of $\pi_i$ alone does not make the best response unique: a demand law whose support has a gap gives $\pi_i$ a flat stretch and an interval of maximizers. Global stability must hold for every sequence of best responses, not for the iterates of one selected best-response function. Finally, the probabilities in (10) use strict inequalities, and their identification with $\Pr(D^s_i\le Q_i)$ uses that $D^s_i$ has no atoms, which needs a measure-theoretic argument about $D^s_i=D_i+g(D_{-i})$ under an absolutely continuous law.

Formalization scope

Products are indexed by Fin n (0-based). The model data and the standing assumptions $r_i>c_i>s_i>0$, $a_{ij}\in[0,1]$, $a_{ii}=0$ and $\sum_j a_{ij}<1$ are fields of a structure Model n. a i j is the share of $i$'s unmet demand going to $j$, so $D^s_i$ uses a j i. The demand law is a probability measure $\mu$ on $\mathbb R^n$ that is absolutely continuous with respect to Lebesgue measure, gives every coordinate a positive value almost surely, and has integrable coordinates; this is the reading of "a known continuous multivariate demand distribution with positive support". Expectations are Bochner integrals and probabilities are μ.real of events, with the strict and weak inequalities as printed.

The stocks range over $[0,\infty)^n$, with no upper bound. A best response maximizes over $[0,\infty)$; a Nash equilibrium is defined by the absence of a profitable deviation, not by (10). Defining equilibria by (10) would make Proposition 3 and half of Proposition 4 true by definition, and is ruled out.

One hypothesis is added beyond the page and disclosed in every statement that uses it: $\mu$ has a Lebesgue density that is strictly positive on the open positive orthant. It is used for single-valued best responses, the slope and contraction bounds, and the goal; the derivative, concavity and Proposition 3 do not use it. In the goal, the second branch of the uniqueness condition, $\sum_j a_{ij}<1$ for all $i$, coincides with the standing assumption of §2, so uniqueness always applies within the model; the disjunction is kept as printed. The paper's proof attaches the one-norm bound $\max_j\sum_i a_{ji}$ to the first branch, which is a column-sum condition on $a$; both branches are true, with the one-norm used for row sums and the infinity-norm for column sums.

A complete development needs: differentiation under the integral sign for piecewise-linear integrands, the absence of atoms of $D_i+g(D_{-i})$ under an absolutely continuous law, quantiles of strictly increasing continuous distribution functions, and the Banach fixed-point theorem on the closed nonnegative orthant (Mathlib's ContractingWith). The first two are reusable for every newsvendor model with substitution. Proofs of the milestones in any order are welcome.

Selected references

• S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, University of Rochester, April 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779
• S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Operations Research 51(2):329–335, 2003. https://doi.org/10.1287/opre.51.2.329.12788
• S. A. Lippman and K. F. McCardle, The Competitive Newsboy, Operations Research 45(1):54–65, 1997. https://doi.org/10.1287/opre.45.1.54
• M. Parlar, Game Theoretic Analysis of the Substitutable Product Inventory Problem with Random Demands, Naval Research Logistics 35(3):397–409, 1988.
• A. R. McGillivray and E. A. Silver, Some Concepts for Inventory Control under Substitutable Demand, INFOR 16(1):47–63, 1978.
• M. Parlar and S. K. Goyal, Optimal Ordering Decisions for Two Substitutable Products with Stochastic Demand, OPSEARCH 21(1):1–15, 1984.
• R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (Theorem 5.6.9).

Why heavy-tailed input matters

Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict. A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.

Two candidate approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments (Taqqu, Willinger and Sherman, 1997; Leland, Taqqu, Willinger and Wilson, 1994), and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same model, and that the answer depends on how fast the connection rate grows relative to the time scale. This mission formalizes their Gaussian answer for the infinite source Poisson model: Theorem 3.

• 1994–1997: Leland et al. measure self-similarity in Ethernet traffic; Willinger, Taqqu, Sherman and Wilson derive fractional Brownian motion from ON/OFF sources with heavy-tailed periods, in an iterated limit (first the number of sources, then time).
• 2002: Mikosch, Resnick, Rootzén and Stegeman take both limits simultaneously and identify a slow-growth regime (stable Lévy limit) and a fast-growth regime (fractional Brownian limit), for both the ON/OFF and the infinite source Poisson model.

The infinite source Poisson model

Connections start at the points $(\Gamma_k)_{k\in\mathbb Z}$ of a homogeneous Poisson process on $\mathbb R$ with rate $\lambda$, labelled so that $\Gamma_0<0<\Gamma_1$; equivalently, $-\Gamma_0$, $\Gamma_1$ and $\Gamma_{k+1}-\Gamma_k$ ($k\neq0$) are iid exponential with parameter $\lambda$. Connection $k$ transmits at unit rate for a length $X_k$; the $X_k$ are iid with law $F_{\mathrm{on}}$ on $[0,\infty)$ and independent of $(\Gamma_k)$. The tail $\bar F_{\mathrm{on}}(x)=P(X_k>x)$ is regularly varying:

$$\bar F_{\mathrm{on}}(x)=x^{-\alpha}L(x),\qquad x>0,\quad 1<\alpha<2,\tag{2.8}$$

with $L$ slowly varying ($L(cx)/L(x)\to1$ for every $c>0$). The mean $\mu_{\mathrm{on}}$ is finite and the variance infinite. The number of active connections and the cumulative input are

$$N(t)=\sum_k\mathbf 1[\Gamma_k\le t<\Gamma_k+X_k],\qquad A(t)=\int_0^tN(s)\,ds .$$

The model is indexed by a time scale $T\to\infty$, with a connection rate $\lambda=\lambda(T)$ that is non-decreasing in $T$. With the quantile function $b(t)=(1/\bar F_{\mathrm{on}})^{\leftarrow}(t)=\inf\{x>0:1/\bar F_{\mathrm{on}}(x)\ge t\}$, the fast growth Condition 2 is

$$\lim_{T\to\infty}\frac{b(\lambda T)}{T}=\infty ,$$

equivalently $\lambda T\bar F_{\mathrm{on}}(T)\to\infty$: many transmissions longer than the observation window start in it. With $\sigma_T^2(1)=\lambda T^3\bar F_{\mathrm{on}}(T)$ the normalised input is

$$G_T(t)=\frac{A(Tt)-\lambda\mu_{\mathrm{on}}Tt}{[\sigma_T^2(1)\,\sigma^2]^{1/2}},\qquad t\ge0 .$$

Standard fractional Brownian motion $B_H$ with Hurst index $H\in(0,1)$ is a mean-zero Gaussian process on $[0,\infty)$ with a.s. continuous paths and $\mathrm{Cov}(B_H(t),B_H(s))=\tfrac12\big(t^{2H}+s^{2H}-|t-s|^{2H}\big)$.

Formalization targets

Goal: Theorem 3 (corrected)

Under (2.8), $\lambda$ non-decreasing and Condition 2,

$$G_T(\cdot)\xrightarrow{d}B_H(\cdot)\quad\text{in }(\mathbb D[0,\infty),J_1),\qquad H=\frac{3-\alpha}2,\qquad \sigma^2=\frac{2}{(\alpha-1)(2-\alpha)(3-\alpha)} .$$

On the constant. The paper takes $\sigma^2$ from its display (6.6), $\sigma^2=\frac1{3-\alpha}\big[\frac{\alpha}{2-\alpha}+\frac2{\mu_{\mathrm{on}}}\big]$. With that value the theorem is false. Two terms are lost in the variance bookkeeping of the proof: (6.4) omits the factor $\lambda m_2\sim\lambda m_3\sim\lambda\mu_{\mathrm{on}}$ in the variances of the second and third regional sums, each of which contributes $1/(3-\alpha)$, and (6.2) discards $(P_4-EP_4)T$ by an argument valid only under slow growth; under Condition 2 its variance is $\sim\lambda T^3\bar F_{\mathrm{on}}(T)/(\alpha-1)$. The sum $\frac{\alpha}{(2-\alpha)(3-\alpha)}+\frac2{3-\alpha}+\frac1{\alpha-1}$ equals $\frac2{(\alpha-1)(2-\alpha)(3-\alpha)}$, which is also what $\mathrm{Var}A(T)=2\int_0^T(T-h)\,\lambda\int_h^\infty\bar F_{\mathrm{on}}(v)\,dv\,dh$ and Karamata's theorem give. Since $\mathrm{Var}B_H(1)=1$, only this value makes the limit standard. All other constants are those of the paper.

Intermediate targets

The milestones follow the proof: Lemma 1 (Condition 2 ⇔ $\lambda T\bar F_{\mathrm{on}}(T)\to\infty$ ⇔ $\mathrm{Cov}(N_T(0),N_T(T))\to\infty$), Lemma 2 (fast part), the covariance identity (2.14), the moment asymptotics (4.9) and (4.14), the central limit theorem (6.3) for the first regional sum, the one-dimensional limit (6.5) with the corrected variance, stationarity of the increments of $G_T$, and the fourth-moment bounds (6.8) and $E(G_T(t+u)-G_T(t))^4\le cu^2$ that give tightness.

Significance

The theorem identifies the fast-growth regime of the infinite source Poisson model (the M/G/∞ input model) with fractional Brownian motion, so that Gaussian long-range-dependent models of network traffic are limits of a mechanistic model, not postulates; together with Theorem 1 it shows that the choice between Gaussian and stable approximations is decided by a single growth condition, $b(\lambda T)/T\to0$ or $\to\infty$. Queueing analyses of fluid queues fed by fractional Brownian motion inherit their justification from limits of this kind.

The result is proved in the paper, apart from the constant discussed above; it is not formalized anywhere. A formalization adds a machine-checked statement with the correct normalisation and a reusable development of regularly varying tails, Poisson marked point processes on $\mathbb R\times[0,\infty)$, fractional Brownian motion, and Skorokhod's $J_1$ topology on $\mathbb D[0,\infty)$.

Difficulty

The obvious argument is a central limit theorem for $A(T)$, but $A(T)$ is not a sum of independent terms of bounded variance: transmissions that straddle the window are long and heavy tailed, and their contribution is of the same order as the bulk. The proof splits the points into four regions according to where a transmission starts and ends, and each region needs its own moment asymptotics through Karamata's theorem; the bookkeeping is exactly where the printed constant goes wrong. The functional statement then needs tightness in $\mathbb D[0,\infty)$: a fourth-moment bound on increments that is uniform in $T$ and in the position of the increment, which requires Potter-type bounds on $\bar F_{\mathrm{on}}(uT)/\bar F_{\mathrm{on}}(T)$ for small $u$. Convergence of finite-dimensional distributions alone does not give the theorem.

Formalization scope

• Time and models. $T\to\infty$ along atTop on $\mathbb R$. Each model $T$ has its own probability space; the theorems hold for every family of models with the stated rate and length law. Time in $G_T$ runs over $\mathbb R_{\ge0}$.
• Standing hypotheses. $F_{\mathrm{on}}$ is a probability measure with $F_{\mathrm{on}}((-\infty,0))=0$ (lengths are non-negative, implicit on the page); (2.8) is stated as "$x\mapsto x^\alpha\bar F_{\mathrm{on}}(x)$ is slowly varying", $1<\alpha<2$; $\lambda(T)>0$ and $\lambda$ is non-decreasing (§3.1); Condition 2. No other hypothesis is added.
• Junk values ruled out. $b$ is an infimum over $\{x>0:t\bar F_{\mathrm{on}}(x)\le1\}$, never a division by zero; $N$ is a cardinality and $A_1$ a sum of non-negative terms, whose junk values ($0$ on an infinite set) occur only on null events; fourth moments are asserted together with integrability; equalities of laws are asserted together with measurability. The limit is pinned completely: Gaussian, mean zero, the covariance above with $\sigma_H=1$, $H=(3-\alpha)/2$, continuous paths. Fidi convergence in place of the functional limit, a free scale in the limit, or a limit identified only by its marginals would each be a different, weaker theorem.
• Weak convergence is stated in coupling form: for every sequence $T_n\to\infty$ there is one probability space with copies $Y_n$ of the laws of $G_{T_n}$ (all finite-dimensional distributions) and a standard fractional Brownian motion $Y'$ such that $Y_n\to Y'$ in $J_1$ almost surely, càdlàg paths included. On the Polish space $\mathbb D[0,\infty)$ this is equivalent to weak convergence. Because $A(T\cdot)$ and $B_H$ have continuous paths, $J_1$ convergence here coincides with locally uniform convergence.
• Infrastructure needed: Karamata's theorem and Potter bounds for regularly varying functions; the Poisson random measure of the marked points and its restriction to disjoint regions; a Lyapunov central limit theorem for Poisson sums; fractional Brownian motion and its existence; Billingsley's moment criterion for tightness in $\mathbb D[0,K]$. The regular-variation and Skorokhod-space material is reusable well beyond this mission; contributions of any of these pieces, and of any milestone, are welcome.

Selected references

• T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman, Is network traffic approximated by stable Lévy motion or fractional Brownian motion?, Ann. Appl. Probab. 12(1) (2002), 23–68. https://doi.org/10.1214/aoap/1015961155
• W. E. Leland, M. S. Taqqu, W. Willinger and D. V. Wilson, On the self-similar nature of Ethernet traffic (extended version), IEEE/ACM Trans. Networking 2 (1994), 1–15. https://doi.org/10.1109/90.282603
• W. Willinger, M. S. Taqqu, R. Sherman and D. V. Wilson, Self-similarity through high-variability: statistical analysis of Ethernet LAN traffic at the source level, IEEE/ACM Trans. Networking 5 (1997), 71–86. https://doi.org/10.1109/90.554723
• N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 12.3, moment criterion for tightness).

Motivation

At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most $k$ positions from its FCFS position, which keeps the sequence fair and predictable.

Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only $75+60=135$ seconds through the departure, while the direct requirement is $196$ seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.

Setting

Time is discrete: all data are integer multiples of one period. There are $n$ aircraft labelled in FCFS order, a maximum shift $k$, a minimum separation $\delta_{ab}\in\mathbb N$ between a leading aircraft $a$ and a trailing aircraft $b$, a time window $[e_a,l_a]$ for each aircraft, a finite set of precedence pairs $(x,y)$ ($x$ lands before $y$), and a cost $c_a(t)$ of landing aircraft $a$ at period $t$.

A $k$-CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$. A feasible schedule is a $k$-CPS sequence with integer landing times $t_p$ such that precedence pairs are respected, $e_{\sigma(p)}\le t_p\le l_{\sigma(p)}$, and

$$t_q-t_p\ \ge\ \delta_{\sigma(p)\sigma(q)}\qquad\text{for all positions } p<q .$$

Its cost is $\sum_p c_{\sigma(p)}(t_p)$.

The CPS network has stages $1,\dots,n$. A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft that may occupy positions $p-\min\{2k+1,p\}+1,\dots,p$; its last aircraft is the final aircraft $\mathrm{fin}(i)$. An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network $G$. For a node $i$, $\Gamma(i)$ is the set of integer times in the window of $\mathrm{fin}(i)$.

The modified network of §6.2 has nodes $(i,t,d)$: a node $i$ of $G$, a time $t\in\Gamma(i)$, and a lower bound $d$ on the separation between $\mathrm{fin}(i)$ and its predecessor, with $d=0$ at stage $1$ and otherwise $d^{\min}_i\le d\le d^{\max}_i$, where, for the penultimate and final aircraft $a,b$ of $i$,

$$d^{\min}_i=\delta_{ab},\qquad d^{\max}_i=\max\Big\{\max_{j:\,i\in P(j)}\big(\delta_{a,\mathrm{fin}(j)}-\delta_{b,\mathrm{fin}(j)}\big),\ d^{\min}_i\Big\}.$$

An arc $(i,t',d')\to(j,t'',d'')$ requires an arc $(i,j)$ of $G$, $t''-t'\ge d^{\min}_j$, $d''=\min\{t''-t',d^{\max}_j\}$, and $d'+t''-t'$ at least the separation between the penultimate aircraft of $i$ and $\mathrm{fin}(j)$. Arcs entering $(i,t,d)$ cost $c_{\mathrm{fin}(i)}(t)$.

Formalization targets

Goal: minimum-cost paths are optimal schedules

Under $k\ge 1$, positive costs, and the polygon inequalities of three or more hops (below):

1. a feasible schedule exists if and only if the modified network has a source-sink path;

$$\min_{(\sigma,t)\ \text{feasible}}\ \sum_p c_{\sigma(p)}(t_p)\;=\;\min_{\text{paths}}\ \sum_{p=1}^n c_{\mathrm{fin}(i_p)}(t_p),$$

each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.

Milestones

• Theorem 1 (with §3.1): the $k$-CPS sequences respecting precedence are exactly the sequences of source-sink paths of $G$.
• Lemma 5: every source-sink path of the modified network represents a feasible schedule.
• Lemma 6: every feasible schedule (in particular an optimal one) is represented by a source-sink path.
• Remark 1: under the triangle inequality, $d^{\min}_i=d^{\max}_i=\delta_{ab}$.
• Lemma 4: under the triangle inequality, a feasible schedule exists if and only if the simpler discrete-time network of §6.1.2, with nodes $(i,t)$, has a source-sink path.

Significance

The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in $n$ for fixed $k$ and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.

The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where $d^{\max}$ has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.

Difficulty

The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state $d$ repairs that but is capped at $d^{\max}$, so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of $d^{\max}$ over the successors of a node in $G$, so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.

Formalization scope

Aircraft and positions are $0$-based (Fin n), stages $1$-based, and $n\ge 1$ (NeZero n). Times, windows and separations are natural numbers (periods); $d$, $d^{\min}$, $d^{\max}$ and time differences are integers, since $d^{\max}$ involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.

The following readings of the paper are committed:

• Polygon inequalities. Lemma 5 and the goal assume that for every chain $x_0,\dots,x_m$ of $m\ge 3$ hops between distinct aircraft, $\delta_{x_0x_m}\le\sum_i\delta_{x_ix_{i+1}}$. Without this hypothesis Lemma 5 is false: there are small instances violating the quadrilateral inequality whose minimum-cost path is infeasible. §7 of the paper asserts these inequalities for mixed operations; this mission states them as a hypothesis and makes no claim about the paper's Table 1.
• $\Gamma(i)$ is the full time window, not the narrowed set of §6.1.3, whose justification needs nondecreasing costs. With the full window Lemma 6 holds for every feasible schedule and arbitrary costs; it is stated in that stronger form.
• $k\ge 1$, so that every node beyond stage $1$ has a penultimate aircraft. Arc condition 4 is not imposed on arcs leaving stage $1$.
• Arc cost $c(i,t)$ of the paper is read as $c_{\mathrm{fin}(i)}(t)$.
• Precedence pruning uses the printed rule of §3.1; nodes unreachable from the source or the sink are not removed (this does not change the set of source-sink paths).
• Running times (§6.1.4, §6.3) and the bound $\lambda$ of recursion (4) are not formalized.

A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.

A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, Massachusetts Institute of Technology, 1976 (as cited in the paper above).
• H. Lee, Tradeoff Evaluation of Scheduling Algorithms for Terminal-Area Air Traffic Control, Master's thesis, Massachusetts Institute of Technology, 2008 (source of the separation table; as cited in the paper above).

Motivation

In a linearly parameterized bandit, a decision maker repeatedly chooses an arm $u$ from a set $\mathcal U_r \subset \mathbb R^r$ and observes a noisy reward whose mean is the inner product $u'Z$ with an unknown parameter vector $Z$. The model covers pricing, assortment and recommendation problems in which arms are described by feature vectors and the number of arms is large or infinite, so that learning arm by arm is hopeless and information must be shared through the common parameter.

Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) give matching lower and upper bounds of order $r\sqrt T$ for this problem when the arm set is the unit sphere. This mission is the lower bound, Theorem 2.1. It says that the dimension enters the regret linearly and that no policy can do better than $r\sqrt T$, which makes the phased exploration policy of the paper's Section 3 optimal up to a constant.

Timeline. For $r = 1$, Mersereau, Rusmevichientong and Tsitsiklis (2009) showed regret $\Theta(\sqrt T)$ and Bayes risk $\Theta(\log T)$. Dani, Hayes and Kakade (2008) proved an $\Omega(r\sqrt T)$ minimax lower bound for a compact arm set built from products of circles. Rusmevichientong and Tsitsiklis (2010) proved the $\Omega(r\sqrt T)$ lower bound for the sphere itself, both for the regret and for the Bayes risk under a Gaussian prior, with the explicit constant $0.006$.

Setting

Fix a dimension $r \ge 2$. The arms are the unit sphere $\mathcal U_r = \{u \in \mathbb R^r : \|u\| = 1\}$, with the Euclidean norm $\|\cdot\|$. The unknown parameter $Z$ is drawn from the prior $N(0, I_r/r)$: each coordinate is an independent normal with mean $0$ and variance $1/r$, so $\mathbb E\|Z\|^2 = 1$. Playing arm $u$ in period $t$ yields the reward

$$X_t = u'Z + W_t,$$

where the noise variables $W_t$ are independent standard normals, independent of $Z$.

A history $H_t = (U_1, X_1, \dots, U_t, X_t)$ lists the arms played and rewards observed up to period $t$. A policy $\psi = (\psi_1, \psi_2, \dots)$ chooses the arm $U_t = \psi_t(H_{t-1}) \in \mathcal U_r$ of period $t$ from the history. Since $\max_{v \in \mathcal U_r} v'z = \|z\|$, the regret of $\psi$ given $Z = z$ and the Bayes risk of $\psi$ over $T$ periods are

$$\mathrm{Regret}(z, T, \psi) = \sum_{t=1}^T \mathbb E\big[\|z\| - U_t'z \,\big|\, Z = z\big], \qquad \mathrm{Risk}(T, \psi) = \mathbb E\big[\mathrm{Regret}(Z, T, \psi)\big].$$

The milestones use the least mean squares estimator $\widehat Z_T = \mathbb E[Z \mid H_T]$ and orthonormal vectors $S^1_T, \dots, S^{r-1}_T$ that are orthogonal to $\widehat Z_T$ and are functions of $H_T$.

Formalization targets

Goal: Theorem 2.1 (p. 8)

For every policy $\psi$ and every $T \ge r^2$,

$$\mathrm{Risk}(T, \psi) \ge 0.006\, r\sqrt T, \qquad\text{and there is } z \in \mathbb R^r \text{ with } \mathrm{Regret}(z, T, \psi) \ge 0.006\, r\sqrt T.$$

The constant $0.006$ is absolute; the parameter $z$ may depend on $\psi$.

Milestones

1. Lemma 2.2 (p. 9), risk decomposition:

$$\mathrm{Risk}(T, \psi) \ge \frac12 \sum_{k=1}^{r-1} \mathbb E\Big[\|Z\| \sum_{t=1}^T (U_t'S^k_T)^2 + \frac{T}{\|Z\|}\big\{(Z - \widehat Z_T)'S^k_T\big\}^2\Big].$$

2. Lemma 2.3 (p. 10): almost surely, $\mathbb E\big[\{(Z - \widehat Z_T)'S^k_T\}^2 \mid H_T\big] \ge 1/\big(r + \sum_{t=1}^T (U_t'S^k_T)^2\big)$.
3. Lemma 2.4 (p. 11): for $\theta \le 1/2$ and $\beta > 0$, $\Pr\{\theta \le \|Z\| \le \beta\} \ge 1 - 4\theta^2 - 1/\beta^2$.
4. Lemma 2.5 (p. 11): for each $k$ and $T \ge r^2$, the expectation of the $k$-th summand of Lemma 2.2 is at least $0.027\sqrt T$.

Significance

The result. Theorem 2.1 shows that the regret and Bayes risk of linearly parameterized bandits grow at least linearly in the dimension, even when the arm set is as regular as a sphere and the noise is Gaussian. Together with the paper's Theorem 3.1 it pins the optimal order at $r\sqrt T$ on the sphere, and it shows that the $\log T$ Bayes risk achievable in dimension one does not survive in dimension two or more. Since the sphere is one compact arm set, the theorem also shows that the paper's upper bounds of order $r\sqrt T \log^{3/2} T$ for general compact arm sets (Section 4) cannot be improved beyond logarithmic factors in that generality (Table 1, p. 8).

Formalizing it. The theorem is proved in the paper; to our knowledge it has not been machine-checked. The platform has a minimax lower bound for the unit ball with a fixed-norm parameter (Lattimore and Szepesvári, Theorem 24.2), which is a different statement: a frequentist bound over a finite family of parameters, not a Bayes risk under a continuous Gaussian prior. Formalizing Theorem 2.1 requires Gaussian posterior computations with an adaptively chosen design, a piece of Bayesian linear regression that is reusable well beyond bandits.

Difficulty

The obvious argument fixes the parameter's norm and treats the problem as a Gaussian estimation problem in each direction orthogonal to the current estimate. That fails because $\|Z\|$ is random under the prior: the risk per direction trades off exploration, weighted by $\|Z\|$, against estimation error, weighted by $T/\|Z\|$, and neither weight is bounded. The proof has to localise $\|Z\|$ to an interval with positive probability uniformly in $r$, which is the content of Lemma 2.4 and the reason the lemma needs $r \ge 2$.

The second obstacle is that the design is adaptive: the arms $U_t$ depend on past rewards, so the posterior of $Z$ given $H_T$ must be identified as Gaussian with covariance $(rI_r + \sum_t U_tU_t')^{-1}$ even though the regressors are random and history-dependent. Lemma 2.3 rests on this identification and on a matrix inequality for diagonal entries of an inverse.

Formalization scope

The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's. All declarations live in the namespace LinParamBandits.LowerBound.

• $\mathbb R^r$ is EuclideanSpace ℝ (Fin r), so norms are Euclidean and inner is $u'z$. Every theorem carries $2 \le r$, the paper's standing assumption.
• The prior is the law of $Y/\sqrt r$ with $Y$ a standard Gaussian vector (Mathlib's stdGaussian); the noise is an i.i.d. standard normal sequence (Measure.infinitePi), independent of $Z$.
• The paper has one noise variable $W^u_t$ for every arm and period. Only $W^{U_t}_t$ is observed and $U_t$ depends on the past only, so the history has the same law with a single sequence; that is what is modelled.
• Policies are deterministic and history-dependent, as in the paper, and each selection rule is required to be measurable, which the paper's expectations use implicitly.
• Periods are 0-based in Lean: arm ψ z η t is the paper's $U_{t+1}$.
• Regret and risk are lower Lebesgue integrals of the nonnegative per-period gaps, with values in $[0, \infty]$, and the regret given $Z = z$ is computed with the parameter fixed to $z$. The tempting encoding $T\max_v v'z - \int \sum_t U_t'z$ is ruled out: there a non-integrable integrand would return $0$ and make the regret equal to $T\|z\|$, so the lower bound would hold trivially.
• $\widehat Z_T$ is Mathlib's conditional expectation with respect to the $\sigma$-algebra generated by $H_T$. The vectors $S^k_T$ are hypotheses of the lemmas: measurable functions of the history, orthonormal, and almost surely orthogonal to $\widehat Z_T$.
• No printed slip was found; no hypothesis beyond measurability of policies is added. The footnote on p. 8 (covariance $I_r$) is not stated.

A complete development needs: measurability of the trajectory map, the Gaussian posterior for a sequentially chosen design, the inequality $[(A)^{-1}]_{kk} \ge 1/A_{kk}$ for positive definite $A$, a chi-square lower-tail bound, and Gaussian tail values. The posterior computation and the chi-square bound are reusable; contributions of either, or of a proof of any single milestone, are welcome.

Selected references

• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010; preprint arXiv:0812.3465v2. https://arxiv.org/abs/0812.3465
• A. J. Mersereau, P. Rusmevichientong, J. N. Tsitsiklis, A Structured Multiarmed Bandit Problem and the Greedy Policy, IEEE Transactions on Automatic Control 54(12), 2009. https://doi.org/10.1109/TAC.2009.2031725
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. https://www.learningtheory.org/colt2008/papers/80-Dani.pdf
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Motivation

Two-stage stochastic linear programming chooses a first-stage decision $x$ before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.

Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.

Setting

The first-stage region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge0\}$. For $x\in X$ the recourse set is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge0\}$ and the second-stage cost of an objective vector $q\in\mathbb R^d$ is

$$\mathcal Q(q,x)=\min_{w\in X(x)} q'w .$$

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge0$. The moment class $\mathcal P$ consists of the distributions $P$ of a random vector $\tilde q\in\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$. The worst-case value at $x$ is

$$Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big].$$

Its dual (6) is

$$Z_D(x)=\min_{Y,y,y_0}\ Q\cdot Y+\mu'y+y_0\quad\text{s.t.}\quad q'Yq+q'y+y_0\ge\mathbb U(\mathcal Q(q,x))\ \ \forall q\in\mathbb R^d ,$$

with $Y$ symmetric and $Q\cdot Y=\sum_{ij}Q_{ij}Y_{ij}$. Its semidefinite reformulation (8) has the dual (9):

$$Z_{DD}(x)=\max\ \sum_{k=1}^K (h-Tx)'p_k+\beta_kv_{k0}\quad\text{s.t.}\quad \sum_{k=1}^K\begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}=\begin{pmatrix}Q&\mu\\ \mu'&1\end{pmatrix},\ \begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}\succeq0,\ W'p_k\le\alpha_kv_k .$$

Its variables are scaled conditional moments: $v_{k0}$ is the probability that the $k$th piece of $\mathbb U$ is active, and $v_k$, $V_k$ are the first and second moments of $\tilde q$ on that event, multiplied by $v_{k0}$.

The standing assumptions are Assumption 3, $\{p\in\mathbb R^r : W'p\le q\}\ne\emptyset$ for every $q$, so that $\mathcal Q(q,x)$ is finite, and Assumption 4, $Q-\mu\mu'\succ0$. Recourse sets are assumed nonempty.

Formalization targets

Goal: Theorem 2.2

For every $x\in X$ there is a sequence $P_j\in\mathcal P$ with $\mathbb E_{P_j}[\mathbb U(\mathcal Q(\tilde q,x))]\to Z(x)$, and

$$Z(x)=Z_D(x)=Z_{DD}(x),$$

where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.

Milestones

1. Lemma 2.1: $Z_{DD}(x)\ge Z(x)$, in the form "each $P\in\mathcal P$ gives a feasible point of (9) whose objective equals $\mathbb E_P[\mathbb U(\mathcal Q)]$".
2. (9) has an optimal solution.
3. $\mathcal Q(\cdot,x)$ is positively homogeneous and superadditive.
4. If $W'p\le\alpha v$ with $\alpha\ge0$ then $\alpha\mathcal Q(v,x)\ge(h-Tx)'p$.
5. Jensen: $\mathbb E[\mathcal Q(\tilde r,x)]\le\mathcal Q(\mathbb E\tilde r,x)$, with $\mathcal Q(\tilde r,x)$ integrable.
6. An optimal solution of (9) can be chosen so that every block has $v_{k0}>0$ or vanishes.
7. Strong duality $Z(x)=Z_D(x)$ (§2.1).

Significance

Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability $v_{k0}$ the cost vector sits at the conditional mean $v_k/v_{k0}$, and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case ($K=1$) the bound collapses to Jensen's bound $\min_{w\in X(x)}\mu'w$. For $K>1$ it is a combination of Jensen bounds, one per piece of the disutility.

Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity $Z=Z_D=Z_{DD}$ and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.

Difficulty

Most of the argument is linear programming and bookkeeping. The step $Z(x)=Z_D(x)$ is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in $\mathcal P$ generally cannot attain $Z(x)$, so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of $\mathbb U$ and of a dual optimal solution of the second-stage program as functions of $q$. When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and $\mathbb E[\tilde q\tilde q']$ is the uncentred second moment. The paper writes $p$ both for the dimension of $q$ and for dual vectors. Here the dimension is $d$ and dual vectors are named π. Indices $k$ are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and $\succeq0$ is Matrix.PosSemidef. $\mathcal Q$ is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.

As printed, Assumption 2 (complete recourse) and Assumption 3 for all $q$ contradict each other whenever $W$ has a row. The formalization keeps Assumption 3 for all $q$ and replaces complete recourse by nonemptiness of $X(x)$, which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by $W=I$, $T=0$, $h=0$, $\mu=0$ and $Q=I$.

The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities $Z=Z_D=Z_{DD}$, with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.

A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on $\mathbb R^d$, compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.

Selected references

• D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903

Motivation

Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.

The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.

Setting

A reference is offered in a finite set of sizes $\mathcal S = \mathcal S^+ \cup \mathcal S^-$, with major sizes $\mathcal S^+$ and minor sizes $\mathcal S^- = \mathcal S \setminus \mathcal S^+$. Sale opportunities for size $s$ follow a Poisson process $N_s(t)$ with rate $\lambda_s > 0$, independent across sizes, where $t$ is the time since the last replenishment and $T > 0$ is the time between replenishments.

Given an inventory vector $q \in \mathbb N^{\mathcal S}$, the virtual stockout time of size $s$ is $\tau_s(q_s) = \inf\{t \ge 0 : N_s(t) = q_s\}$, and $\tau_{\mathcal A} = \min_{s \in \mathcal A}\tau_s(q_s)$ for a set of sizes $\mathcal A$. Writing $a \wedge b = \min(a,b)$, the number of sales in one period is

$$G(q) = \sum_{s \in \mathcal S^+} N_s(\tau_{\mathcal S^+} \wedge T) + \sum_{s \in \mathcal S^-} N_s(\tau_{\mathcal S^+ \cup \{s\}} \wedge T),$$

since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is $g_\lambda(q) = \mathbb E[G(q)]$.

For the approximation, let $\gamma(a,b) = \int_0^b v^{a-1}e^{-v}\,dv$ be the lower incomplete Gamma function, and define the tangent coefficients

$$a_k(\lambda) = \frac{\gamma(k+1, \lambda T)}{\lambda\, k!}, \qquad b_i(\lambda) = \sum_{k=0}^{i-1} a_k(\lambda),$$

with the tangent at $i = \infty$ equal to the constant $T$. For each size choose a nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N \cup \{\infty\}$ of tangent indices. The approximate expected sales function is

$$\tilde g_\lambda(q) = \lambda_{\mathcal S^+} \min_{s \in \mathcal S^+} \min_{i \in \mathcal N(\lambda_s)} \{a_i(\lambda_s)(q_s - i) + b_i(\lambda_s)\} + \sum_{s \in \mathcal S^-} \lambda_s \min_{s' \in \mathcal S^+ \cup \{s\}} \min_{i \in \mathcal N(\lambda_{s'})} \{a_i(\lambda_{s'})(q_{s'} - i) + b_i(\lambda_{s'})\},$$

with $\lambda_{\mathcal S^+} = \sum_{s\in\mathcal S^+}\lambda_s$. In Lean the objects are expectedSales, hA ($\mathbb E[\tau_{\mathcal A}\wedge T]$), a, b, tangent and gTilde in the namespace FastFashion.Approx.

Formalization targets

Goal: the approximation is an upper bound

For every independent Poisson family with positive rates, every $T > 0$, every nonempty $\mathcal S^+$, every choice of nonempty finite tangent sets, and every $q \in \mathbb N^{\mathcal S}$,

$$g_\lambda(q) \le \tilde g_\lambda(q).$$

The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.

Milestones

1. Eq. (2): $g_\lambda(q) = \lambda_{\mathcal S^+}\mathbb E[\tau_{\mathcal S^+}\wedge T] + \sum_{s\in\mathcal S^-}\lambda_s\mathbb E[\tau_{\mathcal S^+\cup\{s\}}\wedge T]$.
2. Eq. (3): $\mathbb E[\tau_{\mathcal D}\wedge T] \le \min_{s\in\mathcal D}\mathbb E[\tau_s\wedge T]$ for nonempty $\mathcal D$.
3. Eqs. (4)–(5): $\mathbb E[\tau_s\wedge T] = \frac1{\lambda_s}\sum_{k=1}^{q_s}\mathbb P(N_s(T)\ge k) = \sum_{k=1}^{q_s}\frac{\gamma(k,\lambda_sT)}{\lambda_s\Gamma(k)}$.
4. The terms $a_k(\lambda)$ are positive and strictly decreasing in $k$.
5. Eq. (6): $\mathbb E[\tau_s\wedge T] = \min_{i\in\mathbb N\cup\{\infty\}}\{a_i(\lambda_s)(q_s-i)+b_i(\lambda_s)\}$, the minimum attained.

Further result: the MIP represents the approximation

In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has $z_j = \tilde g_{\lambda_j}(x_j + I_j)$ at every store $j$.

Significance

The upper bound is what makes the paper's optimization coherent: the MIP maximizes $\sum_j P_j \tilde g_{\lambda_j}$, and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits $\mathbb E[\tau_s \wedge T]$ as a concave function of $q_s$ with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.

The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.

Difficulty

The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process $N_s(t) - \lambda_s t$ in continuous time, applied at $\tau_{\mathcal A} \wedge T$ (the paper cites Karatzas and Shreve 1991), which requires showing that $\tau_{\mathcal A}$ is a stopping time for the joint filtration of the family and that $N_s$ is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of $\tau_s(q_s)$, the $q_s$-th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity $\mathbb P(N(T) \ge k) = \gamma(k, \lambda T)/\Gamma(k)$ between Poisson tails and the incomplete Gamma function.

A tempting shortcut is to define $g_\lambda$ directly by formula (2), or $\mathbb E[\tau_s\wedge T]$ by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines $g_\lambda$ from $G$ and $h^{\mathcal A}$ from the stopping times.

Formalization scope

• Model. Sizes form a finite type; the major sizes are a Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each $N_s$ is a counting process with $N_s(0)=0$, non-decreasing right-continuous paths with unit jumps, Poisson increments of mean $\lambda_s(t-u)$, independent increments, and the processes are independent across sizes. $P$ is a probability measure.
• Stockout times take values in $\mathbb R \cup \{+\infty\}$ (WithTop ℝ), so the infimum of an empty set is $+\infty$, never $0$; $\tau_{\mathcal A}\wedge T$ is a real number in $[0,T]$.
• Expectations are Bochner integrals. They are not junk: $0 \le G(q) \le \sum_s N_s(T)$, which is integrable, and $\tau_{\mathcal A}\wedge T \in [0,T]$.
• Corrected coefficients. As printed, $a_k = \gamma(k,\lambda T)/(\lambda\Gamma(k))$ and $b_1 = a_0$ involves $\Gamma(0)$; the formalization uses $a_k = \gamma(k+1,\lambda T)/(\lambda\,k!)$, matching the paper's description of $a_k$ as the probability that the $(k+1)$-th unit sells.
• Tangent sets. The rule (7), "$b_i(\lambda_s) \approx 0, 0.3T, 0.6T, 0.8T, 0.9T, T$", is approximate and is replaced by an arbitrary nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N\cup\{\infty\}$.
• Added hypotheses. $\mathcal S^+ \ne \emptyset$ (for (8) and the goal), nonempty $\mathcal D$ in (3), and $P_j > 0$ in the MIP statement.
• MIP. Optimality is defined as feasibility plus an objective at least that of every feasible point; existence of an optimum is not asserted.

The paper's further remark that $\tilde g_\lambda$ inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.

Selected references

• F. Caro, J. Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper (August 2, 2007); published in Operations Research 58(2), 2010. https://doi.org/10.1287/opre.1090.0698
• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2