Operations Research

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$. Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$; its traffic intensity is $\rho_i=\lambda_i/\mu_i$, and the queue is stable: $\sum_{i\in E}\rho_i<1$. For $S\subseteq E$ define

$$b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .$$

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

$$\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).$$

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$, the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$, $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

$$\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .$$

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$. The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

$$\mathrm{P2}'=\mathrm{P1}.$$

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$, every positive rate vector and every stable load.

Milestones

1. §8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$, and P1 is their convex hull:

$$\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.$$

2. §8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

$$\mathrm{P2}'\subseteq\mathrm{P1}.$$

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$. We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$. The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$, including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$: inequality for every $S\neq E$, equality at $S=E$, nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$, not $n_i$. $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$, which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$, or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
• J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$). There are finitely many fare classes $i$. Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$, with law $p_i$. The seats are split into allocations $S_i \in \mathbb{N}$, one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

$$b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.$$

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$, and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

$$\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},$$

the expected marginal seat revenue of the $S$-th seat of class $i$. The value of the $k$-th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$, $k = 1, \dots, n$.

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$, $1 \le k \le n$, such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$, and let $S^T_i = \#\{k : (i,k) \in T\}$. Then $\sum_i S^T_i = n$ and

$$\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .$$

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

1. Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
2. Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$.
3. Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$.
4. Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$, $0 \le X_{ik} \le 1$.
5. Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$, for all $i$.

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$.

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

