Stochastic Systems

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$, how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

$$s = \lambda + \gamma\sqrt{\lambda},$$

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$, its mean and variance are both $\lambda$, so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$. The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

• The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
• Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
• Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$, the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$-th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$, the number of arrivals in $(0, t]$. This is a Poisson process of rate $\lambda$.

Customers are numbered $k = 0, 1, 2, \dots$; customer $k$ arrives at $\tau_{k+1}$, is served at once, and has service time $D_k$. Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$. The number of busy servers is

$$N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.$$

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$. Each customer carries a class label $J_k$, the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$. The class-$i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$.

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$, then

$$P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots$$

The law depends on the service-time distribution only through its mean.

Milestones

1. Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$, pathwise.
2. Proof of Proposition 2.4 (p. 712): for $t \ge 1$, $A(t) - A(t-1)$ has the same law as $A(1)$.
3. Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$.
4. §2.5, splitting (p. 713): the class-$i$ arrivals form independent Poisson streams of rates $\lambda p_i$; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
5. §2.5, "Hence" (p. 713): for $t > \max_i d_i$, the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$, and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$, connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$.

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$, the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$-server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

• a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
• Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
• the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$.

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$: the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

• The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
• The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
• Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$, and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$, avoiding pushforwards of possibly non-measurable maps.
• Standing conventions: service rate $1$; the system starts empty at time $0$; arrival counted at $t$, departure not; "steady state" means the law at each fixed $t > \max_i d_i$, with no limit $t \to \infty$; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$, and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$. Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
• Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

• W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

Motivation

The $G/GI/N$ queue has $N$ identical servers, a general arrival process, and independent service times with a common distribution $F$. In the Halfin–Whitt regime the number of servers and the offered load grow together, so that the fraction of delayed customers stays strictly between $0$ and $1$. This is the standard asymptotic model of large call centers and service systems (Halfin and Whitt, Operations Research 29, 1981, doi:10.1287/opre.29.3.567). For exponential service times the diffusion limit has been known since 1981; for general service distributions the queue length is no longer Markov, and its limit requires a different device.

Reed (Annals of Applied Probability 19, 2009, arXiv:0912.2837) supplied that device. The number in system $Q$ satisfies a nonlinear convolution equation, (2.8) on p. 9 of the paper, in which the only nonlinearity is the term $\int_0^t (Q(t-s)-N)^+\,dF(s)$. Section 3 of the paper isolates that equation as a deterministic regulator map: a map that takes an input path to the unique solution of the equation. Its fluid limit (Theorem 4.1) and diffusion limit (Theorem 5.1) are both obtained by applying this map, through the continuous mapping theorem, to the limits of simpler free processes. The regulator map plays here the role that the one-sided reflection map plays in conventional heavy-traffic theory.

Timeline:

• 1981. Halfin and Whitt: the diffusion limit for exponential service times.
• 2000. Puhalskii and Reiman: the $GI/PH/N$ case, with phase-type service (MR1778580).
• 2004. Jelenković, Mandelbaum and Momčilović: deterministic service times (MR2074672).
• 2009. Reed: general service times, via the regulator map of Proposition 3.1. This mission covers that proposition.

Setting

A path is a function $x:[0,\infty)\to\mathbb R$. It is càdlàg if it is right continuous everywhere and has a finite left limit at every $t>0$. $D[0,\infty)$ is the set of càdlàg paths. For $T\ge0$ the supremum metric on $[0,T]$ is $\|x\|_T=\sup_{0\le t\le T}|x(t)|$.

Let $B$ be a cumulative distribution function on $\mathbb R$, that is, $B(t)=\mu((-\infty,t])$ for a probability measure $\mu$, and let $a\in\mathbb R$. Write $y^+=\max(y,0)$. For an input $x\in D[0,\infty)$, the regulator equation (3.1) asks for a path $z\in D[0,\infty)$ with

$$z(t)=x(t)+\int_{[0,t]}\big(z(t-s)+a\big)^+\,dB(s),\qquad t\ge0 .$$

The integral runs over the closed interval $[0,t]$, so an atom of $B$ at $0$ counts. The regulator map $\varphi^a_B$ sends $x$ to the solution $z$. The paper applies it with $B=F$, the service-time distribution: $a=-1$ for the fluid-scaled queue and $a=0$ for the diffusion-scaled one.

