Operations Research

Motivation

A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54

The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56

Setting

All graphs here are finite and simple. The complement $\overline G$ has the same vertices as $G$, and two distinct vertices are adjacent in $\overline G$ exactly when they are not adjacent in $G$. For a vertex set $X$, the notation $G|X$ means the induced subgraph on $X$. A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph $H$ is $\omega(H)$, and $\chi(H)$ is the minimum number of colors in a proper vertex coloring of $H$.

A hole is an induced cycle of length at least four. An antihole of $G$ is a hole in $\overline G$. A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires $\chi(G|X)=\omega(G|X)$ for every $X\subseteq V(G)$, while a Berge graph satisfies a restriction on induced cycles in both $G$ and $\overline G$. “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52

For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices $a_i,b_i$ and $c_j,d_j$ with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54

Formalization targets

Theorem 1.2: perfection and the Berge property

The goal is the exact equivalence for every finite simple graph:

$$G\text{ is perfect}\quad\Longleftrightarrow\quad G\text{ is Berge}.$$

No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2

Structural and reduction milestones

Theorem 1.1 says that $G$ perfect implies $\overline G$ perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has $G$ or $\overline G$ bipartite. Theorem 1.3 states the decomposition conclusion:

$$G\text{ Berge}\Longrightarrow G\text{ basic}\ \lor\ G\text{ or }\overline G\text{ has a proper 2-join}\ \lor\ G\text{ has a proper homogeneous pair}\ \lor\ G\text{ has a balanced skew partition}.$$

The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154

Significance

Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56

The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.

Difficulty

The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154

Formalization scope

Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.

No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both $G$ and $\overline G$; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.

Selected references

• Maria Chudnovsky, Neil Robertson, Paul Seymour, and Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. DOI 10.4007/annals.2006.164.51.

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

• Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
• Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
• Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

• Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ($k\in\mathcal J$), service times $v_k^i>0$, and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$. When the $i$th customer served at station $k$ finishes, it moves to station $\phi_k^i$, or leaves if $\phi_k^i=0$. The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$, the service-time variances $s_k=\operatorname{var} v_k^1$, the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$), and the interarrival variances $a_k=\operatorname{var} u_k^1$. The routing matrix $P=(p_{kj})$, $p_{kj}=P\{\phi_k^1=j\}$, has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$, and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$, with $e_0=0$. The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

$$Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .$$

A sequence of such networks, indexed by $n$, shares $K$, $\mathcal J$ and $P$. Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$. With $\nu(n)=\lambda(n)+\mu(n)P$, the heavy-traffic condition is

$$c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .$$

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$. The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$, $0\le t\le1$.

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$, where

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$. Then

$$Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.$$

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

• the existence and uniqueness claim for (1)–(3);
• the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
• the least-element map $f$ (Proposition 1);
• the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
• the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
• stochastic boundedness of $Z^n$ (Lemma 6);
• vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
• the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

• a formal statement of the network, of its Harrison representation, and of weak convergence in $D$;
• a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
• eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$, which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$. It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

• Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
• A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$.
• The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
• "Spectral radius $<1$" is stated as $P^m\to0$.
• $(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
• The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$, (22) and (26) over $k\in\mathcal J$, and $\mathcal J$ is the same for all $n$.
• Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$. It is defined by continuity, $\xi(0)=0$, independent increments, and the Gaussian characteristic function of increments.
• $Z$ is the reflection of $\xi$ in the sense of (14)–(17).
• Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J$_1$ convergence on $[0,1]$. This form accommodates a separate probability space for each $n$.

Added hypotheses, each implicit on the page:

1. The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
2. Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

• convergence of finite-dimensional distributions only;
• a single network without the index $n$;
• uniform convergence used in place of the Skorohod topology without the coupling;
• a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

• the deterministic reflection-map results;
• Donsker-type theorems for renewal counting processes in $D$;
• the random time-change lemma (Billingsley);
• the continuous mapping theorem in coupling form.

Selected references

• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
• J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
• J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
• D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
• P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

Motivation

A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least $1/6.75$ of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).

Setting

