Operations Research

Completed

Algorithmic Game Theory Probability·Captain: mikedeng1

Correlated Equilibrium as an Expression of Bayesian Rationality II: Two-Person Correlated Equilibrium Distributions Are the Solutions of Linear InequalitiesResearch Paper

Motivation

A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.

That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.

Setting

Player 1 has a finite set $S^1$ of actions and player 2 a finite set $S^2$ . For $j \in S^1$ and $k \in S^2$ , $h^1_{jk}$ and $h^2_{jk}$ are the two players' payoffs at the action pair $(j,k)$ .

A correlated strategy pair is a pair of functions $f^1 : \Gamma \to S^1$ , $f^2 : \Gamma \to S^2$ on a finite probability space $(\Gamma, \mu)$ : a finite set $\Gamma$ with nonnegative weights $\mu(\gamma)$ summing to $1$ . Chance draws $\gamma$ and suggests the action $f^i(\gamma)$ to player $i$ . The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every $\varphi : S^1 \to S^1$ ,

\mathbb E\, h^1(\varphi(f^1), f^2) \le \mathbb E\, h^1(f^1, f^2),

and the analogous inequality holds for player 2 and every $\psi : S^2 \to S^2$ .

A distribution is a family $(p_{jk})_{j \in S^1, k \in S^2}$ with $p_{jk} \ge 0$ and $\sum_j \sum_k p_{jk} = 1$ . The distribution of a correlated strategy pair assigns to $(j,k)$ the probability $\mu\{f^1 = j,\ f^2 = k\}$ . A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.

In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k $= h^1_{jk}$ and p j k $= p_{jk}$ .

Formalization targets

Goal: Proposition 2.3

For every distribution $(p_{jk})$ : $(p_{jk})$ is a correlated equilibrium distribution if and only if

\sum_k \big(h^1_{jk} - h^1_{qk}\big)\, p_{jk} \ge 0 \quad \text{for all } j, q \in S^1, \tag{2.4}

\sum_j \big(h^2_{jk} - h^2_{jr}\big)\, p_{jk} \ge 0 \quad \text{for all } k, r \in S^2. \tag{2.5}

Milestones

Identification with distributions (Sect. 2, p. 4). A correlated strategy pair is a correlated equilibrium if and only if its distribution $p$ satisfies $\sum_j\sum_k p_{jk} h^1_{\varphi(j)k} \le \sum_j\sum_k p_{jk} h^1_{jk}$ for all $\varphi$ , and the analogous condition for player 2.
Conditioning on possible suggestions (proof of Prop. 2.3, p. 6). For a distribution, player 1's condition holds if and only if $H^1(q \mid j) \le H^1(j \mid j)$ for every suggestion $j$ of positive probability and every $q$ , where $H^1(q\mid j) = \sum_k h^1_{qk} p_{jk} / \sum_k p_{jk}$ ; likewise for player 2.
Player 1 gives (2.4): player 1's condition on $p$ is equivalent to (2.4).
Player 2 gives (2.5): player 2's condition on $p$ is equivalent to (2.5).

A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff $(5,5)$ .

Significance

The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution $p$ — into finitely many linear inequalities on $p$ alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating $|S^1|^2 + |S^2|^2$ linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".

Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.

Difficulty

The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given $p$ ; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability $\sum_k p_{jk}$ of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of $\gamma$ gives a stronger notion.

Formalization scope

Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs $H^1$ , $H^2$ use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.

A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on $p$ .

No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the $n$ -player generalization the paper alludes to.

Selected references

R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), 1–18. https://doi.org/10.2307/1911154
R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

6 thms2 active usersReviewed

Control Theory Mechanism Design Stochastic Systems·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$ , $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$ , risk aversions $r,p>0$ , a marginal volatility cost $h>0$ , slopes $\kappa,\theta\in\mathbb R$ , a horizon $T>0$ , an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$ .

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$ , at cost

c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$ , in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$ , and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$ ; write $\delta=\kappa-\theta$ . For a payment $\xi$ made at time $T$ , the consumer's and the producer's criteria are

J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].

A contract is an $\mathcal F_T$ -measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ . Finally $\rho=\frac{rp}{r+p}$ , $L_0=-\frac1r\log(-R_0)$ , $U(x)=-e^{-px}$ , $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$ .

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$ . Then

V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.

Milestones

Proposition 2.1. The best responses $\hat a(z)$ , $\hat b(\gamma)$ attain the infima defining $H_m$ , $H_v$ , and these Hamiltonians have explicit closed forms.
(A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$ .
Proposition A.3 (i), with the explicit solution of p. 28.

\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$ . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$ ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$ . Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ ; a contract remains any $\mathcal F_T$ -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$ , and every value is an extended-real supremum with $\sup\emptyset=-\infty$ . $B$ is read as $[\varepsilon,1]^d$ , with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$ ), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$ , without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$ ; the index range of $\hat b$ is $j=1,\dots,d$ ; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Control Theory Mechanism Design Stochastic Systems·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$ , cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$ , risk aversions $r,p>0$ , a marginal cost of volatility $h>0$ , marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$ , a horizon $T>0$ , an initial consumption $X_0$ and a reservation utility $R_0<0$ . Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$ .

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$ . A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$ .

Criteria. For a payment $\xi$ at time $T$ , the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$ . Contracts $\mathcal C$ are the $\mathcal F_T$ -measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$ , and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$ , the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$ :

V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .

Hamiltonians. $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ .

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$ . With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$ , $L_0=-\frac1r\log(-R_0)$ ,

m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},

V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .

Milestones

Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$ , and

H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).

Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$ , $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$ , and $F_0$ is non-decreasing.
Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$ , and lies in $[y,\frac p{r+p}y]$ when $y\le0$ .

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$ .

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$ -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$ , an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are $\mathbb F$ -martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$ .
Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ .
Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$ ; all suprema are in the extended reals, so the empty supremum is $-\infty$ , as on p. 9.
Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
Indices are Fin N, Fin d; $N=0$ , $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$ ).
Added hypotheses. $\varepsilon\le1$ ( $B\neq\emptyset$ ), $R_0<0$ ( $\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$ . The paper's closed form is computed with the effort cap removed (" $\eta_A\to0$ as $A\nearrow\infty$ ", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$ ; with $H_m$ the infimum is $-\infty$ . The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. " $j=1,\dots,N$ " for $\hat b$ means $j=1,\dots,d$ . In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$ " is read as $\eta_A\equiv0$ .

The goal is an equality of extended reals between $V^{SB}$ , defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 1: Logarithmic Regret for Two ArmsResearch Paper

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$ -armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$ . Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$ , with mean $\mu_i$ . Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$ , and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$ , a success count $S_i$ and a failure count $F_i$ , both starting at $0$ . In each round $t=1,2,\dots$ it

samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$ ;
plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$ ;
performs a Bernoulli trial with success probability $\tilde r_t$ , with outcome $r_t\in\{0,1\}$ ;
increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$ . The expected regret in time $T$ is

\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$ , the binomial cdf $F^B_{n,p}$ , and the random variable $X(j,s,y)$ : the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$ .

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$ , and every $T\ge 2$ ,

\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$ , is not the formal claim.

Milestones

Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$ .
Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$ .
Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$ .
Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$ , where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$ .
Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$ .
Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$ .

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$ -valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$ . Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$ .
Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$ , rewards $X(i,t)\sim D_i$ , and uniforms $V(i,t)$ . Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$ , $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$ . Ties in the arg max go to the smaller index (a null event).
Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$ . $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$ -valued, so Lemma 1 at $y=1$ reads $\infty=\infty$ , as in the paper.
O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$ ) is stated with one universal constant $C>0$ , quantified before the instance, the means and the horizon, for all $T\ge 2$ . Eq. (1) is stated the same way, without its printed numerals.
Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$ , the reward laws or $T$ , would not be Theorem 1.
Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

11 thms2 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources V: A Schedule Is Inventory-Feasible iff It Resolves Every Minimal Surplus and Shortage SetTextbook

Motivation

In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.

A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem $PSc|temp|C_{\max}$ .

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ with $n\ge 1$ , where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i\ge 0$ , with $p_0=p_{n+1}=0$ and $p_i>0$ for the real activities.

For each cumulative resource $k$ in a set $\mathcal R^\gamma$ , every activity $i$ has an integer demand $r_{ik}$ . If $r_{ik}<0$ , activity $i$ withdraws $-r_{ik}$ units of $k$ at its start; if $r_{ik}>0$ , it deposits $r_{ik}$ units at its completion; $r_{ik}=0$ means $k$ is not used. The demand $r_{0k}$ of the project beginning is the initial stock. Write $V_k^-=\{i\mid r_{ik}<0\}$ and $V_k^+=\{i\mid r_{ik}>0\}$ . Each resource has a safety stock $\underline R_k\in\mathbb Z$ and a storage capacity $\overline R_k\in\mathbb Z$ .

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge 0$ . The active set and the inventory of $k$ at time $t\ge 0$ are

\mathcal A_k(S,t)=\{i\in V_k^-\mid S_i\le t\}\cup\{i\in V_k^+\mid S_i+p_i\le t\},\qquad r_k(S,t)=\sum_{i\in\mathcal A_k(S,t)} r_{ik}.

The schedule is inventory-feasible if $\underline R_k\le r_k(S,t)\le\overline R_k$ for all $k$ and all $t\ge 0$ .

Two standing assumptions of the section are used throughout: (2.12.1) $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ , so the final inventory is admissible; and Remark 2.12.2, $\underline R_k\le 0\le\overline R_k$ .

A nonempty $F\subseteq V$ is a $k$ -surplus set if $\sum_{i\in F}r_{ik}>\overline R_k$ , and a $k$ -shortage set if $\sum_{i\in F}r_{ik}<\underline R_k$ . A $k$ -surplus set $F$ is minimal if no $k$ -surplus set arises from $F$ by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal $k$ -shortage sets are defined with the roles of replenishing and depleting activities exchanged. $\mathcal F_k^+$ and $\mathcal F_k^-$ denote the minimal $k$ -surplus and $k$ -shortage sets.

Formalization targets

Goal: Theorem 2.12.4

A schedule $S$ is inventory-feasible if and only if

\forall k,\ \forall F\in\mathcal F_k^+\ \exists j\in F,\ i\notin F:\ r_{jk}>0,\ r_{ik}<0,\ S_j+p_j\ge S_i,

\forall k,\ \forall F\in\mathcal F_k^-\ \exists j\in F,\ i\notin F:\ r_{jk}<0,\ r_{ik}>0,\ S_j\ge S_i+p_i.

Milestones

The invariance claim after Remark 2.12.2 (p. 131): adding the same integer $a_k$ to $r_{0k}$ , $\underline R_k$ and $\overline R_k$ does not change the set of inventory-feasible schedules.
Lemma 2.12.3 (a): for every $k$ -surplus set $F$ there is a minimal $k$ -surplus set $F'$ with $\emptyset\ne F'\cap V_k^+\subseteq F\cap V_k^+$ and $F'\cap V_k^-\supseteq F\cap V_k^-$ .
Lemma 2.12.3 (b): the shortage counterpart.
Theorem 2.12.4 (a) on its own: the upper constraints $r_k(S,t)\le\overline R_k$ hold for all $t\ge 0$ iff condition (a) holds.
Theorem 2.12.4 (b) on its own: the lower constraints hold for all $t\ge 0$ iff condition (b) holds.

Significance