The proof works with the operator $\Psi^a_B(u)(t)=\int_{[0,t]}(u(t-s)+a)^+\,dB(s)$ and the successive approximations $u_0=0$, $u_{n+1}=x+\Psi^a_B(u_n)$ of (A.3).

$D[0,\infty)$ carries the Kolmogorov σ-algebra, the one generated by the evaluations $x\mapsto x(t)$, $t\ge0$. In the Lean development the objects are IsCadlag, supNorm, Dpath, SolvesRegulator, psi and picard.

Formalization targets

Goal: Proposition 3.1

Assume $\mu(\{0\})<1$. Then there is a map $\varphi^a_B:D[0,\infty)\to D[0,\infty)$ with the following properties:

• $\varphi^a_B(x)$ solves (3.1) for every $x$;
• every càdlàg solution of (3.1) agrees with $\varphi^a_B(x)$ on $[0,\infty)$;
• for each $T\ge0$ there is a constant $C_T$ with

$$\|\varphi^a_B(x_1)-\varphi^a_B(x_2)\|_T\le C_T\,\|x_1-x_2\|_T\quad\text{for all } x_1,x_2\in D[0,\infty);$$

• $\varphi^a_B$ is measurable for the Kolmogorov σ-algebra.

The constant $C_T$ is not fixed. The proof gives $(1-\varepsilon)^{-\lceil T/\delta\rceil}$, but the goal asserts only its existence.

Milestones, in the order of the paper's proof

1. Point mass at $c>0$, (A.1)–(A.2). Equation (3.1) is the recursion $z=x$ on $[0,c)$ and $z(t)=x(t)+(z(t-c)+a)^+$ for $t\ge c$. Its solution is unique, and $\|z_1-z_2\|_t\le k\|x_1-x_2\|_t$ for $(k-1)c\le t<kc$.
2. Uniqueness. Assume $B(y+\delta)-B(y)<\varepsilon<1$ for all $y\ge0$ and $\mu([0,\delta])<\varepsilon$. Then two càdlàg solutions agree on $[0,\infty)$.
3. Lipschitz continuity. Under the same assumption, $\|z_2-z_1\|_{k\delta}\le(1-\varepsilon)^{-k}\|x_2-x_1\|_{k\delta}$ for every $k\ge1$.
4. Existence. Under the same assumption, the successive approximations converge uniformly on every $[0,T]$ to a càdlàg solution.
5. Measurability of $\Psi^a_B$. $\Psi^a_B$ maps càdlàg paths to càdlàg paths, and $u\mapsto\Psi^a_B(u)(t)$ is measurable for each $t\ge0$.
6. Example 1. For unit deterministic service times, the fluid equation (4.7) has the unique solution $\bar Q(t)=1+t-\lfloor t\rfloor$.
7. Proof of Corollary 5.1. Take equilibrium initial conditions. The input of (4.7) is then identically $1$, and $\bar Q\equiv1$ is the unique solution.

Significance

Proposition 3.1 is the deterministic core of the paper. Uniqueness makes the queue length a well-defined function of its free process. Lipschitz continuity in the topology of uniform convergence on compacts carries convergence of the inputs over to convergence of the outputs. Measurability is needed because the inputs are random: it makes the output a random element of $D[0,\infty)$, so that the continuous mapping theorem applies. Without the proposition neither Theorem 4.1 nor Theorem 5.1 can be stated in the form the paper gives. Example 1 and Corollary 5.1 are the two explicit solutions the paper extracts from it: a periodic, discontinuous sawtooth, and a constant.

The proposition is proved in the paper's Appendix (pp. 32–36). As far as the platform's records show, none of it has been formalized. The mission produces a machine-checked version with every convention fixed. It also corrects the statement: as printed, the proposition fails when $B$ is the unit mass at $0$, because the equation then reads $z(t)=x(t)+(z(t)+a)^+$. With $a=0$ and $x\equiv1$ this has no solution. The goal therefore carries the hypothesis $\mu(\{0\})<1$. That hypothesis holds for every service distribution of mean $1$ on $[0,\infty)$, which is the only case the paper uses. It also covers the mixed cases that fall between the two cases of the printed proof, such as an atom at $0$ together with mass elsewhere.

