Probability

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$, $T_{iG}\ge 1$ is the first passage time to $G$. The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$. The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$. The mean first passage time is $m_{iG}=E[T_{iG}]$, infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$. A state $i$ is positive recurrent when $m_{ii}<\infty$, and the steady state probability is $\pi_i=m_{ii}^{-1}$. On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$. The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$. Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$, and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$, a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$. The quantities of $\Gamma_N$ are written $m_{iG}(N)$, $c_{iG}(N)$, $\pi_i(N)$ and $J(i)(N)$. An AS is conforming (for a $z$ standard $\Gamma$) if, for large $N$, $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$. It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$:

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$.

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$,

and if $G\subseteq R$ it is also conforming on $R$. No rate of convergence and no constants are involved, and $G$ need not contain $z$.

Milestones

1. Proposition C.4.2: for fixed $t$, $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$.
2. Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$.
3. Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$.
4. Proposition C.4.6: on a positive recurrent class, convergence of $\pi$, of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$, of $c_{zz}$ and of all $c_{iG}$ are equivalent.
5. Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$, and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$.

Further results

6. Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$, the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$.
7. Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$, the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$. First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$, a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$, and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$, $c_{iG}$, $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$. $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$, the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$. $\Gamma_N$ is built as an MC on the subtype of $S_N$, and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$. Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ($N<N_0$ or a state outside $S_N$). For fixed states this affects finitely many $N$, and all statements are limits, $\liminf$s or eventual equalities. All convergence is in $[0,\infty]$. The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$.

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$, is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$, and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
• D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

Motivation

Control problems for queueing systems (admission control, service rate control, routing to parallel servers) are naturally modelled as Markov decision chains whose state is a vector of queue lengths. The state space is therefore denumerably infinite, and the performance measure of interest is usually the long-run average cost per slot. For such models the existence theory of average cost optimal stationary policies is well developed (Chapter 7 of Sennott's book), but existence gives no algorithm: an optimal policy is a function on an infinite set, and value iteration cannot be run on an infinite state space.

The approximating sequence method answers this by replacing the infinite model $\Delta$ with a sequence of finite models $\Delta_N$ on truncated state spaces $S_N$, solving the average cost optimality equation in each, and passing to the limit. Chapter 8 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) gives a set of conditions, the (AC) assumptions, under which this limit procedure provably produces the minimum average cost and an average cost optimal policy of $\Delta$.

Timeline. The approximating sequence method for the average cost criterion and the (AC) assumptions were introduced in Sennott (1997a), with further results in Sennott (1997b) (bibliographic notes, p. 194). The book collects these results, adds the four step verification template (Proposition 8.2.1), the finite-set augmentation route based on the (BOR) assumptions (Proposition 8.2.3), and the weakening (WAC) of Section 8.7, which Chapter 9 uses.

Setting

An MDC $\Delta$ has a countable state space $S$, a finite nonempty action set $A_i$ in each state $i$, a finite cost $C(i,a)\ge0$, and transition probabilities $P_{ij}(a)$. A general policy $\theta$ chooses actions at random using the whole past history. Its average cost is

and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)\in[0,\infty]$. A policy is average cost optimal if $J_\theta\equiv J$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite sets $S_N$ increasing to $S$ and MDCs $\Delta_N$ on $S_N$ with the same actions and costs and with transition probabilities $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$. Write $v^N_n$ and $V^N_\alpha$ for the $n$-horizon and discounted value functions of $\Delta_N$.

The (AC) assumptions are:

• (AC1) there are finite constants $J^N$ and finite functions $r^N$ on $S_N$ with

• (AC2) $\limsup_N r^N(i)<\infty$;
• (AC3) $\liminf_N r^N(i)\ge -Q$ for a constant $Q\ge0$;
• (AC4) $J^*:=\limsup_N J^N<\infty$ and $J^*\le J(i)$ for all $i$.

The (WAC) assumptions of Section 8.7 allow $Q$ to depend on the state, at the price of integrability conditions along every stationary policy.

Formalization targets

Goal: Theorem 8.1.1