The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation $S_j+p_j\ge S_i$ (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation $S_j\ge S_i+p_i$ . Consequences stated in the book: the feasible region of $PSc|temp|C_{\max}$ is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.

The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.

Difficulty

The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family $\mathcal F_k^+$ and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at $t$ , so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock $r_{0k}$ is handled by the same active-set rule as any other demand, which matters for the invariance claim.

Formalization scope

Activities are Fin (n + 2), activity $n+1$ is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.
The inventory constraints are required for every $t\ge 0$ . The book prints (2.12.2) for $0\le t\le\bar d$ , but its proof of Theorem 2.12.4 works with an arbitrary $t\ge 0$ (the necessity half uses the last completion time of a replenishing activity, which need not be at most $\bar d$ ). The two readings coincide for schedules with $S_{n+1}\le\bar d$ whose activities all finish by $S_{n+1}$ .
A schedule satisfies $S_0=0$ and $S_i\ge 0$ and is not required to be time-feasible; time lags play no role in this section's results and are not part of the model.
(2.12.1) and Remark 2.12.2 are explicit hypotheses (TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.
A formalization in which $\mathcal F_k^+$ is empty or trivial (for instance, minimality with non-strict inclusions, which no set satisfies) makes condition (a) vacuous; the definitions here follow p. 131 exactly, and a concrete instance with a nonempty $\mathcal F_k^+$ has been checked locally.

Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of $PSc|temp|C_{\max}$ (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.12.1, pp. 128–135. https://doi.org/10.1007/978-3-540-24800-2
K. Neumann, C. Schwindt, Project scheduling with inventory constraints, Mathematical Methods of Operations Research 56 (2003) 513–533 (cited in the book as 2002). https://doi.org/10.1007/s001860200251

7 thms2 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IV: Every Feasible Schedule Obeys a Minimal Delaying Mode of Each Forbidden SetTextbook

Motivation

Resource-constrained project scheduling with general temporal constraints, written $PS|temp|C_{\max}$ , asks for start times of the activities of a project that respect minimum and maximum time lags between activities and the capacities of renewable resources (staff, machines, reactors), and that minimize the project duration. Deciding whether a feasible schedule exists at all is already NP-complete (Bartusch, Möhring and Radermacher, 1988), so exact methods are branch-and-bound procedures. The dominant family, going back to De Reyck and Herroelen (1998) and presented in Chapter 2 of Neumann, Schwindt and Zimmermann's monograph, branches on resource conflicts: whenever the currently computed schedule overloads a resource at some time $t$ , the set of activities in progress at $t$ is a forbidden set, and the node is split into children, each of which adds precedence constraints that resolve the conflict.

Such a scheme is only correct if the children together retain every feasible schedule. Theorem 2.5.7 of the book is exactly this completeness guarantee, and it is the reason the enumeration can be restricted to the small family of minimal delaying modes instead of arbitrary ways of breaking up a conflict. The same section also contains the preprocessing results (§2.5.2) that exploit two-element forbidden sets before any branching happens. This mission formalizes both.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion, both of duration $0$ , and every real activity $i\in\{1,\dots,n\}$ has an integer duration $p_i>0$ . The project network $N$ has arc set $E$ and integer arc weights $\delta_{ij}$ ; the arc $\langle i,j\rangle$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ . A finite set $\mathcal R$ of renewable resources is given; resource $k$ has capacity $R_k\in\mathbb N$ and activity $i$ uses $r_{ik}\in\mathbb Z_{\ge0}$ units of it, with $r_{ik}\le R_k$ and $r_{0k}=r_{n+1,k}=0$ .

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge0$ . The active set at time $t$ is $\mathcal A(S,t)=\{i\in V\mid S_i\le t<S_i+p_i\}$ . The schedule is time-feasible if it satisfies all temporal constraints, resource-feasible if

\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k\qquad(k\in\mathcal R,\ t\ge0),

and feasible if it is both; $\mathcal S$ denotes the set of feasible schedules.

A set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ , a feasible set otherwise, and minimal forbidden if no proper subset is forbidden. For a forbidden $F$ , a set $B\subseteq F$ is a delaying alternative if $F\setminus B$ is feasible, and a minimal delaying alternative if no proper subset of $B$ is one. A minimal delaying mode for $F$ is a pair $(i,B)$ with $B$ a minimal delaying alternative for $F$ and $i\in F\setminus B$ .

For §2.5.2, fix an integer upper bound $UB$ on the project duration. The temporal scheduling network $N^+$ adds to $N$ the arc $\langle n+1,0\rangle$ with weight $\delta_{n+1,0}=-UB$ , and $d_{ij}$ is the longest path length from $i$ to $j$ in $N^+$ ( $-\infty$ if there is no path, $d_{ii}=0$ ).

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

For every forbidden set $F$ and every feasible schedule $S\in\mathcal S$ there is a minimal delaying mode $(i,B)$ for $F$ with

S_j\ge S_i+p_i\qquad(j\in B).

$F$ is arbitrary (not necessarily minimal); $B$ must be a minimal delaying alternative and $i$ must lie outside $B$ .

Milestones

Eqs. (2.5.2)–(2.5.3), p. 46. $B$ is a minimal delaying alternative for a forbidden $F$ iff $F\setminus B$ is a maximal feasible subset of $F$ , iff $B\subseteq F$ ,

\sum_{i\in F\setminus B}r_{ik}\le R_k\ (k\in\mathcal R)\quad\text{and}\quad\forall j\in B\ \exists k:\ \sum_{i\in F\setminus B}r_{ik}+r_{jk}>R_k.

Bartusch et al.'s criterion (proof of Theorem 2.3.10, p. 35). A schedule is resource-feasible iff every minimal forbidden set $F$ contains distinct $i,j$ with $S_j\ge S_i+p_i$ .
Lemma 2.5.5, p. 49. A minimal delaying alternative for $F$ is an inclusion-minimal set meeting every minimal forbidden $F'\subseteq F$ .
Theorem 2.5.11, p. 55. If $\{i,j\}$ is a two-element forbidden set with $d_{ij}<p_i$ and $d_{ij}>-p_j$ , then every feasible $S$ with $S_{n+1}\le UB$ satisfies $S_j\ge S_i+p_i$ .
Eq. (2.5.7), p. 55. If for a two-element forbidden set $\{i,j\}$ neither $d_{ij}>-p_j$ nor $d_{ji}>-p_i$ holds, then for all $h,l\in V$ and every feasible $S$ with $S_{n+1}\le UB$ ,

S_l\ge S_h+\min\bigl(d_{hi}+p_i+d_{jl},\ d_{hj}+p_j+d_{il}\bigr).

Significance

The result. Theorem 2.5.7 is the completeness statement of the De Reyck–Herroelen enumeration scheme (Algorithm 2.5.8): if every child of a conflict node imposes the precedence constraints $i\to j$ ( $j\in B$ ) of one minimal delaying mode $(i,B)$ , the children's order polyhedra together contain all feasible schedules of the parent. Proposition 2.5.9(a), the correctness of the whole branch-and-bound procedure, rests on it. Because the objective does not enter, the book reuses the theorem for the regular and nonregular objectives of Chapter 3. Theorem 2.5.11 and inequality (2.5.7) are the preprocessing rules that shrink the time-feasible region before enumeration: each adds temporal constraints that every feasible schedule within the bound already satisfies, which raises the lower bound $ES_{n+1}$ and prunes the enumeration.

Formalizing it. All statements are proved in the book (Bartusch et al.'s criterion is quoted from their 1988 paper with the necessity argument sketched). None of them has a machine-checked proof; the Prove2Me catalog contains precedence-only scheduling models (Brucker–Knust) and acyclic event networks (Kelley–Walker) but no model with time windows and forbidden sets. The mission produces a reusable library of forbidden sets, delaying alternatives and longest-path distances in networks with maximum time lags.

Difficulty

The obvious idea — pick any two overlapping activities and delay one — does not give a minimal delaying alternative with a single delaying activity $i$ common to all of $B$ . The proof has to pass from the pairwise separations that resource-feasibility guarantees in each minimal forbidden subset to a set $B$ that is simultaneously minimal as a delaying alternative and ordered behind one activity outside $B$ . This needs the correspondence between delaying alternatives and hitting sets of the minimal forbidden subsets (Lemma 2.5.5) and the positivity of real durations to keep $i$ outside $B$ . For the preprocessing results, the delicate part is relating longest paths in $N^+$ , including the backward arc carrying $-UB$ , to the start-time differences of every feasible schedule within the bound.

Formalization scope

Activities are Fin (n + 2), with $n+1$ as Fin.last (n + 1). Start times are real; durations, capacities, requirements and time lags are integers (natural numbers where the book says so). The standing assumptions of the book (at least one real activity, zero-duration dummies, positive durations of real activities, no loops, $r_{0k}=r_{n+1,k}=0$ , $r_{ik}\le R_k$ , and paths in $N$ from $0$ to every node and from every node to $n+1$ ) are one hypothesis P.StandingAssumptions of every theorem.

Resource constraints are imposed for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.1.4) literally writes. The book's proofs and Remark 2.3.11 use the $t\ge0$ reading; with the literal cut-off, schedules running past $\bar d$ could violate capacities after $\bar d$ , and Bartusch et al.'s criterion would fail.

Longest path lengths are maxima over simple paths, with values in WithBot ℝ (⊥ for $-\infty$ ). If $N^+$ has a cycle of positive length, no schedule satisfies the temporal constraints with $S_{n+1}\le UB$ , and the statements using $d_{ij}$ are vacuous, as in the book. The arc $\langle n+1,0\rangle$ of $N^+$ has weight $-UB$ , or $\max(\delta_{n+1,0},-UB)$ if $N$ already has such an arc. $UB$ is an integer.

The goal is not trivial: it quantifies over minimal delaying modes only. A variant without the minimality of $B$ , or allowing $i\in B$ , would be nearly empty (take $B=F\setminus\{i\}$ ), and the statement here rules both out. Maximality in milestone 1 is taken among subsets of $F$ .

Welcome contributions: the hitting-set correspondence between delaying alternatives and minimal forbidden subsets, the telescoping bound $S_j-S_i\ge d_{ij}$ for feasible schedules, and proofs of any milestone. The definitions restate the setup of the series' earlier missions (II: order polyhedra) locally, because those are still drafts.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.5. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988) 201–240. https://doi.org/10.1007/BF02283745
B. De Reyck, W. Herroelen, A branch-and-bound procedure for the resource-constrained project scheduling problem with generalized precedence relations, European Journal of Operational Research 111 (1998) 152–174. https://doi.org/10.1016/S0377-2217(97)00305-6

8 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming XI: The KKT Conditions and the Unique Smallest Enclosing BallTextbook

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$ , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$ . A convex program in equational form is

\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$ , $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$ . For differentiable $f$ , $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$ , write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$ th column is $p_j$ . The program studied is

\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$ . The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$ , $S\subseteq B(c,r)$ , every ball containing $S$ has radius at least $r$ , and every ball containing $S$ of radius at most $r$ has center $c$ .

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$ , the objective $f$ of (8.15) is convex, and

(8.15) has an optimal solution $x^*$ ;
there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$ , and for every optimal $x^*$

-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .

Milestones

Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$ : $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$ .
Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.

Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$ , then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$ .

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$ ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$ . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$ , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$ , and $\nabla f(x^*)_j$ its value on the $j$ th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$ . "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$ , as "minimizes $f$ over $C$ " presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$ .
Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$ , $Ax=b$ , $x\ge0$ ) / (minimize $b^Ty$ , $A^Ty\ge c$ ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

6 thms2 active usersReviewed

Linear Optimization Optimization Theoretical Computer Science·Captain: mikedeng1

Understanding and Using Linear Programming III: The Simplex Method with Bland's Rule Never CyclesTextbook

Motivation

The simplex method, introduced by G. B. Dantzig in 1947, is the standard algorithm for linear programming and remains the core of commercial solvers. It moves from one basic feasible solution to another by pivot steps, and at each step a pivot rule chooses which variable enters and which leaves the basis. For several natural rules, including Dantzig's original largest-coefficient rule, the method can cycle: on a degenerate linear program it can return to a basis it has already visited and repeat forever without improving the objective. Hoffman (1953) and Beale (1955) gave cycling examples.

R. G. Bland (New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2), 1977) showed that a simple combinatorial rule, choosing the smallest eligible index for both the entering and the leaving variable, never cycles. This makes the simplex method a finite algorithm on every linear program in equational form, and it gives an algorithmic proof of the duality theorem. Chapter 5 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), develops the general theory of simplex tableaus and proves Bland's theorem as Theorem 5.8.1. This mission is the third of a series formalizing that book.

Setting

A linear program in equational form is

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

with $A$ a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ . Following §4.2 of the book, $A$ has $n\ge m$ columns and rank $m$ . For an $m$ -element set $B=\{k_1<\dots<k_m\}\subseteq\{1,\dots,n\}$ let $N=\{\ell_1<\dots<\ell_{n-m}\}$ be its complement, and $A_B$ , $A_N$ the matrices of the columns of $A$ indexed by $B$ and $N$ . $B$ is a feasible basis if $A_B$ is nonsingular and $A_B^{-1}b\ge0$ ; its basic feasible solution is the unique $x$ with $Ax=b$ and $x_j=0$ for $j\notin B$ .

A simplex tableau $T(B)$ is a system

x_B=p+Q\,x_N,\qquad z=z_0+r^{T}x_N

in the variables $x_1,\dots,x_n,z$ with the same solutions as $Ax=b$ , $z=c^Tx$ . A nonbasic variable $x_v$ , $v=\ell_\beta$ , may enter if $r_\beta>0$ ; a basic variable $x_u$ , $u=k_\alpha$ , may then leave if

q_{\alpha\beta}<0\quad\text{and}\quad-\frac{p_\alpha}{q_{\alpha\beta}}=\min\Bigl\{-\frac{p_i}{q_{i\beta}}: q_{i\beta}<0\Bigr\}.\tag{5.3}

The pivot step replaces $B$ by $B'=(B\setminus\{u\})\cup\{v\}$ . Bland's rule takes the entering variable of smallest index among those with $r_\beta>0$ , and the leaving variable of smallest index among those satisfying (5.3).

Formalization targets

Goal: Theorem 5.8.1 (p. 73)

There is no infinite sequence of bases

B_0\to B_1\to B_2\to\cdots

in which each $B_{t+1}$ is obtained from the feasible basis $B_t$ by a pivot step obeying Bland's rule. Since there are finitely many bases and a Bland step is determined by its starting basis, this is the book's "always finite; i.e., cycling is impossible".

Milestones

Lemma 5.5.1 (p. 66): a feasible basis has exactly one simplex tableau, with $Q=-A_B^{-1}A_N$ , $p=A_B^{-1}b$ , $z_0=c_B^TA_B^{-1}b$ , $r=c_N-(c_B^TA_B^{-1}A_N)^T$ .
Optimality criterion (§5.6, p. 67): if $r\le0$ , the basic feasible solution of $B$ is optimal.
Lemma 5.6.1 (p. 68): a pivot step leads to a feasible basis; if no leaving variable exists, the program is unbounded along an explicit ray.
Claim in the proof of Theorem 5.8.1 (p. 73): for any pivot rule, all bases of a cycle have the same basic feasible solution, and every variable that enters during the cycle is $0$ in it.

Significance

With the optimality criterion and Lemma 5.6.1, Theorem 5.8.1 turns the simplex method into an algorithm: started from any feasible basis, it stops after finitely many pivot steps at an optimal basic feasible solution or with a ray certifying unboundedness. Combined with the auxiliary program of §5.6 for finding a first feasible basis, this yields a constructive proof that every feasible, bounded linear program has an optimal basic feasible solution, and the book remarks that the duality theorem follows easily. Bland's rule is also the model for later combinatorial anticycling rules in oriented matroid programming.

The theorem is classical and fully proved in the book. What the mission adds is a machine-checked version stated in the book's own tableau notation. On Prove2Me the simplex method is formalized in the Bertsimas–Tsitsiklis series (Introduction to Linear Optimization IV), for minimization with reduced costs, with termination proved under nondegeneracy and for the lexicographic rule; Bland's rule is not formalized there.

Difficulty

The obvious termination argument is that the objective value strictly increases at each step, so no basis repeats. That argument fails exactly at degenerate pivot steps, where the minimum in (5.3) is $0$ : the basis changes, the basic feasible solution and the objective value do not. Along a degenerate stretch the objective gives no progress measure, and for general pivot rules the method does cycle there. Any proof must therefore use the specific tie-breaking of Bland's rule, which is a statement about indices, not about values, and relate the tableaus of two different bases in the cycle to each other. Counting bases or tracking the objective value alone does not suffice.

Formalization scope

Vectors are Fin n → ℝ and the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Bases are Finset (Fin n); the sorted enumerations $k_1<\dots<k_m$ and $\ell_1<\dots<\ell_{n-m}$ are Finset.orderEmbOfFin, tableau rows are indexed by Fin m and nonbasic columns by Fin (n - m). Nonsingularity of $A_B$ is IsUnit A_B.det, so the Mathlib inverse is the true inverse wherever it appears. The tableau parameters used by the pivot rules are the explicit formulas of Lemma 5.5.1; the tableau itself is also defined as in the book (same solution set) so that Lemma 5.5.1 is a genuine statement. "Smallest index" compares variable indices, not row positions. Optimality and unboundedness are stated against feasible points, not through a supremum. Every theorem assumes $n\ge m$ and $\operatorname{rank}A=m$ , the standing assumption of §4.2.

A formalization in which any improving variable may enter proves a different, false statement, since cycling examples exist for such rules; the step relation here fixes both choices by Bland's rule. The step relation is not empty: it holds whenever the current tableau has a positive last-row coefficient and a negative entry in the entering column, so the goal is not vacuous.

The development needs basic linear algebra over Matrix, the uniqueness of basic feasible solutions, and bookkeeping for sorted index enumerations. Lemma 5.5.1 and Lemma 5.6.1 are reusable for any later formalization of the simplex method in this notation. Contributions are welcome for each milestone, for the cycle-form corollary, and for a sorry-free proof of the goal.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 5. https://doi.org/10.1007/978-3-540-30717-4
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
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.3800020407
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 3.

7 thms2 active usersReviewed

Completed

Markov Chain Numerical Analysis Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory X: Uniformization of Continuous-Time Markov ChainsTextbook

Motivation

Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations $p'(t)=p(t)Q$ for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).

Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).