Theorems 4.1 and 5.1 themselves, which are weak convergence in $D[0,\infty)$ with the Skorohod $J_1$ topology, are not part of this mission.

Difficulty

The equation is a Volterra equation with a nonlinear but $1$-Lipschitz integrand. The first idea is to treat it as a contraction in $\|\cdot\|_T$. That fails: the kernel $B$ has total mass $1$, so on $[0,T]$ the operator $\Psi^a_B$ is only nonexpansive, not contractive. The contraction has to be recovered locally, from windows of length $\delta$ on which $B$ puts mass less than $1$. This works only if such windows exist, and they do not exist when $B$ is a point mass at $0$.

Atoms are the second difficulty. With atoms, $t\mapsto\Psi^a_B(u)(t)$ is càdlàg but not continuous, and the closed-interval convention matters at every step. The third is measurability. The map $u\mapsto\int(u(t-s)+a)^+\,dB(s)$ is not continuous in $u$ for the Skorohod topology when $B$ has atoms, so the paper splits $B$ into its continuous and discrete parts.

Formalization scope

• Paths. A path is ℝ → ℝ, and only its values on $[0,\infty)$ are constrained or read. Every equation is asserted for $t\ge0$, and every uniqueness claim is equality on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). $D[0,\infty)$ is the structure Dpath of càdlàg paths.
• Integrals. $B$ is a probability measure $\mu$ on $\mathbb R$. $\int_0^t\cdots dB(s)$ is the integral over the closed interval Set.Icc 0 t, so it includes an atom at $0$, and mass on $(-\infty,0)$ never enters.
• Explicit readings of the paper's phrases.
  • "Unique solution in $D[0,\infty)$" means unique among càdlàg paths, up to equality on $[0,\infty)$.
  • "Lipschitz continuous in the topology of uniform convergence over bounded intervals" means $\forall T\ \exists C_T\ \forall x_1,x_2$. The constant is chosen before the inputs.
  • "Measurable with respect to the Borel σ-field generated by the Skorohod $J_1$ topology" means measurable for the Kolmogorov σ-algebra generated by the evaluations at times $t\ge0$. The paper uses this identification on p. 35, and it is Theorem 16.6 of Billingsley (1999). $J_1$ is not defined.
  • "Uniform convergence" in the existence proof means $\|u_n-u^\star\|_T\to0$ for every $T$.
• Added hypothesis in the goal: $\mu(\{0\})<1$ (see Significance).
• Window conditions in milestones 2–4. These are the paper's $B(y+\delta)-B(y)<\varepsilon$ for $y\ge0$, plus $\mu([0,\delta])<\varepsilon$ for the first window, which the proof uses as "$B(\delta)<\varepsilon$".
• Junk values. The real supremum $\|\cdot\|_T$ and the Bochner integral take junk values (zero) on unbounded or non-integrable data. Every statement applies them only to càdlàg paths, which are bounded and measurable on $[0,T]$. This is also why solutions are required to be càdlàg: a solution taken among arbitrary functions could exploit the zero value of a non-integrable integral. Likewise, the goal cannot be satisfied by a $\varphi$ whose values solve (3.1) only vacuously, and cannot be satisfied by dropping the càdlàg requirement on the output.
• Printed slips corrected in the Lean and disclosed in the items:
  • (A.2)'s step "$k<t\le(k+1)c$" means $kc\le t<(k+1)c$;
  • (A.3) "for $n\ge1$" starts at $n=0$;
  • (4.18) has $\bar Q(t)$ on the right where (4.7) gives $\bar Q(t-1)$;
  • Corollary 5.1 cites "Theorem 5.1 of Section 4", meaning Theorem 4.1.

Infrastructure. A complete development needs the following, all reusable beyond this mission:

• càdlàg paths on a half-line and their boundedness on compacts;
• Lebesgue–Stieltjes convolution integrals of càdlàg paths against a probability measure;
• the Kolmogorov σ-algebra on path space.

The related platform objects are of other shapes:

• ChenWhitt93.Reflection.Basic (IsCadlagOn, vector-valued paths on $[0,T]$) and EthierKurtz_HasCadlagPaths (processes indexed by $\mathbb R_{\ge0}$) define càdlàg paths in other settings.
• BellmanDP.Inventory.renewal_equation_exists_unique is a linear renewal equation with a density kernel of mass below $1$.

