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

$$V_n = \left[V_{n-1} + D_n - c\right]^+ . \tag{8.1}$$

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

$$V = \sup_{n \ge 0} S_n .$$

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

$$\frac{P\{V > v\}}{\beta e^{-\alpha v}} \to 1 \quad (v \to \infty), \qquad \alpha \text{ the unique positive root of } E\left[e^{-\alpha(c - D)}\right] = 1 .$$

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

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

$$J_\theta(i)=\limsup_{n\to\infty}\frac1n\sum_{t=0}^{n-1}E_\theta[C(X_t,A_t)\mid X_0=i],$$

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

$$J^N+r^N(i)=\min_a\Big\{C(i,a)+\sum_{j\in S_N}P_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N; \tag{8.1}$$

• (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

$$J(i)=\lim_{N\to\infty}J^N\qquad\text{for all } i\in S,$$

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

$$r^N(i)=\lim_{n\to\infty}\big(v^N_n(i)-v^N_n(x)\big)$$

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$,

$$J_{d(a)}=\frac{Hp(1-p)}{a-p}+\frac{pC(a)}{a}.$$

• 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

Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.

This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.

Setting

A random variable $X$ has the exponential distribution with rate $\mu>0$ if $P(X\le t)=1-e^{-\mu t}$ for $t\ge0$. A function $r(\delta)$ is $o(\delta)$ if $r(\delta)/\delta\to0$ as $\delta\to0^+$.

A continuous time Markov decision chain (CTMDC) $\Psi$ has a countable state space $S$ and, for each $i\in S$, a finite nonempty action set $A_i$. Choosing $a\in A_i$ in state $i$ incurs an instantaneous cost $G(i,a)\ge0$ and a cost rate $g(i,a)\ge0$ in effect until the next transition. The time until the next transition is exponential with rate $\nu(i,a)>0$, so its mean is $\tau(i,a)=1/\nu(i,a)$; the next state is $j$ with probability $P_{ij}(a)$, where $P_{ii}(a)=0$. A policy $\theta$ chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy $e$ chooses $e(i)$ in state $i$. With $C_n$ the cost and $T_n$ the time of the first $n$ transition periods, the average cost and the minimum average cost are

$$J^\Psi_\theta(i)=\limsup_{n\to\infty}\frac{E_\theta[C_n\mid X_0=i]}{E_\theta[T_n\mid X_0=i]},\qquad J^\Psi(i)=\inf_\theta J^\Psi_\theta(i).$$

Assumption (CTB) requires constants $\tau$ and $B$ with $0<\tau<\inf_{i,a}\tau(i,a)\le\sup_{i,a}\tau(i,a)\le B<\infty$. The auxiliary MDC $\Delta$ has the same states and actions, costs $C(i,a)=G(i,a)\nu(i,a)+g(i,a)$, and transition probabilities $P^*_{ij}(a)=\tau\nu(i,a)P_{ij}(a)$ for $j\ne i$, $P^*_{ii}(a)=1-\tau\nu(i,a)$. Its average cost $J^\Delta_\theta(i)=\limsup_n n^{-1}\sum_{t<n}E_\theta[C(X_t,Y_t)]$ and minimum average cost $J^\Delta(i)$ are those of Chapter 2. Assumption (CTAC) is $J^\Delta(\cdot)\le J^\Psi(\cdot)$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ for $\Delta$ uses finite state spaces $S_N$ increasing to $S$ and transition probabilities $P^*_{ij}(a;N)$ on $S_N$ converging to $P^*_{ij}(a)$. The (AC) assumptions ask for constants $J^N$ and functions $r^N$ on $S_N$ solving

$$J^N+r^N(i)=\min_{a\in A_i}\Big\{C(i,a)+\sum_{j\in S_N}P^*_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N,\ N\ge N_0,\tag{10.21}$$

with $\limsup_N r^N(i)<\infty$, $\liminf_N r^N(i)\ge-Q$ for a constant $Q\ge0$, and $\limsup_N J^N=:J^*<\infty$, $J^*\le J^\Delta(i)$.

Formalization targets

Goal: Theorem 10.3.3

Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of $\Delta$:

$$J^*=\lim_{N\to\infty}J^N\ \text{exists and}\ J^\Delta(i)=J^\Psi(i)=J^*\quad(i\in S),$$

and every limit point $e^*$ of a sequence $e^N$ of stationary policies realizing the minimum in (10.21) satisfies $J^\Delta_{e^*}=J^\Delta$ and $J^\Psi_{e^*}=J^\Psi$. The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.

Milestones

• Proposition 10.1.2: $P(X>x+y\mid X>y)=P(X>x)$ for $x,y>0$, and $P(X\le\delta)=\mu\delta+o(\delta)$.
• Proposition 10.1.3: for independent exponentials, $P(X_1\le\delta,X_2\le\delta)=o(\delta)$, $P(X_1<X_2)=\mu_1/(\mu_1+\mu_2)$, and $\min(X_1,X_2)$ is exponential with rate $\mu_1+\mu_2$.
• Lemma 10.3.1: if $z$ is bounded below and $Z\tau(i,e)+z(i)\ge G(i,e)+g(i,e)\tau(i,e)+\sum_jP_{ij}(e)z(j)$ for all $i$ (10.15), then $J^\Psi_e\le Z$.
• Lemma 10.3.2: $(Z,w)$ satisfies $Z+w(i)\ge C(i,e)+\sum_jP^*_{ij}(e)w(j)$ (10.20) if and only if $(Z,\tau w)$ satisfies (10.15).
• Proposition 10.4.1: in the M/M/1 queue with arrival rate $\lambda$, holding cost $H(i)=Hi$ and service cost rate $c(a)$, the policy that always serves at rate $a>\lambda$ has average cost $\rho_ac(a)+H\rho_a/(1-\rho_a)$, $\rho_a=\lambda/a$.

Significance

The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.

The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.

Difficulty

The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for $\Delta$ may change action in every time slot, including slots where the state does not change, while a policy for $\Psi$ acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound $J^\Psi\ge J^*$ therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point $e^*$ to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function $z$ is only bounded below, so the telescoping of expectations must be justified without integrability of $z$ from above.

Formalization scope

The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with $P_{ii}(a)=0$) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions $z,w,r^N$ are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so $+\infty$ is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of $n$ transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from $P_{i\cdot}(a)$; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality $\tau<\inf\tau(i,a)$ of (CTB) is kept strict (as a positive margin); weakening it to $\le$ would make $P^*_{ii}(a)$ vanish or turn negative.

The average cost $J^\Psi_\theta$ is a ratio of expectations, not the expectation of a ratio, and the infimum $J^\Psi$ ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.

A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.

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
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, 1994. https://doi.org/10.1002/9780470316887
• S. A. Lippman, Applying a new device in the optimization of exponential queuing systems, Operations Research 23(4), 687–710, 1975. https://doi.org/10.1287/opre.23.4.687
• D. Gross and C. M. Harris, Fundamentals of Queueing Theory, 3rd ed., John Wiley & Sons, 1998.

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$:

$$P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in 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$,

$$\text{every ATAS that sends excess probability to } G \text{ is conforming},$$

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

The r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.

Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.

Setting

Let $E_n$ be $n$-dimensional Euclidean space with inner product $(x, y)$, $n \ge 1$. For a unit vector $\xi$ and $\alpha > 0$ the operator of space dilation is $R_\alpha(\xi)x = x + (\alpha - 1)(x, \xi)\xi$.

Widths. For a compact convex set $W$ and a unit vector $\eta$, the width in direction $\eta$ is $d_\eta(W) = \max_{x \in W}(\eta, x) - \min_{x \in W}(\eta, x)$. The width is $d(W) = \min_{\|\eta\| = 1} d_\eta(W)$ and the diameter is $D(W) = \max_{\|\eta\| = 1} d_\eta(W)$. With $e_\rho(W) = \inf_{z \in W}|(\rho, z)|$ put $K_\rho(W) = d_\rho(W)/e_\rho(W)$ (or $+\infty$ when $e_\rho(W) = 0$) and $p(W) = \inf_{\|\rho\| = 1} K_\rho(W)$.

The class $K$. $E_n$ is partitioned into closed sets $\bar D_1, \dots, \bar D_m$, each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; $f_i$ is continuously differentiable on an open set containing $\bar D_i$; and $f = f_i$ on $\bar D_i$. At a point $x$, the set of almost-gradients $G_f(x)$ is the set of gradients $\nabla f_i(x)$ of the pieces with $x \in \bar D_i$. For $\delta, \varepsilon > 0$, $\bar P_{\delta,\varepsilon}(x)$ is the closed convex hull of all $G_f(y)$, $\|y - x\| < \delta$, together with the $\varepsilon$-balls around the elements of $G_f(x)$.

The $r(\alpha)$-algorithm. Fix $\alpha > 1$, $\beta = 1/\alpha$. Start from $x_0$, $\tilde g_0 = 0$ and a nonsingular $B_0$. At iteration $k + 1$ choose $g_f(x_k) \in G_f(x_k)$ with $(B_k^* g_f(x_k), \tilde g_k) \le 0$; set $g_k^* = B_k^* g_f(x_k)$, $r_k = g_k^* - \tilde g_k$, $\xi_{k+1} = r_k/\|r_k\|$, $B_{k+1} = B_k R_\beta(\xi_{k+1})$, $\tilde g_{k+1} = R_\beta(\xi_{k+1}) g_k^*$, and $x_{k+1} = x_k - h_{k+1}B_{k+1}\tilde g_{k+1}$ with $h_{k+1} \ge 0$ such that $f$ does not increase along the step and some almost-gradient at $x_{k+1}$ makes a non-acute angle with $\tilde g_{k+1}$ in the transformed metric. The standing assumption is $f(x) \to +\infty$ as $\|x\| \to \infty$ (3.50).

Formalization targets

Goal: convergence to an isolated local minimum (Theorem 3.13)

Assume (3.50) and $\|x_{k+1} - x_k\| \to 0$ (3.52). If $x^*$ is an isolated local minimum, the component of $\{x : f(x^*) \le f(x) \le f(x_0)\}$ containing $x_0$ also contains $x^*$, and no other point $z$ of that component has linearly dependent $G_f(z)$, then

$$\lim_{k \to \infty} x_k = x^* .$$

Milestones

• Lemma 3.2 (p. 80): for $B = SO$ with minimum eigenvalue $\lambda(B)$ of $S$, $\lambda(B)d(W) \le d(BW) \le \lambda(B)D(W)$.
• Lemma 3.3 (p. 80): for $z_1, z_2 \in W$, $0 < \beta \le 1$ and $\gamma = \|z_1 - z_2\|/d(W) \ge 1$,

$$d\Big(R_\beta\big(\tfrac{z_1 - z_2}{\|z_1 - z_2\|}\big)W\Big) \ge \frac{d(W)}{\sqrt{1 + (1-\beta^2)/(\beta^2\gamma^2)}} .$$

• Theorem 3.11 (p. 82): for every $\sqrt[n]{\beta} < v < 1$, $\varepsilon, \delta > 0$ and $r \ge 1$ there is $\bar k > r$ with

$$p\big(\bar P_{\delta,\varepsilon}(x_{\bar k})\big) \ge \sqrt{\frac{v^2\sqrt[n]{\alpha^2} - 1}{\alpha^2 - 1}} .$$

• Theorem 3.12 (p. 84): the level set $\{f = f_\infty\}$, $f_\infty = \lim_k f(x_k)$, contains a point $x^*$ with $G_f(x^*)$ linearly dependent.

Significance

Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class $K$, convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of $G_f(x)$ is a generalized stationarity condition that includes $0 \in \operatorname{conv} G_f(x)$. Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.

All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class $K$ and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.

Difficulty

The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with $x_{k+1} = x_k$ while $B_k$ and $\tilde g_k$ change, and its steps are measured in a metric that degenerates as the dilations accumulate ($\det B_k = \beta^k \det B_0$). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.

The difficulty is to relate the geometry of the transformed almost-gradient sets $B_k^*\bar P_{\delta,\varepsilon}(x_k)$ to the decay forced on $B_k$. This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of $\{f(x^*) \le f \le f(x_0)\}$, and that their accumulation points reduce to $x^*$.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$; operators are continuous linear maps; $B_k^*$ is the adjoint. $K_\rho$ and $p$ are valued in $[0, +\infty]$, so $K_\rho(W) = +\infty$ is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.
• A function of class $K$ is given with its representation (pieces, open domains, smooth $f_i$), and $G_f(x)$ is the set of gradients of the incident pieces, as on p. 79. Linear dependence of $G_f(x)$ is the negation of linear independence of that set.
• A run of the algorithm is a predicate on sequences $x_k, \tilde g_k, B_k, g_f(x_k), h_{k+1}$; every theorem holds for every run. Step (3) divides by $\|r_k\|$, so $r_k \ne 0$ is part of the run: a run that reaches a point where no admissible choice gives $r_k \ne 0$ has no continuation, as in the book. The stepsize $h_{k+1} = \operatorname{argmin}$ is one admissible choice, not the definition.
• The standing assumption (3.50) is a hypothesis of Theorem 3.11 as well as of 3.12 and 3.13, because the book imposes it for the rest of the section on p. 79.
• In Lemma 3.3, $\beta > 0$ is added (the bound divides by $\beta^2$). "Body" means nonempty interior. An isolated local minimum is a local minimum with a neighbourhood containing no other local minimum.
• Runs exist, so the hypotheses are not vacuous. For $f(t) = |t_1| + 2|t_2|$ (four quadrant pieces), started at the minimizer $x_0 = 0$ with null steps, one can choose $g_f(x_{k+1}) = -g_f(x_k)$ at every step, and $0 \notin G_f$ keeps $r_k \neq 0$. A formalization under which no infinite run exists would make every theorem vacuous. The run predicate also forbids the degenerate reading $h_{k+1} < 0$, under which the monotonicity condition (a) would hold vacuously on an empty segment.
• Needed infrastructure: widths of compact convex sets under linear maps (via the singular values of $B$), the effect of a rank-one dilation on widths, determinant bounds for products of dilations, and Gram-determinant continuity. The first three apply to any space-dilation method and are welcome as independent lemmas.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §3.7, pp. 77–85. doi:10.1007/978-3-642-82118-9
• N. Z. Shor, N. G. Zhurbenko, A minimization method using the operation of space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 3, 51–59, 1971 (listed in the bibliography of Shor 1985; no online copy known).
• N. Z. Shor, The analysis of convergence of a gradient type method with space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 4, 48–53, 1975 (listed in the bibliography of Shor 1985; no online copy known).

Motivation

Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.

The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. The primal linear program is to maximize $c^T x$ subject to $Ax \le b$, $x \ge 0$; its dual is to minimize $b^T y$ subject to $A^T y \ge c$, $y \ge 0$. With slack variables $w \in \mathbb{R}^m$ and $z \in \mathbb{R}^n$ they read (17.1)

$$Ax + w = b,\ x, w \ge 0 \qquad\text{and}\qquad A^T y - z = c,\ y, z \ge 0.$$

For a vector $\xi$, $\xi > 0$ means that every component is strictly positive. The primal feasible region has nonempty interior when some $(\bar x, \bar w)$ satisfies $A\bar x + \bar w = b$ with $\bar x > 0$, $\bar w > 0$; the dual feasible region has nonempty interior when some $(\bar y, \bar z)$ satisfies $A^T \bar y - \bar z = c$ with $\bar y > 0$, $\bar z > 0$.

For a parameter $\mu > 0$, the barrier function (17.7) is

$$f(x, w) = c^T x + \mu \sum_{j=1}^n \log x_j + \mu \sum_{i=1}^m \log w_i ,$$

and the barrier problem (17.2) is to maximize $f(x, w)$ subject to $Ax + w = b$, over the domain $x > 0$, $w > 0$ where the logarithms are finite. A solution of the barrier problem is a point of that domain at which $f$ attains its maximum over the domain.

Writing $X, Z, Y, W$ for the diagonal matrices carrying $x, z, y, w$ and $e$ for the all-ones vector, the primal–dual central-path system (17.6) is

$$Ax + w = b, \qquad A^T y - z = c, \qquad XZe = \mu e, \qquad YWe = \mu e,$$

with $x, w, y, z > 0$. The last two equations say $x_j z_j = \mu$ and $y_i w_i = \mu$ for all $j$ and $i$. The set of its solutions $(x_\mu, w_\mu, y_\mu, z_\mu)$, $\mu > 0$, is the primal–dual central path.

The chapter also uses one fact from nonlinear programming: for the problem "maximize $f(x)$ subject to $g_i(x) = 0$, $i = 1, \dots, m$", a critical point is a feasible $x^*$ with $\nabla f(x^*) = \sum_i y_i \nabla g_i(x^*)$ for some Lagrange multipliers $y_i$ (17.3), and $H_f(x^*)$ is the Hessian of $f$ at $x^*$.

Formalization targets

Goal: Theorem 17.2 (p. 265)

For each fixed $\mu > 0$,

$$\exists\, (x, w) \text{ solving the barrier problem} \iff \big(\exists\, \bar x, \bar w > 0 : A\bar x + \bar w = b\big) \wedge \big(\exists\, \bar y, \bar z > 0 : A^T\bar y - \bar z = c\big).$$

Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.

Milestones

1. Theorem 17.1 (p. 261), second-order sufficiency under linear constraints: if the constraints are linear, a critical point $x^*$ with $\xi^T H_f(x^*)\xi < 0$ for every $\xi \ne 0$ satisfying $\xi^T \nabla g_i(x^*) = 0$ for all $i$ is a local maximum on the feasible set.
2. Exercise 10.7 (p. 150): if the primal is feasible and its feasible set $\{x : Ax \le b,\ x \ge 0\}$ is bounded, then there are $y > 0$, $z > 0$ with $A^T y - z = c$.
3. Corollary 17.3 (p. 266): if the primal feasible set (or the dual feasible set) has nonempty interior and is bounded, then for each $\mu > 0$ the system (17.6) has exactly one solution with $x, w, y, z > 0$.

The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).

Significance

The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed $\mu$, and Corollary 17.3 turns it into the statement that the central path is a well-defined curve $\mu \mapsto (x_\mu, w_\mu, y_\mu, z_\mu)$ for all $\mu > 0$. Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.

Formalizing it. These results are classical and proved in the book; none is formalized in the $Ax \le b$, $x \ge 0$ form used here. The platform has the converse fact in the standard form $Ax = b$, $x \ge 0$ (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.

Difficulty

The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain $x > 0$, $w > 0$ is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize $0$ subject to $x \ge 0$" (p. 264), whose barrier $\mu \log x$ has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.

Theorem 17.1 needs a second-order Taylor expansion with a remainder that is $o(\|\xi\|^2)$ uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations $x_j z_j = \mu$, $y_i w_i = \mu$ admit sign-flipped solutions.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in $Ax \le b$, $x \ge 0$ form with slacks is used throughout; there are no explicit constants in this chapter.

Conventions committed to:

• "Nonempty interior" means a feasible point with every component strictly positive, as the proof of Theorem 17.2 says. The topological interior of $\{(x, w) : Ax + w = b,\ x, w \ge 0\}$ in $\mathbb{R}^{n+m}$ is empty whenever $m \ge 1$; reading the theorem that way would make its right-hand side always false for $m \ge 1$, and that reading is ruled out.
• The barrier problem is posed over $x > 0$, $w > 0$ explicitly; Real.log returns $0$ at nonpositive arguments and is never evaluated there.
• Solutions of (17.6) are required to be strictly positive, as in Exercise 17.3 (p. 267).
• "Bounded" is Bornology.IsBounded of the feasible set in $\mathbb{R}^n$ (resp. $\mathbb{R}^m$).
• In Theorem 17.1 the constraints are $Gx = \beta$; $f$ is differentiable near $x^*$ with derivative differentiable at $x^*$, and $\xi^T H_f(x^*) \xi$ is the second Fréchet derivative applied to $(\xi, \xi)$. The local maximum is relative to the feasible set.

Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 17 and Exercise 10.7. https://doi.org/10.1007/978-1-4614-7630-6
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968. https://doi.org/10.1137/1.9781611971316
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984), 373–395. https://doi.org/10.1007/BF02579150
• N. Megiddo, Pathways to the optimal set in linear programming, in Progress in Mathematical Programming, Springer, 1989, 131–158. https://doi.org/10.1007/978-1-4613-9617-8_8
• D. A. Bayer and J. C. Lagarias, The nonlinear geometry of linear programming I, II, Transactions of the AMS 314 (1989), 499–526 and 527–581. https://doi.org/10.1090/S0002-9947-1989-1005525-6