Setting

A continuous-time Markov chain $X(t)$ on the states $\{0,1,\dots,N\}$ is described by its infinitesimal generator $Q=(q_{ij})$ : for $i\ne j$ , $q_{ij}\ge0$ is the rate of jumps from $i$ to $j$ , and the diagonal entry is $-q_i$ with

q_i=\sum_{j\ne i}q_{ij},\qquad i=0,1,\dots,N.

The transient state-probability vector $p(t)=(p_0(t),\dots,p_N(t))$ , $p_n(t)=\Pr\{X(t)=n\}$ , is the solution of the forward equations

p'(t)=p(t)Q\quad(t\ge0),

started from a given probability vector $p(0)$ . Fix a constant $\Lambda>0$ with $\Lambda\ge q_i$ for every $i$ (the book takes $\Lambda=\max_i q_i$ ) and define the uniformized matrix

\tilde P=\frac{Q}{\Lambda}+I,\qquad \tilde p_{in}=\begin{cases}q_{in}/\Lambda&(i\ne n),\\1-q_i/\Lambda&(i=n).\end{cases}

It is the transition matrix of a discrete-time chain $Y_k$ : the state of $X$ after the $k$ -th event of a Poisson process of rate $\Lambda$ that has been thinned. Write $\phi^{(k)}=p(0)\tilde P^{k}$ for its distribution after $k$ steps.

For the second half of the chapter, the Laplace transform of a real function $f$ on $[0,\infty)$ is $\bar f(s)=\int_0^\infty e^{-st}f(t)\,dt$ , and the Fourier-series approximant with parameter $A$ is

f_{A,n}(t)=\frac{e^{A/2}}{2t}\Big[\bar f\Big(\frac{A}{2t}\Big)+2\sum_{k=1}^{n}(-1)^k\,\mathrm{Re}\,\bar f\Big(\frac{A+2k\pi i}{2t}\Big)\Big],

with $f_A(t)=\lim_{n\to\infty}f_{A,n}(t)$ .

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

The forward equations have a solution, and every solution satisfies, for all $t\ge0$ ,

p(t)=\sum_{k=0}^{\infty}p(0)\tilde P^{(k)}\,\frac{e^{-\Lambda t}(\Lambda t)^k}{k!},

and whenever $\sum_{k=0}^{T}e^{-\Lambda t}(\Lambda t)^k/k!>1-\epsilon$ , every component of the sum truncated at $k=T$ is within $\epsilon$ of $p_n(t)$ .

Milestones

Eq. (8.12): $\tilde P$ has the entries above and is a stochastic matrix.
Eqs. (8.13)–(8.14): $\phi^{(k)}=\phi^{(k-1)}\tilde P$ and each $\phi^{(k)}$ is a probability vector.
p.385: $\phi=\phi\tilde P\iff0=\phi Q$ .
Eqs. (8.27)–(8.28): for bounded Lipschitz $f$ , $A>0$ and $t>0$ ,

f_A(t)-f(t)=\sum_{k=1}^{\infty}e^{-kA}f\big((2k+1)t\big),\qquad |f_A(t)-f(t)|\le\frac{Ce^{-A}}{1-e^{-A}}\ \text{ if } |f(x)|\le C \text{ for } x>3t.

The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy $p_{in}(t)=\sum_k\tilde p^{(k)}_{in}e^{-\Lambda t}(\Lambda t)^k/k!$ , and $p_n(t)=\sum_i p_i(0)p_{in}(t)$ .

Significance

The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of $Q$ . Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like $e^{-A}$ .

All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.

Difficulty

The book's derivation is probabilistic: it conditions on the number of events of the Poisson( $\Lambda$ ) process and thins them. A formal statement cannot rest on that picture, because $p(t)$ is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on $[0,\infty)$ with one-sided derivative at $0$ , which the book never mentions. The componentwise bound then needs $\tilde P$ to be stochastic, so that every $\phi^{(k)}_n$ lies in $[0,1]$ . That is exactly where $\Lambda\ge\max_i q_i$ is used; with a smaller $\Lambda$ the matrix $\tilde P$ has negative diagonal entries and the bound fails.

For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of $f$ at all odd multiples of $t$ . The convergence of the conditionally summed series (8.24) is the delicate point: continuity of $f$ at $t$ , the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from $f$ does not have.

Formalization scope

States are Fin (N+1); a row vector is Fin (N+1) → ℝ; $pQ$ is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal $-\sum_{j\ne i}q_{ij}$ .
$p(t)$ is not defined as the series. It is any function with $p(0)=p_0$ and one-sided derivative $p(t)Q$ within $[0,\infty)$ at every $t\ge0$ . The goal also asserts that such a function exists, so it cannot hold vacuously, and it asserts the series identity for every solution. Defining $p(t)$ as the series (8.9) would make the goal a tautology and is ruled out.
$\Lambda$ is any real with $\Lambda>0$ and $\Lambda\ge q_i$ for all $i$ (the book takes equality with $\max_i q_i$ ).
The truncation bound is stated componentwise, as on p.384 ("an error bound on $p_n(t)$ of $\epsilon$ "), for an arbitrary real $\epsilon$ and truncation point $T$ .
The series (8.8), (8.9) are stated with HasSum, so convergence is part of the claim.
The Laplace transform is the Lebesgue integral over $(0,\infty)$ at a complex argument. $f_A(t)$ is the limit of the partial sums $f_{A,n}(t)$ , and the convergence is part of milestone 4.
Strengthened hypotheses in milestone 4: $f$ bounded and Lipschitz on $[0,\infty)$ replaces " $t$ is a continuity point of $f$ ", which is not sufficient for convergence.
Corrected misprints: $e^{-\lambda t}$ in (8.9) is $e^{-\Lambda t}$ ; $q_{ij}/\Lambda$ in (8.12) is $q_{in}/\Lambda$ ; $\phi(Q/\Lambda-I)$ on p.385 is $\phi(Q/\Lambda+I)$ .
Not formalized: Theorem 8.1 (Bromwich inversion) and the real form (8.21), which the book states without hypotheses on $f$ ; the limit claim $\lim_k\phi^{(k)}=\lim_t p(t)$ on p.385, which fails when $\tilde P$ is periodic; the Euler-summation approximation (8.26) and the round-off discussion, which are stated with "≈".

Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§8.1.2–8.2. https://doi.org/10.1002/9781118625651
A. Jensen, "Markoff chains as an aid in the study of Markoff processes", Skandinavisk Aktuarietidskrift 36 (1953) 87–91.
W. K. Grassmann, "Transient solutions in Markovian queueing systems", Computers & Operations Research 4 (1977) 47–53.
D. Gross, D. R. Miller, "The randomization technique as a modeling tool and solution procedure for transient Markov processes", Operations Research 32 (1984) 343–361. https://doi.org/10.1287/opre.32.2.343
J. Abate, W. Whitt, "The Fourier-series method for inverting transforms of probability distributions", Queueing Systems 10 (1992) 5–87. https://doi.org/10.1007/BF01158520
J. Abate, G. L. Choudhury, W. Whitt, "An introduction to numerical transform inversion and its application to probability models", in W. Grassmann (ed.), Computational Probability, Kluwer, 1999, 257–323.

8 thms2 active usersReviewed

Probability Statistics Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory VIII: Lindley's Integral Equation for the G/G/1 QueueTextbook

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$ , the service times $S^{(n)}$ are independent with common distribution $B$ , and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$ . The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$ , and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$ .

The line delay $W_q^{(n)}$ of the $n$ th customer satisfies Lindley's recursion

W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$ , one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$ . A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$ .

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$ , then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

