Operations Research

Motivation

Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.

The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).

This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.

Setting

Let $A$ be a real matrix with $m$ rows and $n$ columns, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Vector inequalities are componentwise. The primal and dual linear programs are

$$\text{(P)}\quad\max\ c^{T}x \ \text{ s.t. } Ax\le b,\ x\ge 0, \qquad\qquad \text{(D)}\quad\min\ b^{T}y \ \text{ s.t. } A^{T}y\ge c,\ y\ge 0.$$

A feasible solution of (P) is an $x\in\mathbb{R}^n$ satisfying its constraints; an optimal solution is a feasible $x^*$ with $c^{T}x\le c^{T}x^*$ for every feasible $x$. (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal $y^*$ has $b^{T}y^*\le b^{T}y$ for all feasible $y$, and (D) is unbounded if $b^{T}y$ takes arbitrarily small values.

For $a_1,\dots,a_n\in\mathbb{R}^m$, the convex cone generated by them is $C=\{t_1a_1+\dots+t_na_n : t_i\ge 0\}$; a primitive cone is one generated by $k\le m$ linearly independent vectors. A system $Ax\le b$ of $m$ inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.

Formalization targets

Goal: the duality theorem (§6.1, p. 83)

For (P) and (D) as above, exactly one of the following occurs:

1. neither (P) nor (D) is feasible;
2. (P) is unbounded and (D) is infeasible;
3. (P) is infeasible and (D) is unbounded;
4. both are feasible; then both have optimal solutions, and every optimal $x^*$ of (P) and optimal $y^*$ of (D) satisfy

$$c^{T}x^*=b^{T}y^*.$$

Milestones

• Proposition 6.1.1 (weak duality). $c^{T}x\le b^{T}y$ for all feasible $x$ of (P) and $y$ of (D); hence (P) unbounded forces (D) infeasible, and (D) unbounded forces (P) infeasible.
• Proposition 6.4.1 (Farkas lemma). Exactly one of: $Ax=b$ has a solution $x\ge 0$; some $y$ has $y^{T}A\ge 0^{T}$ and $y^{T}b<0$. Already on the platform as LinearOptimization.farkas_lemma (Proved) and linked as a reference.
• Proposition 6.4.3 (three variants). Solvability of $Ax=b$, $x\ge0$; of $Ax\le b$, $x\ge 0$; and of $Ax\le b$ with $x$ free, each characterized by a certificate condition on $y$.
• Proposition 6.4.2 (geometric Farkas lemma). $b$ lies in the cone generated by $a_1,\dots,a_n$, or a hyperplane through $0$ separates the cone from $b$ strictly — exactly one.
• Lemmas 6.5.4, 6.5.5, 6.5.3, 6.5.1. Primitive cones are closed; a finitely generated cone is a finite union of primitive cones; hence it is closed (6.5.3, on the platform as Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any $b\notin C$.
• Lemmas 6.6.2 and 6.6.1. $Ax=b$ is solvable iff every $y$ with $y^{T}A=0^{T}$ has $y^{T}b=0$; in a minimally infeasible system, for every $i$ some $\tilde x^{(i)}$ satisfies all inequalities except the $i$th with equality.

Significance

The result. The duality theorem converts optimality into feasibility: a pair $(x,y)$ of primal and dual feasible solutions with $c^{T}x=b^{T}y$ is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.

Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.

Difficulty

Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over $\mathbb{R}$: either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to $b$ — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.

Formalization scope

• Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. The row vector $y^{T}A$ is Aᵀ *ᵥ y, so $y^{T}A\ge 0^{T}$ is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.
• Optimal solutions and unboundedness are stated against every feasible point; no sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case $k$ at index $k-1$; a plain disjunction would be weaker than the book.
• Cone items live in EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and $y^{T}x$ is the inner product. The convex cone generated by $a_1,\dots,a_n$ is the set of nonnegative combinations (it contains $0$, also for $n=0$).
• A trivializing formalization — case 4 read as "if both have optimal solutions then their values agree", which is weak duality plus nothing — is ruled out: case 4 asserts the existence of both optima from feasibility alone.
• Lemma 6.3.1 (the dual solution read off the final simplex tableau) and Lemma 6.5.2 (nearest point in a nonempty closed set, available in Mathlib as IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.
• Contributions welcome: proofs of any milestone, the two Farkas-lemma chains, and bridges to the general-form duality already on the platform.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 6. https://doi.org/10.1007/978-3-540-30717-4
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• 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.
• M. Conforti, M. Di Summa and G. Zambelli, Minimally infeasible set-partitioning problems with balanced constraints, Mathematics of Operations Research (cited in the book as to appear; the source of the proof in §6.6).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 4.

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

Motivation

Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of $\mathrm{conv}(X)$ does not give back the integer program, because an optimal integer point may lie in the interior of $\mathrm{conv}(X)$.

Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.

Setting

Let $D$ be an $m \times n$ matrix and $\mathbf d$ an $m$-vector with rational entries. The polyhedron is

$$P = \{\mathbf x \in \mathbb R^n \mid D\mathbf x \geqslant \mathbf d,\ \mathbf x \geqslant \mathbf 0\},$$

and its set of integer points is $X = P \cap \mathbb Z^n$, the points of $P$ whose coordinates are all integers. Because $P \subseteq \mathbb R^n_+$, $X = P \cap \mathbb Z^n_+$.

The recession cone of $P$ is $\{\mathbf r \in \mathbb R^n \mid D\mathbf r \geqslant \mathbf 0,\ \mathbf r \geqslant \mathbf 0\}$. An integer ray of $P$ is a nonzero vector of $\mathbb Z^n$ in this cone. Extreme rays are not required.

In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

If $P \neq \emptyset$, there exist a finite set of integer points $\{\mathbf p_q\}_{q \in Q} \subseteq X$ and a finite set of integer rays $\{\mathbf p_r\}_{r \in R}$ of $P$ such that

$$X = \Bigl\{\mathbf x \in \mathbb R^n_+ \ \Big|\ \mathbf x = \sum_{q \in Q} \mathbf p_q \lambda_q + \sum_{r \in R} \mathbf p_r \lambda_r,\ \sum_{q \in Q} \lambda_q = 1,\ \boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}\Bigr\}. \qquad (24)$$

Since the multipliers are nonnegative integers summing to one over $Q$, (24) says that $X$ is the union, over $q \in Q$, of the translates $\mathbf p_q + \mathbb Z_+\{\mathbf p_r\}_{r\in R}$ of the monoid generated by the rays. No bound on $|Q|$ or $|R|$ is part of the goal.

Milestone: Remark in §3.3 (p. 1012)

If $X \subseteq [0,1]^n$, every point of $X$ is a vertex of $\mathrm{conv}(X)$. In this case convexification and discretization coincide.

Significance

The result. Theorem 1 converts an integer program $\min\{c(\mathbf x) \mid A\mathbf x \geqslant \mathbf b,\ \mathbf x \in X\}$ into the integer master program (25) over the multipliers $\boldsymbol\lambda$, with one column per generating point and per generating ray. When $X$ is bounded the rays disappear, exactly one $\lambda_q$ equals one, and (25) is a linear integer program even for a nonlinear cost $c$. The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.

Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over $\mathrm{conv}(X)$, is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.

Difficulty

The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of $P$ need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of $P$ generate the recession cone over $\mathbb R_+$, but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of $Q$ is also not automatic: $X$ itself is typically infinite, and taking $Q = X$ trivializes the statement.

Rationality of the data is essential. For $P = \{\mathbf x \in \mathbb R^2_+ \mid \sqrt2\,x_1 - x_2 \geqslant 0\}$, every integer ray has slope below $\sqrt 2$, so finitely many base points and rays generate only points with $x_2 \leqslant \rho x_1 + C$ for some $\rho < \sqrt 2$, while $X$ contains $(k, \lfloor\sqrt2 k\rfloor)$ for every $k$.

Formalization scope

• Vectors are Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.
• $D$ and $\mathbf d$ are ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.
• The hypothesis $P \neq \emptyset$ is kept as on the page. $X$ may still be empty (e.g. $P = \{1/2\}$); then $Q = \emptyset$ and both sides of (24) are empty. The statement allows this.
• $Q$ and $R$ are Fin k and Fin l for existentially chosen $k, l \in \mathbb N$; the finiteness is the content of the theorem. The multiplier vector $\boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}$ is written as a pair of ℕ-valued vectors.
• "Integer rays of $P$" is read as nonzero integer vectors in the recession cone $\{D\mathbf r \geqslant \mathbf 0, \mathbf r \geqslant \mathbf 0\}$; extremality is not required, as the page does not require it (contrast (8), which says "extreme rays").
• The constraint $\mathbf x \in \mathbb R^n_+$ on the right side of (24) is kept although it is implied.
• In the Remark, "vertices of $\mathrm{conv}(X)$" is read as extreme points of the convex hull; $X$ is finite there, so the two notions agree.

A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with $Q$ or $R$ infinite would be trivial; both are excluded by the statement.

Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• G. L. Nemhauser and L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• R. R. Meyer, On the existence of optimal solutions to integer and mixed-integer programming problems, Mathematical Programming 7:223–235, 1974. https://doi.org/10.1007/BF01585518
• F. Vanderbeck, On Dantzig–Wolfe decomposition in integer programming and ways to perform branching in a branch-and-price algorithm, Operations Research 48(1):111–128, 2000. https://doi.org/10.1287/opre.48.1.111.12453
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$. Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$, $d$, $d$. These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic two-server ratio is $2$.
• 1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
• Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$-server conjecture.

Setting

Fix an integer $d\ge1$. The isosceles triangle $M$ has three points $a$, $b$, $c$ with

$$\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.$$

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$. A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$. It is $\rho$-competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

$$\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.$$

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

$$\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.$$

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$:

$$\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,$$ $$\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.$$

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

$$(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,$$

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$, $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

$$\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}$$

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$, it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$. The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

• The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$, with $d$ a natural number and $d\ge1$. Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
• Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
• The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
• In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
• "Grows" in the limit remark is read as strictly increasing.
• The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$. The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$.

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
• S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk $\delta$. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity $\mathbb E_{\boldsymbol\mu}[\tau_\delta]$, the expected number of samples a strategy takes before stopping.

Timeline of the question this mission formalizes:

• Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
• Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every $\delta$-PAC strategy (arXiv:1407.4443).
• Garivier and Kaufmann (COLT 2016) identified the exact constant $T^*(\boldsymbol\mu)$ in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as $\delta\to0$ (arXiv:1602.04589). This mission covers the upper-bound half of that paper.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$; $b$ is twice differentiable and strictly convex, and $\nu_\theta$ has mean $\dot b(\theta)$. Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence $d(\mu,\mu')$ is the Kullback–Leibler divergence between the members with means $\mu$ and $\mu'$.

A bandit model $\boldsymbol\mu=(\mu_1,\dots,\mu_K)$ assigns a member of the family to each arm. The class $\mathcal S$ consists of models with a unique optimal arm $a^*(\boldsymbol\mu)$. At each round $t=1,2,\dots$ the learner picks an arm $A_t$ as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time $\tau_\delta$ recommends an arm. $N_a(t)$ is the number of draws of arm $a$ in the first $t$ rounds and $\hat\mu_a(t)$ its empirical mean.

With $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S: a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ and $\Sigma_K$ the probability simplex, the characteristic time is

$$T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}\ \inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\ \sum_{a=1}^K w_a\,d(\mu_a,\lambda_a),$$

and the maximizer $w^*(\boldsymbol\mu)$ are the optimal proportions of arm draws.

Track-and-Stop combines two ingredients:

• a sampling rule that tracks the plug-in proportions $w^*(\hat{\boldsymbol\mu}(t))$ while forcing each arm to be drawn about $\sqrt t$ times: C-Tracking tracks the cumulated sum of projections of $w^*(\hat{\boldsymbol\mu}(s))$ onto $\Sigma^{\epsilon_s}_K=\{w\in\Sigma_K: w_a\ge\epsilon_s\}$, $\epsilon_s=(K^2+s)^{-1/2}/2$; D-Tracking draws an under-sampled arm when some $N_a(t)<\sqrt t-K/2$, and otherwise the arm maximizing $t\,w^*_a(\hat{\boldsymbol\mu}(t))-N_a(t)$;
• Chernoff's stopping rule, which stops at the first $t$ at which some arm $a$ beats every other arm $b$ in a generalized likelihood ratio test, $Z_{a,b}(t)>\beta(t,\delta)$, here with $\beta(t,\delta)=\log(r(t)/\delta)$.

Formalization targets

Goal: Theorem 14 (p. 13)

For $\alpha\in[1,e/2]$ and $r(t)=O(t^\alpha)$, Chernoff's stopping rule with $\beta(t,\delta)=\log(r(t)/\delta)$ combined with C-Tracking or D-Tracking satisfies

$$\limsup_{\delta\to0}\frac{\mathbb E_{\boldsymbol\mu}[\tau_\delta]}{\log(1/\delta)}\le\alpha\,T^*(\boldsymbol\mu)$$

for every $\boldsymbol\mu\in\mathcal S$.

Milestones

• Lemma 15 (p. 20): greedy tracking of cumulated proportions $P(k)$ keeps $\max_i|N_i(n)-P_i(n)|\le K-1$.
• Lemma 7 (p. 7): C-Tracking ensures $N_a(t)\ge\sqrt{t+K^2}-2K$ and $\max_a|N_a(t)-\sum_{s<t}w^*_a(\hat{\boldsymbol\mu}(s))|\le K(1+\sqrt t)$.
• Lemma 8 (p. 7): D-Tracking ensures $N_a(t)\ge(\sqrt t-K/2)_+-1$, and proportions within $3(K-1)\epsilon$ of $w^*(\boldsymbol\mu)$ after a time $t_\epsilon$ that does not depend on the trajectory, once the plug-in targets are within $\epsilon$.
• Proposition 9 (p. 8): under either rule, $N_a(t)/t\to w^*_a(\boldsymbol\mu)$ almost surely.
• Lemma 18 (p. 27): an explicit $x$ with $c_1x\ge\log(c_2x^\alpha)$ for $\alpha\in[1,e/2]$.
• Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to $w^*$, $\tau_\delta<\infty$ almost surely and $\limsup_{\delta\to0}\tau_\delta/\log(1/\delta)\le\alpha T^*(\boldsymbol\mu)$ almost surely.

Significance

Theorem 1 of the same paper shows $\mathbb E_{\boldsymbol\mu}[\tau_\delta]\ge T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ for every $\delta$-PAC strategy, and $\mathrm{kl}(\delta,1-\delta)\sim\log(1/\delta)$. Theorem 14 with $\alpha=1$ therefore shows that the lower bound is attained: $T^*(\boldsymbol\mu)$ is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.

The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.

Difficulty

The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of $\tau_\delta/\log(1/\delta)$ does not control $\mathbb E[\tau_\delta]$, because on the rare events where the empirical means are far from $\boldsymbol\mu$ the stopping time may be very large. Theorem 14 needs a quantitative concentration of $\hat{\boldsymbol\mu}(t)$ on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the $\sqrt t$ lower bounds on $N_a(t)$ (the concentration step of App. D, Lemmas 19–20).

A second obstacle is the regularity of $w^*$: the tracking lemmas only transfer convergence of $\hat{\boldsymbol\mu}(t)$ to convergence of $N_a(t)/t$ through the continuity of $\boldsymbol\mu\mapsto w^*(\boldsymbol\mu)$ on $\mathcal S$, proved from the characterization of $w^*$ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near $\boldsymbol\mu$, which requires the empirical means to lie in the interior of the mean space.

Formalization scope

• Model. The exponential family is a structure $(\xi,\Theta,b)$ with $\Theta$ a nonempty open interval, each $\nu_\theta$ normalized, $b$ twice continuously differentiable and $\ddot b>0$ on $\Theta$. Openness and $\ddot b>0$ are added to the paper's "convex, twice differentiable"; strict convexity is what makes $\nu^\mu$ unique. Bandit models are parameter vectors $\theta\in\Theta^K$ with $K\ge2$; arms are indexed $0,\dots,K-1$. $\mathcal S$ is the set of parameter vectors with a unique arm of largest mean $\dot b(\theta_a)$.
• Protocol. Policies, the trajectory law $\mathbb P_{\boldsymbol\mu}$, pull counts, empirical means and $T^*(\boldsymbol\mu)$ are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). $T^*$ uses Kullback–Leibler divergences of the arm laws over the class $\mathcal S$ and takes values in $[0,\infty]$. Trajectory coordinate $t$ is round $t+1$. An arm never drawn has empirical mean $0$.
• Target map. $w^*(\hat{\boldsymbol\mu}(t))$ is undefined in the paper when $\hat{\boldsymbol\mu}(t)\notin\mathcal S$ (an unsampled arm, ties, a mean outside $\dot b(\Theta)$). Every tracking statement quantifies over every target map with values in $\Sigma_K$ that returns optimal proportions on $\mathcal S$, over every choice of $L^\infty$ projections, and over every tie-breaking, including randomized ones.
• Stopping rule. The two maxima in $Z_{a,b}(t)$ are suprema over $\Theta$ in the extended reals. $Z_{a,b}(t)>\beta$ is written without subtracting infinities. The stopping time is the first $t\ge1$ at which the test succeeds, $+\infty$ if none. "$r(t)=O(t^\alpha)$" is $r(t)\le Dt^\alpha$ for $t\ge1$; $r>0$ is added so that $\log(r(t)/\delta)$ is defined.
• Values in $[0,\infty]$. Expectations of $\tau_\delta$, the ratios and $T^*$ live in $[0,\infty]$. No statement converts them to reals, so an infinite expected stopping time is never read as $0$.
• Corrections, disclosed. Proposition 9's printed $\mathbb P_w$ is $\mathbb P_{\boldsymbol\mu}$. Lemma 18 adds $c_2/c_1^\alpha>1$ and $x>0$, without which its expressions are undefined.
• Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
• Welcome contributions. Exponential-family facts ($\dot b$ is the mean, the KL formula, concentration of empirical means); the continuity of $w^*$ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
• H. Chernoff, Sequential Design of Experiments, Ann. Math. Statist. 30(3), 1959. doi:10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 33. doi:10.1017/9781108571401