Under (AC), the limit $\lim_{N\to\infty}J^N$ exists and

and every limit point $e^*$ of stationary policies $e^N$ realizing the minimum in (8.1) is average cost optimal for $\Delta$. The statement fixes no constants; it asserts the shape of the conclusion for any model satisfying (AC).

Milestones

• Proposition 8.2.1 (the four step template): unichain and aperiodicity of the finite models, an $x$ standard policy at which the approximating sequence is conforming, a comparison of $v^N_n$ (or $V^N_\alpha$) with $v_n$ (or $V_\alpha$), and a lower bound on $v^N_n - v^N_n(x)$ together imply that the value iteration limits

exist and satisfy (AC).

• Corollary 8.2.2: on $S=\{0,1,2,\dots\}$ with $S_N=\{0,\dots,N\}$ and excess probability sent to $N$, monotonicity of $v^N_n$, $v_n$ and of the first passage moments of a $0$ standard policy suffices.
• Proposition 8.2.3: an augmentation type approximating sequence that sends excess probability to a finite set of cheap states satisfies the template.
• Proposition 8.5.1: in the single-server queue with Bernoulli($p$) arrivals and constant service rate $a>p$,

• Proposition 8.7.1: the conclusions of Theorem 8.1.1 hold under (WAC).

Significance

The result itself. Theorem 8.1.1 is what turns the existence theory of Chapter 7 into a computation. It certifies that the minimum average costs of the truncations converge to the minimum average cost of the infinite model, that this cost is constant, and that the policies produced by value iteration on $\Delta_N$ converge, along subsequences, to an optimal policy for $\Delta$. Propositions 8.2.1–8.2.3 reduce (AC) to properties that can be checked model by model; Section 8.3 checks them for queues with reject option, service rate control, and routing to parallel queues. Proposition 8.7.1 is the version used in Chapter 9 for models whose relative values are not uniformly bounded below. Proposition 8.5.1 gives the closed-form open-loop benchmark used in the numerical study of Section 8.5.

Formalizing it. All results are proved in the book; none has a machine-checked proof. A formalization would give the first verified convergence theorem for truncations of denumerable-state average cost MDPs, and would make the approximating sequence method usable as a certified reduction from infinite to finite models. The template results (8.2.1–8.2.3) additionally require a formal treatment of conformity of approximating Markov chains (Appendix C.4–C.5), which is of independent use.

Difficulty

The naive argument takes limits in (8.1) along $N$: the minimum over $a$ and the finite sums pass to the limit only in the inequality direction, and only after a Fatou-type lemma for sums against the converging distributions $P_{ij}(a;N)$ with integrands $r^N$ that are neither bounded nor monotone. The lower bound $-Q$ in (AC3) is exactly what makes this possible; without it the limit inequality can fail. The limit inequality then produces only an average cost optimality inequality, and turning it into optimality of the limit policy requires a separate argument that a function bounded below and satisfying the inequality yields an upper bound on the average cost. Existence of $\lim_N J^N$ is not given: (AC4) controls only the limit superior, and the limit must be identified through every subsequence. For the template results, the difficulty is in the Markov chain side: the convergence of first passage times and costs of the truncated chains, which fails for general approximating sequences (Examples C.4.4, C.4.7).

Formalization scope

The Lean development is in the namespace SennottDP.AvgASM. The state space is any countable type; action sets are Finsets, assumed nonempty; costs are finite and nonnegative (ℝ≥0); transition probabilities are ℝ≥0∞-valued, with each row a probability distribution for admissible actions. All value functions and average costs take values in $[0,\infty]$ (ℝ≥0∞), and every infimum over policies ranges over the full class of history-dependent randomized policies. The $J^N$ and $r^N$ of (AC1) are real; the limits superior and inferior over $N$ in (AC2)–(AC4) and (WAC) are taken in EReal, so an unbounded sequence cannot produce a junk finite value. The equality $J(i)=\lim_N J^N$ is stated in EReal, which also asserts that $J(i)$ is finite. Quantities of $\Delta_N$ at states outside $S_N$ are junk values that affect only finitely many $N$ for each state.