Contributions are welcome on any milestone, in any order. The windowed estimates (milestones 2–4) and the measurability step (milestone 5) are independent of each other.

Selected references

• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Annals of Applied Probability 19(6), 2009, 2211–2269. arXiv:0912.2837v1, doi:10.1214/09-AAP609
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981, 567–588. doi:10.1287/opre.29.3.567
• A. A. Puhalskii, M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Advances in Applied Probability 32, 2000, 564–595. MR1778580
• P. Jelenković, A. Mandelbaum, P. Momčilović, Heavy traffic limits for queues with many deterministic servers, Queueing Systems 47, 2004, 53–69. MR2074672
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Chapter 16. doi:10.1002/9780470316962

Motivation

In a wireless multihop network, a switch, or a parallel computer, transmissions interfere: two links that share a receiver, or two crossbar paths that share a port, cannot be active in the same time slot. The scheduler must choose, slot by slot, a set of links that may operate together and decide which traffic each one carries. The basic question is which arrival rates a network can sustain at all, and whether a single scheduling rule sustains every one of them without knowing the rates.

Tassiulas and Ephremides answered both questions in 1992 for a general slotted model with interference constraints, multihop routing and several traffic classes (IEEE Trans. Automat. Control 37(12):1936–1948). Their policy, here called $\pi_0$, weighs each link by the largest queue-length difference it can reduce and activates a maximum-weight feasible set. It is the origin of the max-weight and back-pressure scheduling rules that later became standard in switch scheduling (McKeown, Mekkittikul, Anantharam and Walrand, 1999) and in stochastic network optimization (Georgiadis, Neely and Tassiulas, 2006).

Setting

A constrained queueing network has $L$ nodes, $N$ servers (links) and $J$ customer classes. Server $i$ moves customers from its origin node $q(i)$ to its destination node $h(i)$. Class $j$ leaves the network on reaching a node of its destination set $V_j$; at every other node $l$ it has a queue $(l,j)$, whose length at the end of slot $t$ is $X_{lj}(t)\in\mathbb N$.

The constraint set $S$ is the family of sets of servers that may be active in the same slot. Assumption C.1 says that every subset of an activation set is an activation set. In each slot a stationary policy, given the state $x=X(t-1)$, chooses a set of servers in $S$ and the class each active server serves; an activation rule never activates more servers of queue $(l,j)$ than there are customers $x_{lj}$. The class of all such rules is $H$. An activated server $i$ completes its service with probability $m_i$, independently. New arrivals $A_{lj}(t)$ are i.i.d. over slots, independent across queues and of the services, with finite second moments and means $a_{lj}$. Under a stationary rule the vector $X(t)$ is a Markov chain on $\mathbb N^{\{\text{queues}\}}$.

The chain is stable (Definition 3.1) if, from every transient state, it enters a closed communicating class with probability one, and every state of a closed communicating class is positive recurrent. The stability region $C_\pi$ of a policy is the set of rate vectors $a$ for which the system is stable under $\pi$; the stability region of the system is $C=\bigcup_{\pi\in H}C_\pi$.

A family $f=(f_{ij})\ge0$ is an $a$-admissible flow if it satisfies flow conservation, $a_{lj}=\sum_{q(i)=l}f_{ij}-\sum_{h(i)=l}f_{ij}$ at every queue; $\hat f_i=\sum_jf_{ij}$ is its total flow through server $i$. With $\mathrm{co}(S)$ the convex hull of the indicator vectors of the activation sets,

$$C'=\{a\ge0:\ \exists f\in F_a,\ c\in\mathrm{co}(S),\ m_i^{-1}\hat f_i<c_i\text{ if }\hat f_i>0,\ \hat f_i=0\text{ if }c_i=0\}.$$

Formalization targets

Goal: Theorem 3.2

$$C'\subset C\subset\bar C',\qquad C'\subset C_{\pi_0}\subset C\subset\bar C_{\pi_0}.$$

The system stability region is pinned between $C'$ and its closure, and policy $\pi_0$, whatever its tie-breaking, stabilizes every rate vector in $C'$. Inclusions are not strict.

Milestones