Motivation

Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces $K$ unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed $\delta$. The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.

Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant $T^*(\boldsymbol\mu)$ is exactly matched, as $\delta \to 0$, by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).

Setting

A canonical one-parameter exponential family is given by a reference measure $\xi$ on $\mathbb R$, an open interval $\Theta \subset \mathbb R$ and a function $b$, twice continuously differentiable on $\Theta$ with $\ddot b > 0$, such that the laws $\nu_\theta$ with density $\exp(\theta x - b(\theta))$ with respect to $\xi$ are probability measures for $\theta \in \Theta$. The mean of $\nu_\theta$ is $\dot b(\theta)$. Bernoulli laws and Gaussian laws of known variance are examples.

A bandit model is a vector $\theta = (\theta_1, \dots, \theta_K) \in \Theta^K$; arm $a$ returns i.i.d. rewards with law $\nu_{\theta_a}$ and mean $\mu_a = \dot b(\theta_a)$. Arm $a^*(\boldsymbol\mu)$ is the unique optimal arm if $\mu_{a^*} > \mu_a$ for every $a \ne a^*$. Let $\mathcal S$ be any set of bandit models of the family each having a unique optimal arm, and put $\mathrm{Alt}(\boldsymbol\mu) = \{\boldsymbol\lambda \in \mathcal S : a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)\}$.