(6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$ .
The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$ .
(6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$ , and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$ , one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$ , exactly $k$ distinct roots in the open unit disk.
(6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$ .
(6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$ , $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$ . The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$ , the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$ . Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ( $\rho<1$ ) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$ . $A$ and $B$ are probability measures with no mass on $(-\infty,0)$ , with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$ . Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$ , and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$ . Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

(6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$ .
(6.9) as an integral against the law of $T+x$ .
$U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$ . The division is stated only where $A^*(-s)B^*(s)\ne1$ .
(6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$ , and (6.20) for $c\ge2$ . The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$ , and exhausting the roots in the closed disk.
(6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$ .

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$ " would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$ , and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273

12 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$ , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$ , and the iterates $x^s$ are required to follow the time path of the optimal solutions,

\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$ , nor of $f^0$ . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ .

The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$ , the unique nearest point of $X$ to $y$ .
A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$ . The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$ .
The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots

with step sizes $\rho_s \ge 0$ .

For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$ ) and a sequence $(x^s)$ , the exit time from the $\varepsilon$ -ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ .
The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$ , the squared distance to $X^*$ .

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$ , $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$ , $\|g_s\| \le C$ , $\rho_s \ge 0$ , $\rho_s \to 0$ and $\sum_s \rho_s = \infty$ . Then the iterates of (6.41) satisfy

F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$ , with $x^*(s)$ a point of $X^*$ nearest to $x^s$ .
p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$ .
p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$ .
Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$ , the sequence leaves every small ball around a subsequential limit outside $X^*$ , and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$ , then $V(x^s)$ converges and all accumulation points lie in $X^*$ .
pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$ :

\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$ . Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$ , not on $f^0$ , so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$ , and only while the iterate stays away from $X^*$ ; near $X^*$ , $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$ , and $F^0(\cdot, s)$ , $f^0$ are convex and continuous on all of $\mathbb R^n$ .
projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$ ; $V$ is Metric.infDist · X* ^ 2.
Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$ , and that is the constant in milestone 2. All other results are qualitative.
Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as " $\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$ ", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$ " is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$ ", and condition (3) is imposed for the same $\varepsilon$ . (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$ ); the right limit is $V(x')$ . (iii) The display on p. 155 prints " $=$ " where the projection gives " $\le$ ". (iv) The proof on p. 155 prints " $x^{s_k} \to x' \in X^*$ " where $x' \notin X^*$ is meant.
Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

8 thms2 active usersReviewed

Combinatorics Graph Theory Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources II: A Time-Feasible Strict Order Is Feasible iff It Breaks Up Every Minimal Forbidden SetTextbook

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem $PS|temp|C_{\max}$ in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints " $j$ starts after $i$ has finished".

This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.

Setting

A project has activities $V = \{0, 1, \dots, n+1\}$ , where $0$ and $n+1$ are fictitious activities marking the project's start and completion and $1, \dots, n$ are the real activities ( $n \ge 1$ ). Activity $i$ has duration $p_i \in \mathbb Z_{\ge 0}$ , with $p_0 = p_{n+1} = 0$ and $p_i > 0$ for real activities. Time lags are encoded in the project network $N$ : an arc $\langle i, j\rangle \in E$ with integer weight $\delta_{ij}$ imposes $S_j - S_i \ge \delta_{ij}$ . The book's standing assumptions give, for every node $i$ , a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ .

A schedule is a vector $S \in \mathbb R^{n+2}$ with $S_0 = 0$ and $S_i \ge 0$ . It is time-feasible if $S_j - S_i \ge \delta_{ij}$ for all arcs. The set of time-feasible schedules is $\mathcal S_T$ .

Each renewable resource $k \in \mathcal R$ has a capacity $R_k$ , and activity $i$ uses $r_{ik} \le R_k$ units of it while in progress, with $r_{0k} = r_{n+1,k} = 0$ . The active set at time $t$ is $\mathcal A(S,t) = \{ i \mid S_i \le t < S_i + p_i\}$ , and $S$ is resource-feasible if $\sum_{i \in \mathcal A(S,t)} r_{ik} \le R_k$ for all $k$ and all $t \ge 0$ . The feasible region $\mathcal S$ consists of the schedules that are both time-feasible and resource-feasible.

A strict order $O \subseteq V \times V$ is an asymmetric, transitive relation. Its order polyhedron is

\mathcal S_T(O) = \{ S \in \mathcal S_T \mid S_j \ge S_i + p_i \ \text{for all } (i,j) \in O\}.

$O$ is time-feasible if $\mathcal S_T(O) \ne \emptyset$ , and feasible if moreover $\mathcal S_T(O) \subseteq \mathcal S$ . The order network $N(O)$ adds to $N$ , for each $(i,j) \in O$ , an arc $\langle i,j\rangle$ of weight $p_i$ , or raises the weight of an existing arc to $\max(\delta_{ij}, p_i)$ . A schedule $S$ induces the strict order $O(S) = \{(i,j) \mid i \ne j,\ S_j \ge S_i + p_i\}$ .

A set $F \subseteq V$ is forbidden if $\sum_{i \in F} r_{ik} > R_k$ for some resource $k$ . It is a minimal forbidden set if no proper subset of it is forbidden. $\mathcal F$ denotes the set of minimal forbidden sets.

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

For every time-feasible strict order $O$ ,

O \text{ feasible} \iff \forall F \in \mathcal F\ \exists\, i, j \in F:\ N(O) \text{ has a path from } i \text{ to } j \text{ of length} \ge p_i .

Milestones

Proposition 2.3.3. A strict order $O$ is time-feasible if and only if $N(O)$ has no cycle of positive length.
Bartusch et al.'s criterion (quoted in the proof of Theorem 2.3.10). A schedule $S$ is resource-feasible if and only if every $F \in \mathcal F$ contains distinct $i, j$ with $S_j \ge S_i + p_i$ .
Proposition 2.3.6. For time-feasible $S$ , the strict order $O(S)$ is feasible if and only if $S \in \mathcal S$ .
Theorem 2.3.7. $\mathcal S = \bigcup_{O \in \mathcal O} \mathcal S_T(O)$ , where $\mathcal O$ is the finite set of inclusion-minimal feasible strict orders.
Remark 2.3.11. A time-feasible schedule partitions $F$ if and only if every $\mathcal A(S,t) \cap F$ , $t \ge 0$ , is feasible. A time-feasible order is feasible if and only if it breaks up all (equivalently, all minimal) forbidden sets. A time-feasible schedule is feasible if and only if it partitions all forbidden sets.

Significance

Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times $t$ , into a finite check: one longest-path computation in $N(O)$ for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that $\mathcal S$ is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.

All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.

Difficulty

The sufficiency half of the goal is short once the criterion is available: a path of length $\ge p_i$ in $N(O)$ forces $S_j \ge S_i + p_i$ on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set $F$ no path in $N(O)$ between elements of $F$ reaches the required length, one must construct a schedule in $\mathcal S_T(O)$ in which all activities of $F$ are simultaneously in progress. This means adding the reverse constraints $S_j - S_i < p_i$ for all $i, j \in F$ to the temporal system without creating a cycle of positive length, while keeping $S_0 = 0$ and $S \ge 0$ . The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside $F$ . The standing assumption that every node is reachable from $0$ by a path of nonnegative length is needed here: without it the equivalence is false.

Formalization scope

The activity set is Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.
Strict orders are finite sets of pairs, Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.
Resource constraints hold for every $t \ge 0$ . The book's (2.1.4) writes $0 \le t \le \bar d$ . In Chapter 2 schedules are not bounded by $\bar d$ , and the book's proofs and Remark 2.3.11 use all $t \ge 0$ . This is a convention of the whole series, not a strengthening.
A path is a walk (nodes may repeat) and its length is the sum of its arc weights. A cycle of positive length is a closed walk with at least one arc and positive length. For a time-feasible order, $N(O)$ has no cycle of positive length. In that case "some path of length $\ge p_i$ " coincides with the book's "longest path length $\ge p_i$ ", so no supremum over paths appears.
The standing assumptions of the book form a single predicate Project.StandingAssumptions, which is a hypothesis of every theorem: $n \ge 1$ ; $p_0 = p_{n+1} = 0$ and $p_i > 0$ otherwise; no loops; $r_{0k} = r_{n+1,k} = 0$ and $r_{ik} \le R_k$ ; and the two path conditions of p. 8.
Minimal forbidden sets and inclusion-minimal feasible orders use Mathlib's Minimal, taken among forbidden sets and among feasible strict orders respectively.
The goal is an equivalence, and both directions are required. Weakening it to sufficiency, or dropping the time-feasibility of $O$ or the minimality of $F$ , would change the theorem. Keeping the book's cut-off $t \le \bar d$ would also change it, because a schedule could then have an unresolved conflict after $\bar d$ and still be called feasible.
Theorem 1.3.3 of Chapter 1 (a time-feasible schedule exists if and only if the network has no cycle of positive length) is needed for Proposition 2.3.3 and is restated here for $N(O)$ . Chapter 1's mission is drafted separately.
Useful infrastructure beyond this mission: longest-path potentials on integer-weighted digraphs without positive cycles (feasibility of difference constraints), and the walk and cycle API on Network. Contributions of this general lemma layer are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745

9 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming X: Pairwise Intersecting d-Intervals Have a Transversal of Size 2d²Textbook

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$ -problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$ . A $d$ -interval is a union of $d$ closed intervals on the real line,

J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .

The numbers $a_k$ and $b_k$ are the endpoints of $J$ . A finite family $\mathcal J$ of $d$ -intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$ . A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$ .

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$ : a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .

Formalization targets

Goal: Theorem 8.6.1

\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .

This is the book's theorem with its constant $2d^2$ .

Milestones

Lemma 8.6.2. If $J_1,\dots,J_n$ ( $n \ge 1$ , repetitions allowed) are $d$ -intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$ , then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$ .
§8.6, p. 182. For every finite set system with nonempty members,

\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).

Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$ -intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$ , $p \in P$ , with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$ .

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$ -intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$ -intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$ -intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$ -interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$ . Components are indexed $0,\dots,d-1$ . Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$ .

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$ , not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

6 thms2 active usersReviewed

Completed

Linear Optimization Optimization Random Matrix Theory·Captain: mikedeng1

Understanding and Using Linear Programming IX: Basis Pursuit Recovers Sparse Solutions Exactly iff the Kernel Misses the CrosspolytopeTextbook

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$ , and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$ , and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$ -norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$ -sparse vectors with probability exponentially close to 1 (FOCS 2005).
2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$ , $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$ . The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$ . For an integer $r\ge 0$ , a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$ . The $\ell_1$ -norm is $\|x\|_1=|x_1|+\dots+|x_n|$ .

Basis pursuit is the optimization problem

\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,

which is equivalent to the linear program

\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$ : whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$ , the kernel of $A$ is $L=\{x: Ax=0\}$ , and $L+z=\{\ell+z:\ell\in L\}$ . For $z$ with $\|z\|_1=1$ , the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$ , and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$ .

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$ :

A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
The remark after it (p. 169): under $m<n$ , that column condition forces $m\ge 2r$ .
Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$ ; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
From the proof of Lemma 8.5.4 (p. 173): if $Az=b$ , the solution set of $Ax=b$ is exactly $L+z$ .
From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$ , $L$ is good for $z$ iff $L\cap C_z=\{0\}$ .

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$ , $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$ -sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$ , the case $\tilde x=0$ , and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$ -dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$ .

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$ ) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$ -norm is written out as $\sum_i|x_i|$ , since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$ .

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$ , and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$ , and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1

7 thms2 active usersReviewed

Completed

Combinatorics Information Theory Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming VIII: The Delsarte Linear Programming Bound for Binary CodesTextbook

Motivation

A binary error-correcting code is a set of $n$ -bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
1973: Delsarte proves the linear programming bound using association schemes.
1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$ .
2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$ , and a code is any set $C \subseteq \{0,1\}^n$ . The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$ . The weight $|\mathbf w|$ is the number of ones in $\mathbf w$ . The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$ , the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$ .

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$ .

For $0 \le i,t \le n$ the Krawtchouk numbers are

K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.

The distance distribution of a code $C$ is

\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.

The Delsarte linear program has variables $x_0,\dots,x_n$ . It maximizes $x_0+\dots+x_n$ subject to:

$x_0 = 1$ ;
$x_i = 0$ for $1 \le i \le d-1$ ;
$\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$ ;
$x \ge 0$ .

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$ .

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

Lemma 8.4.5. For every $I$ and $C$ , the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$ .
Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$ .
Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$ .
§8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$ . For a nonempty code with distance $d$ , the vector $\tilde x(C)$ is feasible for the program.
Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$ .
Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$ , while the sphere-packing bound gives $7281$ . Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$ , no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$ .

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$ , and $\tilde x_i = 0$ for $i < d$ . The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$ , and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$ , has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
The maximum $A(n,d)$ . $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$ . This family contains the empty code, so the maximum is attained.
Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$ .
LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$ , so they are vacuous for $d \le 1$ .
The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$ . Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$ .
Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$ .

No trivialization. The goal is not stated as " $A(n,d) \le \sup$ " with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$ ;
counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$ .

These are reusable for other LP and SDP bounds in coding theory.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

10 thms2 active usersReviewed

Combinatorics Linear Optimization Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming VII: LP Rounding Schedules Unrelated Machines Within Twice the Optimal MakespanTextbook

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$ . The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$ . This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$ ; $d_{ij} > 0$ is the running time of job $j$ on machine $i$ . A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$ , the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$ , the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}

Its optimal value is $t^*(T)$ , with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$ ; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$ , $1$ in the row of job $j$ , and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$ .

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .

Milestones

Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$ .
Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$ .
Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ .
Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$ .

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ , and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$ : the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$ . The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$ . The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$ , which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$ . The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$ , as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$ . This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$ " is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$ ). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Optimization·Captain: mikedeng1

Understanding and Using Linear Programming VI: The Minimax Theorem for Zero-Sum GamesTextbook

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$ . A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$ th and Bob his $j$ th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$ , $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$ . When the players randomize independently, Alice's expected payoff is

\mathbf x^T M \mathbf y = \sum_{i,j} m_{ij} x_i y_j .

The worst-case payoffs are

\beta(\mathbf x) = \min_{\mathbf y} \mathbf x^T M \mathbf y, \qquad \alpha(\mathbf y) = \max_{\mathbf x} \mathbf x^T M \mathbf y,

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$ ; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$ ; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$ ; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$ , $\sum_j y_j = 1$ , $\mathbf y \ge \mathbf 0$ .

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$ : worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$ , the value of the game, with

\beta(\tilde{\mathbf x}) = \tilde{\mathbf x}^T M \tilde{\mathbf y} = \alpha(\tilde{\mathbf y}) = v

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

$\beta$ and $\alpha$ are attained minima and maxima (p. 135).
Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$ , hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$ .
Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$ .
Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .
Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
The minimax equality (p. 137):

\max_{\mathbf x}\min_{\mathbf y}\mathbf x^T M \mathbf y = \min_{\mathbf y}\max_{\mathbf x}\mathbf x^T M \mathbf y .

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$ . The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$ . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

12 thms2 active usersReviewed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Understanding and Using Linear Programming V: The Primal–Dual Central Path and the Self-Dual EmbeddingTextbook

Motivation

Interior point methods solve linear programs in a number of iterations polynomial in the input size, and in practice they compete with the simplex method on large instances. Their modern form goes back to Karmarkar's projective algorithm (Karmarkar 1984); the primal–dual path-following variant analysed in textbooks follows a curve, the central path, defined by a perturbed system of optimality conditions. Two facts make the method well defined. First, the central path exists and is unique whenever the primal and dual programs have strictly feasible points. Second, an arbitrary linear program, possibly infeasible or unbounded, can be embedded in an auxiliary program that has an explicit starting point on its own central path and whose suitable optimal solutions either solve the original program or certify that it has no optimum.

Chapter 7, §7.2 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer 2007), presents both facts in elementary form, following Terlaky (2001). This mission formalizes its three numbered lemmas.

Timeline. The homogeneous system bearing their names is due to Goldman and Tucker (1956), in the study of the structure of optimal solution sets; the self-dual embedding for interior point methods was introduced by Ye, Todd and Mizuno (1994), and the book's presentation follows the skew-symmetric form in Roos, Terlaky and Vial (2005).

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ . The linear program in equational form (7.2) is

\text{maximize } c^{T}x \text{ subject to } Ax=b,\ x\ge 0,

where $A$ has rank $m$ ; its dual (7.5) is: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\in\mathbb{R}^m$ . The notation $x>0$ means that all coordinates of $x$ are strictly positive. For $\mu>0$ the barrier function is $f_\mu(x)=c^{T}x+\mu\sum_{j=1}^n\ln x_j$ , defined for $x>0$ . The central-path system (7.4), in unknowns $x,s\in\mathbb{R}^n$ and $y\in\mathbb{R}^m$ , is

Ax=b,\qquad A^{T}y-s=c,\qquad (s_1x_1,\dots,s_nx_n)=\mu\mathbf 1,\qquad x,s\ge 0 .

For the embedding, the book switches to the inequality form (7.7): maximize $c^{T}x$ subject to $Ax\le b$ , $x\ge 0$ , with dual: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\ge 0$ . The Goldman–Tucker system (GTS) is

Ax-\tau b\le 0,\qquad -A^{T}y+\tau c\le 0,\qquad b^{T}y-c^{T}x\le 0,\qquad x,y\ge 0,\ \tau\ge 0,

and $\rho=\rho(x,y)=c^{T}x-b^{T}y$ is the slack of its last inequality. With $u=(y,x,\tau)\in\mathbb{R}^k$ , $k=n+m+1$ , (GTS) reads $M_0u\le 0$ , $u\ge 0$ for the skew-symmetric matrix

M_0=\begin{pmatrix}0&A&-b\\-A^{T}&0&c\\b^{T}&-c^{T}&0\end{pmatrix}.

Put $r=\mathbf 1+M_0\mathbf 1$ , $M=\begin{pmatrix}M_0&-r\\r^{T}&0\end{pmatrix}$ and $q=(0,\dots,0,k+1)\in\mathbb{R}^{k+1}$ . The self-dual program (SD) in $v=(u,\vartheta)$ is: maximize $-q^{T}v$ subject to $Mv\le q$ , $v\ge 0$ . Its slacks are $z=q-Mv$ , and a feasible $v$ is strictly complementary if $v_j>0$ or $z_j>0$ for every $j=1,\dots,k+1$ .

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

If (7.2) has a feasible $\tilde x>0$ and (7.5) has a feasible $\tilde y$ with $\tilde s=A^{T}\tilde y-c>0$ , then for every $\mu>0$

\exists!\,(x^*,y^*,s^*)\ \text{solving (7.4)},\qquad x^*=\arg\max\{f_\mu(x): Ax=b,\ x>0\}\ \text{(uniquely)}.

Milestones

Claim in the proof of Lemma 7.2.1 (p. 121): under the lemma's assumptions and for fixed $\mu>0$ , the set $Q=\{x: Ax=b,\ x>0,\ f_\mu(x)\ge f_\mu(\tilde x)\}$ is bounded.
Lemma 7.2.2 (p. 126): no solution of (GTS) has $\tau\ne 0$ and $\rho\ne 0$ ; exactly one of "a solution with $\tau>0$ " and "a solution with $\rho>0$ " exists; in the first case $\frac1\tau x$ and $\frac1\tau y$ are optimal for (7.7) and its dual; in the second, (7.7) is infeasible or unbounded.
Lemma 7.2.3 (p. 128): (SD) is feasible and bounded, every optimal solution has $\vartheta=0$ and its $u$ -part solves (GTS), and every strictly complementary optimal solution gives a solution of (GTS) with $\tau>0$ or $\rho>0$ .

Significance

Lemma 7.2.1 is what makes "the central path" a well-defined object: without existence, a path-following method has nothing to follow, and without uniqueness the point $x^*(\mu)$ that the algorithm approximates is not determined. It also identifies the barrier maximizer with the solution of the Lagrange system (7.4), which is the system the Newton steps of the algorithm linearize. Lemmas 7.2.2 and 7.2.3 remove the need for an interior starting point and for knowing in advance that the program has an optimum: every linear program reduces to computing a strictly complementary optimal solution of a program with a known interior point on its central path.

The three lemmas are classical and proved in the book (7.2.2 as a sketch). Formalizing them adds a machine-checked account of the central path in equational form, and of the Goldman–Tucker and self-dual constructions with explicit block matrices, reusable by any later formalization of interior point complexity bounds. As far as a search of the platform shows, no formal statement of the Goldman–Tucker system or of the self-dual embedding exists there; the nearest item, Lemma 9.5 of Introduction to Linear Optimization XII (Bertsimas–Tsitsiklis), characterizes the central path by KKT conditions and is not linked to a formal statement.

Difficulty

For Lemma 7.2.1, uniqueness of a maximizer follows from strict concavity, but existence does not: the feasible region $\{Ax=b,\ x>0\}$ is open relative to its affine hull and typically unbounded, and $f_\mu$ need not attain its supremum on such a set. The interior dual point is what rules out escape to infinity; the primal interior point is what rules out escape to the boundary. Identifying the maximizer with the unique solution of (7.4) further needs the Lagrange multiplier rule on an open set and the full row rank of $A$ to determine $y$ from $s$ .

For Lemma 7.2.2 the exclusivity and the optimality statements are weak-duality arguments, but existence of a solution with $\rho>0$ when (7.7) is infeasible or unbounded requires a Farkas-type alternative for both the primal and the dual, and the case split in the book's sketch ("the dual case is analogous") must be carried out. Lemma 7.2.3 requires bookkeeping with the block structure of $M$ and the skew-symmetry of $M_0$ .

Formalization scope

Vectors are functions Fin n → ℝ and Fin m → ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Matrices are Matrix (Fin m) (Fin n) ℝ, inequalities between vectors are componentwise, $x>0$ is ∀ j, 0 < x j. The rank condition of (7.2) is the hypothesis A.rank = m. Optimal solutions and unboundedness are expressed against every feasible point, never through a real supremum. The vector $u=(y,x,\tau)$ is indexed by Fin m ⊕ Fin n ⊕ Unit and $v=(u,\vartheta)$ by (Fin m ⊕ Fin n ⊕ Unit) ⊕ Unit; $M_0$ , $r$ , $M$ and $q$ are defined entrywise on these index types, with the last entry of $q$ equal to $k+1=n+m+2$ . "Exactly one" in Lemma 7.2.2 is Xor.

Lean's Real.log returns $0$ for nonpositive arguments, so a statement comparing $f_\mu$ over $\{Ax=b\}$ or $\{Ax=b,\ x\ge 0\}$ would be a different, and generally false or trivial, claim; every comparison of barrier values is restricted to points with all coordinates strictly positive. The unique solution of (7.4) is stated as existence plus equality of every solution with it, not as existence of some solution.

Useful infrastructure: strict concavity of sums of logarithms, the Lagrange multiplier rule for affine constraints (Mathlib's IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt or a direct orthogonality argument), compactness of closed bounded sets in Fin n → ℝ, and Farkas' lemma in the forms of Proposition 6.4.1 of the book. Proofs of the milestones, alternative arguments, and general lemmas about skew-symmetric linear programs are all welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4
T. Terlaky, An easy way to teach interior-point methods, European Journal of Operational Research 130(1), 2001, 1–19.
C. Roos, T. Terlaky, J.-P. Vial, Interior Point Methods for Linear Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/b100325
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt{n}L)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 1994, 53–67. https://doi.org/10.1287/moor.19.1.53
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
F. A. Potra, S. J. Wright, Interior-point methods, Journal of Computational and Applied Mathematics 124, 2000, 281–302.

6 thms2 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

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

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$ . An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$ . The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$ .

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$ , $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$ . A basis is an $m$ -element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$ .

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$ : $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$ ,

\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},

\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$ .
Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$ .
The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$ , $c^{T}\tilde x\ge c^{T}x_0$ .
Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$ , solve $A_Bx_B=b$ , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$ , extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$ -element basis, which requires the rank- $m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
$Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
a subset $B$ of indices is a Finset (Fin n); " $A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$ , together with B.card = m;
the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
"optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
"vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
Theorem 4.4.1 carries the extra hypothesis $n\ge 1$ : for $n=0$ there is no nonzero vector in $\mathbb{R}^0$ , the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$ , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

6 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory VII: The Geometric Arrival-Point Law of the G/M/1 QueueTextbook

Motivation

Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).

The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity $\rho$ replaced by a number $r_0$ that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).