Single-parameter problem (BSMD). Finitely many agents $i$ have independent private values $v_i \sim F_i$, each with a density on a bounded interval. A seller may serve any set in a downward-closed set system $\mathcal J$. A deterministic mechanism $M$ maps reported values $v$ to a served set $M(v) \in \mathcal J$ and payments $\pi_i(v)$; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_v[\sum_i \pi_i(v)]$. For prices $p$, agent $i$ desires service if $p_i \le v_i$, and $\mathcal S_v$ is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{v}\Big[\min_{S \in \mathcal S_v} \sum_{i \in S} p_i\Big],$$

a lower bound on the revenue of posting the prices $p$ to the agents in an adversarial order.

Multi-parameter unit-demand problem (BMUMD). There are $m$ buyers and a finite set $J$ of services, partitioned into the groups $J_i$ of services targeted at buyer $i$. Buyer $i$ has value $v_j$ for each $j \in J_i$, all values independent with $v_j \sim F_j$, and the set system $\mathcal J \subseteq 2^J$ is unit-demand: $|S \cap J_i| \le 1$ for feasible $S$. A mechanism $\mathcal A$ is truthful if no buyer gains by misreporting its whole vector $(v_j)_{j \in J_i}$, and individually rational if a buyer receiving $j$ pays at most $v_j$ and a buyer receiving nothing pays $0$.

Copies. The instance $\mathcal I^{\mathrm{copies}}$ replaces each buyer $i$ by $|J_i|$ single-parameter agents, one per service $j \in J_i$ with value $v_j$, under the same $\mathcal J$.

Price menus. Given prices $(p_j)$ and an arrival order $\sigma$, the price-menu mechanism approaches the buyers in order; buyer $i$ is offered the services of $J_i$ that can still be feasibly allocated, at prices $p_j$, and buys a utility-maximizing one if some has $p_j \le v_j$.

Multiple copies of items. With items $K$ and $\mathrm{cap}(k)$ copies of item $k$, services are pairs $(i,k)$ and a set of services is feasible if it gives each buyer at most one item and uses at most $\mathrm{cap}(k)$ copies of $k$: the intersection of two partition matroids.

Formalization targets

Goal: Theorem 14

For regular distributions there are prices $p$ such that, for every arrival order $\sigma$, the price-menu mechanism $\mathcal P_\sigma$ is truthful and

$$\mathcal R^{\mathcal A} \le \tfrac{27}{4}\,\mathcal R^{\mathcal P_\sigma}$$

for every individually rational, truthful deterministic mechanism $\mathcal A$.

Milestones