• Integer demand. The law of class $i$'s requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$. The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
• Tail convention. $\bar P(S) = P[r \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
• Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$, as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
• Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
• Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
• Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
• No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
• "Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
• LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$. Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$, and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
• P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

Motivation

Nash equilibrium is the standard solution concept for strategic games, but it is usually justified by appeal to what players "would" do once they somehow coordinate on a profile. Correlated equilibrium, introduced by Aumann (J. Math. Econ. 1, 1974), enlarges the set of outcomes by letting players condition their actions on correlated private signals. In Correlated Equilibrium as an Expression of Bayesian Rationality (Econometrica 55, 1987), Aumann gave the concept a decision-theoretic foundation: if the players share a common prior over the states of the world and each player maximizes expected utility given his information at every state, then what they play is a correlated equilibrium — and every correlated equilibrium arises this way. The result is a standard entry point to the epistemic foundations of game theory, and correlated equilibria are central in algorithmic game theory because no-swap-regret learning dynamics converge to them (Foster–Vohra 1997; Hart–Mas-Colell 2000).

Timeline:

• 1974, Aumann: correlated equilibrium defined, in a measure-theoretic model with subjective probabilities and information σ-fields.
• 1987, Aumann: the Main Theorem (Bayes rationality at every state under a common prior implies correlated equilibrium play) and its converse, in a finite model with information partitions.

Setting

A game $G$ in strategic form has players $i$, action sets $S^i$, action $n$-tuples $s\in S=S^1\times\dots\times S^n$, and payoffs $h^i(s)\in\mathbb R$.

A correlated strategy $n$-tuple is a function $f:\Gamma\to S$ on a finite probability space $(\Gamma,q)$, with $q\ge 0$ and $\sum_\gamma q(\gamma)=1$. Its expected payoff is $Eh^i(f)=\sum_\gamma q(\gamma)h^i(f(\gamma))$. For $g^i:\Gamma\to S^i$, the profile $(f^{-i},g^i)$ replaces player $i$'s coordinate of $f$ by $g^i$. The function $f$ is a correlated equilibrium (Definition 2.1) if

$$Eh^i(f)\ \ge\ Eh^i(f^{-i},g^i)\qquad(2.2)$$

for every player $i$ and every $g^i$ that is a function of $f^i$ (i.e. $g^i=\varphi\circ f^i$). The distribution of $f$ assigns to each $s\in S$ the number $q\{f^{-1}(s)\}$, and a correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium.

An information system consists of a finite set $\Omega$ of states of the world, a common prior $p$ on $\Omega$, an information partition $\mathcal P^i$ of $\Omega$ for each player, and action functions $\mathbf s^i:\Omega\to S^i$ with $\mathbf s=(\mathbf s^1,\dots,\mathbf s^n)$, each $\mathbf s^i$ constant on the elements of $\mathcal P^i$ (each player knows his own action). For a random variable $x$, $E(x\mid\mathcal P^i)(\omega)$ is the $p$-average of $x$ over the element of $\mathcal P^i$ containing $\omega$. Player $i$ is Bayes rational at $\omega$ if

$$E\big(h^i(\mathbf s)\mid\mathcal P^i\big)(\omega)\ \ge\ E\big(h^i(\mathbf s^{-i},a)\mid\mathcal P^i\big)(\omega)\quad\text{for every }a\in S^i .$$

Formalization targets

Goal: Main Theorem with its converse

$$Q\ \text{is a c.e.d. of }G\iff\exists\ \text{information system }(\Omega,p,(\mathcal P^i),\mathbf s):\ \text{every player is Bayes rational at every state, and } Q(a)=p\{\mathbf s=a\}\ \forall a.$$

This is the two-sided statement the paper announces in its introduction (p. 2) and closes in Sect. 4d (p. 11): "under Bayesian rationality, the set of all information systems corresponds precisely to the set of all correlated equilibria."

Milestones

1. Main Theorem, proof: summing the cell-wise inequalities over the partition, $Eh^i(\mathbf s^{-i},g^i)\le Eh^i(\mathbf s)$ for $g^i$ constant on the cells of $\mathcal P^i$.
2. Main Theorem, proof: $\mathbf s$ itself is a correlated equilibrium on $(\Omega,p)$.
3. Main Theorem (p. 7): the distribution of $\mathbf s$ is a c.e.d.
4. Sect. 4d: in the system generated by $f$ (partitions generated by $f^i$), Bayes rationality everywhere is equivalent to (2.2).
5. Sect. 4d: every correlated equilibrium is realized by a Bayes-rational information system with the same distribution.

The mission also states, as a supporting lemma without a milestone, the cell-wise step of the proof of the Main Theorem: Bayes rationality at every state gives $E(h^i(\mathbf s^{-i},g^i)\mid P)\le E(h^i(\mathbf s)\mid P)$ on every cell $P$ for $g^i$ constant on cells.

Significance

The theorem identifies correlated equilibrium as the outcome of individual Bayesian decision making under a common prior, without any assumption that players randomize or that their choices are independent. It shows that the Nash equilibrium's independence requirement is not implied by rationality alone, and it is the template for later epistemic characterizations of solution concepts. On the computational side, correlated equilibrium distributions form a polytope described by linear inequalities (the companion mission of this series), which is why they are the tractable equilibrium notion in algorithmic game theory.

The result is proved in the paper; it has no machine-checked formalization known to this mission. Formalizing it pins down the exact role of the standing assumptions — finiteness, a common prior, measurability of each player's action with respect to his own partition, rationality at every state — and of the conditional expectation on cells of probability zero. The definitions (information systems, Bayes rationality, correlated equilibria as functions on a finite probability space) are reusable for later formalizations of the paper's Sect. 5 (subjective correlated equilibrium) and of other epistemic results.

Difficulty

The mathematics is short; the difficulty lies in the bookkeeping that the paper's notation hides. The hypothesis is interim (a conditional inequality at each state), while Definition 2.1 is ex ante (an unconditional inequality). Passing between them requires the law of total expectation over a partition whose cells may have probability zero, where conditional expectations are undefined. Deviations in Definition 2.1 are functions of $f^i$, not arbitrary maps, and must be shown constant on cells, which uses measurability of $\mathbf s^i$. A tempting first idea — that rationality against every fixed action already gives rationality against every deviation — fails without measurability: a player who does not know his own action could be rational at each state against constant deviations while a deviation $\varphi\circ\mathbf s^i$ varies inside his cells. The converse direction needs an information system that satisfies every axiom of the goal's right-hand side, not just one that is Bayes rational.

Formalization scope

• Players form a finite type ι with decidable equality; action sets S i are arbitrary types (the paper's finiteness of $S^i$ is not used); payoffs are h : ι → (∀ i, S i) → ℝ.
• Probability spaces are finite types with a real weight vector satisfying AGT.IsLottery (from the published definition agt_games). State spaces and the witnessing probability spaces of a c.e.d. range over Type; for finite sets this loses nothing.
• Partitions are Setoids. The Common Prior Assumption is built into the information system, which has a single prior. Measurability of each action function is a field of the structure.
• Conditional expectation on a cell is a ratio of finite sums; on a cell of probability zero Lean returns $0$, so Bayes rationality at such states holds vacuously. The prior is not required to have full support. This matches the paper, whose argument multiplies each cell inequality by the cell's probability.
• Deviations in Definition 2.1 are exactly the compositions $\varphi\circ f^i$; neither all maps nor only constant maps. A c.e.d. requires a genuine probability vector, ruling out the trivializing reading in which the zero weight function witnesses every $Q$.
• Contributions welcome: proofs of the milestones, a general law-of-total-expectation lemma for finite partitions, and lemmas relating distr to sums over action profiles.

Selected references

• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), no. 1, 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

Motivation

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

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 4.1 (p. 94)

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

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

Milestones for the goal

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

Further results of the chapter

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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