1. Lemma A.1: $\mathrm{co}(S)$ is closed under $0\le a\le c$ (under C.1).
2. Lemma 3.1: $\bar C'=\{a:\exists f\in F_a,\ c\in\mathrm{co}(S),\ M^{-1}\hat f\le c\}$.
3. Theorem 3.1: a function bounded below with drift $\le-\epsilon$ outside a finite set, and finite conditional expectation on it, makes a countable chain stable in the sense of Definition 3.1.
4. (A.6)–(A.7): for $V(x)=\sum_{l,j}x_{lj}^2$, the one-step drift under $\pi_0$ is finite everywhere and below $-\epsilon$ once $V(x)\ge b$.
5. Lemma 3.2: $C'\subset C_{\pi_0}$.
6. Lemma 3.3: for $a\notin\bar C'$, the system is unstable under every policy in $H$.

An optional item states the claim of Remark 1: if $a\in\bar C'\setminus C'$, then $\delta a\notin\bar C'$ for every $\delta>1$.

Significance

Theorem 3.2 shows that a throughput-optimal stationary policy exists, which is not obvious: stability regions of different policies need not be nested, so a policy whose region contains all the others has to be exhibited. It also describes the system stability region by a deterministic flow condition, $C'$, which can be checked without simulating any policy. The same drift argument underlies the stability proofs of max-weight switch schedulers, back-pressure routing and the drift-plus-penalty method.

The result is proved in the paper, with a proof sketched in places (Theorem 3.1 is called "a trivial extension of Foster's criteria", Lemma A.1 is omitted, Lemma 3.3 is argued by ergodicity in a paragraph). As far as a search of the platform shows, none of these statements has a machine-checked proof: Foster's criterion is posed on the platform only for irreducible chains on $\mathbb N$, and the back-pressure results already posed concern fluid models of other networks. A complete formal development would supply the reducible-chain Foster criterion, the convex-geometry lemma on $\mathrm{co}(S)$, the quadratic drift computation and the ergodic converse.

Difficulty

The obvious argument is a quadratic Lyapunov drift bound, but it does not go through as is in three places. First, the drift bound needs a direction of decrease from every large state: the largest queue must be connected to a destination through servers that can actually be activated, which is where assumption C.2 and the topology of $S$ enter (A.21)–(A.24). Second, stage 3 of $\pi_0$ defers some activations to respect the rule "no service for nonexisting customers", so the chosen schedule is not exactly maximum-weight and the loss has to be bounded uniformly. Third, the chain is in general reducible, so Foster's criterion for irreducible chains does not apply; the extension must show that every closed class meets the finite exceptional set and that transient states are left almost surely. The converse, Lemma 3.3, needs a law-of-large-numbers argument for an arbitrary stationary rule on a positive recurrent class, together with compactness of acyclic flows (Lemma 3.1).

Formalization scope

Nodes, servers and classes are Fin L, Fin N, Fin J (0-based). $S$ is a Set (Finset (Fin N)); a queue is a pair $(l,j)$ with $l\notin V_j$, and a state is a function from queues to $\mathbb N$. A multiclass activation vector assigns to each server an optional class. The transition matrix of the queue-length chain is written out explicitly as a sum over arrival vectors and Bernoulli service outcomes; Definition 3.1 is stated through this matrix (first-entry probabilities, essential states, positive recurrence), with values in $[0,\infty]$.

Conventions committed to, and hypotheses added relative to the page:

• Standing assumptions of the goal: C.1; $\emptyset\in S$ (the idle schedule is always allowed); $0<m_i\le1$; and C.2 in a topological form, a chain of servers from every non-destination node of class $j$ to $V_j$ (stronger than the printed sentence, which covers only nodes that class $j$ can reach).
• Every single server is an activation set, $\{i\}\in S$. The proof of Lemma 3.2 uses this at (A.24) without stating it; without it a server that can never be activated breaks the drift bound and Lemma 3.2.
• Stability regions quantify over laws. $C_\pi$ is the set of nonnegative rate vectors for which the chain is stable for every arrival law with finite second moments and those means. $C'$ is intersected with $a\ge0$.
• $\pi_0$ is a family. Statements hold for every rule satisfying the three stages, with arbitrary tie-breaking.
• Expectations of unbounded functions are real series with explicit summability, so a divergent expectation is never read as $0$.

A formalization in which $C_\pi$ asks for stability under one convenient arrival law, or in which negative rates are admitted, or in which $\pi_0$ is one fixed tie-break, would be a different theorem; the definitions rule each of these out.