Setting

Customers arrive at a single server. The interarrival times are independent with common law $A$ , a probability distribution on $[0,\infty)$ with CDF $A(t)$ and finite mean $E[T] = 1/\lambda$ , $\lambda > 0$ . Service times are independent exponential random variables with rate $\mu > 0$ , and the discipline is first come, first served.

Let $X_n$ be the number of customers in the system just before the $n$ th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so $\{X_n\}$ is a Markov chain on $\{0,1,2,\dots\}$ . Its transition probabilities are built from

b_k = \int_0^\infty \frac{e^{-\mu t}(\mu t)^k}{k!}\,dA(t) \qquad (k \ge 0),

the probability of exactly $k$ completions during one interarrival time (Eq. (5.50)): $p_{i0} = 1 - \sum_{k=0}^{i} b_k$ , $p_{ij} = b_{i+1-j}$ for $1 \le j \le i+1$ , and $p_{ij} = 0$ otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector $q = \{q_n\}$ with $qP = q$ and $qe = 1$ (Eq. (5.52)); $q_n$ is the long-run probability that an arrival finds $n$ customers present.

The characteristic equation of the chain is

z = \beta(z), \qquad \beta(z) = \sum_{n \ge 0} b_n z^n ,

where $\beta$ is the probability generating function of $\{b_n\}$ (Eq. (5.55)). Equivalently $z = A^*[\mu(1-z)]$ (Eq. (5.56)), where $A^*(s) = \int_0^\infty e^{-sx}\,dA(x)$ is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is $\rho = \lambda/\mu$ .

Formalization targets

Goal: Eq. (5.60), the geometric arrival-point law

If $\rho = \lambda/\mu < 1$ , there is a number $r_0$ with $0 < r_0 < 1$ and $r_0 = \beta(r_0)$ , it is the only complex root of $z = \beta(z)$ in the open unit disk, and

q_n = (1 - r_0)\, r_0^{\,n} \qquad (n \ge 0)

is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.

Milestones

Eqs. (5.51)–(5.53): for a probability vector $q$ , $qP = q$ is equivalent to $q_i = \sum_{k\ge0} q_{i+k-1}b_k$ ( $i \ge 1$ ) and $q_0 = \sum_{j\ge0} q_j\bigl(1 - \sum_{k=0}^{j} b_k\bigr)$ .
p.261: $0 < b_0 < 1$ , $b_n > 0$ for all $n$ , $\beta(1) = 1$ , and $\beta'(1) = \sum_n n b_n = \mu/\lambda$ .
Eq. (5.56): $\beta(z) = A^*[\mu(1-z)]$ for $|z| \le 1$ .
Eq. (5.58), Figure 5.2: $z = \beta(z)$ has at most one root in $(0,1)$ , and one exists if and only if $\lambda/\mu < 1$ .
p.262: when $\lambda/\mu < 1$ , $z = \beta(z)$ has exactly one root with $|z| < 1$ .
Eq. (5.59): successive substitution $z^{(k+1)} = \beta(z^{(k)})$ from any $0 < z^{(0)} < 1$ converges to $r_0$ .
Eq. (5.61): $L^{(A)} = r_0/(1-r_0)$ and $L_q^{(A)} = r_0^2/(1-r_0)$ .
Eq. (5.62): $W_q(t) = 1 - r_0 e^{-\mu(1-r_0)t}$ and $W(t) = 1 - e^{-\mu(1-r_0)t}$ for $t \ge 0$ .
Eq. (5.63): $W_q = r_0/(\mu(1-r_0))$ and $W = 1/(\mu(1-r_0))$ .

Significance

The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with $\rho$ replaced by $r_0$ : the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: $q_n$ is the distribution seen by arrivals, and it equals the time-average distribution $p_n$ only when the input is Poisson.

Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.

Difficulty

Locating a real root in $(0,1)$ is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves $qP = q$ does not show that no other probability vector does, and the goal asserts both. Computing $\sum_n n b_n = \mu/\lambda$ requires interchanging a sum with the integral against $A$ , which is where the finite mean of the interarrival law enters.

Formalization scope

The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes $\lambda > 0$ and $\mu > 0$ . The integrals defining $b_k$ and $A^*$ are over $[0,\infty)$ , closed at $0$ . The generating function $\beta$ takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with $q_n \ge 0$ , HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every $j$ .

The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); $\beta(z) = A^*[\mu(1-z)]$ (5.56); $\beta'(1) = \mu/\lambda$ ; $q_n = (1-r_0)r_0^n$ (5.60); $r_0/(1-r_0)$ and $r_0^2/(1-r_0)$ (5.61); $1 - r_0e^{-\mu(1-r_0)t}$ and $1 - e^{-\mu(1-r_0)t}$ (5.62); $r_0/(\mu(1-r_0))$ and $1/(\mu(1-r_0))$ (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: $W_q(t) = q_0 + \sum_{n\ge1} q_n \Pr\{n \text{ completions in} \le t\}$ with the Erlang type- $n$ CDF, and $W(t)$ likewise with $n+1$ completions. The means in (5.63) are $\int_0^\infty [1 - W_q(t)]\,dt$ and $\int_0^\infty [1 - W(t)]\,dt$ .

A trivializing formalization would take " $r_0 \in (0,1)$ solves $z = \beta(z)$ " as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.

Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on $\mathbb N$ . Contributions of either kind are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.1, pp.259–263. https://doi.org/10.1002/9781118625651
D. G. Kendall, "Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain", Annals of Mathematical Statistics 24(3), 1953, 338–354. https://doi.org/10.1214/aoms/1177728975

12 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory VI: The Pollaczek–Khintchine Transform for the M/G/1 QueueTextbook

Motivation

The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.

