Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems X: Average Cost Optimization of Continuous Time Markov Decision ChainsTextbook

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.

11 thms3 active users

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIII: Lyapunov Criteria and z Standard Markov Chains with CostsTextbook

Motivation

Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the $z$ standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.

The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).

Setting

A Markov chain $\Gamma$ on a countable set $S$ is given by transition probabilities $P_{ij}\ge 0$ with $\sum_j P_{ij}=1$ . $X_t$ is the state at time $t$ and $P^{(t)}_{ij}$ the $t$ -step transition probability ( $P^{(0)}_{ij}=\delta_{ij}$ ). State $i$ leads to $j$ if $P^{(t)}_{ij}>0$ for some $t\ge0$ ; states that lead to each other communicate, which partitions $S$ into communicating classes.

For a nonempty $G\subseteq S$ the first passage time from $i$ is $T_{iG}=\min\{t\ge1: X_t\in G\}$ given $X_0=i$ , and $m_{iG}=E[T_{iG}]\in[0,\infty]$ ; $m_{ij}$ is the case $G=\{j\}$ and $m_{ii}$ the expected return time. The taboo probability $_G P^{(t)}_{ik}$ is the probability of going from $i$ to $k$ in $t$ steps without visiting $G$ at the intermediate times, and $_G u_{ik}$ is the expected number of visits to $k$ at times $0\le t<T_{iG}$ . A state is transient if $P(T_{ii}<\infty)<1$ and positive recurrent if $m_{ii}<\infty$ ; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is $\pi_j=(m_{jj})^{-1}$ (zero when $m_{jj}=\infty$ ).

Each state carries a finite cost $C(i)\ge0$ . The expected average cost over $[0,n-1]$ from $i$ is

J^{(n)}_i=\frac1n\,E\Big[\sum_{t=0}^{n-1}C(X_t)\,\Big|\,X_0=i\Big]=\frac1n\sum_{t=0}^{n-1}\sum_j P^{(t)}_{ij}C(j),

$c_{iG}$ is the expected cost $E[\sum_{t=0}^{T_{iG}-1}C(X_t)\mid X_0=i]$ of a first passage (defined when $m_{iG}<\infty$ ), and $J_R=\sum_{j\in R}\pi_jC(j)$ is the average cost on a positive recurrent class $R$ . The chain is $z$ standard (Definition C.2.5) if for a distinguished state $z$

m_{iz}<\infty\quad\text{and}\quad c_{iz}<\infty\qquad\text{for all } i\in S.

Formalization targets

Goal: Proposition C.2.6

If $\Gamma$ is $z$ standard, then $S$ is the union of a positive recurrent class $R\ni z$ and a set of transient states, $J_R<\infty$ , and

\lim_{n\to\infty}J^{(n)}_i=J_R\qquad\text{for every } i\in S.

The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.

Milestones

Proposition C.1.2: $\pi$ is the unique stationary distribution of a positive recurrent class, and $\pi_j=e_{ij}/m_{ii}=\pi_ie_{ij}$ .
Proposition C.1.4: the first-step equations (C.2)–(C.4) for taboo probabilities, visit counts and $m_{iG}$ ; $\sum_{i\in G}\pi_im_{iG}=1$ for $G$ inside a positive recurrent class; $m_{ij}<\infty$ within such a class.
Proposition C.1.5: if $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ off $G$ , then $m_{iG}\le y(i)/\epsilon$ .
Corollary C.1.6: the same with $G=\{z\}$ and $\sum_jP_{zj}y(j)<\infty$ makes $z$ positive recurrent.
Proposition C.2.1: on a positive recurrent class, $J^{(n)}_i\to J_R=c_{ii}/m_{ii}$ .
Proposition C.2.2: $c_{iG}=\sum_kC(k)\,{}_Gu_{ik}$ , the first-step equation (C.13), and $J_R=\sum_{i\in G}\pi_ic_{iG}$ .
Proposition C.2.3 and Corollary C.2.4: the cost drift condition $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ off a finite set bounds $c_{iG}\le r(i)+Fm_{iG}$ , and gives $c_{zz}<\infty$ .
Remark C.2.7: the hypotheses of C.1.6 and C.2.4 together imply the chain is $z$ standard; so do irreducibility, positive recurrence and finite average cost.

Significance

Proposition C.2.6 is what makes the $z$ standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.

All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.

Difficulty

The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate $n$ times and let $n\to\infty$ " must be made rigorous for $[0,\infty]$ -valued expectations.

The central difficulty is part (iii) of the goal for transient initial states. On the class $R$ , the limit of $J^{(n)}_i$ is a renewal reward theorem over successive returns to $z$ ; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding $J^{(n)}_i$ between $J_R$ and the average over the first $n$ steps of the chain started in $z$ , fails because $P^{(t)}_{ij}$ need not converge (periodic classes) and because finite $c_{iz}$ does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.

Formalization scope

The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be $\infty$ . The first passage time is $T_{iG}\ge1$ ; $m_{iG}$ is the expectation of $T_{iG}$ from its law (and $\infty$ when $P(T_{iG}<\infty)<1$ ), not defined by the recursion (C.4), so that (C.4) is a theorem. $_Gu_{ik}$ counts visits at times $0\le t<T_{iG}$ . $c_{iG}$ is computed over first passage paths and is used only when $m_{iG}<\infty$ , as in the book. $\pi_j$ is $(m_{jj})^{-1}$ , which the book states equals the Cesàro limit $\lim_nQ^{(n)}_{jj}$ . $J^{(n)}_i$ is meaningful for $n\ge1$ , and limits are taken in $[0,\infty]$ . The drift conditions $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ and $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ are written in the equivalent additive form $\sum_jP_{ij}y(j)+\epsilon\le y(i)$ , which is equivalent for finite $y$ and makes the case $\sum_jP_{ij}y(j)=\infty$ fail, as it does in the book.

A trivializing formalization, such as defining $m_{iG}$ or $c_{iG}$ by the equations (C.4) or (C.13), defining $J_R$ as the limit of $J^{(n)}_i$ , or allowing a $z$ standard chain whose return time or return cost to $z$ is infinite, is ruled out: $z$ standard requires $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ including $z$ , and each quantity is defined from path probabilities.

Needed infrastructure: path-sum manipulation in $[0,\infty]$ (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the $z$ standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, pp. 292–302. doi:10.1002/9780470317037
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967. doi:10.1007/978-3-642-62015-7
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. doi:10.1214/aoms/1177728976
S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. doi:10.1017/CBO9780511626630
D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. I, McGraw-Hill, 1982.

12 thms3 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

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

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}$ .
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$ .
Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$ .
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.
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

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

10 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions III: Convergence of the Normalized Subgradient Method with Divergent-Series StepsizesTextbook

Motivation

Many optimization problems of operations research have objectives that are convex but not differentiable: Lagrangian duals of integer and combinatorial programs, maxima of finitely many affine or smooth functions, penalty functions for systems of inequalities, and the value functions produced by decomposition. For such functions the gradient method and steepest descent fail. Constant steps cannot work because the subgradients need not tend to zero at a nondifferentiable minimum, and exact line search along the negative gradient can converge to a point that is not a minimizer (the example on pp. 22–23 of the source).

The subgradient method replaces the gradient by an arbitrary subgradient and gives up monotone decrease of the objective. Its convergence theory is the foundation of nondifferentiable optimization and of Lagrangian relaxation in integer programming.

Timeline. N. Z. Shor proposed the method with normalized steps in 1962 (Kiev). Yu. M. Ermoliev proved convergence in finite dimensions with divergent-series stepsizes (Kibernetika, 1966), and B. T. Polyak proved it for constrained problems in Hilbert space (Doklady Akad. Nauk SSSR, 1967). Held, Wolfe and Crowder (Mathematical Programming, 1974) brought the method to large combinatorial problems through Lagrangian relaxation. This mission formalizes the exposition of Section 2.1–2.2 of Shor's monograph (Springer, 1985), which gives self-contained proofs of these results.

Setting

Let $E_n$ be the $n$ -dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$ . Let $f : E_n \to \mathbb{R}$ be a convex function finite everywhere. A vector $g$ is a subgradient of $f$ at $x_0$ if

f(x) - f(x_0) \ge (g, x - x_0) \quad \text{for all } x \in E_n.

Every convex $f$ has at least one subgradient at every point. Let $M^* = \{x : f(x) \le f(y) \ \forall y\}$ be the set of minimum points and, when it is nonempty, $f^* = \min f$ .

A subgradient selection $g_f$ assigns to each $x$ some subgradient $g_f(x)$ of $f$ at $x$ . No particular choice is made: every result holds for every selection. Given stepsizes $h_1, h_2, \dots > 0$ and a starting point $x_0$ , the normalized subgradient method is

x_{k+1} = x_k - h_{k+1}\, \frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, \dots \tag{2.4}

If $g_f(x_k) = 0$ , then $x_k$ is a minimizer and the computation stops. The unnormalized method is $x_{k+1} = x_k - h_{k+1} g_f(x_k)$ (2.5), and the method with restarts takes that step when $h_{k+1}\|g_f(x_k)\| \le c$ and returns to $x_0$ otherwise.

Formalization targets

Goal: Theorem 2.2 (p. 25)