A strategy consists of a sampling rule $\pi$ (the arm $A_t$ drawn at round $t$ depends, possibly with extra randomization, on the first $t - 1$ observations), a stopping time $\tau$ of the natural filtration $\mathcal F_t = \sigma(A_1, X_1, \dots, A_t, X_t)$, and an $\mathcal F_\tau$-measurable decision $\hat a_\tau$. It is $\delta$-PAC on $\mathcal S$ if for every $\boldsymbol\mu \in \mathcal S$, $\mathbb P_{\boldsymbol\mu}(\tau < \infty) = 1$ and $\mathbb P_{\boldsymbol\mu}(\hat a_\tau \ne a^*(\boldsymbol\mu)) \le \delta$. $N_a(t)$ is the number of draws of arm $a$ among the first $t$ rounds.

Write $d(\mu_a, \lambda_a) = \mathrm{KL}(\nu_{\theta_a}, \nu_{\lambda_a})$ for the divergence between two arm laws, $\mathrm{kl}(x, y) = x\log\frac{x}{y} + (1 - x)\log\frac{1 - x}{1 - y}$, and $\Sigma_K$ for the probability simplex on the $K$ arms. The characteristic time is defined by eq. (1):

$$T^*(\boldsymbol\mu)^{-1} = \sup_{w \in \Sigma_K}\ \inf_{\boldsymbol\lambda \in \mathrm{Alt}(\boldsymbol\mu)} \sum_{a=1}^K w_a\, d(\mu_a, \lambda_a).$$