The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$ . Service times $S$ are independent with distribution $B$ , a probability distribution on $[0,\infty)$ with mean $\mathrm E[S]$ , and the discipline is first-come first-served. The traffic intensity is $\rho = \lambda\,\mathrm E[S]$ .

Let $X_n$ be the number of customers the $n$ th departing customer leaves behind. The number of arrivals during one service time equals $i$ with probability

k_i = \int_0^\infty \frac{e^{-\lambda t}(\lambda t)^i}{i!}\,dB(t),

and $(X_n)$ is a Markov chain on $\{0,1,2,\dots\}$ whose transition matrix $P$ has first row $(k_0,k_1,k_2,\dots)$ and, for $i \ge 1$ , entries $p_{ij} = k_{j-i+1}$ for $j \ge i-1$ and $0$ otherwise. A stationary distribution is a probability vector $\pi$ with $\pi P = \pi$ . Its generating function is $\Pi(z) = \sum_i \pi_i z^i$ , and that of the arrivals per service is $K(z) = \sum_i k_i z^i$ , for complex $|z| \le 1$ . The Laplace–Stieltjes transform of a distribution $F$ on $[0,\infty)$ is $F^*(s) = \int_0^\infty e^{-st}\,dF(t)$ . In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.

Formalization targets

Goal: the Pollaczek–Khintchine transform formula (5.15)–(5.16)

If $\mathrm E[S] < \infty$ and $\rho < 1$ , the chain has a stationary distribution, and every stationary distribution satisfies $\pi_0 = 1-\rho$ and

\Pi(z) = \frac{(1-\rho)(1-z)K(z)}{K(z)-z}, \qquad |z| \le 1,\ z \ne 1,

with $K(z) \ne z$ at each such $z$ . It leaves the service distribution completely general.

Milestones

The stationary equations (5.12): $\pi_i = \pi_0 k_i + \sum_{j=1}^{i+1}\pi_j k_{i-j+1}$ .
The transform (5.14), $\Pi(z) = \pi_0(1-z)K(z)/(K(z)-z)$ , with $\pi_0$ free and no condition on $\rho$ .
Ergodicity (§5.1.4): a unique stationary distribution exists if and only if $\rho < 1$ .
The departure-point mean (5.7): $L^{(D)} = \rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ .
$K(z) = B^*[\lambda(1-z)]$ (5.32).
The system-wait transform (5.29), (5.33): $\Pi(z) = W^*[\lambda(1-z)]$ and $W^*(s) = (1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ .
The line-wait transform (5.34): $W_q^*(s) = (1-\rho)s/(s-\lambda[1-B^*(s)])$ .
The busy-period equation (5.37): $G^*(s) = B^*[s+\lambda-\lambda G^*(s)]$ .
The mean busy period: $\mathrm E[X] = 1/(\mu-\lambda)$ with $\mu = 1/\mathrm E[S]$ .

Significance

The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at $z = 1$ give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.

All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.

Difficulty

Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex $z$ on the closed disk, which needs the non-vanishing of $K(z)-z$ away from $z = 1$ . That fact fails for $\rho > 1$ , where $K$ has a fixed point inside the disk. Second, (5.15) evaluates $\pi_0$ from $\Pi(1) = 1$ by a limit at the point where the formula is $0/0$ , and this uses $K'(1) = \rho$ , an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real $s > 0$ , while the generating-function route reaches only $s = \lambda(1-z) \in (0, 2\lambda]$ . Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.

Formalization scope

The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that $\mu = 1/\mathrm E[S]$ is the book's service rate.

Closed forms carried by the statements: $\pi_0 = 1-\rho$ (5.15); $(1-\rho)(1-z)K(z)/(K(z)-z)$ (5.16); $\pi_0(1-z)K(z)/(K(z)-z)$ (5.14); $\rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ (5.7); $B^*[\lambda(1-z)]$ (5.32); $(1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ (5.33); $(1-\rho)s/(s-\lambda[1-B^*(s)])$ (5.34); $B^*[s+\lambda-\lambda G^*(s)]$ (5.37); $1/(\mu-\lambda)$ for the mean busy period.

The waiting-time distribution $W$ enters through the book's FCFS relation $\pi_n = \frac1{n!}\int(\lambda t)^n e^{-\lambda t}\,dW(t)$ , and $W_q$ through $W = W_q * B$ ; both are hypotheses, as in the book. The busy-period distribution $G$ enters through the equation (5.36) in CDF form, with $n$ -fold convolutions built from Mathlib's Measure.conv.

The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: $\pi$ must be a probability vector, $\pi_0$ is determined as $1-\rho$ , and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.

Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on $[0,\infty)$ , and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.1. https://doi.org/10.1002/9781118625651
D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Annals of Mathematical Statistics 24 (1953) 338–354. https://doi.org/10.1214/aoms/1177728975
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953) 355–360. https://doi.org/10.1214/aoms/1177728976
L. Takács, Introduction to the Theory of Queues, Oxford University Press, 1962.
F. Pollaczek, Über eine Aufgabe der Wahrscheinlichkeitstheorie, Mathematische Zeitschrift 32 (1930) 64–100. https://doi.org/10.1007/BF01194620

12 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory V: Closed Jackson Networks and the Mean-Value RecursionTextbook

Motivation

Networks of queues model systems in which a job visits several service stations in turn: jobs in a computer system alternating between CPU and disks, machines cycling between operation and repair, parts routed through a job shop. In a closed network no job enters or leaves; a fixed population of $N$ customers circulates among $k$ nodes. Closed networks are the standard model of multiprogrammed computer systems and of machine-repair and finite-source systems, and they are the setting of chapter 4 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, doi:10.1002/9781118625651).

The chapter's results form a short line of computational ideas:

Jackson (1957, 1963) showed that open networks of exponential servers with Markovian routing have a product-form steady state; Gordon and Newell (1967) gave the closed-network version, (4.15)–(4.18) of the book.
Buzen (1973) gave a convolution recursion for the normalizing constant $G(N)$ and for marginal distributions, (4.19)–(4.22).
Reiser and Lavenberg (1980) introduced mean-value analysis (MVA), which computes mean queue lengths, waiting times and throughputs population by population without ever forming $G(N)$ , (4.23)–(4.25); the book presents it following Bruell and Balbo (1980).
The book closes the section with a recursion for the full marginal distributions, (4.26), which it proves from the product form (pp.207–209).

This mission formalizes that line, ending at (4.26).

Setting

A closed Jackson network has nodes $i = 1, \dots, k$ , each with a single server whose service times are exponential with rate $\mu_i > 0$ . A customer finishing service at node $i$ moves to node $j$ with probability $r_{ij}$ ; the routing matrix $R = (r_{ij})$ has nonnegative entries and rows summing to one, and it is irreducible: every node can be reached from every other. The state is $\bar n = (n_1, \dots, n_k)$ , the number of customers at each node, with $n_1 + \cdots + n_k = N$ ; this state space is finite.

The steady-state distribution $p_{\bar n}$ is the probability vector on the state space that solves the flow-balance equations (4.14),

\sum_{j=1}^{k}\sum_{\substack{i=1\\ i\ne j}}^{k} \mu_i r_{ij}\, p_{\bar n;i^+j^-} = \sum_{i=1}^{k}\mu_i(1-r_{ii})\,p_{\bar n},

where $\bar n;i^+j^-$ has one more customer at $i$ and one fewer at $j$ , and terms with a negative subscript or with $\mu_i$ at an empty node vanish. The traffic equations (4.16) are $\mu_i\rho_i = \sum_j \mu_j r_{ji}\rho_j$ ; they determine $\rho = (\rho_1, \dots, \rho_k)$ up to a positive factor. The normalizing constant is

G(N) = \sum_{n_1+\cdots+n_k=N}\rho_1^{n_1}\cdots\rho_k^{n_k},

and more generally, with $f_i(n) = \rho_i^{\,n}/a_i(n)$ for $c_i$ -server nodes ((4.13)), $G(N) = \sum \prod_i f_i(n_i)$ and Buzen's function $g_m(n) = \sum_{n_1+\cdots+n_m=n}\prod_{i\le m} f_i(n_i)$ .

For each population $N$ write $p_i(n, N) = \Pr\{N_i = n\}$ for the marginal distribution at node $i$ , $\bar P_i(n; N) = \Pr\{N_i \ge n\}$ , $L_i(N)$ for the mean number at node $i$ , and

\lambda_i(N) = \Pr\{\text{server busy at node } i\}\cdot\mu_i

for the throughput of node $i$ .

Formalization targets

Goal: the marginal recursion (4.26)

For every node $i$ ,

p_i(0,0) = 1, \qquad p_i(n, N) = \frac{\lambda_i(N)}{\mu_i}\,p_i(n-1, N-1) \quad (n, N \ge 1).

It involves only the steady-state distributions and quantities computed from them; it holds for every irreducible routing matrix and every choice of rates.

Milestones

Product form (4.14)–(4.16). For any positive solution $\rho$ of (4.16), a probability distribution solves (4.14) if and only if $p_{\bar n} = G(N)^{-1}\rho_1^{n_1}\cdots\rho_k^{n_k}$ .
Buzen's algorithm (4.19)–(4.21). $G(N) = g_k(N)$ , $g_m(n) = \sum_{i=0}^{n} f_m(i)\,g_{m-1}(n-i)$ , $g_1 = f_1$ , $g_m(0) = 1$ .
Marginal at the last node (4.22). $p_k(n) = f_k(n)\,g_{k-1}(N-n)/G(N)$ for $0 \le n \le N$ .
Complementary marginal (p.208). $\bar P_i(n_i; N) = \rho_i^{\,n_i}G(N-n_i)/G(N)$ .
Mean-value analysis (4.23)–(4.25). $L_i(0) = 0$ ; $L_i(N) = \lambda_i(N)W_i(N)$ with $W_i(N) = (1 + L_i(N-1))/\mu_i$ ; and for $v$ solving $v_i = \sum_j v_j r_{ji}$ with $v_l = 1$ , $\lambda_l(N) = N/\sum_i v_iW_i(N)$ and $\lambda_i(N) = \lambda_l(N)v_i$ .

Significance

The product form reduces a $\binom{N+k-1}{N}$ -state Markov chain to the constants $G(0), \dots, G(N)$ , and Buzen's recursion computes them in $O(kN^2)$ operations. Mean-value analysis goes further and avoids $G(N)$ , whose magnitude can overflow or underflow for large populations; it is the method used in capacity planning of computer systems. The recursion (4.26) extends MVA from means to full marginal distributions, so a single pass over $N$ yields every nodal distribution.

All of these results are classical and proved in the literature; the book proves (4.26) itself. What the mission adds is a machine-checked development of them from the global balance equations: the product form with its uniqueness, the convolution identities, the marginal formulas, and the correctness of the MVA iteration as stated by the book, all over one shared definition layer. A search of the platform on 2026-09-28 found no formal statement of Buzen's algorithm or of MVA. The platform has Kelly's closed migration process theorem (KellyStochasticNetworks.closed_migration_equilibrium), which shows that the unnormalized product form satisfies the equilibrium equations under Kelly's conventions; the normalization, uniqueness and everything downstream of the product form are new here.

Difficulty

The combinatorial identities (Buzen's recursion, the tail marginal) are reindexings of finite sums over compositions of $N$ ; in Lean the work is in bijections between the state spaces $\{n_1+\cdots+n_k = N\}$ for different $k$ and $N$ . The substantive step is uniqueness in the product-form theorem: the global balance equations have a one-dimensional solution space only because the chain on the $N$ -customer states is irreducible on the population level, which is a property of the network chain and not of the routing matrix alone. The goal and MVA also need a positive solution of the traffic equations, which is not among the hypotheses and has to come from irreducibility of $R$ . The book's own intuitive derivation of MVA via the arrival theorem is not the route the statements require; they are stated in terms of the steady-state distributions alone.

Formalization scope

Nodes are Fin k (book node $i$ is index $i-1$ ); states are n : Fin k → ℕ with ∑ i, n i = N, collected in a Finset, and all sums are finite. A distribution is a real function on $\mathbb N^k$ that is nonnegative, vanishes off the $N$ -customer states and sums to one there. The balance equations are (4.14) verbatim with the book's boundary convention (p.188), not detailed balance. All results except Buzen's algorithm and (4.22) are for single-server nodes, as in the book; (4.13)'s multiserver factor $a_i(n)$ enters only (4.19)–(4.22).

Closed forms instantiated in the statements: the product form $G(N)^{-1}\prod_i\rho_i^{n_i}$ ((4.15)); $G(N)$ as the explicit sum (4.18)/(4.19); $a_i(n)$ from (4.13); $g_m$ from (4.20); $p_k(n) = f_k(n)g_{k-1}(N-n)/G(N)$ ((4.22)); $\bar P_i(n;N) = \rho_i^nG(N-n)/G(N)$ (p.208); $W_i(N) = (1+L_i(N-1))/\mu_i$ ((4.23)); $\lambda_l(N) = N/\sum_i v_iW_i(N)$ (MVA step (iii)(b)).

Two trivializing formalizations are ruled out: $\lambda_i(N)$ in (4.26) and (4.24) is the throughput computed from the steady-state distribution, not a free constant (which would make (4.26) a definition); and $g_m$ is defined by the sum (4.20), so the recursion (4.21) is a theorem rather than rfl. The product-form statement is an equivalence, so it asserts both that the product form is a steady state and that it is the only one.

Needed infrastructure: bijections between compositions of $N$ into $k$ and $k-1$ parts, uniqueness of stationary distributions of irreducible finite continuous-time chains (stated directly via the balance equations), and existence of positive solutions of $v = vR$ for irreducible stochastic $R$ . The last two are reusable beyond this mission. Contributions welcome: proofs of the milestones in any order, and helper lemmas on these three points.

Not formalized: open Jackson networks (4.11) and Burke's theorem (4.5)–(4.6), multiclass networks (§4.2.1), the multiserver recursion (4.27) and cyclic queues (§4.4).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §4.3, pp.195–209. https://doi.org/10.1002/9781118625651
J. R. Jackson, "Jobshop-like queueing systems", Management Science 10(1), 1963. https://doi.org/10.1287/mnsc.10.1.131
W. J. Gordon, G. F. Newell, "Closed queuing systems with exponential servers", Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
J. P. Buzen, "Computational algorithms for closed queueing networks with exponential servers", Communications of the ACM 16(9), 1973. https://doi.org/10.1145/362342.362345
M. Reiser, S. S. Lavenberg, "Mean-value analysis of closed multichain queuing networks", Journal of the ACM 27(2), 1980. https://doi.org/10.1145/322186.322195
S. C. Bruell, G. Balbo, Computational Algorithms for Closed Queueing Networks, North-Holland, 1980.

7 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory IV: The Stationary Distribution of the M/M/1 Retrial QueueTextbook

Motivation

In many service systems a customer who finds every server busy does not join a queue. A caller who hears a busy signal hangs up and redials later; a request rejected by a saturated server is resent after a timeout; an aircraft that cannot land circles and tries again. These retrial queues are the subject of a substantial literature in telephone traffic engineering, computer networks and call-centre design, surveyed in the monograph of Falin and Templeton (1997) and the bibliography of Artalejo (1999). Their analysis is harder than that of ordinary queues: the blocked customers form an orbit whose size is part of the state, so even the simplest model is a two-dimensional Markov chain, and explicit stationary distributions are rare.

This mission is the fourth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008). Its goal is the explicit stationary distribution of the single-server retrial queue, Eq. (3.57) of §3.5.1, one of the few retrial models solvable in closed form. Chapter 3 of the book treats Markovian queues that are not birth–death processes: bulk arrivals, bulk service, Erlang phases, priority disciplines and retrials. The milestones also collect three capstone formulas from the chapter's other sections: the bulk-input queue, the partial-batch bulk-service queue, and Cobham's formula for nonpreemptive priorities (Cobham, 1954).