A trivializing formalization is ruled out: $J^N$ and $r^N$ are the witnesses of (AC1), not free variables, the policies $e^N$ must realize the minimum in (8.1) for those witnesses, and the minimum average cost $J$ is an infimum over all policies, so the goal cannot be satisfied by choosing $J^*$ or the limit policy.

A complete development needs: the induced process law of a general policy; the average cost optimality inequality argument (Lemma 7.2.1); the finite-state average cost results of Chapter 6 (Propositions 6.4.1, 6.5.1, 6.6.3); a Fatou lemma for converging distributions (Proposition A.2.5); limit points of policy sequences (Proposition B.5); and, for the template results, the theory of $z$ standard chains and conformity (Appendix C.2–C.5). The Markov chain layer and the approximating sequence definitions are reusable beyond this mission. Contributions of any of these intermediate results as separate theorems are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997), 114–137 (cited as Sennott (1997a) in the book).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR — Mathematical Methods of Operations Research 45 (1997), 45–62 (cited as Sennott (1997b) in the book).

Motivation

Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.

The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.

Setting

A single item is produced in periods $n = 1, 2, \dots$ of an infinite horizon; at most $c$ units can be produced per period. The demand of period $n$ is $D_n$; the demands are nonnegative, independent and identically distributed, with generic demand $D$ and $E[D] < c$ (the standing assumption of Section 8.1.1).

Under the modified $(s-1, s)$ policy with target level $s$, the facility observes $D_n$ and produces $\min\{c, s - I_{n-1} + D_n\}$ units, where $I_n$ is the end-of-period net inventory and $I_0 = s$. The shortfall $V_n = s - I_n$ satisfies $V_0 = 0$ and

With the random walk $S_n = \sum_{k=1}^{n} (D_k - c)$ ($S_0 = 0$), the stationary shortfall is

A law on $\mathbb R$ is lattice if it is concentrated on a progression $a + d\mathbb Z$ with $d > 0$.

In the discrete case ($c$ and $D$ integer valued) $(V_n)$ is a Markov chain on $\{0, 1, 2, \dots\}$ with transition probabilities $p_{ij}$ (p. 185). In the repair model of Section 8.3.1, reparable units of item $i$ arrive at rate $\lambda_i$, $\lambda = \sum_i \lambda_i$, a single exponential server repairs at rate $\mu > \lambda$, $N$ is the number of units in repair and $N_i$ the number of item-$i$ units, and $\eta_i = \lambda_i/(\mu - \lambda + \lambda_i)$.

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Assume $E[e^{\alpha D}] < \infty$ for all $\alpha < \delta$, with $\delta > 0$; $P[D > c] > 0$; the law of $D$ is non-lattice; and $E[e^{-\alpha(c-D)}] = 1$ has a root in $(0, \delta)$. Then there are $\beta > 0$ and $\alpha > 0$ with

The constant $\beta$ is left unspecified, as in the book.

Milestones, in attack order

1. Eq. (8.1): under the modified policy, $s - I_n = V_n$ for every $n$, independently of $s$.
2. Section 8.1.1: $V < \infty$ almost surely, $P\{V_n > v\} \to P\{V > v\}$ for every $v$, and the law of $V$ is stationary for (8.1).
3. Eq. (8.2): for $v > 0$, $P\{V_n > v\} = P\{D_n > v + c\} + E_D[1(d \le v + c)\, P\{V_{n-1} > v + c - d\}]$.
4. Theorem 11, second sentence: $E[e^{-\alpha(c-D)}] = 1$ has at most one positive root.
5. Section 8.1.2: with integer demand, $(V_n)$ is a Markov chain with transition probabilities $p_{ij}$.
6. Section 8.1.2: $\pi_i = \lim_n P\{V_n = i\}$ exists and solves $\pi\mathcal P = \pi$, $\sum_i \pi_i = 1$, $\pi_i \ge 0$.
7. Section 8.3.1: if $N$ is geometric with parameter $\lambda/\mu$ and $N_i$ given $N = j$ is binomial$(j, \lambda_i/\lambda)$, then $P[N_i = j] = (1 - \eta_i)\eta_i^j$.
8. Section 8.3.1: $\sum_{j > s} p_i(j) = \eta_i^{s+1}$, and the smallest cost-minimising stock level is the smallest $s$ with $\eta_i^{s+1} \le h_i/(h_i + b)$.