• Truthful BMUMD mechanisms are weakly monotone (p. 13), and the allocation of $\mathcal A^{\mathrm{copies}}$ is monotone in each $v_j$ (p. 13).
• Lemma 3: $\mathcal R^{\mathcal A} \le \mathcal R^{\mathcal A'}$ for some truthful $\mathcal A'$ on $\mathcal I^{\mathrm{copies}}$.
• The price-menu mechanism allocates a maximal feasible set of services (p. 14).
• Theorem 4: if $\mathcal R^{M'} \le \alpha\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M'$ on $\mathcal I^{\mathrm{copies}}$, then $\mathcal R^{\mathcal A} \le \alpha\,\mathcal R^{\mathcal P_\sigma}$ for every $\sigma$ and every truthful IR $\mathcal A$.
• Lemma 2 (regular part): $\mathcal R^M \le \sum_i p^M_i q^M_i$, with $q^M_i$ the probability that $M$ serves $i$ and $F_i(p^M_i) = 1 - q^M_i$.
• Theorem 19 (existence form): a revenue-optimal truthful mechanism exists.
• The claim $c_i \ge 4/9$ of App. D.4: under $\sum_{i' \in P} q_{i'} \le \mathrm{cap}(P)/3$ in every part, with probability at least $4/9$ neither part of $i$ is full without $i$.
• Theorem 13: for two partition matroids there are prices with $\mathcal R^M \le \tfrac{27}{4}\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M$.

Significance

The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.

All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant $6.75$, and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.

Difficulty

Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.

Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by $1/3$. The step that is easy to get wrong is the probability that an agent is considered: the events "part $P_1$ is not full" and "part $P_2$ is not full" depend on overlapping agents, so the product bound $(2/3)(2/3)$ does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.

Formalization scope

• Distributions (P1): each $F_j$ has a measurable density, strictly positive on a bounded interval $[\underline v_j, \overline v_j] \subseteq [0, \infty)$, with no mass outside. Values are independent (product prior).
• Regularity (P2): the virtual value $\phi(v) = v - (1 - F(v))/f(v)$ is non-decreasing on the support. It is assumed in Lemma 2, Theorem 19, Theorem 13 and the goal. Theorem 14 does not state it, but its proof goes through Theorem 13, which the paper proves for regular distributions; the non-regular extension (App. E, randomized prices) is out of scope, as is the second paragraph of Lemma 2.
• Mechanisms (P3): deterministic; dominant-strategy truthful with misreports in the support (a buyer misreports all coordinates of $J_i$ at once); single-parameter IR is ex-post nonnegative utility; multi-parameter IR is the paper's ($\pi_i \le v_j$ if served $j$, $\pi_i = 0$ if unserved); allocation events and payments measurable, payments integrable.
• Benchmarks (P4): Myerson's mechanism is not constructed. "Approximates $\mathcal R^{\mathcal M}$" is stated against every truthful mechanism, and Lemma 3 and Theorem 19 in existence form.
• Price menus: ties between utility-maximizing services are broken by a fixed enumeration of $J$; a service of utility $0$ is bought. Theorem 4 assumes $\alpha \ge 0$.
• Dropped: the last sentence of Theorem 14 (polynomial-time computability of the prices) has no cost model here.
• Constant: $6.75$ is written $27/4$ everywhere.
• Not trivializable: the prices in Theorem 13 and the goal are chosen before the mechanism, and the benchmark includes every truthful mechanism, so a degenerate price vector cannot meet the bound; $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over a nonempty finite class.

Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• S. Chawla, J. D. Hartline, R. Kleinberg, Algorithmic Pricing via Virtual Valuations, EC 2007. https://arxiv.org/abs/0711.3203
• A. M. Manelli, D. R. Vincent, Multidimensional mechanism design: Revenue maximization and the multiple-good monopoly, Journal of Economic Theory 137(1), 2007. https://doi.org/10.1016/j.jet.2006.12.007
• T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc. 56, 1960. https://doi.org/10.1017/S0305004100034241

Motivation

Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.

This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$, $n\ge1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Temporal constraints are the arcs of a project network $N=\langle V,E;\delta\rangle$: an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ requires $S_j-S_i\ge\delta_{ij}$ for the start times $S_i$. A maximum project duration $\bar d$ is the arc $\langle n+1,0\rangle$ with weight $-\bar d$. The time-feasible region is

$$\mathcal S_T=\{S\in\mathbb R^{n+2}_{\ge0}\mid S_0=0,\ S_j-S_i\ge\delta_{ij}\ (\langle i,j\rangle\in E)\}.$$

Let $0<\beta\le1$ be the discount rate ($\beta=1/(1+I)$ for an interest rate $I$) and $c_i^F\in\mathbb R$ the cash flow of activity $i$, paid at its completion time $C_i=S_i+p_i$. The problem (3.9.1) is

$$\text{minimize } f(S)=-\sum_{i\in V}c_i^F\beta^{S_i+p_i}\quad\text{subject to } S\in\mathcal S_T,$$

and a minimizer is a time-optimal schedule. A vertex of $\mathcal S_T$ is an extreme point. A spanning tree $G=\langle V,E^G\rangle$ is associated with $S$ if $E^G\subseteq E$, $E^G$ has $n+1$ arcs and a connected underlying undirected graph, and $S$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ for $\langle i,j\rangle\in E^G$. Deleting a tree arc $\langle i,j\rangle$ splits $G$ into two subtrees; $V_{ij}$ is the node set of the one not containing $0$. The arc is forward if the tree path from $0$ passes it from $i$ to $j$ and backward otherwise, and

$$npv^{ij}(S)=\sum_{h\in V_{ij}}c_h^F\beta^{S_h+p_h}$$

is the net present value of the subproject $V_{ij}$. Finally, $f$ is binary-monotone if it is monotone on every line $\{S+\lambda z\ge0\mid\lambda\in\mathbb R\}$ with direction $z\in\{0,1\}^{n+2}$ (Definition 3.3.2).

Formalization targets

Goal: Proposition 3.9.2, pinned reading

Assume every node is reached from $0$ by a path of nonnegative length (the standing convention of §1.2) and let $S$ be a vertex of $\mathcal S_T$.

$$\text{(sufficiency)}\quad G \text{ associated with } S,\ \ npv^{ij}(S)\ge0 \text{ on forward arcs},\ npv^{ij}(S)\le0 \text{ on backward arcs}\ \Longrightarrow\ S \text{ time-optimal};$$ $$\text{(necessity, } \beta<1)\quad S \text{ time-optimal}\ \Longrightarrow\ \exists\, G \text{ associated with } S \text{ satisfying the sign conditions}.$$

The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.

Milestones

1. §3.3.5: the net present value objective is binary-monotone and sum-separable.
2. §3.9.1: if $\mathcal S_T$ is nonempty and bounded, some vertex of $\mathcal S_T$ is time-optimal.
3. Proposition 3.2.16: every vertex of $\mathcal S_T$ has an associated spanning tree, an outtree rooted at $0$ if the vertex is a minimal point.
4. Proposition 3.5.4: a directed forest with at least one node has a source with at most one successor or a sink with exactly one predecessor.

Significance

Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.

The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.

Difficulty

The objective $f$ is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of $\mathcal S_T$ is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than $n+1$ temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree $V_{ij}$, forward and backward orientation relative to the root) have to be connected to the geometry of $\mathcal S_T$ through Proposition 3.2.16, whose proof in the book is a citation.

Formalization scope

Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. $\beta^x$ is Real.rpow, and every statement assumes $0<\beta\le1$ as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of $n+1$ arcs whose SimpleGraph.fromRel is connected; $V_{ij}$ is the set of nodes not reachable from $0$ once the arc is deleted.

Three readings are committed and disclosed in the item statements. Necessity is stated only for $\beta<1$: at $\beta=1$ the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from $0$ to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by $S_i\ge0$ rather than by arcs of $N$, and necessity fails. The existence of an optimal vertex assumes $\mathcal S_T$ nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns $PS\infty|temp,\bar d|f$ only.

The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of $N$ that are binding at $S$ and determine $S$ uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1 (p. 203), §3.3.5 (pp. 224–225), §3.5.2 (p. 252), §3.9.1 (pp. 333–334). https://doi.org/10.1007/978-3-540-24800-2
• A. H. Russell, "Cash flows in networks", Management Science 16 (1970), 357–373. https://doi.org/10.1287/mnsc.16.5.357
• R. C. Grinold, "The payment scheduling problem", Naval Research Logistics Quarterly 19 (1972), 123–136.
• C. Schwindt, J. Zimmermann, "A steepest ascent approach to maximizing the net present value of projects", Mathematical Methods of Operations Research 53 (2001), 435–450.
• C. Schwindt, J. Zimmermann, "Parametrische Optimierung als Instrument zur Bewertung von Investitionsprojekten", Zeitschrift für Betriebswirtschaft 72 (2002), 593–617.
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993.
• C. Berge, Graphs and Hypergraphs, North-Holland, Amsterdam, 1976.

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$. Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$, and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

$$\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}$$

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$, the derivatives $G_i'(v)$, $i\in I(v)$, are linearly independent in $V^*$.

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$, and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