Setting

In the $M/M/1$ retrial queue customers arrive according to a Poisson process with rate $\lambda$ and are served one at a time by a single server, with exponential service times of mean $1/\mu$ . An arrival that finds the server busy enters the orbit and stays there for an exponential time with mean $1/\gamma$ , after which it tries again; each customer in orbit retries independently. No customer leaves because of impatience. With $N_s(t) \in \{0,1\}$ the number in service and $N_o(t)$ the number in orbit, the pair is a continuous-time Markov chain on states $\{i, n\}$ , $i \in \{0,1\}$ , $n \in \{0,1,2,\dots\}$ . Writing $p_{i,n}$ for the steady-state probability of $\{i,n\}$ , the rate-balance equations are

\begin{aligned} (\lambda + n\gamma)p_{0,n} &= \mu p_{1,n}, && n \ge 0, && (3.47)\\ (\lambda+\mu)p_{1,n} &= \lambda p_{0,n} + (n+1)\gamma p_{0,n+1} + \lambda p_{1,n-1}, && n \ge 1, && (3.48)\\ (\lambda+\mu)p_{1,0} &= \lambda p_{0,0} + \gamma p_{0,1}. && && (3.49) \end{aligned}

Following the book's convention (§1.9, and the footnote on p.118), a steady-state solution is a nonnegative solution of these equations whose total mass $\sum_n (p_{0,n} + p_{1,n})$ equals $1$ . The traffic intensity is $\rho = \lambda/\mu$ , and the partial generating functions are $P_0(z) = \sum_n z^n p_{0,n}$ and $P_1(z) = \sum_n z^n p_{1,n}$ .

The other models of the mission use the same convention. In the bulk-input queue $M^{[X]}/M/1$ , batches arrive at rate $\lambda$ with batch-size probabilities $c_n = \Pr\{X = n\}$ , $n \ge 1$ , and batch-size generating function $C(z) = \sum_n c_n z^n$ . In the partial-batch bulk-service queue $M/M^{[K]}/1$ , single arrivals come at rate $\lambda$ and the server serves up to $K$ customers together in an exponential time of mean $1/\mu$ . In the nonpreemptive priority queue there are $r$ classes with rates $\lambda_k$ and $\mu_k$ , loads $\rho_k = \lambda_k/\mu_k$ and cumulative loads $\sigma_k = \rho_1 + \cdots + \rho_k$ .

Formalization targets

Goal: the stationary distribution (3.57)

For $\lambda, \mu, \gamma > 0$ and $\rho < 1$ , the numbers

p_{0,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^n}{n!\,\gamma^n}\prod_{i=0}^{n-1}(\lambda+i\gamma), \qquad p_{1,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^{n+1}}{n!\,\gamma^n}\prod_{i=1}^{n}(\lambda+i\gamma)

form a steady-state solution of (3.47)–(3.49), and every steady-state solution equals them.

Milestones on the retrial queue

The generating functions satisfy (3.50)–(3.52) on $(-1,1)$ , including the separable equation

P_0'(z) = \frac{\lambda\rho}{\gamma(1-\rho z)}P_0(z),

their closed form is (3.55),

P_0(z) = (1-\rho z)\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1}, \qquad P_1(z) = \rho\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1},

and the mean orbit size is (3.58), $L_o = \frac{\rho^2}{1-\rho}\cdot\frac{\mu+\gamma}{\gamma}$ .

Milestones from the rest of Chapter 3

The bulk-input generating function (3.3), $p_0 = 1 - \rho$ with $\rho = \lambda\mathrm E[X]/\mu$ , and the mean (3.4); the unique root $r_0 \in (0,1)$ of $\mu r^{K+1} - (\lambda+\mu)r + \lambda = 0$ and the geometric law $p_n = (1-r_0)r_0^n$ (3.9); and Cobham's formula (3.41)/(3.43), the unique solution of the linear system (3.40).

Significance

The closed form (3.57) makes every performance measure of the $M/M/1$ retrial queue explicit. The server is busy a fraction $\rho$ of the time, exactly as without retrials. The mean orbit size (3.58) is the $M/M/1$ mean queue length multiplied by $(\mu+\gamma)/\gamma$ , and the mean time in orbit (3.59) follows from Little's law. These formulas quantify the cost of retrials against an ordinary queue and are the reference case against which approximations for multi-server retrial systems are checked.

The results are classical and proved in the book, partly through exercises (Problems 3.39–3.41). None of them is formalized in any proof assistant, as far as the platform's catalogue shows: there is no retrial, bulk or priority queue on Prove2Me. The mission produces machine-checked statements and, once solved, proofs of the chapter's main closed forms. It also produces a small reusable layer: generating functions of probability sequences on the closed unit disc, and the "probability solution of the balance equations" pattern for chains with countable state spaces.

Difficulty

The derivation in the book is formal. It differentiates power series term by term, divides by $1 - z$ , integrates $\ln P_0$ , and fixes the constant by setting $z = 1$ , without justifying any of these steps. A formal proof has to show that the series converge and are differentiable on $(-1,1)$ , that the differential equation determines $P_0$ up to a constant, and that the values at $z = 1$ are the limits of the values inside the disc (Abel's theorem). The uniqueness half of the goal is the hardest part. The book never proves it; it follows from the ODE argument only once every step is shown to hold for an arbitrary probability solution. Verifying that (3.57) solves (3.47)–(3.49) is only the easy half. The same pattern recurs in the bulk-input queue, where $z = 1$ is a removable singularity of (3.3). In the bulk-service queue the root $r_0$ is only characterized as the unique root in $(0,1)$ , so existence and uniqueness of the root are part of the claim.

Formalization scope

A steady-state solution is a pair p0 p1 : ℕ → ℝ (resp. one sequence p : ℕ → ℝ) that is pointwise nonnegative, has total mass $1$ as a HasSum, and solves the book's balance equations exactly as printed, global balance and not detailed balance. Every "the steady-state solution is X" is stated with both halves: X is a steady-state solution, and every steady-state solution equals X. Stating only that (3.57) solves (3.47)–(3.49), without normalization or uniqueness, would be a trivializing formalization. So would taking $r_0$ as a given root in (3.9), or taking the $W_q^{(i)}$ in (3.41) as numbers assumed to satisfy it. None of these is used. The closed forms instantiated are (3.52), (3.55), (3.57), (3.58), (3.3), (3.4), (3.9), (3.41) and (3.43), each written out in full, with the real power $(1-\rho)^{(\lambda/\gamma)+1}$ as Real.rpow.

The conventions are as follows. The retrial generating functions take real arguments, on $(-1,1)$ for the differential equations and on $[-1,1]$ for the closed form. The bulk-input generating function takes complex arguments with $|z| \le 1$ , $z \ne 1$ , because (3.3) is $0/0$ at $z = 1$ . The condition $\rho < 1$ is a hypothesis of every retrial statement. For the bulk-service queue the book's unnamed condition is stated as $\lambda < K\mu$ . For bulk input, $\mathrm E[X] < \infty$ is assumed throughout, and the mean (3.4) is asserted under the further condition $\mathrm E[X^2] < \infty$ , which it requires. For Cobham's formula only the algebraic content is formalized; the mean-value argument that yields (3.40) and (3.42) is not.

Needed infrastructure: power series of summable nonnegative sequences on the closed unit disc (convergence, term-by-term differentiation, Abel continuity), the binomial series $(1 - x)^{-a} = \sum_n \frac{a(a+1)\cdots(a+n-1)}{n!}x^n$ for real $a$ , and uniqueness of invariant probability vectors for irreducible chains. All of this is reusable beyond the mission. Proofs of any milestone, of the easy half of the goal, or of the needed series facts are welcome contributions.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§3.1, 3.2.0.1, 3.4.2, 3.5.1. https://doi.org/10.1002/9781118625651
G. I. Falin, J. G. C. Templeton, Retrial Queues, Chapman & Hall, 1997. https://doi.org/10.1007/978-1-4899-2977-8
J. R. Artalejo, Accessible bibliography on retrial queues, Mathematical and Computer Modelling 30 (1999) 1–6. https://doi.org/10.1016/S0895-7177(99)00128-4
A. Cobham, Priority assignment in waiting line problems, Journal of the Operations Research Society of America 2 (1954) 70–76. https://doi.org/10.1287/opre.2.1.70

10 thms2 active usersReviewed

Analysis Markov Chain Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory III: The Transient M/M/1 Queue via Modified Bessel FunctionsTextbook

Motivation

Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution $p_n(t) = \Pr\{N(t) = n\}$ of the number $N(t)$ in the system at a finite time $t$ . It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.

For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.

This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$ . Each service takes an exponential time of rate $\mu > 0$ , and $\rho = \lambda/\mu$ . The number in the system is a continuous-time Markov chain on $\{0, 1, 2, \dots\}$ , and its state probabilities $p_n(t)$ satisfy the forward (differential–difference) equations. For M/M/1 started with $N(0) = i$ they are, for $t \ge 0$ ,

p_n'(t) = -(\lambda+\mu)p_n(t) + \lambda p_{n-1}(t) + \mu p_{n+1}(t)\ (n > 0), \qquad p_0'(t) = -\lambda p_0(t) + \mu p_1(t), \tag{2.72}

with $p_n(0) = 1$ if $n = i$ and $0$ otherwise. The other systems are variants:

M/M/1/1, no waiting room: two states and equations (2.70).
M/M/∞, ample service: the death rate in state $n$ is $n\mu$ , giving (2.76).
The busy-period system: (2.72) with $0$ made absorbing ( $\lambda_0 = 0$ ) and $N(0) = 1$ . Its $p_0(t)$ is the distribution function of the busy period $T_{bp}$ .

A family $(p_n)$ solves a system on $[0,\infty)$ when each $p_n$ has, at every $t \ge 0$ , the prescribed derivative (a right derivative at $t = 0$ ). It is a probability solution when $p_n(t) \ge 0$ and $\sum_n p_n(t) = 1$ for every $t \ge 0$ . The modified Bessel function of the first kind is

I_n(y) = \sum_{k=0}^{\infty} \frac{(y/2)^{n+2k}}{k!\,(n+k)!}, \qquad I_{-n} = I_n,

and the Laplace transform of $f$ is $\bar f(s) = \int_0^\infty e^{-st} f(t)\,dt$ for $\operatorname{Re} s > 0$ .

Formalization targets

Goal: the transient M/M/1 law, (2.75)

With $y = 2t\sqrt{\lambda\mu}$ ,

p_n(t) = e^{-(\lambda+\mu)t}\Big[\rho^{(n-i)/2} I_{n-i}(y) + \rho^{(n-i-1)/2} I_{n+i+1}(y) + (1-\rho)\rho^n \sum_{j=n+i+2}^{\infty} \rho^{-j/2} I_j(y)\Big].

The goal asserts five things for every $\lambda, \mu > 0$ and every $i$ , with no restriction on $\rho$ :

the series converges;
these functions solve (2.72);
they meet the initial condition;
they form a probability distribution at every $t$ ;
they are the only probability solution.

Milestones

(2.71): the M/M/1/1 solution $p_1(t) = \frac{\lambda}{\lambda+\mu}(1-e^{-(\lambda+\mu)t}) + p_1(0)e^{-(\lambda+\mu)t}$ , and the matching formula for $p_0$ .
(2.74) and Rouché's theorem: for $\operatorname{Re} s > 0$ , the quadratic $(\lambda+\mu+s)z - \mu - \lambda z^2$ has exactly one zero in $|z| < 1$ , namely $z_1 = (\lambda+\mu+s-\sqrt{(\lambda+\mu+s)^2-4\lambda\mu})/(2\lambda)$ .
The transform of $p_0$ : $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ .
The limit of (2.75): $p_n(t) \to (1-\rho)\rho^n$ if $\rho < 1$ , and $p_n(t) \to 0$ if $\rho \ge 1$ .
(2.77), M/M/∞: started empty, $p_n(t) = a(t)^n e^{-a(t)}/n!$ with $a(t) = (1-e^{-\mu t})\lambda/\mu$ . The statement says that this family solves (2.76), is the unique probability solution, and has generating function $\exp((z-1)a(t))$ .
The busy-period transform: $\bar p_0(s) = 2\mu/(s[\lambda+\mu+s+\sqrt{(\lambda+\mu+s)^2-4\lambda\mu}])$ .
The busy-period density: $p_0'(t) = \sqrt{\mu/\lambda}\,e^{-(\lambda+\mu)t} I_1(2\sqrt{\lambda\mu}\,t)/t$ .
(2.79): for $\lambda < \mu$ , $E[T_{bp}] = 1/(\mu-\lambda)$ and $E[T_{bc}] = 1/\lambda + 1/(\mu-\lambda)$ .

Significance

The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload ( $\rho \ge 1$ ), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.

All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at $t = 0$ , and the class in which the solution is unique.

Difficulty

The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.

The Bessel form is a second, independent difficulty. The transform $\bar p_0(s)$ is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum $\sum_{j} \rho^{-j/2} I_j$ has to be controlled uniformly enough to be differentiated term by term. For $\rho \ge 1$ the factor $(1-\rho)$ is non-positive, so the nonnegativity of $p_n(t)$ is not visible from the formula.

Formalization scope

Conventions committed to:

Parameters. Rates are real with $\lambda, \mu > 0$ , and $\rho = \lambda/\mu$ . States are ℕ (Fin 2 for M/M/1/1).
Solutions. "Solves on $[0,\infty)$ " is HasDerivWithinAt on Set.Ici 0 at every $t \ge 0$ . Uniqueness is asserted among solutions that are probability distributions at every time.
Special functions. Half-integer powers of $\rho$ are real powers, and $I_{-m} = I_m$ is part of the definition. Laplace transforms are complex Bochner integrals over $(0,\infty)$ , and each statement also asserts the integrability it needs. Square roots with positive real part are hypotheses $r^2 = (\lambda+\mu+s)^2 - 4\lambda\mu$ , $\operatorname{Re} r > 0$ .

The closed forms stated exactly as in the book are:

(2.71);
$z_1$ and $z_2$ of (2.74);
$\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ ;
(2.75), with the Bessel series of p.101;
the M/M/∞ law and (2.77);
the busy-period transform and density of p.102;
(2.79).

The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.

A statement of (2.75) that only asserts the right-hand side is well defined, or checks only $n = 0$ , is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.

Needed infrastructure that Mathlib lacks:

modified Bessel functions of integer order;
Laplace transforms;
a Rouché-type zero count or a direct root-location lemma;
uniqueness for countable linear ODE systems with bounded or linearly growing rates.

The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§2.11–2.12, pp.97–103. https://doi.org/10.1002/9781118625651
N. T. J. Bailey, "A continuous time treatment of a simple queue using generating functions", J. Royal Statistical Society B 16 (1954) 288–291. https://doi.org/10.1111/j.2517-6161.1954.tb00172.x
W. Ledermann, G. E. H. Reuter, "Spectral theory for the differential equations of simple birth and death processes", Phil. Trans. Royal Society A 246 (1954) 321–369. https://doi.org/10.1098/rsta.1954.0001
D. G. Champernowne, "An elementary method of solution of the queueing problem with a single server and constant parameters", J. Royal Statistical Society B 18 (1956) 125–128. https://doi.org/10.1111/j.2517-6161.1956.tb00217.x
J. Abate, W. Whitt, "Calculating time-dependent performance measures for the M/M/1 queue", IEEE Trans. Communications 37 (1989) 1102–1104. https://doi.org/10.1109/26.41165

15 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory II: Erlang's Formulas and the Halfin–Whitt Square-Root Staffing LawTextbook

Why birth–death queues and Erlang's formulas

Every call center, hospital ward, cloud server pool and telephone exchange that is sized by formula is sized by one of a handful of explicit expressions from Markovian queueing theory. The two oldest are A. K. Erlang's: the Erlang-B (loss) formula of 1917, which gives the fraction of calls lost when $c$ trunks carry an offered load of $r$ erlangs, and the Erlang-C formula, which gives the probability that a customer of a $c$ -server queue must wait. Both are still the default dimensioning rules of telecommunications and call-center workforce management (Gans, Koole & Mandelbaum 2003).

This mission formalizes Chapter 2, §§2.1–2.10, of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), which derives these formulas from a single result about birth–death processes and closes with the modern answer to the staffing question.