Significance

The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate $\alpha$ depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of $N_i$ reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.

The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.

Difficulty

The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root $\alpha$ turns $P\{V > v\}$ into an expectation under a law with positive drift, but it only yields the upper bound $P\{V > v\} \le e^{-\alpha v}$ (Lundberg's inequality); it does not show that $e^{\alpha v}P\{V > v\}$ converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of $V_n$ with that of $\max_{k \le n} S_k$, plus the strong law of large numbers to show $V < \infty$ from $E[D] < c$.

Formalization scope

• Model. Demands are real, nonnegative, measurable, i.i.d. (iIndepFun plus IdentDistrib with $D_1$), integrable, with $E[D] < c$; these are fields of ShortfallModel. Periods are numbered from $1$ as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with $\mathbb N$-valued demand and capacity.
• Stationary shortfall. The book's "stationary distribution ... Let $V$ represent this random variable" is pinned to $V = \sup_{n \ge 0} S_n$, taken in $[0, \infty]$ and converted to a real number; milestone 2 proves that it is the limit law of $V_n$ from $V_0 = 0$ and a stationary law of (8.1). The discrete $\pi_i$ is pinned to $\lim_n P\{V_n = i\}$.
• Corrections to Theorem 11. The printed theorem is false. For integer demand $P\{V > v\}$ is a step function, and no $\beta e^{-\alpha v}$ is asymptotic to it. If $E[e^{\alpha D}]$ is finite only for $\alpha < \delta$, the equation $E[e^{-\alpha(c-D)}] = 1$ may have no root in $(0,\delta)$. The goal therefore adds two labelled hypotheses: a non-lattice demand law, and a root in $(0, \delta)$. The mass-exponential demand of Section 8.1.3 (an atom at $0$ plus a density) is non-lattice. The approximation $\beta \approx e^{-2(.583)(c-E(D))/\sigma}$ is not stated.
• Repair model. The M/M/1 queue is not built. The geometric law of $N$ (asserted on p. 202) and the binomial split of $N$ (quoted from Chapter 3) enter milestone 7 as hypotheses, exactly as the page's proof uses them. The stability condition $\lambda < \mu$, not written on the page, is a hypothesis. "The optimal $s_i$" is read as the smallest minimiser of the cost.
• Ruled out. Stating Theorem 11 with $\alpha$ or $\beta$ allowed to depend on $v$, with $\beta = 0$ (the ratio would be a division by zero, which Lean evaluates to $0$), or for a $V$ postulated to have an exponential tail proves nothing. Here $\beta, \alpha$ are quantified before $v$, both are asserted positive, and $V$ is constructed from the demands.
• Not formalized. The mass-exponential approximations (8.3)–(8.4), the Roundy–Muckstadt refinement, the fill-rate formula $\eta(s)$ (a definition, whose steady-state identity needs uniform integrability the book does not discuss), the random-capacity chain on p. 186, and the monotonicity of $s_i$ in $\mu$.
• Reusable infrastructure. Welcome: the Lindley recursion and its reversal identity, the Loynes existence theorem, Lundberg's inequality, and a non-lattice renewal theorem. All of these are needed well beyond this mission, in queueing (GI/G/1 waiting times) and ruin theory.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 8. https://doi.org/10.1007/b138879
• P. Glasserman, Bounds and asymptotics for planning critical safety stocks, Operations Research 45(2), 244–257, 1997. https://doi.org/10.1287/opre.45.2.244
• P. Glasserman and S. Tayur, Sensitivity analysis for base-stock levels in multiechelon production-inventory systems, Management Science 41(2), 263–281, 1995 (the book's reference [97]). https://doi.org/10.1287/mnsc.41.2.263
• R. O. Roundy and J. A. Muckstadt, Heuristic computation of periodic-review base stock inventory policies, Management Science 46(1), 104–109, 2000. https://doi.org/10.1287/mnsc.46.1.104.15131
• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Chapter XII.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Chapter XIII. https://doi.org/10.1007/b97236

Motivation

Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level $s$. Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.

Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.

Setting

A single item is stocked at one location. Customer orders arrive at epochs $T_0 < T_1 < \cdots$ of a Poisson process with rate $\lambda > 0$, started empty at time $0$: the interarrival times $A_k$ are independent and exponential with rate $\lambda$, and $T_k = A_0 + \cdots + A_k$. The $k$-th order triggers a resupply order with resupply time $L_k \ge 0$. The resupply times are independent and identically distributed, independent of the arrival process, with a density $g$, distribution function $G(u) = P[L \le u]$ and finite mean

With backorders allowed, the number of units in resupply at time $t$ is

and $N(t) = \#\{k : T_k \le t\}$ counts the orders placed in $[0,t]$. On-hand stock and backorders at time $t$ are $(s - X(t))^+$ and $(X(t) - s)^+$.

In the compound Poisson version the $k$-th order asks for $X_k \ge 1$ units, the sizes are i.i.d. with $u_j = P[X_k = j]$, independent of arrivals and resupply times, and all units of one order share its resupply time $L_k$. The units in resupply are $Y(t) = \sum_{k : T_k \le t < T_k + L_k} X_k$. Writing $u^{(y)}_n$ for the probability that $y$ orders ask for $n$ units in total, the compound Poisson probabilities with parameter $\mu$ are

In the lost-sales version an order that finds no stock on hand is lost, so at most $s$ units are ever in resupply.

Formalization targets

Goal: Palm's theorem (Theorem 6, p. 39)

For every $x \ge 0$,

The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.

The proof's milestones (pp. 38–41)

1. Eq. (3.5): $P[N(t) = n] = e^{-\lambda t}(\lambda t)^n/n!$.
2. Eq. (3.3): given $N(t) = n$, the epochs $(T_0, \dots, T_{n-1})$ have density $n!/t^n$ on $0 < t_1 < \cdots < t_n < t$.
3. Eq. (3.7): given $N(t) = n$, $X(t)$ is binomial with parameters $n$ and $p = \frac1t\int_0^t[1-G(u)]\,du$.
4. Eq. (3.8): for every $t > 0$, $X(t)$ is Poisson with mean $\lambda\int_0^t[1-G(u)]\,du$.
5. Eq. (3.10): $\int_0^t[1-G(u)]\,du \to \bar\tau$.

Extensions in Section 3.1

6. Theorem 7 (pp. 43–44): with compound Poisson demand, $\lim_{t\to\infty}P[Y(t) = n] = p(n \mid \lambda\bar\tau)$.
7. Theorem 8 (p. 44): in the lost-sales system with exponential resupply times of rate $\beta$, the probability vectors solving the balance equations are exactly the truncated Poisson law $\pi_x \propto (\lambda/\beta)^x/x!$, $0 \le x \le s$.
8. Theorem 9 (pp. 46–47): for a due-date delay $T \ge 0$, the units in resupply that have been there for at least $T$ satisfy $\lim_{t\to\infty}P[Y_T(t) = n] = p(n \mid \lambda\bar\tau\alpha)$ with $\alpha = \frac1{\bar\tau}\int_T^\infty[1-G(t)]\,dt$.

Significance

The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, $\bar\tau$. This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level $s$ are $\sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$, the fill rate is $P[X \le s - 1]$, and both can be optimized over $s$ with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.

Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.

Difficulty

The algebra of the proof (summing the binomial against the Poisson law of $N(t)$) is short. The work is in the probabilistic step the book treats in a sentence: that, given $N(t) = n$, the $n$ orders behave like independent uniform epochs, each of which independently is still in resupply at time $t$ with the same probability $p$. This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing $P[X(t) = x]$ by conditioning on individual epochs does not go through without that exchangeability step. The limit $t \to \infty$ is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.

Formalization scope

The model is a structure on a probability space $(\Omega, P)$: exponential interarrival times with rate $\lambda > 0$, nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from $0$, so the book's $X_1, \dots, X_n$ are $T_0, \dots, T_{n-1}$. Counts are cardinalities of sets of order indices, with value $0$ on the probability-zero event where infinitely many orders fall in a bounded interval.

Commitments and pinnings:

• "Steady state probability" (Theorems 6, 7, 9) is $\lim_{t\to\infty}P[\cdot(t) = x]$ for the system empty at time $0$, which is what the proofs compute via (3.8)–(3.11).
• Independence of resupply times from arrivals is not written in Theorem 6 but is used on p. 40; it is part of the model.
• The stock level $s$ does not enter the backorder model; it matters only in Theorem 8.
• Theorem 8 is stated algebraically: a vector on $\{0, \dots, s\}$ solves the balance equations (3.26), (3.25) for $0 < j < s$ and (3.32), and sums to one, if and only if it is the truncated Poisson law. The book obtains these equations by letting $t \to \infty$ in the forward equations under the unproved assumption $P_j'(t) \to 0$. The book writes (3.25) "for $0 \le j \le s$", which at $j = s$ contradicts its own (3.32); the boundary equation (3.32) is used. The sentence on p. 46 extending Theorem 8 to arbitrary resupply densities is asserted without proof and is not stated.
• Theorem 7 identifies the limit law by its probabilities (3.22)–(3.23); its mean $\lambda\bar\tau\bar u$ is a property of that law. Theorem 9 is stated for compound demand as the book states it, although the book's proof covers only the Poisson case.

A model in which $X(t)$ is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here $X(t)$ is computed from the primitive arrival and resupply times, whose joint law is fully specified.

Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 3. https://doi.org/10.1007/b138879
• C. Palm, "Analysis of the Erlang traffic formula for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
• G. J. Feeney and C. C. Sherbrooke, "The (s–1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
• C. C. Sherbrooke, "METRIC: A multi-echelon technique for recoverable item control", Operations Research 16(1), 1968, 122–141. https://doi.org/10.1287/opre.16.1.122
• S. M. Ross, Stochastic Processes, 2nd ed., Wiley, 1996, Section 2.3 (conditional distribution of arrival times) and Section 2.4 (the M/G/∞ queue).

Why certify nonconvex scenario solutions

The scenario approach replaces an optimization problem with uncertain constraints $\theta\in\Theta_\delta$, $\delta\in\Delta$, by the program that enforces only $N$ constraints $\Theta_{\delta_1},\dots,\Theta_{\delta_N}$ drawn at random from the distribution $\mathbb P$ of the uncertainty. Its solution $\theta^*$ is then judged by its violation, the probability that a new instance $\delta$ is not satisfied. For convex programs in $\mathbb R^d$ the violation is controlled by the dimension $d$ alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most $d$ support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.

Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:

• 2006–2008: the violation of convex scenario solutions is bounded, and then characterized exactly, in terms of $d$.
• 2018: the wait-and-judge theory (Campi and Garatti, Math. Programming 2018) evaluates the violation from the number of support constraints counted after solving the program; it extends to nonconvex programs but requires a nondegeneracy assumption.
• 2018: Campi, Garatti and Ramponi (IEEE TAC 2018) prove a bound in terms of the size of any support set, with no convexity and no nondegeneracy assumption. This is the result formalized here, stated in the book as Eq. (8.15).

Setting

Let $\Theta$ be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let $f:\Theta\to\mathbb R$ be a cost and $\Theta_\delta\subseteq\Theta$ constraint sets indexed by $\delta\in\Delta$, where $\Delta$ carries a probability $\mathbb P$. Neither $f$ nor the $\Theta_\delta$ is required to be convex. With a sample $\delta_1,\dots,\delta_N$ drawn independently from $\mathbb P$, the scenario program is

and $\theta^*$ denotes its solution, assumed to exist and be unique for every sample.

The violation of a decision is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$ (Definition 3.1).

A support set (Definition 8.8) is a subset $\{\Theta_{\delta_{i_1}},\dots,\Theta_{\delta_{i_k}}\}$ of the constraints such that the program with only these constraints in place has the same solution $\theta^*$ as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let $\sigma^*$ be the cardinality of the support set returned, for every sample, by some fixed algorithm.

Formalization targets

Goal: the support-set bound, Eq. (8.15)

For every function $\epsilon:\{0,1,\dots,N\}\to[0,1]$ with $\epsilon(N)=1$,

The level function $\epsilon$ is free: the statement is one inequality per admissible $\epsilon$, and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.

Milestone: the level function for a confidence $\beta$, Eq. (8.16)

For $\beta\in[0,1]$ let

The arithmetic half states that $\epsilon$ maps $\{0,\dots,N\}$ into $[0,1]$, $\epsilon(N)=1$, and the right-hand side of (8.15) equals $\beta$ (for $N\ge1$). The probabilistic half states $\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\beta$.

Significance

The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size $\sigma^*$ can assert $V(\theta^*)\le\epsilon(\sigma^*)$ with confidence $1-\beta$. The book's Figure 8.12 shows that $\epsilon(k)$ for $\beta=10^{-6}$ remains well below $1$ for $k$ up to a sizeable fraction of $N$. Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.

The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size $\sigma^*$ or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.

Difficulty

The natural first step is: condition on the support set being a particular index set $I$ with $|I|=k$, and argue that the solution is then a function of the $k$ sampled constraints in $I$ alone, while the other $N-k$ samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns $I$" depends on all $N$ samples, and the solution of the reduced program on $I$ is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that $\sigma^*$ is random and data-dependent: a bound for each fixed $k$ does not directly give a bound at the random level $\epsilon(\sigma^*)$, and the role of the condition $\epsilon(N)=1$ must be accounted for at $k=N$.

Formalization scope

Lean representation and committed conventions:

• $\Theta$ and $\Delta$ are arbitrary types with measurable structures; $\mathbb P$ is a probability measure on $\Delta$; a sample is ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over $0,\dots,N-1$.
• A subset of constraints is a Finset (Fin N); the reduced program with index set $I$ has feasible set $\bigcap_{i\in I}\Theta_{\delta_i}$ (all of $\Theta$ for $I=\emptyset$).
• The solution map $\theta^*$ is a parameter with the hypothesis that $\theta^*(\omega)$ is the unique solution of the full program for every sample.
• "Has the same solution" in Definition 8.8 means: the reduced program has a unique solution and it equals the unique solution of the full program. Existence of solutions is not assumed for reduced programs in general, only for those that are support sets.
• The algorithm is an arbitrary map alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; $\sigma^*$ is the cardinality of its output. The goal is universal over such maps.
• $\epsilon$ is a real function on $\mathbb N$ with $\epsilon(k)\in[0,1]$ for $k\le N$ and $\epsilon(N)=1$.
• The violation is real-valued in $[0,1]$; the probability of the event is compared in $[0,\infty]$ with ENNReal.ofReal of the real right-hand side.

Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is measurable in $\Theta\times\Delta$; the solution map is measurable; each event $\{\omega:\text{the algorithm returns }J\}$ is measurable; $\theta^*$ exists and is unique for every sample; $N\ge1$ in the arithmetic half of (8.16).

A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when $f$ has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.

Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018, §8.6, pp. 101–105. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, F. A. Ramponi, A general scenario theory for nonconvex optimization and decision making, IEEE Transactions on Automatic Control, 2018. https://doi.org/10.1109/TAC.2018.2808446
• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control, 2006. https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization, 2008. https://doi.org/10.1137/07069821X
• S. Floyd, M. Warmuth, Sample compression, learnability, and the Vapnik–Chervonenkis dimension, Machine Learning, 1995. https://doi.org/10.1007/BF00993593