$$F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,$$ $$\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.$$

Milestones, in the order of the paper's proof

1. (3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$; no regularity needed).
2. (3.16): at a regular feasible point $v$, every $h$ with $\langle G_i'(v),h\rangle=0$ ($i\le p$) and $\langle G_i'(v),h\rangle\ge0$ ($i>p$, $i\in I(v)$) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$.
3. Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$.
4. Lemma 3.3: an $\varepsilon$-Farkas–Minkowski lemma in $V^*$: if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$, then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$.

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$, $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$, then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$.

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$, but that function is not differentiable at $v_\varepsilon$, so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$; closing this gap requires the regularity assumption and completeness of $V$, and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$, must be turned into an approximate multiplier representation in $V^*$, an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

• $V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
• Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$, an equality constraint iff its index is $<p$. p ≤ m is assumed in the goal.
• $C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
• No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and "$F(v)\le\inf_{\mathcal C}F+\varepsilon^2$" is "$F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$". A real infimum over an empty or unbounded set would be a junk value.
• Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ($\inf\emptyset=+\infty$) while the conclusion asks for a feasible point.
• Lemma 3.3 is stated with $\le\varepsilon$. The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$, no constraints and $w^*=\varepsilon\,\mathrm{id}$; its proof gives $\le$, and Theorem 3.1 uses $\le$.
• Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
• Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$, so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$, and a closedness result for finitely generated cones in $V^*$.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$, a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$. The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$, and $\mathcal K=\mathrm{Conv}(\mathcal C)$. An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$. In round $t$ the learner plays a random arm $v_t\in\mathcal C$, pays $\ell_t^\top v_t$, and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$. The pseudo-regret is