Formalization targets

Goal: Theorem 1 (p. 3)

For $\delta \in (0, 1/2]$, every $\delta$-PAC strategy on $\mathcal S$ and every $\boldsymbol\mu \in \mathcal S$,

$$\mathbb E_{\boldsymbol\mu}[\tau] \ \ge\ T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta, 1 - \delta).$$

The statement fixes no constant beyond those of the paper, and it holds for every $\delta$, not only in the limit.

Milestone: eq. (2) (p. 4)

For every $\boldsymbol\lambda \in \mathcal S$ with $a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)$,

$$\sum_{a=1}^K d(\mu_a, \lambda_a)\, \mathbb E_{\boldsymbol\mu}[N_a(\tau)] \ \ge\ \mathrm{kl}(\delta, 1 - \delta).$$

This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.

Significance

Theorem 1 identifies $T^*(\boldsymbol\mu)$ as the exact problem-dependent complexity of fixed-confidence best arm identification: since $\mathrm{kl}(\delta, 1 - \delta) \sim \log(1/\delta)$, it gives $\liminf_{\delta \to 0} \mathbb E_{\boldsymbol\mu}[\tau_\delta]/\log(1/\delta) \ge T^*(\boldsymbol\mu)$, and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer $w^*(\boldsymbol\mu)$ of eq. (1) (mission II).

Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant $\log(1/(4\delta))$; for $\delta \le 1/2$, $\mathrm{kl}(\delta, 1 - \delta) \ge \log(1/(2.4\delta)) > \log(1/(4\delta))$, so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.