Infrastructure needed: hitting probabilities and positive recurrence for countable chains (reusable beyond this mission), convex hulls of finite point sets, a cycle-cancelling bound for multicommodity flows, and the ergodic theorem for positive recurrent chains. Proofs of any milestone, and reusable lemmas on countable Markov chains, are welcome.

Selected references

• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Trans. Automat. Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3):355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• N. McKeown, A. Mekkittikul, V. Anantharam and J. Walrand, Achieving 100% throughput in an input-queued switch, IEEE Trans. Commun. 47(8):1260–1267, 1999. https://doi.org/10.1109/26.780463
• L. Georgiadis, M. J. Neely and L. Tassiulas, Resource allocation and cross-layer control in wireless networks, Found. Trends Netw. 1(1):1–144, 2006. https://doi.org/10.1561/1300000001

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$, $j\in\mathbb Z$, be independent, identically distributed random variables in $[0,1]$. The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$. Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$, moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$. The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$.

Fix $\theta>1$ and $0<\gamma<1$. Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$. Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$. A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$, with $T_j=\infty$ if it never does. For $b>0$, $\log_b x$ means the logarithm in base $b$, and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

$$\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.$$

When $\gamma\theta>1$, the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

$$\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.$$

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$. The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$.

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$, then

$$\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.$$

The second clause describes the supercritical case. If $\gamma\theta>1$, $n_k\to\infty$, and $\{\log_\theta n_k\}\to\varepsilon$, then for each $x>0$,

$$P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).$$

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$; the two passage-time results use base $1/\gamma$, exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$. The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$, their accumulation produces a logarithmic correction; at $\gamma\theta>1$, the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$, $0<\gamma<1$, $\gamma\theta\ge1$. The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$.

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

• Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$, the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

• 1949. Feller proves the central limit theorem for the renewal counting process.
• 1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
• 1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$, let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$. The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ($k \ge 0$), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$, where $T_{-1} = 0$). Write $\mu_r = E t_1^r$.

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$, $n \ge 1$, are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$. Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$.

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$. Put $\kappa^{(i)}_1 = E y^{(i)}_1$. The covariance matrices are

$$a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).$$

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$, then as $t \to \infty$

$$\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),$$

and if in addition $\mu_2 < \infty$,

$$\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).$$

Milestones

• The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
• Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$, then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$.
• Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
• Its $M$-dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
• Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$, then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$.
• Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$.

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$, the basis of the regenerative method of simulation output analysis. With $w_t = n_t$, Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$, needs only $\mu_1 < \infty$, which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$, not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

• Time is real; every limit is along $t \to \infty$ in $\mathbb R$. Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$.
• $n_t$ is a natural number, the number of epochs $T_j \le t$; on the null event where infinitely many epochs are $\le t$ it is $0$. Finiteness is never assumed.
• $\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$, set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
• Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$. No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
• "Jointly normally distributed with covariance matrix $a$" is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
• The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$. The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
• $\mu_1 < \infty$, $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$; the Cramér–Wold step.

Selected references

• W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
• F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
• W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
• J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

Motivation

Inventory systems in which unmet demand is lost, not backlogged, are the norm in retail: a customer who finds an empty shelf buys elsewhere. With a positive lead time $L$ between ordering and delivery, the optimal policy for such a system depends on the entire pipeline of outstanding orders, so dynamic programming is intractable beyond small $L$. Optimal policies are not of base-stock type, and for decades no policy with a provable guarantee on its expected cost was known for this model.

Levi, Janakiraman and Nagarajan (Math. Oper. Res. 33(2), 2008) gave the first such guarantee. Their dual-balancing policy balances, in every period, the expected holding cost against the expected lost-sales penalty of the units ordered now, and it costs at most twice as much as an optimal policy.

Timeline.

• 2007. Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2)) introduce marginal cost accounting and the dual-balancing policy for the backlogging model, with a worst-case guarantee of 2.
• 2008. Levi, Janakiraman and Nagarajan extend the guarantee to lost sales (this mission). In their model the truncated inventory positions of the two policies can cross back and forth inside a lead time, which the backlogging argument never meets.
• 2009. Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science, 2009) prove that order-up-to policies are asymptotically optimal in the lost-sales model as the penalty cost grows.
• 2021 onward. Xin (Oper. Res., 2021; SSRN 7134538) analyses capped base-stock policies for i.i.d. lost-sales demand, culminating in a 2.33-approximation guarantee for that policy class, whose main theorem is proved on Prove2Me.