If $M^*$ is nonempty and bounded, $h_k > 0$ , $h_k \to 0$ and $\sum_{k \ge 1} h_k = +\infty$ , then for every $x_0$ and every subgradient selection, the method (2.4) either reaches $M^*$ at some index $\bar k$ or

\lim_{k \to \infty} \min_{y \in M^*} \|x_k - y\| = 0, \qquad \lim_{k \to \infty} f(x_k) = f^*.

Milestones

Eq. (2.3), the one-step inequality $\|x_{k+1} - x^*\|^2 \le \|x_k - x^*\|^2 + h^2 - 2h\,\rho(x^*, U_k)$ , where $U_k = \{x : f(x) = f(x_k)\}$ .
Theorem 2.1: with constant step length $h$ , some level surface $\{f = f(x_{k^*})\}$ passes within $h(1+\varepsilon)/2$ of any $x^* \in M^*$ .
Corollaries 1 and 2: a suitable constant step length yields a subsequence with $f(x_{k_i}) - f^* < \delta$ . If $M^*$ contains a ball of radius $r > h/2$ , the method terminates in $M^*$ .
Theorem 2.5: if $M^*$ contains a ball of radius $r$ , $\sum h_k = \infty$ and $\limsup h_k < 2r$ , then (2.4) terminates in $M^*$ .
Theorem 2.3: for the unnormalized method (2.5), bounded subgradients along the trajectory imply convergence, and unbounded subgradients rule it out.
Theorem 2.4: the method with restarts converges for every $c > 0$ .

Significance

Theorem 2.2 is the basic convergence guarantee for first-order methods on general nonsmooth convex functions. It needs no Lipschitz constant, no bound on the subgradients and no smoothness: normalizing the step makes the step length independent of the size of the subgradient. The divergent-series rule $h_k \to 0$ , $\sum h_k = \infty$ is the standard stepsize condition of stochastic approximation and of Lagrangian relaxation codes. Theorems 2.3–2.5 mark its boundaries. The unnormalized method needs bounded subgradients (Theorem 2.3), restarts remove that need (Theorem 2.4), and a solution set with nonempty interior gives finite termination (Theorem 2.5). The last result is the basis of the finite methods for systems of convex inequalities and for the dual of an assignment problem with a unique solution (pp. 28–29).

All of these results are classical and proved in the source. None of them is formalized in Lean's Mathlib. The platform has neighbouring results that are not the same statements: Poljak's divergent-series theorem for concave piecewise-linear maximization (in Validation of Subgradient Optimization I), and rate bounds for Lipschitz objectives (First-Order and Stochastic Optimization Methods for ML II, Understanding Machine Learning X). This mission adds the general convex case with normalized steps, the dichotomy for unnormalized steps, and finite termination.

Difficulty