Difficulty

The obvious proof applies the finite-horizon divergence decomposition $\mathrm{KL}(\mathbb P^n_{\boldsymbol\mu}, \mathbb P^n_{\boldsymbol\lambda}) = \sum_a \mathbb E_{\boldsymbol\mu}[N_a(n)]\,d(\mu_a, \lambda_a)$ at a deterministic horizon $n$. That fails here: $\tau$ is random and unbounded, the decision is $\mathcal F_\tau$-measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into $\mathrm{kl}(\delta, 1 - \delta)$, is the central difficulty. A second, smaller difficulty is to identify the paper's divergence $d$ and its means $\dot b(\theta)$ with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.

Formalization scope

Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); $\mathrm{kl}$ is the platform's bernoulliRelativeEntropy and $N_a(t)$ is trajPullCount. Conventions:

• arms are Fin K, 0-based (the paper's arm $a$ is index $a - 1$); trajectory coordinate $t$ is round $t + 1$;
• $\Theta$ is a nonempty open interval and $\ddot b > 0$ on $\Theta$ (added: the paper says $b$ is convex and twice differentiable; strict convexity is what makes "the unique distribution with mean $\mu$" meaningful); the paper's $d$ is written as the KL divergence of the arm laws (its first equality on p. 3), and the unique optimal arm is defined through the parameter means $\dot b(\theta_a)$;
• $\mathcal S$ is an arbitrary set of models with a unique optimal arm, not the specific set the paper fixes from p. 4 on;
• $\delta$-PAC keeps both halves of the paper's definition (almost-sure stopping and error at most $\delta$);
• $T^*(\boldsymbol\mu)$, divergences and expectations of $\tau$ take values in $[0, \infty]$, never truncated to reals; $T^* = 0$ when $\mathrm{Alt}(\boldsymbol\mu) = \emptyset$ and $T^* = \infty$ when the supremum in eq. (1) is $0$;
• $\delta \le 1/2$ is added. The paper states $\delta \in (0, 1)$, but the theorem and eq. (2) are false for $\delta \in (1/2, 1)$: with two unit-variance Gaussian arms, drawing arm 1 once and naming arm 1 exactly when the fractional part of the reward is below $1/2$ is $0.9$-PAC, while $T^*(\boldsymbol\mu) \to \infty$ as the two means merge. At $\delta = 1/2$ the bound is $0$.

A statement with $\log(1/(4\delta))$ in place of $\mathrm{kl}(\delta, 1 - \delta)$, or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates $\mathbb E[\tau]$ or $T^*$ to real numbers.

Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an $\mathcal F_\tau$-measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of $\nu_\theta$ $= \dot b(\theta)$" and "KL of two family members $= b(\theta') - b(\theta) - \dot b(\theta)(\theta' - \theta)$", and $\mathbb E[\tau] = \sum_a \mathbb E[N_a(\tau)]$. All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, Journal of Machine Learning Research 17(1), 2016. https://arxiv.org/abs/1407.4443
• T. L. Graves, T. L. Lai, Asymptotically Efficient Adaptive Choice of Control Laws in Controlled Markov Chains, SIAM Journal on Control and Optimization 35(3), 1997. https://doi.org/10.1137/S0363012994275440
• S. Mannor, J. N. Tsitsiklis, The Sample Complexity of Exploration in the Multi-Armed Bandit Problem, Journal of Machine Learning Research 5, 2004. https://www.jmlr.org/papers/v5/mannor04b.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

Motivation

The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of $d$ actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.

The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time $t$ (or with a horizon $n$ fixed in advance), and its guarantee is on the expected regret, which grows like $\log n$. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.

Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the $d$-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB($\delta$), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least $1-\delta$. This mission formalizes that section.

Setting

There are $d \ge 1$ arms with unknown means $\mu_1, \dots, \mu_d \in \mathbb R$. Write $\mu_* = \max_{1 \le i \le d} \mu_i$ for the best mean and $\Delta_i = \mu_* - \mu_i \ge 0$ for the gap of arm $i$.

Randomness lives on a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_t)_{t \ge 0}$. In round $t = 1, 2, \dots$ the learner plays an arm $I_t$ that is $\mathcal F_{t-1}$-measurable and receives the reward $\mu_{I_t} + \eta_t$. The noise $\eta_t$ is $\mathcal F_t$-measurable and conditionally 1-sub-Gaussian:

$$\mathbf E\left[e^{\lambda\eta_t} \mid \mathcal F_{t-1}\right] \le e^{\lambda^2/2} \qquad \text{for all } \lambda \in \mathbb R .$$

The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.

After $t$ rounds, $N_{i,t}$ is the number of plays of arm $i$ and $\overline X_{i,t}$ is the average reward received from it. For a confidence level $\delta > 0$ the confidence width is

$$c_{i,t} = \sqrt{\frac{1 + N_{i,t}}{N_{i,t}^2}\left(1 + 2\log\frac{d\,(1 + N_{i,t})^{1/2}}{\delta}\right)} \qquad (3)$$

with $c_{i,t} = +\infty$ when $N_{i,t} = 0$. UCB($\delta$) plays, in round $t$, an arm that maximizes $\overline X_{i,t-1} + c_{i,t-1}$; in particular every arm is played once before any comparison is made. The pseudo-regret after $n$ rounds is

$$R_n = \sum_{t=1}^n \left(\mu_* - \mu_{I_t}\right).$$

This is the linear bandit of the paper with the standard basis of $\mathbb R^d$ as decision set and $\theta_* = \mu$.

Formalization targets

Goal: Theorem 7 (constant regret of UCB($\delta$))

For every $\delta > 0$, with probability at least $1-\delta$, for all $n \ge 0$ simultaneously,