Timeline. Erlang (1917) obtained the loss formula; Vaulot (1927), Pollaczek (1932), Palm (1938) and Kosten (1948) completed its proof for general service times. Halfin and Whitt (1981) showed that in the $M/M/n$ queue the delay probability converges to a limit strictly between $0$ and $1$ exactly when the number of servers exceeds the offered load by an amount of order $\sqrt n$ . This is the quality-and-efficiency-driven (QED) regime on which square-root staffing rests.

Setting

A birth–death process is a continuous-time Markov chain on the states $n \in \{0, 1, 2, \dots\}$ that moves from $n$ to $n+1$ at rate $\lambda_n \ge 0$ (a birth, or arrival) and, for $n \ge 1$ , from $n$ to $n-1$ at rate $\mu_n > 0$ (a death, or departure). A steady-state solution is a probability sequence $\{p_n\}$ ( $p_n \ge 0$ , $\sum_n p_n = 1$ ) solving the global balance equations (2.1):

(\lambda_n + \mu_n)p_n = \lambda_{n-1}p_{n-1} + \mu_{n+1}p_{n+1}\ (n \ge 1), \qquad \lambda_0 p_0 = \mu_1 p_1.

The queues of the chapter are birth–death processes with particular rates. The $M/M/1$ queue has $\lambda_n = \lambda$ , $\mu_n = \mu$ and traffic intensity $\rho = \lambda/\mu$ . The $M/M/c$ queue has $\lambda_n = \lambda$ , $\mu_n = \min(n, c)\mu$ (2.30), offered load $r = \lambda/\mu$ and $\rho = r/c$ . The $M/M/c/c$ loss system is the same with $\lambda_n = 0$ for $n \ge c$ . The $M/M/\infty$ queue has $\mu_n = n\mu$ .

The explicit functions are the Erlang-B formula

B(c, r) = \frac{r^c/c!}{\sum_{i=0}^{c} r^i/i!},

the Erlang-C formula, defined for $\rho = r/c < 1$ ,

C(c, r) = \frac{r^c/(c!(1-\rho))}{r^c/(c!(1-\rho)) + \sum_{n=0}^{c-1} r^n/n!},

and, with $\phi$ , $\Phi$ the standard normal density and distribution function,

\alpha(\beta) = \frac{\phi(\beta)}{\phi(\beta) + \beta\Phi(\beta)}.

Formalization targets

Goal: the Halfin–Whitt theorem (§2.4, p.75)

For offered loads $0 < r_n < n$ ,

\lim_{n\to\infty} C(n, r_n) = \alpha \in (0,1) \iff \lim_{n\to\infty} \frac{n - r_n}{\sqrt n} = \beta > 0, \qquad \alpha = \alpha(\beta).

It is stated as three facts: $\alpha$ maps $(0, \infty)$ into $(0, 1)$ ; each $\alpha \in (0, 1)$ has exactly one preimage $\beta > 0$ ; and for every $\beta > 0$ the two limits are equivalent.

Milestones

(2.3)–(2.4): the steady-state solution of a general birth–death process, $p_n = p_0\prod_{i=1}^n \lambda_{i-1}/\mu_i$ , and its existence if and only if $1 + \sum_{n\ge1}\prod_{i=1}^n \lambda_{i-1}/\mu_i < \infty$ .
(2.9): $M/M/1$ , $p_n = (1-\rho)\rho^n$ , existing iff $\rho < 1$ .
(2.31)–(2.32): the $M/M/c$ law, existing iff $\lambda/(c\mu) < 1$ .
(2.33): $L_q = r^c\rho\,p_0/(c!(1-\rho)^2)$ .
(2.37)–(2.38): $1 - \sum_{n<c} p_n = C(c, r)$ .
(2.52)–(2.53): the $M/M/c/c$ law and $p_c = B(c, r)$ .
(2.54): $B(c, r) = rB(c-1, r)/(c + rB(c-1, r))$ , $B(0, r) = 1$ .
(2.55): $C(c, r) = cB(c, r)/(c - r + rB(c, r))$ .
(2.57): $M/M/\infty$ , $p_n = r^n e^{-r}/n!$ .

Significance

The results. Items 1–9 are the working formulas of Markovian capacity planning: a stationary law for each basic model and the measures read off from it. (2.54) and (2.55) are how $B$ and $C$ are computed in practice, since the factorials of the closed forms overflow for $c > 170$ . The Halfin–Whitt theorem is the reason the rule $c \approx r + \beta\sqrt r$ holds a fixed service level, and it is the entry point to the QED heavy-traffic literature (diffusion limits of many-server queues, Garnett–Mandelbaum–Reiman, Gamarnik–Momčilović).

Formalizing them. All results are classical and proved in the literature. The book states the Halfin–Whitt theorem without proof, and (2.54)–(2.55) are left to exercises. The formalization would supply machine-checked versions of the Erlang identities and of the Halfin–Whitt limit theorem. No Lean development of either was found on the platform when this mission was drafted. A related Erlang-B statement from Kelly and Yudovina is on the platform, stated with detailed balance on a finite state space.

Difficulty

The stationary laws are induction plus geometric and exponential series, and the Erlang identities are finite algebra. The difficulty is concentrated in the goal. $C(n, r_n)$ is a ratio of a Poisson-type tail to a truncated exponential sum in which both $n$ and $r_n$ grow. The naive route, substituting Stirling's formula term by term, fails: the sums have $\Theta(\sqrt n)$ significant terms, each of relative size $\exp(-k^2/2n)$ , and the error has to be controlled uniformly over them. The converse direction also requires showing that $\alpha(\cdot)$ is strictly monotone. Without that, convergence of $C(n, r_n)$ does not force convergence of $(n - r_n)/\sqrt n$ .

Formalization scope

Rates are real sequences indexed by $\mathbb N$ , and a steady-state solution is a real sequence with HasSum p 1, nonnegative entries, and the balance equations (2.1) exactly as printed (global balance, not detailed balance). Every "the steady-state solution is X" is stated in both halves: X is a steady-state solution, and every steady-state solution equals X; the book's existence conditions ( $\rho < 1$ , $\lambda/(c\mu) < 1$ , convergence of the series) are part of the statements. The $M/M/c/c$ system is the $\mathbb N$ -indexed process with $\lambda_n = 0$ for $n \ge c$ , as §2.5 sets it up; the statement records that states above $c$ carry no mass.

The closed forms that are fixed in Lean: $\prod_{i=1}^n \lambda_{i-1}/\mu_i$ over Finset.Icc 1 n; $B(c, r)$ and $C(c, r)$ exactly as displayed above; $\phi$ = gaussianPDFReal 0 1, $\Phi$ = the CDF of gaussianReal 0 1; $W_q(0) = \sum_{n=0}^{c-1} p_n$ , as evaluated on p.69; $L_q = \sum_{n > c}(n - c)p_n$ as a convergent series.

$C(c, r)$ is a total function in Lean, but its value for $r \ge c$ carries no meaning. The goal assumes $0 < r_n < n$ for $n \ge 1$ , the book's standing condition $\rho < 1$ . A statement about some other function with the same limiting behaviour, or with $B$ and $C$ left abstract, would not be this mission. Neither would one-directional or existence-only versions of the stationary laws.

Not included: the waiting-time distributions (2.28) and (2.39), which need an FCFS waiting-time model with arrival-point probabilities; the $M/M/c/K$ measures (2.45)–(2.48); finite-source and state-dependent models (§§2.8–2.10). Useful contributions beyond the milestones are Poisson tail estimates at the $\sqrt n$ scale and monotonicity of $\alpha(\beta)$ . Both are reusable in other many-server heavy-traffic statements.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manufacturing & Service Operations Management 5(2), 79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917 (English translation in The Life and Works of A. K. Erlang, 1948).
F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

12 thms2 active usersReviewed

Operations Research

Missions

Correlated Equilibrium as an Expression of Bayesian Rationality II: Two-Person Correlated Equilibrium Distributions Are the Solutions of Linear InequalitiesResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1 (i)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.2 (i)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 1: Logarithmic Regret for Two ArmsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Project Scheduling with Time Windows and Scarce Resources V: A Schedule Is Inventory-Feasible iff It Resolves Every Minimal Surplus and Shortage SetTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.12.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Project Scheduling with Time Windows and Scarce Resources IV: Every Feasible Schedule Obeys a Minimal Delaying Mode of Each Forbidden SetTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming XI: The KKT Conditions and the Unique Smallest Enclosing BallTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.7.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming III: The Simplex Method with Bland's Rule Never CyclesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.8.1 (p. 73)

Milestones

Significance

Difficulty