The standard rate analysis of the subgradient method bounds $\|x_{k+1} - x^*\|^2 - \|x_k - x^*\|^2$ by $-2h_{k+1}(f(x_k) - f^*)/\|g_f(x_k)\| + h_{k+1}^2$ . It then needs a uniform bound on $\|g_f(x_k)\|$ , which is exactly what is not assumed here. Nothing a priori keeps the iterates in a bounded set, and the subgradients of a general convex function (for instance $f(x) = x^4$ , the source's example on p. 26) grow without bound away from $M^*$ ; with unnormalized steps this makes the method diverge. Even with normalized steps, the distance to a minimizer decreases only outside a neighbourhood of $M^*$ whose size is of the order of the current step, so a monotone decrease argument gives at best a subsequence with small function values. Convergence of the whole sequence $\min_{y \in M^*}\|x_k - y\|$ to zero is a stronger statement, and boundedness of $M^*$ is essential to it.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere) with ConvexOn ℝ Set.univ f.
The subgradient selection g is arbitrary, with the hypothesis ∀ x, IsSubgradient f x (g x). The starting point is arbitrary.
The iterations are defined recursively (normalizedIter, plainIter, resetIter); the stepsize sequence is h : ℕ → ℝ with h (k+1) used at step $k$ . In (2.4), a zero subgradient is handled by an explicit branch that repeats the current iterate (which is then in $M^*$ ). No statement relies on Lean's convention $x/0 = 0$ .
$M^*$ is required to be nonempty wherever the book writes $\min_{y \in M^*}$ or $f^* = \min f$ . $\min_{y \in M^*}\|x_k - y\|$ is Metric.infDist, and $f^*$ is ⨅ y, f y.
$\sum_{k \ge 1} h_k = +\infty$ is Tendsto (fun N => ∑ k ∈ Finset.range N, h (k+1)) atTop atTop. $\limsup h_k < 2r$ is "for some $q < 2r$ , eventually $h_k \le q$ ", so it cannot hold vacuously for an unbounded sequence.
Corollary 1's step length $h_\delta$ is quantified before the selection and the starting point: it depends only on $f$ and $\delta$ .
Theorem 2.3 is stated as two implications, (bounded subgradients ⇒ convergence) and (unbounded ⇒ no convergence), not as a disjunction that one case could satisfy trivially.
A formalization of Theorem 2.2 that assumes bounded subgradients, a Lipschitz $f$ , or a specific subgradient choice (such as the minimal-norm one) proves a different and weaker theorem, and does not close the goal.

Needed infrastructure: continuity of convex functions on $E_n$ (in Mathlib), compactness of sublevel sets when $M^*$ is bounded, and the geometry of level surfaces relative to supporting hyperplanes. The one-step inequality (2.3) and the level-set compactness lemma are reusable by the later missions of this series (linear rate, Polyak's stepsize, stochastic subgradient). Contributions that prove Eq. (2.3) or Theorem 2.1 first are welcome.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Chapter 2, pp. 22–30. https://doi.org/10.1007/978-3-642-82118-9
B. T. Polyak, A general method for solving extremal problems, Doklady Akademii Nauk SSSR 174 (1967), 33–36 (the source's reference [64]).
Yu. M. Ermoliev, Methods for solving nonlinear extremal problems, Kibernetika (Kiev), no. 4 (1966), 1–17 (the source's reference [24]).
M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223

9 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions VII: Geometric Convergence of Subgradient Methods with Space Dilation along the GradientTextbook

Motivation

The subgradient method for a nonsmooth convex function converges, but slowly: when the level sets of the objective are elongated, the subgradient is nearly orthogonal to the direction towards the minimum, and the method zigzags. For smooth functions the remedy is a change of metric (Newton and quasi-Newton methods); for nonsmooth functions no Hessian exists to supply one. N. Z. Shor's answer was to learn a metric from the subgradients themselves: after each step, stretch the space along the latest (transformed) subgradient, so that components of future subgradients parallel to it are damped. These subgradient methods with space dilation along the gradient (SDG methods) are the ancestors of Shor's r-algorithm and of the ellipsoid method, which the book (p. 49) describes as a special case of the same family and which Khachiyan later used to show that linear programming is solvable in polynomial time.

Section 3.4 of Shor's monograph (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński, doi:10.1007/978-3-642-82118-9) proves that, under a two-sided condition on the objective, a suitable SDG method decreases function values at the speed of a geometric progression whose ratio is invariant under nonsingular linear changes of variables. This mission formalizes that chain of results.

Setting

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

R_\alpha(\xi)\,x = x + (\alpha - 1)(x,\xi)\,\xi ,

which multiplies the component of $x$ along $\xi$ by $\alpha$ and leaves the orthogonal complement fixed.

Let $f : E_n \to \mathbb{R}$ and let $g : E_n \to E_n$ be a generalized gradient: a subgradient of $f$ when $f$ is convex, an almost-gradient when $f$ is almost differentiable. The SDG method starts from $x_0$ and a nonsingular operator $B_0 = A_0^{-1}$ . At step $k = 0, 1, \dots$ : if $g(x_k) = 0$ it stops; otherwise it forms the transformed gradient $\tilde g_k = B_k^* g(x_k)$ , the direction $\xi_{k+1} = \tilde g_k/\|\tilde g_k\|$ , and

x_{k+1} = x_k - h_{k+1} B_k \xi_{k+1}, \qquad B_{k+1} = B_k R_{1/\alpha_{k+1}}(\xi_{k+1}), \qquad A_{k+1} = R_{\alpha_{k+1}}(\xi_{k+1}) A_k ,

with a stepsize $h_{k+1}$ and a dilation coefficient $\alpha_{k+1}$ . So $A_k$ is the accumulated space transformation, $B_k = A_k^{-1}$ , and each step is a subgradient step for $\varphi_k(y) = f(B_k y)$ in the variables $y = A_k x$ .

The quantitative results assume, for a point $x^*$ and the ball $S_d = \{x : \|x - x^*\| \le d\}$ , the two-sided condition

N\,[f(x) - f(x^*)] \le (g(x),\, x - x^*) \le M\,[f(x) - f(x^*)], \qquad x \in S_d, \quad M > N > 0. \qquad (3.18)

For a convex function the lower inequality holds with $N = 1$ ; the upper one bounds how far $f$ is from a positively homogeneous function around $x^*$ .

Formalization targets

Goal: Theorem 3.4

Under (3.18), with $B_0 = I$ , $x_0 \in S_d$ , stepsizes $h_{k+1} = \frac{2MN}{M+N}\frac{f(x_k)-f(x^*)}{\|\tilde g_k\|}$ , a constant coefficient $1 < \alpha \le \frac{M+N}{M-N}$ , and $G$ a bound for $\|g\|$ on $S_d$ : there are $c > 0$ and indices $k_1 < k_2 < \cdots$ with

f(x_{k_p}) - f(x^*) \le c\,\alpha^{-k_p/n},

and for every $k \ge 1$

\min_{0 \le i \le k-1}\,[f(x_i) - f(x^*)] \le \frac{G\sqrt{k(\alpha^2-1)}\,d}{N\sqrt{\alpha^{2k/n}-1}} .

Milestones

Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$ .
Theorem 3.1: if $\|g(x_k)\| \le d$ and $1+\delta \le \alpha_k \le \alpha^*$ , then $\|\tilde g_{k_p}\| < c\,(\prod_{j\le k_p}\alpha_j)^{-1/n}$ along a subsequence.
Theorem 3.2: for constant $\alpha > 1$ and $B_0 = I$ , $\min_{0\le r\le k-1}\|\tilde g_r\| \le d\sqrt{k(\alpha^2-1)}/\sqrt{\alpha^{2k/n}-1}$ .
Theorem 3.3: under (3.18) and the rules above, $\|A_k(x_k - x^*)\| \le d$ for all $k$ .

Significance

The result shows that one fixed rule, depending only on $M$ , $N$ and $n$ , yields linear convergence of function values for every objective satisfying (3.18), at a ratio $\alpha^{-1/n}$ that does not deteriorate when the problem is badly scaled: the method, and hence its rate, is invariant under nonsingular linear changes of variables. This is the property the ellipsoid method inherits (Section 3.8 of the book), and the same space-dilation machinery drives the r-algorithm (Section 3.7), still used for large nonsmooth problems such as Lagrangian duals of integer programs.

The theorems are proved in the book; none of them, and no space-dilation method, has a machine-checked proof to our knowledge, and the platform has no statement about variable-metric subgradient methods. The mission provides a reusable formal model of the SDG iteration, the eigenvalue-growth arguments behind Theorems 3.1–3.2, and the one-step invariant of Theorem 3.3. The formalization also corrects two points of the printed text (see Formalization scope).

Difficulty

Theorem 3.3 is a one-step computation, but Theorems 3.1 and 3.2 are not: they relate the size of the transformed gradients to the growth of the singular values of $A_k$ , whose determinant is $\prod_j \alpha_j$ . A bound on $\|\tilde g_k\|$ at a single step says nothing, since the dilations can concentrate in few directions; the argument has to control the largest singular value of $A_k$ over many steps against the geometric-mean lower bound $(\det A_k)^{1/n}$ . The dimension $n$ enters the rate exactly through this comparison. Theorem 3.4 then needs the invariant of Theorem 3.3 to keep every iterate inside $S_d$ , where (3.18) and the bound $G$ are available.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ in the rate statements. Operators are continuous linear maps; $B_0$ is a continuous linear equivalence and $A_0$ its inverse. The state $(x_k, B_k, A_k)$ is produced by a defined recursion sdg, not assumed; $\tilde g_k$ is gTilde.
The stepsize rule receives the index, the current point and $\tilde g_k$ ; the dilation coefficient at step $k$ is α (k+1). When $g(x_k) = 0$ the state is repeated, which encodes the book's stop; no division by zero is used.
The book states Theorems 3.1–3.4 for almost differentiable $f$ with $g$ an almost-gradient; the proofs use only the bounds on $\|g\|$ and (3.18), so the Lean statements quantify over every map $g$ with those properties. $G$ is any bound for $\|g\|$ on $S_d$ in place of the maximum.
Theorems 3.2–3.4 take $B_0 = I$ , as their proofs do; Theorem 3.1 allows any nonsingular $B_0$ .
Two corrections to the printed statements, both following the proofs: Theorem 3.4's record bound carries the factor $1/N$ that the proof derives, and the record minima in Theorems 3.2 and 3.4 range over the indices $0, \dots, k-1$ that the proof controls, rather than $1, \dots, k$ .
Constants $c$ and subsequences are existential and chosen after the data of the run, before the index $p$ . A statement placing $c$ after $p$ , or dropping (3.18) on $S_d$ , would be trivially true or false and is ruled out.

Useful infrastructure, reusable for the r-algorithm and ellipsoid chapters: identities for $R_\alpha(\xi)$ , determinants and singular values of products of rank-one dilations, and the invariance of the SDG iteration under a linear change of variables. Proofs of any milestone, and alternative arguments for Theorem 3.1, are welcome.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.2–3.4, pp. 49–62 (translated by K. C. Kiwiel and A. Ruszczyński). https://doi.org/10.1007/978-3-642-82118-9

17 thms4 active usersReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions IX: Convergence of the r-Algorithm with Exact Directional MinimizationTextbook

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

7 thms1 active userReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions X: The Space-Dilation Ellipsoid Method Localizes the Solution in Ellipsoids Shrinking by the Ratio q_nTextbook

Motivation

The ellipsoid method is the algorithm that settled the polynomial-time solvability of linear programming (Khachiyan, 1979) and that underlies the equivalence of separation and optimization in combinatorial optimization (Grötschel, Lovász and Schrijver, 1981). Its origin is in nonsmooth convex optimization. In 1976 Yudin and Nemirovskii proposed a modified method of centered sections that localizes an optimum inside a sequence of ellipsoids, and in 1977 N. Z. Shor observed independently that the same scheme is a subgradient method with space dilation along the gradient, the family of methods he had developed since 1969. Section 3.8 of Shor's monograph Minimization Methods for Non-Differentiable Functions (Springer 1985) presents the method in this second form and proves its basic localization property.

Timeline:

1965. A. Yu. Levin proposes the method of centered sections (cuts through the center of gravity of a polyhedron); each cut removes at least a fixed fraction of the volume, but computing centers of gravity is impractical for $n > 3$ .
1969–1972. Shor introduces subgradient methods with space dilation along the gradient (SDG methods).
1976. Yudin and Nemirovskii replace the polyhedron by a minimal ellipsoid containing a half-ellipsoid, obtaining a geometric volume decrease depending only on the dimension ([Yudin–Nemirovskii 1976]).
1977. Shor shows that the same method is an SDG algorithm with coefficient $\beta = \sqrt{(n-1)/(n+1)}$ ([Shor 1977]).
1979. Khachiyan applies the method to linear inequalities with integer data, obtaining the first polynomial-time algorithm for linear programming ([Khachiyan 1979]).

Setting

Let $E_n$ be $n$ -dimensional Euclidean space with inner product $(x, y)$ , and $n > 1$ . For a unit vector $\xi$ and a number $\alpha$ , the operator of space dilation along $\xi$ with coefficient $\alpha$ is $R_\alpha(\xi) = I + (\alpha - 1)\xi\xi^T$ : it multiplies the component of a vector along $\xi$ by $\alpha$ and leaves the orthogonal component unchanged.

Let $g : E_n \to E_n$ be a vector field, not necessarily continuous. The problem is to find a point $x^*$ with

(g(x), x - x^*) \ge 0 \quad \text{for all } x \in E_n,

where it is known that such an $x^*$ exists in the closed ball $S(x_0, R)$ of radius $R > 0$ about a given point $x_0$ . Put $\beta = \sqrt{(n-1)/(n+1)}$ and $r = n/\sqrt{n^2-1}$ . The algorithm (3.57)–(3.60) starts from $x_0$ , $B_0 = I_n$ , $h_0 = R/(n+1)$ , and at iteration $k+1$ stops if $g(x_k) = 0$ , and otherwise sets

\xi_k = \frac{B_k^T g(x_k)}{\|B_k^T g(x_k)\|}, \quad x_{k+1} = x_k - h_k B_k \xi_k, \quad B_{k+1} = B_k R_\beta(\xi_k), \quad h_{k+1} = r h_k .

With $A_k = B_k^{-1}$ , the localizing ellipsoid is $\Phi_k = \{x : \|A_k(x - x_k)\| \le (n+1)h_k\}$ , and the dimension-dependent ratio is

q_n = \sqrt{\frac{n-1}{n+1}}\left(\frac{n}{\sqrt{n^2-1}}\right)^n < 1 .

Three problems produce such a field: minimizing a convex $f$ on a ball (the field (3.62), a subgradient inside the ball and the outward radial direction outside); the convex program $\min f_0$ s.t. $f_i \le 0$ (the field (3.65), a subgradient of the objective at feasible points and of a most violated constraint otherwise); and a convex–concave saddle point problem (the field $\{g_f^x, -g_f^y\}$ ).

Formalization targets

Goal: Theorem 3.14 (p. 86)

For every $k$ ,

\|A_k(x_k - x^*)\| \le h_k (n+1), \tag{3.61}

that is, $x^* \in \Phi_k$ . The statement holds for every field $g$ satisfying the monotonicity condition at $x^*$ ; nothing about continuity or convexity is assumed.

Milestones

Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$ for unit $\xi$ .
Volume of $\Phi_k$ (p. 87): $(n+1)h_k = R r^k$ and $v(\Phi_k) = v_0 R^n r^{nk}/\det A_k$ , $v_0$ the volume of the unit ball.
Volume ratio (p. 87–88): $v(\Phi_{k+1}) = q_n\, v(\Phi_k)$ with $q_n < 1$ , the volumes being positive and finite.
Eq. (3.62): the ball field satisfies $(g(x), x - x^*) \ge 0$ .
Eq. (3.65): the convex-programming field satisfies $(g(x), x - x^*) \ge 0$ .
Saddle point field (p. 90): $(g(z), z - z^*) \ge 0$ .

Significance

The result. Theorem 3.14 with the volume identity says that after $k$ steps the solution is confined to an ellipsoid of volume $q_n^k$ times that of the initial ball, for any field of the above kind. Milestones 4–6 turn this into localization guarantees for constrained convex minimization, general convex programming and convex–concave saddle points, with a rate that depends only on the dimension. The same localization underlies the complexity bounds of the ellipsoid method for linear programming and the polynomial equivalence of separation and optimization.

Formalizing it. The results are classical and proved in the book. No machine-checked proof of the space-dilation form of the method is known to exist. The platform already contains a proved version of the Bertsimas–Tsitsiklis form (LinearOptimization.ellipsoid_update_halfspace_subset, LinearOptimization.ellipsoid_update_volume_lt: a half-ellipsoid $E(z, D) \cap \{a^Tx \ge a^Tz\}$ is covered by an updated ellipsoid whose volume is smaller by a factor below $e^{-1/(2(n+1))}$ ), and Khachiyan's feasibility algorithm (SmaleNinth.khachiyan_ellipsoid_decides). Those statements are about a center/shape-matrix update and give a volume inequality; this mission is about the iterates of Shor's matrix recursion $B_{k+1} = B_k R_\beta(\xi_k)$ and the exact ratio $q_n$ . Relating the two parametrizations ( $D_k = (n+1)^2 h_k^2 B_k B_k^T$ ) is a welcome side result.

Difficulty

The obvious approach, tracking the ellipsoid through the center and shape matrix and invoking a minimum-volume covering argument, is not what the algorithm computes: here the iterate is updated through the factor $B_k$ and the stepsize $h_k$ is fixed in advance, independent of the field, so the induction must be carried out in the transformed coordinates $z_k = A_k(x_k - x^*)$ in which the ellipsoid is a ball. The difficulty is that the monotonicity condition gives only the sign of one inner product, $(z_k, \xi_k) \ge 0$ , while the norm of $z_{k+1}$ depends on both $(z_k,\xi_k)$ and $\|z_k\|$ ; the constants $\beta$ and $r$ are exactly those for which the resulting quadratic estimate closes. For the volume identity, the main technical step is computing $\det R_\beta(\xi) = \beta$ and the Lebesgue measure of a linear image of a ball in EuclideanSpace.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; $B_k^*$ is the transpose. $R_\alpha(\xi)$ is the matrix $I + (\alpha-1)\xi\xi^T$ (the book's property 10); for unit $\xi$ this is the operator of the book's definition.
The algorithm is the definition ellipsoidMethod g R x₀ : ℕ → EllState n, with state $(x_k, B_k, h_k)$ , $B_0 = I$ , $h_0 = R/(n+1)$ . If $g(x_k) = 0$ the state is repeated from then on (the book stops); the normalization in (3.57) is only performed when $g(x_k) \ne 0$ . $A_k$ is the matrix inverse of $B_k$ , which is nonsingular.
Theorem 3.14 is stated for $n > 1$ , $R > 0$ , $x^*$ with $\|x_0 - x^*\| \le R$ and $(g(x), x - x^*) \ge 0$ for all $x$ , for every $k$ . The book's additional assumption that $g(x) \ne 0$ for $x \ne x^*$ is not used by its proof and is omitted. The iterates are those of the recursion; a statement about an arbitrary ellipsoid containing $x^*$ , or about an arbitrary invertible matrix in place of $B_k$ , would not be this theorem and is ruled out by the definitions.
Volumes are Lebesgue measure in ℝ≥0∞. The ellipsoid is given for an arbitrary center (the book writes $x^*$ in one place and $x_k$ in another; the volume is the same). The volume formula requires the first $k$ iterations to have been performed ( $g(x_j) \ne 0$ , $j < k$ ); the ratio requires iteration $k+1$ to be performed.
The printed chain on p. 87 has misprints (exponents $2$ and $1$ on $n/\sqrt{n^2-1}$ where $n$ is meant, and $(n-1)/(n+1)$ for $\sqrt{(n-1)/(n+1)}$ ); the statement follows the value of $q_n$ given on p. 88. The estimate for $x \notin S(x_0,R)$ before (3.62) has a sign misprint; only the conclusion is stated.
Needed infrastructure: determinant of a rank-one perturbation of the identity ( $\det(I + c\,\xi\xi^T) = 1 + c\|\xi\|^2$ , available in Mathlib as the matrix determinant lemma), the measure of a linear image (MeasureTheory.Measure.addHaar_image_linearMap), and elementary real inequalities for $q_n < 1$ . The space-dilation lemmas are reusable in the other Shor missions on SDG methods and the $r$ -algorithm.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §3.8. https://doi.org/10.1007/978-3-642-82118-9
D. B. Yudin and A. S. Nemirovskii, Informational complexity and efficient methods for the solution of convex extremal problems, Ekonomika i Matematicheskie Metody 12 (1976), 357–369 (English translation: Matekon 13 (1977), 25–45).
N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13 (1977), 94–96.
L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20 (1979), 191–194.
R. G. Bland, D. Goldfarb and M. J. Todd, The ellipsoid method: a survey, Operations Research 29 (1981), 1039–1091. https://doi.org/10.1287/opre.29.6.1039
M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

8 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions XI: Convexity and Subgradients of the Value Function in Decomposition with Respect to VariablesTextbook

Motivation

Large convex programs often have a block structure: a small set of "complicating" variables $x$ couples otherwise separate subproblems in the remaining variables $y$ . Decomposition with respect to variables fixes $x$ , solves the subproblem in $y$ , and treats the optimal subproblem value as a function of $x$ alone. The outer problem in $x$ is then small but nonsmooth, because the optimal value of a constrained program is generally not differentiable in its parameters. Shor's Chapter 4 (Shor 1985, Ch. 4) presents this reduction as a principal application of subgradient methods: once a subgradient of the outer function can be read off from the subproblem, the methods of Chapters 2–3 apply directly. The same construction underlies Benders decomposition (Benders 1962) and its convex generalization (Geoffrion 1972), and parametric decomposition schemes for linear programs.

The chapter's other numbered results serve the same programme from the dual side: the Lagrangian dual function of a program over a compact set gives a lower bound usable in branch and bound (Theorem 4.3), exact nonsmooth penalty functions turn a constrained convex program into one unconstrained nonsmooth minimization (Theorem 4.2; nonsmooth penalties were first studied systematically by I. I. Eremin, 1967), and a stochastic transportation model is shown to be a convex program before being solved through its dual (Lemma 4.3).

Setting

The variables split into $x \in E^x_l$ and $y \in E^y_m$ (Euclidean spaces, inner product $(\cdot,\cdot)$ ). The problem is

\min_{x,y} f_0(x,y) \quad \text{s.t.} \quad f_i(x,y) \le 0,\quad i = 1,\dots,n, \qquad (4.1)\text{–}(4.2)

with $f_0, f_1, \dots, f_n$ convex functions of $z = (x,y)$ (jointly convex), finite everywhere. For a fixed $\bar x$ , the subproblem (4.3)–(4.4) is $\min_{y \in D(\bar x)} f_0(\bar x, y)$ with $D(\bar x) = \{y : f_i(\bar x,y) \le 0\}$ . Where it has a solution $y(\bar x)$ , the value function is

\Phi(\bar x) = \min_{y \in D(\bar x)} f_0(\bar x,y). \qquad (4.5)

The Slater condition at $\bar x$ asks for a $y$ with $f_i(\bar x,y) < 0$ for all $i$ . The Lagrange function is $L_U(x,y) = f_0(x,y) + \sum_i U_i f_i(x,y)$ , and $U \ge 0$ are Kuhn–Tucker multipliers at $\bar x$ when $\Phi(\bar x) = \min_y L_U(\bar x,y)$ . A subgradient of a function of $(x,y)$ is written through its projections $(g^x, g^y)$ on the two blocks; a subgradient of $\Phi$ at $\bar x$ is a $g$ with $\Phi(x) - \Phi(\bar x) \ge (x - \bar x, g)$ .

Formalization targets

Goal: Theorem 4.1 (p. 94)

If $W$ is a convex set of $x$ -values at which the subproblem has a solution, then $\Phi$ is convex on $W$ ; and if $\bar x \in W$ satisfies the Slater condition, then for every optimal $y(\bar x)$ , multipliers $U$ exist, $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with vanishing $y$ -projection, and the $x$ -projection of any such subgradient satisfies

g_\Phi(\bar x) = g^x_{L_U}(\bar x, y(\bar x)) \in \partial \Phi(\bar x). \qquad (4.6)

Milestones for the goal

Convexity of $\Phi$ on $W$ (Theorem 4.1, first assertion).
Existence of Kuhn–Tucker multipliers for the subproblem under Slater (p. 95, display).
Existence of a subgradient of $L_U$ with vanishing $y$ -projection (p. 95).
Formula (4.6) for a given multiplier vector and such a subgradient (p. 95, final display).

Further results of the chapter

Corollary (4.7): if each $f_\alpha(x,\cdot)$ is continuously differentiable in $y$ , then $g^x_{f_0} + \sum_i U_i g^x_{f_i}$ , built from arbitrary subgradients of the $f_\alpha$ , is a subgradient of $\Phi$ .
Lemma 4.3: the stochastic transportation problem (4.163)–(4.165) is a convex program.
Theorem 4.2: with nonsmooth penalties $p_i$ whose slopes $c_i = \lim_{t\to0+} p_i(t)/t$ exceed a Lagrange multiplier vector $\bar y$ , the minimizers of $S = f_0 + \sum p_i \circ f_i$ are exactly the solutions of the constrained program; and if a minimizer of $S$ solves the program, some multiplier vector satisfies $\bar y \le c$ .
Theorem 4.3: for $\Phi(u) = \min_{x\in X}[f_0 + \sum u_i f_i]$ over a compact $X$ , $Q = \max_{u\ge0}\Phi(u) \le f^*$ .

Significance

The result itself. Theorem 4.1 is what makes decomposition with respect to variables an instance of convex nonsmooth minimization: the outer problem is convex, and one subproblem solve returns both $\Phi(\bar x)$ and a subgradient. The algorithm on p. 96 — solve the subproblem at $x_k$ , form $g_\Phi(x_k)$ by (4.6) or (4.7), take a subgradient step — is exactly this, and the step-size theory of Chapter 2 then gives convergence. The Corollary is the version used in practice for linear and quadratic subproblems, where multipliers and partial subgradients are computed directly. Theorem 4.2 justifies replacing constraints by nonsmooth penalties of finite slope, and Theorem 4.3 is the weak-duality bound behind Lagrangian relaxation in branch and bound.

Formalizing it. All results are classical and proved in the book; none is formalized as stated here. The platform already has related statements with different shapes: convexity of the perturbation value function in the constraint right-hand side (VectorSpaceOpt.perturbationValue_convex, Luenberger), Slater strong duality over the whole space (ConvexOptimization.slater_strong_duality), weak duality with an unconstrained domain (ConvexOptimization.weak_duality), weak Lagrangean duality for integer programs (LinearOptimization.integer_program_weak_lagrangean_duality), and the LP special case of convexity of the optimal cost (LinearOptimization.lp_optimal_cost_convex_in_rhs). This mission adds the partial-minimization form in which one block of variables is minimized out under joint convexity, its subgradient calculus, exact nonsmooth penalties, and weak duality over a compact domain.

Difficulty

Convexity of $\Phi$ is elementary once the minimum is attained. The subgradient formula is where the obvious argument fails: an arbitrary subgradient of $L_U$ at $(\bar x, y(\bar x))$ does not project to a subgradient of $\Phi$ , because its $y$ -projection contributes a term $(y(x) - y(\bar x), g^y)$ of unknown sign. The theorem needs a subgradient whose $y$ -projection vanishes, and its existence is a separate fact about partial minimization of a jointly convex, everywhere-finite function. The multipliers come from the Kuhn–Tucker theorem for the subproblem, which requires the Slater condition. In the Corollary, the difficulty is to show that differentiability in $y$ forces the $y$ -projection of any combination $g_{f_0} + \sum U_i g_{f_i}$ to vanish. In Theorem 4.2 the necessity part needs a subdifferential chain rule for $p_i \circ f_i$ .

Formalization scope

$E^x_l$ , $E^y_m$ and $E_N$ are EuclideanSpace ℝ (Fin l), EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin N); constraints are indexed by Fin n (or Fin m). All functions are real-valued and finite everywhere; joint convexity is convexity on the product $E^x_l \times E^y_m$ .
$\Phi$ is a real infimum over $D(x)$ . It is the book's minimum wherever the minimum is attained, and every statement assumes attainment at each point of $W$ . A statement about $\Phi$ at points where the subproblem has no solution would be about Lean's default value $0$ , and is ruled out by these hypotheses.
"Convex on some convex subset $W$ of $E_n$ " is read as convexity on every convex $W$ on which $\Phi$ is defined. A formalization quantifying over a single unspecified $W$ (e.g. a singleton) would be trivially true.
Formula (4.6) is stated for subgradients of $L_U$ whose $y$ -projection is zero, as the book's proof uses it; the subgradient inequality for $\Phi$ is stated on all of $W$ .
Kuhn–Tucker multipliers relative to an optimal $\bar y$ : $U \ge 0$ , $U_i f_i(\bar x,\bar y) = 0$ , and $\bar y$ minimizes $L_U(\bar x,\cdot)$ over all $y$ .
Theorem 4.2: a Lagrange multiplier vector is $\bar y \ge 0$ with $f_0 + \sum\bar y_i f_i \ge f^*$ everywhere, $f^*$ the finite optimal value; the necessity clause is read as "for some multiplier vector" (for all multiplier vectors it is false); the limits $c_i$ are given as hypotheses.
Theorem 4.3: the minimum (4.187) attained for every $u \ge 0$ (the book's "min"; no continuity assumed); $f^*$ attained; $Q$ attained as the book's "max" presupposes.
Lemma 4.3: demands with densities and finite mean, penalty coefficients $r_j \ge 0$ .

Useful infrastructure beyond this mission: partial minimization of jointly convex functions, subgradients on product spaces, and a Kuhn–Tucker saddle-point theorem for convex programs with inequality constraints. Proofs of any milestone, and reusable lemmas for these, are welcome.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Ch. 4, pp. 93–96, 131–133, 146–148. https://doi.org/10.1007/978-3-642-82118-9
J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4, 1962, 238–252. https://doi.org/10.1007/BF01386316
A. M. Geoffrion, Generalized Benders decomposition, Journal of Optimization Theory and Applications 10, 1972, 237–260. https://doi.org/10.1007/BF00934810
I. I. Eremin, The penalty method in convex programming, Soviet Mathematics Doklady 8, 1967, 459–462 (Shor's reference [22]).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29 (partial minimization and perturbation functions). https://doi.org/10.1515/9781400873173

12 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Linear Programming: Foundations and Extensions I: Degeneracy and Termination of the Simplex Method under Bland's RuleTextbook

Motivation

The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).

The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.

Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).

Setting

A linear program in standard form has $m$ constraints and $n$ decision variables:

\text{maximize } \sum_{j=1}^n c_j x_j \quad\text{subject to}\quad \sum_{j=1}^n a_{ij}x_j \le b_i\ (i=1,\dots,m),\qquad x_j \ge 0\ (j=1,\dots,n).

A solution $x$ is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.

The slack variables $w_i = b_i - \sum_j a_{ij}x_j$ are appended to the list of variables as $x_{n+i} = w_i$ , so that the constraints become the linear system $[A\ I]\,x = b$ with $x \ge 0$ in $\mathbb{R}^{n+m}$ . A dictionary is given by a set $\mathcal B$ of $m$ basic indices whose columns of $[A\ I]$ are linearly independent; the remaining indices $\mathcal N$ are nonbasic. Solving for the basic variables gives

\zeta = \bar\zeta + \sum_{j\in\mathcal N}\bar c_j x_j,\qquad x_i = \bar b_i - \sum_{j\in\mathcal N}\bar a_{ij}x_j\quad (i\in\mathcal B).

The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if $\bar b_i \ge 0$ for every $i\in\mathcal B$ , and degenerate if $\bar b_i = 0$ for some $i\in\mathcal B$ .

The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable $x_k$ is chosen among the nonbasic variables with $\bar c_k > 0$ , and a leaving variable $x_l$ among the basic variables with $\bar a_{lk} > 0$ that minimize the ratio $\bar b_l/\bar a_{lk}$ ; then $x_k$ becomes basic and $x_l$ nonbasic. The method stops when no $\bar c_j$ is positive (the dictionary is optimal) or when the entering column has no positive $\bar a_{ik}$ (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols $0<\epsilon_m\ll\dots\ll\epsilon_1\ll$ all data and chooses the leaving variable by the perturbed ratio test.

Formalization targets

Goal: Theorem 3.3 (termination under Bland's rule, p. 31)

From every feasible dictionary $D_0$ , there is no infinite sequence of pivots

D_0\to D_1\to D_2\to\cdots

in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary $D_T$ at which the method stops, optimal or exhibiting unboundedness.

Milestones

Theorem 3.1 (p. 27): if the simplex method fails to terminate, it must cycle, i.e. an infinite run visits some dictionary twice.
Theorem 3.2 (p. 30): the simplex method always terminates when the leaving variable is selected by the lexicographic rule.
Theorem 3.4 (p. 33), the fundamental theorem: (1) with no optimal solution the problem is infeasible or unbounded; (2) if a feasible solution exists, a basic feasible solution exists; (3) if an optimal solution exists, a basic optimal solution exists.

Significance

The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.

Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form $Ax=b$ , $x\ge 0$ , full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over $[A\ I]$ . This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.

Difficulty

The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length $\bar b_l/\bar a_{lk}$ is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.

For Theorem 3.2, the symbols $\epsilon_i$ cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.

Formalization scope

Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The $n+m$ variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order $x_1,\dots,x_n,x_{n+1}=w_1,\dots,x_{n+m}=w_m$ that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has $m$ elements and a proof that its columns of $[A\ I]$ are linearly independent; the coefficients $\bar b,\bar a,\bar c,\bar\zeta$ are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.

Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors $(\bar b_i, r_{i1},\dots,r_{im})/\bar a_{ik}$ of the perturbed ratios; the symbol $\epsilon_p$ is attached in the starting dictionary to its $p$ -th basic variable in increasing index order, which for the initial dictionary is the $p$ -th constraint. Unboundedness in Theorem 3.4 is "for every $M$ a feasible solution with objective $>M$ ", as defined on p. 7. The statements carry no explicit constants.

A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.

A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 3. https://doi.org/10.1007/978-1-4614-7630-6
R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
G. B. Dantzig, A. Orden, P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2):183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020406
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.4 (lexicographic rule and Bland's rule in tableau form).

10 thms4 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions II: Farkas' Lemma and Strict Complementary SlacknessTextbook

Motivation

Every linear program comes with a second linear program, its dual, and most of what is known about linear programming is a statement about how the two interact. Weak duality gives certificates of optimality; strong duality says those certificates always exist; complementary slackness turns optimality into a system of equations. These three facts are the core of any first course in optimization and of every correctness argument for the simplex method.

Strict complementarity is the sharpest statement of the same kind. Complementary slackness says that in each pair (a primal variable and its dual slack, a dual variable and its primal slack) at least one member vanishes at optimality. Strict complementarity says that some optimal pair can be chosen so that exactly one member vanishes in each pair. The result is due to Goldman and Tucker (1956). It is what identifies the optimal face of a linear program and its partition of the variables into those that can be positive at an optimum and those that cannot, and it is a standing ingredient in the analysis of interior-point methods, which approach this strictly complementary optimum rather than a vertex.

This mission formalizes the chain from duality to strict complementarity as it is developed in Chapters 5 and 10 of Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, doi:10.1007/978-1-4614-7630-6). It is the second mission of a series on that book.

Timeline:

1902 — Farkas publishes the lemma on the solvability of linear inequality systems.
1947–1951 — von Neumann, and Gale, Kuhn and Tucker, establish linear programming duality.
1956 — Goldman and Tucker prove the existence of strictly complementary optimal solutions (in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38).

Setting

Fix integers $m, n \ge 0$ , a real $m \times n$ matrix $A = (a_{ij})$ , a vector $b \in \mathbb{R}^m$ and a vector $c \in \mathbb{R}^n$ . The primal problem is

\text{maximize } c^T x \quad\text{subject to}\quad Ax + w = b,\quad x \ge 0,\ w \ge 0, \qquad (10.9)

where $w = b - Ax$ is the primal slack. The dual problem is

\text{minimize } b^T y \quad\text{subject to}\quad A^T y - z = c,\quad y \ge 0,\ z \ge 0, \qquad (10.10)

where $z = A^T y - c$ is the dual slack. A vector $x$ is primal feasible if $x \ge 0$ and $w \ge 0$ ; it is primal optimal if it is feasible and $c^T x' \le c^T x$ for every feasible $x'$ . Dual feasibility and dual optimality are defined in the same way, with minimization. Inequalities between vectors are componentwise, and $\xi > 0$ means that every component of $\xi$ is strictly positive.

A halfspace of $\mathbb{R}^n$ is a set $\{x : a^T x \le \beta\}$ with $a \ne 0$ ; a polyhedron is a set $\{x : Ax \le b\}$ for some $m$ , $A$ and $b$ .

In the Lean development these objects live in the namespace VanderbeiLP.StrictComp: primalSlack A b x, dualSlack A c y, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, IsHalfspace, IsPolyhedron.

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

If the primal (10.9) has an optimal solution, then there exist a primal optimal $x^*$ and a dual optimal $y^*$ , with slacks $w^* = b - Ax^*$ and $z^* = A^T y^* - c$ , such that

x^* + z^* > 0 \qquad\text{and}\qquad y^* + w^* > 0.

The only hypothesis is primal optimality; the existence of a dual optimum is part of the conclusion.

Milestones

Theorem 5.1 (Weak Duality). Primal feasible $x$ and dual feasible $y$ satisfy $c^T x \le b^T y$ .
Theorem 5.2 (Strong Duality). If the primal has an optimal $x^*$ , the dual has an optimal $y^*$ with $c^T x^* = b^T y^*$ .
Theorem 5.3 (Complementary Slackness). Feasible $x$ , $y$ are both optimal if and only if $x_j z_j = 0$ for all $j$ and $w_i y_i = 0$ for all $i$ .
Lemma 10.5 (Farkas' Lemma). $Ax \le b$ has no solution if and only if some $y$ satisfies $A^T y = 0$ , $y \ge 0$ , $b^T y < 0$ .
Theorem 10.4 (Separation of polyhedra). Two disjoint nonempty polyhedra lie in two disjoint halfspaces.
Theorem 10.6. If both problems are feasible, there are feasible $\bar x$ , $\bar y$ with $\bar x + \bar z > 0$ and $\bar y + \bar w > 0$ .

Theorem 10.6 is the feasible-solution version of the goal; Theorem 10.4 is a further consequence of Farkas' Lemma in the same chapter.

Significance

Strict complementarity determines the optimal partition: the set of indices $j$ for which some optimal $x^*$ has $x^*_j > 0$ is exactly the complement of the set for which some optimal dual slack $z^*_j$ is positive. This partition describes the optimal faces of both problems, is the object that interior-point methods recover in the limit, and is the starting point of sensitivity analysis beyond a single optimal basis. Farkas' Lemma and the separation theorem are the linear-algebraic form of convex separation and are reused across optimization, game theory and polyhedral combinatorics.

All results of this mission are classical and proved in the literature. What the mission adds is a machine-checked version of them in one fixed linear-programming form, the inequality form with explicit slacks used throughout Vanderbei's book. Weak duality, strong duality and complementary slackness are already formalized on this platform for other forms (Bertsimas–Tsitsiklis's general form, a minimization, and a covering pair with the roles of primal and dual exchanged). Those statements are equivalent to the ones here only after a transformation (negating the objective, swapping primal and dual), so they are not the same theorems. The Farkas variant for inequality systems, the separation theorem for two polyhedra, and both strict complementarity theorems have no formal counterpart on the platform.

Difficulty

Weak duality and the converse direction of complementary slackness are short computations. The substance lies elsewhere. Strong duality and Farkas' Lemma require a genuine existence argument; the book obtains them from the simplex method, whose termination is itself a nontrivial fact, and any other route needs an independent theorem of the alternative.

For strict complementarity the obvious attempt fails. Complementary slackness gives, for each optimal pair, only that one member of each complementary pair vanishes; nothing in a single optimal basic solution forces the other member to be positive, and in degenerate problems every basic optimal pair can fail strictness. A strictly complementary pair is in general not a vertex of either optimal face, so it cannot be found by inspecting basic solutions. The goal also asks for more than Theorem 10.6: the positivity must be achieved within the optimal sets, which are faces cut out by an additional objective-level constraint, so the feasible-solution argument does not transfer verbatim.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; the constraint matrix is Matrix (Fin m) (Fin n) ℝ; m and n are arbitrary natural numbers, including zero. The slacks are functions of the solution (primalSlack A b x = b - A *ᵥ x, dualSlack A c y = Aᵀ *ᵥ y - c), never free variables, so a "solution $(x, w)$ " of the book is the vector $x$ with the slack it determines. Optimality is attainment of the maximum (minimum) over the feasible set; no supremum, value function or extended reals are involved. The strict inequality $\xi > 0$ is written componentwise as ∀ j, 0 < x j + dualSlack A c y j and ∀ i, 0 < y i + primalSlack A b x i.

A halfspace carries a nonzero normal vector. Without that requirement the empty set would be a halfspace and the separation theorem would be trivial; the formal definition rules this out.

The book states every result in this mission with its hypotheses explicit, and none of them asserts the existence of an unspecified constant, so no explicit-constant instantiation was needed. The remark after Theorem 10.7 refers to "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3, and the milestones follow the theorem numbering.

A complete development needs a theorem of the alternative for real linear inequality systems (Mathlib has Farkas-type results for cones and the geometric Hahn–Banach theorem, but no ready-made matrix version of Lemma 10.5) and elementary convex-combination arguments on feasible sets. The definitions of this mission are self-contained and reusable for any later chapter that works in Vanderbei's inequality form. Proofs of any milestone are welcome, as are proofs that avoid the simplex method.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014. doi:10.1007/978-1-4614-7630-6
J. Farkas, "Theorie der einfachen Ungleichungen", Journal für die reine und angewandte Mathematik 124 (1902), 1–27. doi:10.1515/crll.1902.124.1
A. J. Goldman and A. W. Tucker, "Theory of linear programming", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

9 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$ . Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$ , and arc $(i,j)$ carries a cost $c_{ij}$ . The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$ , $-1$ in row $i$ , and $0$ elsewhere. The network flow problem (14.1) is

\text{minimize } c^{T}x\quad\text{subject to}\quad Ax=-b,\ x\ge 0 .

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$ . A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$ , and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$ , a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$ , $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$ , $t\notin C$ , and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$ .

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .

Milestones

Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .

Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
Theorem 15.1, Max-Flow Min-Cut (p. 234):

\max\{x_{ts}\}=\min_C \kappa(C),

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$ , bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
"Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
A basis is $m-1$ linearly independent columns of the $(m-1)$ -row matrix $\tilde A$ , the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$ , and for $k=0<n$ the claim is false. No connectedness is assumed.
For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

7 thms2 active usersReviewed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions IV: Existence of the Central PathTextbook

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

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

5 thms1 active userReviewed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions V: Convergence Rates of the Path-Following MethodTextbook

Motivation

Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.

Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ . The primal problem is to maximize $c^Tx$ subject to $Ax + w = b$ , $x, w \ge 0$ ; the dual is to minimize $b^Ty$ subject to $A^Ty - z = c$ , $y, z \ge 0$ . A primal–dual point is a quadruple $(x, w, y, z)$ with $x, z \in \mathbb{R}^n$ , $w, y \in \mathbb{R}^m$ ; it is strictly positive, $(x, w, y, z) > 0$ , if every component is. Write $X, W, Y, Z$ for the diagonal matrices of $x, w, y, z$ and $e$ for the all-ones vector. The norms are $\|v\|_1 = \sum_j |v_j|$ and $\|v\|_\infty = \max_j |v_j|$ .

At a point $(x, w, y, z)$ the three measures of progress are the primal infeasibility $\rho = b - Ax - w$ , the dual infeasibility $\sigma = c - A^Ty + z$ , and the complementarity $\gamma = z^Tx + y^Tw$ . Fix parameters $0 < \delta < 1$ and $0 < r < 1$ . One iteration of the method, from a strictly positive point, sets $\mu = \delta\gamma/(n+m)$ , takes any solution $(\Delta x, \Delta w, \Delta y, \Delta z)$ of the Newton system

A\Delta x + \Delta w = \rho, \quad A^T\Delta y - \Delta z = \sigma, \quad Z\Delta x + X\Delta z = \mu e - XZe, \quad W\Delta y + Y\Delta w = \mu e - YWe,

computes the step length

\theta = r\left(\max_{i,j}\left\{\left|\tfrac{\Delta x_j}{x_j}\right|, \left|\tfrac{\Delta w_i}{w_i}\right|, \left|\tfrac{\Delta y_i}{y_i}\right|, \left|\tfrac{\Delta z_j}{z_j}\right|\right\}\right)^{-1} \wedge 1 \qquad (18.7)

(with $\theta = 1$ when all ratios vanish), and moves to $(x + \theta\Delta x, w + \theta\Delta w, y + \theta\Delta y, z + \theta\Delta z)$ . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts $^{(k)}$ denote the quantities at the $k$ -th iterate, and $\theta^{(k)}$ is the step length computed there.

Formalization targets

Goal: Theorem 18.1 with the explicit constant

If $t > 0$ , $M$ is real, and for all $k \le K$ one has $\theta^{(k)} \ge t$ , $\|x^{(k)}\|_\infty \le M$ , $\|y^{(k)}\|_\infty \le M$ , then for all $k \le K$ , with $\tilde t = t(1-\delta)$ ,

\|\rho^{(k)}\|_1 \le (1-t)^k\|\rho^{(0)}\|_1, \qquad \|\sigma^{(k)}\|_1 \le (1-t)^k\|\sigma^{(0)}\|_1, \qquad \gamma^{(k)} \le (1-\tilde t)^k \left(\gamma^{(0)} + \frac{M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)}{\delta t}\right).

Milestones

The one-step identities for the infeasibilities, $\tilde\rho = (1-\theta)\rho$ (18.8) and $\tilde\sigma = (1-\theta)\sigma$ (18.9); the one-step complementarity estimate

\tilde\gamma \le (1 - (1-\delta)\theta)\gamma + M\|\rho\|_1 + M\|\sigma\|_1 \qquad (18.10)

under $\|x\|_\infty, \|y\|_\infty \le M$ ; and the recursion $\gamma^{(k)} \le (1-\tilde t)\gamma^{(k-1)} + M(1-t)^{k-1}(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ (18.11). Two unnumbered statements complete the picture: every iteration has $0 < \theta \le 1$ and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies $|b^Ty - c^Tx| \le \gamma + \|\sigma\|_1\|x\|_\infty + \|\rho\|_1\|y\|_\infty$ (§18.5.3).

Significance

Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor $1 - t$ per iteration while the complementarity, and hence (by the duality-gap estimate) the gap $b^Ty - c^Tx$ , falls only by $1 - \tilde t$ . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.

All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.

Difficulty

The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term $\theta^2(\Delta y^T\rho - \sigma^T\Delta x)$ that has no sign. Bounding it requires relating the size of the step $\theta\Delta$ to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon $K$ is what makes the statement non-trivial.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, $A$ is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case $\theta = 1$ when all ratios vanish, since Lean's r / 0 = 0 would otherwise give $\theta = 0$ . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current $+\ \theta \cdot$ direction. The hypotheses $0 < \delta < 1$ , $0 < r < 1$ (pp. 272–273) are stated in every theorem; $M$ is an arbitrary real number and $K$ a natural number. As in the book, the hypotheses of Theorem 18.1 range over $k \le K$ , so the iteration from index $K$ is part of the data.

Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant $\bar M < \infty$ ". Because $K$ is fixed, that existential is satisfied trivially by $\max_{k \le K}\gamma^{(k)}/(1-\tilde t)^k$ , and a statement with $\exists \bar M$ would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): $\bar M = \gamma^{(0)} + M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)/(\delta t)$ . Eq. (18.11) is stated with the book's $\tilde M = M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ written out.

The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 18, pp. 269–283. https://doi.org/10.1007/978-1-4614-7630-6
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

6 thms1 active userReviewed

Completed

Analysis Operations Research Probability+1·Captain: mikedeng1

Elements of Queueing Theory I: The Swiss Army Formula of Palm CalculusTextbook

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of `P⁰_N`

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

11 thms2 active usersReviewed

Analysis Operations Research Probability+1·Captain: mikedeng1

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

13 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory II: The Loynes Stability Theorem and CouplingTextbook

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

13 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory III: Stationary Regimes of Stochastic RecurrencesTextbook

Stationary Regimes of Stochastic Recurrences

Background

Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence

W_{n+1} = h(W_n, ξ_n),

driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this mission is about both.

Exact sampling, and what "exact" means

§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a stationary law π, and the classical way to sample it is to run the chain and wait. That gives a sample whose law converges to π and is never equal to it.

Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state, all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started further and further in the past. Once two chains meet they stay together, so eventually all r coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function preserves a partial order with a least and a greatest state, and a single uniform sequence drives every chain, the two extremal chains funnel all the others and their coalescence suffices.

Neither theorem is a statement about a program. Each says that a random variable is almost surely finite, and that another has a distribution equal to π.

Renovating events: sufficient, and then necessary

§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a finite random index.

Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime, reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences with a constant initial condition, strong backwards coupling produces renovating events. So the method characterises stability rather than merely detecting it.

The saturation rule

§2.11 treats the multidimensional case, where the state is a vector and the natural models are monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks it: under homogeneity, monotone and non-expansive are the same property. That is what puts these models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not depend on the initial condition.

The goal

Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues fed by the external stream, measure the departure intensity µ of the saturated system, and declare the network stable when λ < µ. The book is careful that this saturation rule "does not hold for all systems".

Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:

If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1.    If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.

Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.

Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.

What this mission provides

Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.

Formalization scope

The standing assumptions of §2.5.1 (p.104) are part of every §2.5.4 statement: (P⁰, θ) is ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.
Theorem 2.5.4 is stated for {W_n^{[C]}}, the sequence its proof on p.119 builds the renovating events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary 2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the page prints W_n.
Theorem 2.11.2 carries all four limits, a.s. and in expectation, for every integrable ℝ^K-valued random initial condition Y, under the book's linear lower bound E[X_n^{[0]}] > −Cn.
The goal is stated on the Palm space of a stationary ergodic marked point process: T_0 = 0, T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four framework assumptions for every point process. γ(0) is the a.s. limit of Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service, and dropping the link between the points and θ makes the second implication false. Neither is done.
Stating only one of the goal's two implications, or collapsing them into an equivalence, would be a different theorem. Both implications are stated, with the gap between ≥ 1 and > 1 left open.

12 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory IV: PASTA and the Formulas of Palm CalculusTextbook

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

14 thms2 active usersReviewed

Operations Research Probability Statistics+1·Captain: mikedeng1

Elements of Queueing Theory V: Strassen's Theorems and the Stochastic Ordering of QueuesTextbook

Strassen's Theorems and the Stochastic Ordering of Queues

Background

Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?

That requires an order on distributions. The chapter builds a family of them — integral orders — by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic) order; {cx} the convex functions, giving the convex order; and their intersection {icx}.

The goal

An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.

Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:

F ≤_cx G   ⟺   ∃ X ~ F, Y ~ G on one space with  E[Y | X] = X  a.s.
F ≤_icx G  ⟺   the same with  E[Y | X] ≥ X  a.s.

The convex order holds exactly when G is a martingale dilation of F — obtained by spreading each point out without moving its conditional mean. That is what makes the order usable: comparison results for queues become induction arguments on a coupling instead of analytic manipulations of convolutions of c.d.f.'s.

Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In dimension n there is no such formula, and that is why these are Strassen's theorems. The book attributes both to Strassen (1965) and proves neither.

Why FIFO is optimal

§4.1 is a different kind of comparison: not between two queues, but between two service disciplines for the same queue. The order there is majorization ≺, which compares how spread out two vectors of the same total are.

The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof is an interchange argument. Under any non-preemptive discipline that uses no information on the service times, customer k effectively receives service σ_{γ(k)} for some permutation γ; Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.

Feller's paradox, and what survives it

§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited", exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one fails. The order does not pass from the Palm probability to the stationary one.

For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second differences of f against Palm expectations, and a convex f makes every coefficient non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean cycle length, and shows that the normalisation does not hide the comparison it normalises by.

Formalization scope

Orders. ≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's test classes (§4.2.1), with the page's qualification that only test functions with well-defined integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.
Strassen. Both theorems are stated as equivalences, with the coupling existential over the probability space. Theorem 4.2.2 carries both clauses — E[Y | X] = X for ≤_cx, E[Y | X] ≥ X for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable; Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is not the theorem.
The queue of §4.1.3 is constructed: a GI/GI input (i.i.d. inter-arrival and service times, independent), a single work-conserving server started empty, and any non-preemptive discipline whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals, service times of customers already started) plus external randomisation. FIFO is one such discipline. The interchange permutations γ_n and their limit γ are built from the schedule as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.
Lemma 4.4.1 is stated with the exact second-difference series and assumes that series converges absolutely; the page states it for all f, which fails for heavy-tailed counts and sparse f.
The S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions — and apply only to distributions whose first coordinate is a.s. positive with a finite mean.

What this mission provides

None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing from Palm calculus, so this mission can be read on its own.

14 thms2 active usersReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Introduction to the Scenario Approach IV: The FAST Algorithm Keeps the Beta Bound and Adds a Factor (1−ε)^{N₂}Textbook

Motivation

The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample $N$ instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in $N$ and in the number $d$ of optimization variables. To reach a failure level $\varepsilon$ with confidence $1-\beta$ , the number of scenarios grows roughly like $\frac{2}{\varepsilon}\big(\ln\frac1\beta+d-1\big)$ (Theorem 1.1 of the book). The product of $d$ and $1/\varepsilon$ is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.

FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number $N_1$ of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers $N_2$ further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.

Timeline:

2006, Calafiore and Campi: violation bounds for the solution of convex scenario programs.
2008, Campi and Garatti: the exact binomial bound, tight for fully supported problems (Theorem 3.7 of the book).
2014, Carè, Garatti and Campi: FAST and its two-stage bound, Eq. (8.5).
2018, Campi and Garatti's textbook, §8.3, the source of this mission.

Setting

Let $\Delta$ be a measurable space carrying a probability measure $\mathbb P$ , and let $\ell(\nu,\delta)$ be a real loss of a decision $\nu\in\mathbb R^{d-1}$ under the uncertain parameter $\delta\in\Delta$ . As a standing assumption of the book, $\ell(\cdot,\delta)$ is convex for every $\delta$ .

Given scenarios $\delta_1,\dots,\delta_m$ drawn independently from $\mathbb P$ , the scenario program (1.4) is

\min_{\nu\in\mathbb R^{d-1}}\ \Big[\max_{i=1,\dots,m}\ \ell(\nu,\delta_i)\Big].

Its solution is $\nu^*$ and its optimal value $\ell^*$ . Assumption 3.6 requires that for every $m$ and every sample the solution exist and be unique. The pair $(\nu,\ell)$ has $d$ components, and $d$ is the number that enters every bound.

The risk (Definition 8.2) of a decision $\nu$ with cost level $\ell$ is

R(\nu,\ell)=\mathbb P\{\delta\in\Delta:\ \ell(\nu,\delta)>\ell\},

the probability that a new instance costs more than promised. It is the violation $V(\nu,\ell)$ of the epigraphic constraint $\ell\ge\ell(\nu,\delta)$ .

FAST takes $N_1+N_2$ independent scenarios. It solves (1.4) with the first $N_1$ of them, obtaining $\nu^*_{N_1}$ . In the detuning step it then sets

\ell^*_F=\max_{i=1,\dots,N_1+N_2}\ \ell(\nu^*_{N_1},\delta_i),

the smallest level that covers every scenario seen. The output is $(\nu^*_F,\ell^*_F)$ with $\nu^*_F=\nu^*_{N_1}$ .

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

For every $\varepsilon\in[0,1]$ ,

\mathbb P^{N_1+N_2}\{V(\nu^*_F,\ell^*_F)>\varepsilon\}\ \le\ (1-\varepsilon)^{N_2}\sum_{i=0}^{d-1}\binom{N_1}{i}\varepsilon^i(1-\varepsilon)^{N_1-i}.

No relation between $N_1$ and $d$ is required. When $N_1<d$ the sum equals $1$ and the bound reads $(1-\varepsilon)^{N_2}$ .

Milestone: Theorem 3.7 for program (1.4)

The first stage is an ordinary scenario program with $N_1$ scenarios. For $N\ge d$ ,

\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\ \le\ \sum_{i=0}^{d-1}\binom{N}{i}\varepsilon^i(1-\varepsilon)^{N-i},

that is, $R(\nu^*,\ell^*)$ is dominated by a $B(d,N-d+1)$ distribution (recalled on p. 90).

Milestone: the $N_2$ rule

For $\varepsilon,\beta\in(0,1)$ , $N_2\ge\frac1\varepsilon\ln\frac1\beta$ makes the right-hand side of (8.5) at most $\beta$ (p. 95).

Significance

The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With $N_1=Kd$ (the book suggests $K\approx20$ ) and $N_2\ge\frac1\varepsilon\ln\frac1\beta$ , the total number of scenarios is $Kd+\frac1\varepsilon\ln\frac1\beta$ . This is additive in $d$ and $1/\varepsilon$ rather than multiplicative, and the added $N_2$ scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: $\ell^*_F$ is in general higher than the value a classical scenario program with the same confidence would return.

Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The $N_2$ rule is an elementary but explicit sample-size certificate.

Difficulty

The obvious route treats the detuning step as a fresh scenario program with $N_1+N_2$ scenarios and applies Theorem 3.7 to it. That fails: $\nu^*_F$ is not the solution of that program, and Theorem 3.7 with $N_1+N_2$ scenarios gives a bound that is not of the product form (8.5). The level $\ell^*_F$ depends on all $N_1+N_2$ scenarios at once, including those that determined $\nu^*_{N_1}$ , and the map $c\mapsto R(\nu,c)$ is monotone but need not be continuous, so the event $V(\nu^*_F,\ell^*_F)>\varepsilon$ is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.

Formalization scope

Lean representation:

The decision space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin n); the book's $d$ is written $n+1$ , never with natural-number subtraction.
A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same $\mathbb P$ defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.
The maximum in (1.4) and in $\ell^*_F$ is Finset.sup' over a nonempty index set. $\ell^*_F$ runs over all $N_1+N_2$ scenarios, not over the $N_2$ new ones only.
The risk is (P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event $V>\varepsilon$ of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.
The first-stage solution is a map νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.

Hypotheses the book leaves implicit, stated explicitly:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (standing assumption, p. 6).
Existence and uniqueness of the solution (Assumption 3.6) for every $m\ge1$ and every sample. The program with no scenario has no minimum, so $m=0$ is excluded.
$N_1\ge1$ , since the first stage needs a scenario.
$\varepsilon\in[0,1]$ ; for $\varepsilon>1$ the factor $(1-\varepsilon)^{N_2}$ can be negative.
The loss is jointly measurable in $(\nu,\delta)$ and the first-stage solution map is measurable. The book glosses over measurability (p. 6, footnote 1; p. 33).

A formalization that bounds only the $N_2$ new scenarios is ruled out, because $\ell^*_F$ is defined as a maximum over all $N_1+N_2$ scenarios. So is one that takes $\ell^*_F$ as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.

A complete development needs the scenario program in loss form, product-measure conditioning on $\Delta^{N_1}\times\Delta^{N_2}$ , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018, §8.3 and Theorem 3.7. https://doi.org/10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, FAST—Fast Algorithm for the Scenario Technique, Operations Research 62(3):662–671, 2014. https://doi.org/10.1287/opre.2014.1257
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3):1211–1230, 2008. https://doi.org/10.1137/07069821X
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5):742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

6 thms1 active userReviewed

The OR Formalization Drive

Missions

Stochastic Dynamic Programming and the Control of Queueing Systems X: Average Cost Optimization of Continuous Time Markov Decision ChainsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 10.3.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Dynamic Programming and the Control of Queueing Systems XIII: Lyapunov Criteria and z Standard Markov Chains with CostsTextbook

Motivation

Setting

Formalization targets

Goal: Proposition C.2.6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Setting

Formalization targets

Goal: Proposition C.5.2

Milestones

Further results

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions III: Convergence of the Normalized Subgradient Method with Divergent-Series StepsizesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.2 (p. 25)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions VII: Geometric Convergence of Subgradient Methods with Space Dilation along the GradientTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions IX: Convergence of the r-Algorithm with Exact Directional MinimizationTextbook

Motivation

Setting

Formalization targets

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

Milestones

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions X: The Space-Dilation Ellipsoid Method Localizes the Solution in Ellipsoids Shrinking by the Ratio q_nTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.14 (p. 86)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions XI: Convexity and Subgradients of the Value Function in Decomposition with Respect to VariablesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 94)

Milestones for the goal

Further results of the chapter

The local meaning of `P⁰_N`