$$R_n \le \sum_{i : \Delta_i > 0}\left(3\Delta_i + \frac{16}{\Delta_i}\log\frac{2d}{\Delta_i\delta}\right).$$

The right-hand side depends only on the gaps, $d$ and $\delta$.

Milestone: Lemma 6 (confidence intervals)

For any adapted choice of arms (not only UCB($\delta$)) and every $\delta > 0$, with probability at least $1-\delta$,

$$|\overline X_{i,t} - \mu_i| \le c_{i,t} \qquad \text{for all arms } i \text{ and all } t \ge 0 .$$

Significance

The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability $1-\delta$ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability $\delta$ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.

Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for $V = \lambda I$ and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.

Difficulty

Two points separate this from textbook UCB analyses. First, the number of samples $N_{i,t}$ of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of $t$: a union bound over all $t$ costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale $\sum_s \eta_s \mathbf 1\{I_s = i\}$. Second, the regret statement is uniform in $n$ with constants depending on the gaps; converting a condition of the form "$c(N) \ge \Delta_i/2$" into an explicit bound on $N$ requires solving an inequality in which $N$ appears both polynomially and inside a logarithm, and the explicit constants $3$ and $16$ must come out of that step.

Formalization scope

The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.

• Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, $\mu_*$ is ⨆ i, μ i (the maximum over a nonempty finite type).
• Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index $0$ are unused.
• The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
• "With probability at least $1-\delta$, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most $\delta$. For $\delta \ge 1$ the statements are trivially true, as in the paper.
• The rule (4) is read with the statistics of rounds $1, \dots, t-1$, because the printed $\overline X_{i,t}$, $c_{i,t}$ already count round $t$. An unplayed arm, whose width is $+\infty$ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
• The printed Theorem 7 has no quantifier on $n$; it is formalized in the uniform-in-$n$ form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
• Lean's division by zero makes $\overline X_{i,t}$ and $c_{i,t}$ equal to $0$ when $N_{i,t} = 0$. Lemma 6 therefore excludes $N_{i,t} = 0$ explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with $\Delta_i > 0$, so its divisions are well defined.

A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.

Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case ($d = 1$, $\lambda = 1$, $A_s = \mathbf 1\{I_s = i\}$, $\overline V_t = 1 + N_{i,t}$), a union bound over arms, and elementary inequalities inverting $N \mapsto \frac{1+N}{N^2}(1 + 2\log(d\sqrt{1+N}/\delta))$. Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• T. L. Lai, H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation tradeoff using variance estimates in multi-armed bandits, Theoretical Computer Science 410, 2009. https://doi.org/10.1016/j.tcs.2009.01.016