Page and display numbers in this mission refer to the authors' accepted manuscript (28 pages, pp. 1–28), not to the journal's pages 351–374.

Setting

Periods are $t=1,\dots,T$. An order $Q_s\ge0$ placed in period $s$ arrives at the start of period $s+L$, where $L\ge1$ is an integer. Before the horizon there are $x_0\ge0$ units on hand and pipeline orders $Q_j=q_j\ge0$ for $1-L\le j\le0$. Demands $D_1,\dots,D_T\ge0$ have finite means. The information $\mathcal F_s$ available at the start of period $s$ contains $D_1,\dots,D_{s-1}$ and possibly more. A feasible policy chooses $Q_s$ as an $\mathcal F_s$-measurable quantity.

The on-hand inventory $I_t$ at the start of period $t$, after the arrival, satisfies $I_1=x_0+Q_{1-L}$ and

$$I_{t+1}=(I_t-D_t)^+ + Q_{t+1-L}.$$

Demand $(D_t-I_t)^+$ is lost. Costs are a holding rate $h_t\ge0$, a lost-sales penalty $p_t\ge0$ and an ordering cost $c_t\ge0$ per unit, where $p_t$ and $c_t$ are non-increasing in $t$.

Marginal cost accounting. Under first-ordered-first-consumed bookkeeping, $H_s$ is the ordering cost $c_sQ_s$ plus the holding cost that the $Q_s$ units incur until the end of the horizon, and $\Pi_s=p_{s+L}(D_{s+L}-I_{s+L})^+$ is the lost-sales penalty in the period in which they arrive. The cost of a policy $P$ is

$$\mathcal C(P)=\sum_{s=1}^{T-L}\bigl(H^P_s+\Pi^P_s\bigr).$$

It omits only costs that are the same for every policy.

The truncated inventory position of period $s$ with respect to $t\le s$ is $Y_{st}=I_s+\sum_{j=s+1-L}^{t}Q_j$. For two policies $B$ and $P$, the set $\mathcal T_H$ holds the periods $t\le T-L$ with $Y^B_{st}<Y^P_{st}$ for every $s\in[t,t+L]$, and $\mathcal T_\Pi$ holds the remaining periods $t\le T-L$.

A dual-balancing policy $B$ orders, in each period $t\le T-L$, the amount that equalises the two conditional expectations

$$E[H^B_t\mid\mathcal F_t]=E[\Pi^B_t\mid\mathcal F_t]=:Z_t.$$

Formalization targets

Goal: Theorem 3.1

If demands are independent, then for every feasible policy $P$

$$E[\mathcal C(B)]\le 2\,E[\mathcal C(P)].$$

Comparing with every feasible $P$, rather than with an optimal policy, gives the guarantee without assuming that an optimum is attained.

Milestones, in attack order

1. (11) For $t\le s\le t+L$, $I_{t+L}=Y_{st}-D_{[s,t+L)}+\sum_{r=s}^{t+L-1}(D_r-I_r)^+$.
2. Lemma 3.2. On every sample path, $\sum_{t\in\mathcal T_H}H^B_t\le\sum_{t}H^P_t$.
3. Lemma 3.3. On every sample path, $\sum_{t\in\mathcal T_\Pi}\Pi^B_t\le\sum_{t}\Pi^P_t$.
4. (14) $E[\mathcal C(P)]\ge E\bigl[\sum_t(\mathbb 1_{t\in\mathcal T_H}H^B_t+\mathbb 1_{t\in\mathcal T_\Pi}\Pi^B_t)\bigr]$.
5. Lemma 3.1. $E[\mathcal C(B)]=2\sum_{t=1}^{T-L}E[Z_t]$.
6. Lemma 3.4. This lemma characterises the crossing events $A_{st}=[Y^B_{st}<Y^P_{st}]\cap[Y^B_{s+1,t}\ge Y^P_{s+1,t}]$.
7. Lemmas 3.5 and 3.6. Under independence, conditioning on $t\in\mathcal T_H$ (respectively $t\in\mathcal T_\Pi$) does not lower the conditional expected holding (respectively lost-sales) cost of $B$ below $Z_t$.