$$\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .$$

A Legendre function on $\bar D$, for a nonempty open convex $D$, is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$. Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$, and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$.

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$. It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$. OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

$$\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}$$

A $0$-potential is a convex, $C^1$, increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$, $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$. It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$. With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$-potential $\psi$ and non-negative unbiased estimates,

$$\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].$$

For $\psi(x)=(-x)^{-q}$ with $q>1$, the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$,

$$\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.$$

Milestones

1. Lemma 5.1: $F^{**}=F$, $\nabla F^*=(\nabla F)^{-1}$ on $D^*$, and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$.
2. Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
3. Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$.
4. Theorem 5.5, linear losses, and its corrected general form.
5. Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$.
6. Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$.

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$, with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$. Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$. A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$.

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$, so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$, and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$.

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$, and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$, sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$, which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$, $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$.

Corrections and instantiations, each labelled in the item's Formalization Note:

• Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$. The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$, which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$.
• Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$. That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$. The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$, as the proof's first inequality does. The linear-loss bound is stated as printed.
• Lemma 5.2. "For all $z\in K\cap D$" is read as "for the projection $z$", which lies in $K\cap D$.
• Hypotheses made explicit: $q>1$; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$); a subgradient selection as an explicit input.
• Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$, $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$, a Lean division $x/0=0$, or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$.

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$-potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$, which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

• 1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
• 1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$.
• 1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
• 1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
• Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$, where $1\le k\le\min(m,n)$, keeps $k$ rows and $k$ columns of $A$. The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$. So $\Delta(0)=0$, and $\Delta(A)\ge 1$ whenever $A\ne 0$. Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$.

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$. An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$. For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$. A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$, $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$.

If $ay\le\beta$ for all $y\in P$, with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$. The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$. Then $P_I\subseteq P^{(i)}$ for all $i$. The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$. The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$.

Formalization targets

Goal: Theorem 10 (p. 260)

$$\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.$$

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$.

Milestones, in attack order

1. Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$-distance $n\Delta(A)$, and every IP optimum has an LP optimum within the same distance.
2. Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$.
3. Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$. This result is off the goal's path.
4. Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$-distance $n\Delta(A)$.
5. Theorem 7 (p. 257). A single integral matrix $M$, with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
6. Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$.
7. Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$.

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$. They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$: polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$. That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$. Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$, and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

• Rationality. Everything is over $\mathbb{Q}$, following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$, and a polyhedron is a finite system of rational inequalities.
• $\Delta(A)$. Only nonempty submatrices count, so $\Delta(0)=0$.
• Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
• Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$, using all integral $a$ and rational $\beta$. The rank is valued in $\mathbb{N}\cup\{\infty\}$, with $\infty$ if no iterate equals $P_I$. A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$, as printed.
• Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$. For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
• Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$.

A complete development needs the following:

• cone generation with Cramer bounds and Carathéodory's theorem;
• LP duality and Farkas' lemma over $\mathbb{Q}$;
• the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
• Schrijver's face lemma and unimodular invariance;
• a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

• W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
• V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
• A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
• W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
• F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322