Significance

The result. The theorem gives a constant-factor guarantee for a lost-sales system with lead times, for arbitrary independent and non-identical demand distributions. The policy is computed online, one period at a time, from one-dimensional conditional expectations, which an optimal policy cannot be. The guarantee holds with time-dependent holding costs and with non-increasing ordering and penalty costs. Section 5 of the paper extends it to correlated demand structures, which are out of this mission's scope.

Formalizing it. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The mission produces the lost-sales dynamics, the truncated inventory position, marginal cost accounting and the sample-path amortization lemmas as reusable Lean objects. It also produces a formal treatment of the conditional-expectation step under independence, which the backlogging analysis does not need. The sibling mission on the backlogging model, LeviBalancing.DualBalancing, provides the shared instance and policy definitions that are reused here.

Difficulty

In the backlogging model, $t\in\mathcal T_H$ is decided by information available at time $t$, so the cost comparison can be made period by period after conditioning on $\mathcal F_t$. With lost sales this fails: the truncated positions of $B$ and of the benchmark can cross from below to above and back inside the window $[t,t+L]$. Whether $t\in\mathcal T_H$ is therefore not known at time $t$, and conditioning on that event moves the conditional expectations of $H^B_t$ and $\Pi^B_t$ away from $Z_t$. A newcomer's first idea, to reuse the backlogging argument with $\mathcal F_t$-measurable indicators, does not apply. The lost-sales penalty also cannot be charged period by period: Lemma 3.3 is a global amortization over intervals. The non-increasing penalties are what make that amortization possible when $p_t$ varies.

Formalization scope

• Periods are integers. The pipeline $Q_j$, $j\le0$, is shared by every policy through the published order. Instance, cumDemand, order, DemandProcess and IsFeasiblePolicy are reused from LeviBalancing.DualBalancing. The new layer is one definition file, LostSalesBalancing.DualBalancing.Model.
• Orders and demands are real (fractional orders, as in §3.1). The randomized integral-order variant is out of scope.
• Cost generality is that of Theorem 3.1. Rates are only required to be $\ge0$, which strengthens the paper's stationary $h,p>0$. Accordingly (11) is stated in lost units, and Lemma 3.4(iv) is stated as positive lost demand, not positive penalty.
• Independence. The paper assumes independent demands but lets $\mathcal F_s$ hold more than past demands. The formalization requires $\mathcal F_t$ to be independent of $(D_t,\dots,D_T)$ for every $t$, which for the natural filtration is exactly mutual independence. Finite means are integrability.
• "OPT" becomes every feasible policy in Theorem 3.1, (14) and Lemmas 3.5–3.6. In the sample-path statements, (11) and Lemmas 3.2–3.4, it becomes every nonnegative order sequence.
• Conditional events. $\Pr(A\mid\mathcal F)\,E[X\mid\mathcal F,A]$ is written $E[\mathbb 1_AX\mid\mathcal F]$, which never divides by a zero probability.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$. The dual-balancing predicate requires $H^B_t$ and $\Pi^B_t$ to be integrable, so no conditional expectation takes Mathlib's default value $0$.
• Lemma 3.4(iii) is stated with $D_s\ge I^P_s-\Delta Q_s$. The printed strict inequality excludes a tie at which the event $A_{st}$ does occur.
• A trivializing formalization is ruled out: the dual-balancing predicate and the independence hypothesis are jointly satisfiable with $T>L$ (checked locally on an explicit instance), and no statement is meaningful only when $T\le L$, the case in which every cost is zero.

Contributions welcome: proofs of the sample-path lemmas, which need only finite sums and the recursion; the conditional-expectation lemmas, which need a Harris-type argument for independent coordinates; and the existence of a measurable balancing order, which this mission does not pose.

Selected references

• R. Levi, G. Janakiraman, M. Nagarajan, A 2-Approximation Algorithm for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research 33(2), 351–374, 2008. https://doi.org/10.1287/moor.1070.0285
• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2), 284–302, 2007. https://doi.org/10.1287/moor.1060.0205
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science, 2009. https://doi.org/10.1287/mnsc.1080.0945
• L. Xin, capped base-stock policies in lost-sales inventory models, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2019
• L. Xin, Capped Base-Stock Policies: A 2.33-Approximation, SSRN working paper 7134538, 2026. https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538