All missions

Motivation

Interior-point methods for linear programming generate a sequence of strictly positive primal-dual points that converges to the optimal set but never reaches it. The simplex method, by contrast, stops at an exact optimal vertex. Practical solvers and sensitivity analysis both need an exact answer: which variables are positive at optimality, and what the exact optimal solution is. The question of finite termination, of when an interior iterate carries enough information to recover an exact solution, was settled in the early 1990s (Ye 1992, doi:10.1007/BF01581087; Güler and Ye 1993, doi:10.1007/BF01580610; Mehrotra and Ye 1993, doi:10.1007/BF01585180).

Chapter 5 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) presents the answer for real data. It works under the real-number model of computation, where the data are real rather than integers of bit length $L$. Once the duality gap of a well-centered iterate is below a threshold set by a condition number $\xi(A,b,c)$ of the data, the comparison $x_j\ge s_j$ identifies the strict complementarity partition exactly. That happens after a number of iterations polynomial in $\sqrt n$, $\log(R/\xi^2)$ and $\log n$. The chapter also bounds the arithmetic cost of an iteration through rank-one updating (§5.1).

Setting

Let $A$ be a real $m\times n$ matrix with $n\ge1$, $b\in\mathbb R^m$, $c\in\mathbb R^n$. The standard-form pair is

$$(\mathrm{LP})\ \min\{c^Tx: Ax=b,\ x\ge0\},\qquad (\mathrm{LD})\ \max\{b^Ty: A^Ty+s=c,\ s\ge0\}.$$

Vector inequalities are componentwise. A triple $(x,y,s)$ is an interior point if $Ax=b$, $x>0$, $A^Ty+s=c$, $s>0$.

The strict complementarity partition $(P^*,Z^*)$ is defined as follows: $P^*$ is the set of indices $j$ with $x_j>0$ for some optimal $x$, and $Z^*$ is the set of indices with $s_j>0$ for some optimal $(y,s)$. When optimal solutions exist, these two sets partition $\{1,\dots,n\}$ (Goldman–Tucker; the book's Theorem 1.14). The optimal faces are

$$\Omega_p=\{x: Ax=b,\ x\ge0,\ x_{Z^*}=0\},\qquad \Omega_d=\{(y,s): A^Ty+s=c,\ s\ge0,\ s_{P^*}=0\}.$$

The condition number (5.3) is

$$\xi(A,b,c)=\min\Big\{\min_{j\in P^*}\max_{x\in\Omega_p}x_j,\ \min_{j\in Z^*}\max_{(y,s)\in\Omega_d}s_j\Big\}.$$

It is how far the optimal faces reach into the open orthant. For an iterate $(x^k,s^k)$ let $\sigma^k=\{j: x^k_j\ge s^k_j\}$.

An interior-point sequence has property (5.7) with constant $\eta>0$ if $\min_j x^k_js^k_j/((x^k)^Ts^k)>n^{-\eta}$ for every $k$, i.e. it stays away from the boundary relative to its gap. It satisfies the polynomial bound with constant $\kappa>0$ if $(x^k)^Ts^k\le R\,e^{-\kappa k/\sqrt n}$, where $R\ge(x^0)^Ts^0$ (the chapter's standing assumption, p. 147).

For §5.1, given positive iterates $x^t$, the rank-one updating scaling is defined by $d^0=x^0$, and $d^t_j=d^{t-1}_j$ if $1/1.1\le d^{t-1}_j/x^t_j\le1.1$, else $d^t_j=x^t_j$. The update set $I^t$ collects the indices that were reset at iteration $t$.

Formalization targets

Goal: Theorem 5.3

For every interior sequence with property (5.7) and the polynomial bound,

$$\sigma^k=P^*\qquad\text{for all }k\ge K=\Big\lceil\frac{\sqrt n}{\kappa}\Big(\log\frac{R}{\xi(A,b,c)^2}+\eta\log n\Big)\Big\rceil.$$

Milestones

• Lemma 5.1: $\|(D^t)^{-1}(x^t-d^t)\|_\infty\le0.1$ for every $t$, and $\sum_{t=1}^k|I^t|\le11\sqrt n\sum_{t=1}^k\|(D^{t-1})^{-1}(x^t-x^{t-1})\|$.
• (5.3): with an interior point, the optimal faces have strictly feasible solutions, the maxima over them are attained, and $\xi(A,b,c)>0$.
• (5.4): for an interior point and $x^*\in\Omega_p$, $(y^*,s^*)\in\Omega_d$: $\sum_{i\in P^*}x^*_is^k_i+\sum_{i\in Z^*}s^*_ix^k_i=(x^k)^Ts^k$.
• (5.5): for $j\in P^*$, $s^k_j\le(x^k)^Ts^k/x^*_j$, and $(x^k)^Ts^k<\epsilon$ implies $s^k_j<\epsilon/\xi$.
• (5.8): under (5.7), $x^k_j>n^{-\eta}x^*_j\ge n^{-\eta}\xi$ for $j\in P^*$.
• Proof of Theorem 5.3: under (5.7) and $(x^k)^Ts^k\le n^{-\eta}\xi^2$, $\sigma^k=P^*$.

The mission also references Proposition 5.5 (skew-symmetric self-dual programs are self-dual with optimal value zero), already proved on the platform as SelfDualLP.Complexity.proposition_1.

Significance

Theorem 5.3 shows that an interior-point method has a finite, data-dependent termination time. After $K$ iterations the partition is known. Projecting the iterate onto $\{x: A_{P^*}x_{P^*}=b\}$ and the dual face then costs one least-squares solve and yields an exact optimal pair (§5.2.2). The iteration count depends on the data only through $\xi(A,b,c)$, not on a bit length. This is what makes the result meaningful under the real-number model. Lemma 5.1 is the counting step behind the $\sqrt n$ saving in arithmetic operations: the number of rank-one corrections to the normal matrix is controlled by the scaled movement of the iterates.

None of these results is on the platform. The homogeneous self-dual results of §5.3 are already posed there from the Ye–Todd–Mizuno paper and are not re-posed. A formal proof would give the first machine-checked statement linking the duality gap, centrality and the optimal partition. That link is reused in the analysis of predictor directions (Chapter 7) and in basis identification.

Difficulty

The arithmetic of the proof is short; the difficulty is in the linear-programming facts it rests on. First, the existence of a strictly complementary pair, so that $P^*$ and $Z^*$ cover all indices and are disjoint. Without it, $\sigma^k=P^*$ cannot even be concluded on the indices outside both sets. Second, the optimal faces must be shown nonempty and bounded whenever an interior point exists, so that the maxima in $\xi$ are attained and positive. Third, the orthogonality $(x^k-x^*)^T(s^k-s^*)=0$ must be derived for feasible pairs. A newcomer's first idea is to argue from convergence of the iterates to a limit point. That gives no iteration count, and the theorem needs the quantitative threshold $n^{-\eta}\xi^2$ instead.

For Lemma 5.1 the obstacle is the telescoping of $\|(D^t)^{-1}(x^t-d^t)\|_1$ across updates. The book's final step writes $\|\cdot\|_1\le\|\cdot\|_2$, but the bound needs $\|\cdot\|_1\le\sqrt n\|\cdot\|_2$.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ, with indices starting at $0$. The Euclidean norm is written out as norm2 because Mathlib's norm on Fin n → ℝ is the sup norm. Optimality is defined by comparison with every feasible point. $P^*$ and $Z^*$ are defined as unions of supports of optimal solutions; no Goldman–Tucker property is assumed. Each maximum in $\xi$ is Lean's sSup over the face; xi_pos asserts that it is attained. $\xi$ is one minimum over all indices, taking the primal maximum on $P^*$ and the dual maximum elsewhere. Property (5.7) is written coordinatewise.

Explicit constants replacing the book's $O(\cdot)$: Theorem 5.3 writes $K=O(\sqrt n(\log(R/\xi^2)+\log n))$ and appeals to the polynomial bound of the algorithms. The Lean statement makes that bound a hypothesis, $(x^k)^Ts^k\le R\,e^{-\kappa k/\sqrt n}$ with the algorithm's constant $\kappa>0$; the per-step reduction $(1-\kappa/\sqrt n)^kR$ implies it. The threshold $(x^k)^Ts^k\le n^{-\eta}\xi^2$ from the proof then gives $K=\lceil(\sqrt n/\kappa)(\log(R/\xi^2)+\eta\log n)\rceil$. The standing assumption $(x^0)^Ts^0\le R$ (p. 147) and interior feasibility are explicit hypotheses. Because $\min(Xs)\le x^Ts/n$, property (5.7) can only hold when $n^{-\eta}<1/n$. It never holds at $n=1$, so the theorems are vacuous there, as in the book.

A trivializing formalization is ruled out: $K$ is an explicit function of $n,\kappa,\eta,R,\xi$, not an existential "for some $K$", and $\xi$ is computed from $(A,b,c)$, not a free parameter.

The update set of §5.1 is printed with $d^t$ in the numerator, which makes it empty for every $t$. The mission defines it with $d^{t-1}$, as the proof of Lemma 5.1 uses it (finding F2).

Needed infrastructure: LP weak duality and Goldman–Tucker strict complementarity (both proved elsewhere on the platform for other encodings), boundedness of optimal faces under interior feasibility, and attainment of linear maxima on compact polyhedra. The definitions module YeIPA.WorstCase.Termination (partition, faces, $\xi$) is reusable for Chapter 7's asymptotic analysis.

Not in scope: Theorem 5.14 and Lemma 5.15 (the infeasible-starting algorithm; Lemma 5.15's proof is an exercise and overloads $\eta$), Theorem 5.9(i) (its uniqueness claim needs $A$ of full row rank, finding F1), and the remaining §5.3 homogeneous self-dual results, which are posed on the platform for the paper's special starting point.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, Chapter 5. doi:10.1002/9781118032701
• Y. Ye, On the finite convergence of interior-point algorithms for linear programming, Mathematical Programming 57 (1992) 325–335. doi:10.1007/BF01581087
• O. Güler and Y. Ye, Convergence behavior of interior-point algorithms, Mathematical Programming 60 (1993) 215–228. doi:10.1007/BF01580610
• S. Mehrotra and Y. Ye, Finding an interior point in the optimal face of linear programs, Mathematical Programming 62 (1993) 497–515. doi:10.1007/BF01585180

Motivation

Primal–dual interior-point methods are the standard polynomial-time algorithms for linear programming. They do not walk along the vertices of the feasible polyhedron as the simplex method does. They follow a smooth curve through its interior, the central path, toward the optimal set. Every complexity bound for these methods is a statement about iterates kept close to that curve. Their practical value, recovering an optimal basis or the optimal partition of the variables, depends on where the curve ends.

Chapter 2 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) develops the geometry behind these methods. It covers analytic centers of polytopes, potential functions, and, in §2.5, the central path of a linear program and its limit. The limit result is due to Güler and Ye and to McLinden (Güler and Ye, Mathematical Programming 60, 1993; McLinden, Pacific Journal of Mathematics 88, 1980). The central path converges to the analytic center of the optimal face, a strictly complementary optimal solution singled out among all optimal solutions. This mission formalizes that theorem (Theorem 2.17), with the boundedness and neighbourhood results (Theorems 2.17 (i), 2.18) that accompany it.

Setting

Let $A$ be a real $m\times n$ matrix of rank $m$ with $n>m$, $b\in\mathbb R^m$ and $c\in\mathbb R^n$. Ye's standard-form primal and dual linear programs are

$$(LP)\quad \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad\qquad (LD)\quad \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .$$

Vector inequalities are componentwise. A point is interior feasible if, in addition, $x>0$ (resp. $s>0$). It is assumed throughout that both programs have interior feasible points. A feasible $x$ is optimal if $c^Tx\le c^Tx'$ for every feasible $x'$; a feasible $(y,s)$ is optimal if $b^Ty'\le b^Ty$ for every feasible $(y',s')$.

For $\mu>0$, a central path point is a triple $(x(\mu),y(\mu),s(\mu))$ of interior feasible points with

$$x(\mu)_j\,s(\mu)_j=\mu\qquad (j=1,\dots,n).$$

Theorem 2.16 says that it exists and is unique.

A pair of feasible $x$ and $(y,s)$ is strictly complementary if $x_js_j=0$ and $x_j+s_j>0$ for every $j$. Such pairs exist (Goldman–Tucker, Theorem 1.14 in the book), and the supports $P^*=\{j:x_j>0\}$ and $Z^*=\{j:s_j>0\}$ do not depend on the pair. $(P^*,Z^*)$ is the strict complementarity partition. The primal optimal face is $\{x: A_{P^*}x_{P^*}=b,\ x_{P^*}\ge0,\ x_{Z^*}=0\}$, and the dual optimal face is $\{y: c_{Z^*}-A^T_{Z^*}y\ge0,\ c_{P^*}-A^T_{P^*}y=0\}$. The analytic center of the primal optimal face is the point $x$ of the face with $x_{P^*}>0$ that maximizes $\sum_{j\in P^*}\log x_j$. On the dual side, the slack $s=c-A^Ty$ of the dual optimal face maximizes $\sum_{j\in Z^*}\log s_j$ over the face.

With $\mu=x^Ts/n$, the neighbourhood of the central path is

$$\mathcal N(\eta)=\big\{(x,y,s)\text{ interior feasible}:\ \|Xs-\mu e\|\le\eta\mu\big\},\qquad 0<\eta<1,$$

where $X=\mathrm{diag}(x)$, $e$ is the all-ones vector, and $\|\cdot\|$ is any norm, or the one-sided "norm" $\|v\|_{-\infty}=|\min(0,\min_j v_j)|$, that dominates $\|\cdot\|_{-\infty}$ (every $\ell_p$ norm does).

Formalization targets

Goal: Theorem 2.17 (iii)

For any choice of central path points $\mu\mapsto(x(\mu),y(\mu),s(\mu))$, $\mu>0$, there are $x(0)$ and an optimal $(y(0),s(0))$ with

$$\lim_{\mu\to0^+}x(\mu)=x(0),\qquad \lim_{\mu\to0^+}s(\mu)=s(0),$$

$x(0)$ optimal for (LP), $x(0)_{P^*}$ the analytic center of the primal optimal face, and $s(0)_{Z^*}$ the analytic center of the dual optimal face.

Milestones

1. Theorem 2.16 (existence and uniqueness of the central path point), referenced from the platform.
2. Theorem 2.17 (i): for every $\mu^0>0$, $\{(x(\mu),s(\mu)): 0<\mu\le\mu^0\}$ is bounded.
3. Theorem 2.18 (i): $\mathcal N(\eta)\cap\{x^Ts\le n\mu^0\}$ is bounded.
4. Theorem 2.18 (ii): every limit of points of $\mathcal N(\eta)$ with $\mu\to0$ is an optimal pair. For every $(x,y,s)\in\mathcal N(\eta)$, every optimal $x^*$ and every optimal $(y^*,s^*)$,

$$x_j\ge\frac{(1-\eta)x^*_j}{n}\ (j\in P^*),\qquad s_j\ge\frac{(1-\eta)s^*_j}{n}\ (j\in Z^*).$$

5. Theorem 2.17 (ii), as printed: for $0<\mu'<\mu$, $c^Tx(\mu')<c^Tx(\mu)$ and $b^Ty(\mu')>b^Ty(\mu)$.

Significance

The goal identifies the end point of the central path: not an arbitrary optimal solution, but the unique strictly complementary one at the center of the optimal faces. This yields the optimal partition $(P^*,Z^*)$ in the limit. It underlies finite termination and basis-identification procedures and the asymptotic analysis of later chapters, where predictor directions are measured on $P^*$ and $Z^*$. Theorem 2.18 extends the picture from the path to the neighbourhood that path-following algorithms actually maintain, with an explicit rate, $(1-\eta)/n$, at which coordinates in the optimal partition stay away from zero.

The results are classical and proved in the literature. None is formalized on Prove2Me. Theorem 2.16 is already there, as a proved statement for Matoušek and Gärtner's equivalent max-form LP. The formalization adds machine-checked statements of the limit theorem, which so far exists only in prose, together with a precise record of which hypotheses each part needs. Reading the chapter turned up three: Theorem 2.17 (ii) is false as printed when an objective is constant on its feasible region; boundedness of the $y$-component in Theorem 2.18 (i) needs $A$ of full row rank; and the "any norm" in the definition of $\mathcal N(\eta)$ is too permissive for Theorem 2.18 (ii).

Difficulty

The limit is taken along a curve defined only implicitly, as the solution of a nonlinear system for each $\mu$. The obvious argument, compactness of the bounded path, only produces limit points. It says nothing about uniqueness of the limit or about which optimal solution is reached. The difficulty is that the claim pins down a single point among the typically infinitely many optimal solutions, and it must do so for any selection of path points, with no continuity of $\mu\mapsto x(\mu)$ assumed. The book leaves the proof of Theorem 2.17 (ii) as an exercise and gives no proof of Theorem 2.18.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is Matrix (Fin m) (Fin n) ℝ; indices run over $0,\dots,n-1$. Every theorem carries the chapter's standing assumptions explicitly: $\operatorname{rank}A=m$ and $n>m$ (p. 48), and interior feasible points for both programs (pp. 63, 70). The central path enters the goal as an arbitrary selection of central path points for $\mu>0$; no continuity is assumed, and limits are taken along $\mu\to0^+$. $P^*$ and $Z^*$ are constructed from the data, as the indices positive in some strictly complementary pair. The optimal faces are written for full vectors in $\mathbb R^n$, and analytic centers are attained maximizers of $\sum\log$, never a supremum. $\mathcal N(\eta)$ takes the size function $\|\cdot\|$ as a parameter, and Theorem 2.18 is stated for every $\|\cdot\|$ with $\|v\|\ge\|v\|_{-\infty}$; the book allows "any norm, or even a one-sided norm", and with an arbitrary norm (say $0.1\|\cdot\|_\infty$) the lower bounds of 2.18 (ii) fail. There are no $O(\cdot)$ constants in these statements; the bound $(1-\eta)/n$ of Theorem 2.18 (ii) is the book's exact constant.

A trivializing formalization would take $P^*$, $Z^*$ or the limit points as free parameters constrained by hypotheses, or define the analytic center through a real supremum that defaults to $0$. Both are ruled out: the partition and the faces are computed from $(A,b,c)$, and the analytic center is an attained maximizer over points with positive coordinates.

Beyond the paper. Two variant items are posed beside the faithful ones. [Corrected] Theorem 2.17 (ii) replaces both strict inequalities by weak ones, because the strict ones fail when $c^Tx$ or $b^Ty$ is constant on its feasible region, e.g. $A=(1,1)$, $b=2$, $c=(1,1)$ (findings F1, F6, F8). [Sharpness probe] Theorem 2.18 (i) drops $\operatorname{rank}A=m$: with a zero row in $A$ a coordinate of $y$ is free and the set is unbounded (finding F7); a disproof is the sought outcome.

A complete development needs strong LP duality and the Goldman–Tucker strict complementarity theorem for standard-form LPs, strict concavity of $\sum\log x_j$ on a polyhedron, and compactness arguments in $\mathbb R^n$. The duality and complementarity layers are reusable across the whole series; contributions of these as standalone lemmas are welcome.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, Chapter 2, §2.5. https://doi.org/10.1002/9781118032701
• O. Güler and Y. Ye, Convergence behavior of interior-point algorithms, Mathematical Programming 60 (1993) 215–228.
• L. McLinden, An analogue of Moreau's proximation theorem, with application to the nonlinear complementarity problem, Pacific Journal of Mathematics 88 (1980) 101–161.
• A. J. Goldman and A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4

Motivation

A bandit sampling process models a population from which values are drawn one at a time: the values are independent with a distribution $f(\cdot \mid \theta)$ whose parameter $\theta$ is unknown, the decision maker holds a prior on $\theta$ and updates it by Bayes' theorem, and each draw earns a reward. When several such populations compete for the same sampling effort, the Gittins index theorem reduces the allocation problem to computing one index per population (Gittins, J. R. Stat. Soc. B 1979). The obstacle is computation: the state is a posterior distribution, so the index is a function of every parameter of the posterior.

Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), shows that location and scale structure removes most of that dependence. For a normal population with unknown mean and variance, Theorem 7.15 says that the index in the state $(\bar x, s, n)$ is $\bar x + s\,\nu(0, 1, n)$, so a single function of $n$ suffices; the tables of Chapter 8 rest on this. The same reduction holds for target processes, where the aim is to observe a value above a target $T$ as soon as possible (Theorems 7.19–7.23).

This mission continues the public series Multi-armed Bandit Allocation Indices I–VI in the namespace AllocationIndices. Mission VI formalized the location and scale halves of the theory (Theorems 7.9 and 7.11) and the location invariance of target processes (Theorem 7.17), all now proved; this mission states the joint location–scale results on the same published definitions.

Setting

A sampling model SamplingModel Θ Q (published, AllocationIndices_Sampling) consists of a likelihood $f(\cdot \mid \theta)$, a family of priors $\pi(\cdot \mid p)$ on $\theta \in \Theta$ indexed by the parameters $p \in Q$ of a conjugate family, and the update $p \mapsto p_x$ of those parameters when $x$ is the next value sampled; the family is conjugate on a set of parameters if the update computes the Bayesian posterior there. The reward process has state $p$, draws $x$ from the predictive distribution $f(\cdot \mid p) = \int f(\cdot \mid \theta)\,\pi(d\theta \mid p)$, moves to $p_x$, and earns the predictive mean $r(p)$. Rewards are discounted by $a^t$, $0 < a < 1$; for a stopping time $\tau$, $R_\tau(p)$ is the expected discounted reward before $\tau$, and $\nu(p)$ is the Gittins index (2.6). The target process with target $T$ stops as soon as a sampled value is $\ge T$.

Two calibration quantities compare a process with a known one. The calibration payoff against a standard bandit process paying $\lambda$ per period is

$$R(\lambda, p) = \sup_\tau \big\{ R_\tau(p) + \lambda (1 - a)^{-1} E(a^\tau \mid p) \big\},$$

the supremum over all stopping times, $\tau$ being the time at which the standard process is first selected (calibrationPayoff). The target cost against a standard target process with known success probability $\varphi$ is

$$M(\varphi, p, T) = \inf_\tau \big\{ C_\tau(p, T) + \varphi^{-1} Q_\tau(p, T) \big\},$$

where $C_\tau$ is the expected number of samples drawn before $\tau$ or before the target is reached, and $Q_\tau$ the probability that $\tau$ comes first (targetCost, undiscounted, valued in $[0, \infty]$).

Parameters $\mu$ and $\sigma > 0$ are joint location and scale parameters if $f(\cdot \mid b\mu + c, b\sigma)$ is the image of $f(\cdot \mid \mu, \sigma)$ under $x \mapsto bx + c$ for $b > 0$, $c \in \mathbb R$. With $\sigma$ unknown the conjugate prior on $(\mu, \sigma)$ has parameters $(\bar x, s, n)$, which change by the rules of the sample mean, the sample standard deviation and the number of observations, and $\bar x, s$ are joint location and scale parameters of the prior family: the prior with parameters $(b\bar x + c, bs, n)$ is the image of that with parameters $(\bar x, s, n)$ under $(\mu, \sigma) \mapsto (b\mu + c, b\sigma)$. With $\sigma$ known the parameters are $(\bar x, n, \sigma)$ and only $\bar x, n$ change.

Formalization targets

Goal: Theorem 7.15 (p. 193)

For the reward process with $\sigma$ unknown, in a state with $s > 0$, $n > 1$, for all $\lambda$, $b > 0$ and $c$,

$$R(b\lambda + c,\ b\bar x + c,\ bs,\ n) = c(1 - a)^{-1} + b\,R(\lambda, \bar x, s, n), \qquad \nu(\bar x, s, n) = \bar x + s\,\nu(0, 1, n).$$

Both conclusions are part of the goal (AllocationIndices.Targets.location_scale_invariance).

Milestones

• Theorem 7.13 (p. 192), $\sigma$ known: $R(b\lambda + c, b\bar x + c, n, b\sigma) = c(1 - a)^{-1} + bR(\lambda, \bar x, n, \sigma)$ and $\nu(\bar x, n, \sigma) = \bar x + \sigma\nu(0, n, 1)$.
• Theorem 7.19 (p. 194), target process with a scale parameter: $M(\varphi, \bar x, n, T) = M(\varphi, b\bar x, n, bT)$ and, for $T > 0$, $\nu(\bar x, n, T) = \nu(\bar x / T, n, 1)$.
• Theorem 7.21 (p. 194), target process, $\sigma$ known, as printed: $M(\varphi, \bar x, n, \sigma, T) = M(\varphi, \bar x + c, n, b\sigma, bT + c)$ and $\nu(\bar x, n, \sigma, T) = \nu((\bar x - T)/\sigma, n, 1, 0)$.
• Theorem 7.23 (p. 194), target process, $\sigma$ unknown: $M(\varphi, \bar x, s, n, T) = M(\varphi, b\bar x + c, bs, n, bT + c)$ and $\nu(\bar x, s, n, T) = \nu((\bar x - T)/s, 1, n, 0)$.

Significance

The result reduces the index of a two-parameter family of posteriors to a function of one variable and makes the normal reward process with unknown variance computable at all; the Chapter 8 tables of $\nu(0, 1, n)$ and the corresponding target-process tables are only meaningful because of it. The identities for $R$ and $M$ are what the calibration method of computing those tables uses, so they are stated too.

The theorems are proved in the book only in outline: the proofs of Theorems 7.13 and 7.15 are "left as exercises", and those of 7.19–7.23 are said to be similar to their reward-process counterparts. A formal proof supplies the arguments the book omits. Mission VI proved the one-parameter cases on the platform; the joint cases, the calibration payoff $R$ and the target cost $M$ have no machine-checked version.

Difficulty

The book reasons with densities and improper priors. In the formal model the state is a parameter vector, the posterior is Mathlib's Bayesian inverse, defined only almost everywhere with respect to the predictive distribution, and stopping times are measurable functions of an entire trajectory of states. Relating the processes started at $(\bar x, s, n)$ and at $(b\bar x + c, bs, n)$ requires relating two Markov chains on an uncountable state space, together with their stopping times, rather than two densities. The two index identities are also not formal consequences of the identities for $R$ and $M$ in the published model, whose index is defined as a supremum of reward rates rather than by calibration.

Formalization scope

Discrete time throughout; $R$ uses the factor $(1 - a)^{-1}$ exactly as printed in (7.15), so no unit conversion is involved; the index is gittinsIndex (2.6) of the reward or target chain with $0 < a < 1$, and $M$ is undiscounted as in (7.16). The book's improper priors ($\pi_0(\mu)$ uniform, $\pi_0(\mu, \sigma) \propto \sigma^{-d}$) are used only through the proper posteriors they generate; as in Corollaries 7.14, 7.16 and mission VI, the state is the parameter vector of a proper conjugate family, required to be conjugate on $n > 0$ (σ known) or on $s > 0$, $n > 1$ (σ unknown), the domain on which the sample-standard-deviation update is defined and keeps $s > 0$. "σ known" means the prior is concentrated on the scale coordinate of the state. The prior family's location–scale property is an image of measures; the printed density form (7.25) has a Jacobian $b$ where $b^2$ is needed and lacks the shift $+c$ in the conditioning argument, so as printed no probability density satisfies it. The reward theorems assume integrable observations and finite expected discounted absolute rewards from every state, which makes $R$ a finite supremum over a nonempty set; this rules out the trivializing reading in which a real supremum of an unbounded set defaults to $0$, and the goal states both the identity for $R$ and the index identity, not the reward shift $r(b\bar x + c, bs, n) = b\,r(\bar x, s, n) + c$ alone. In Theorem 7.19 the index identity carries $T > 0$, which the book leaves implicit; in Theorem 7.23 the stray argument $\sigma$ of $\nu(\bar x, s, n, \sigma, T)$ is dropped.

Beyond the paper. The first identity of Theorem 7.21 scales $\sigma$ and $T$ by $b$ but shifts $\bar x$ without scaling it; with normal observations, $\varphi = 1/2$, $n = 1$, $T = 0$, $\bar x = 3$, $b = 2$, the two sides are at most $1.034$ and at least $1.144$. The faithful item states it as printed; a corrected variant with $b\bar x + c$ is posed beside it.

Definitions are in AllocationIndices.Targets.Model; the model, conjugacy, reward and target chains, HasScaleParameter, PriorHasScaleParameter and meanUpdate are the published AllocationIndices_Sampling. Lemmas on transporting a Markov chain's path measure and its stopping times along a measurable bijection of the state space are reusable beyond this mission; proofs of single milestones are welcome.

Selected references

• J. C. Gittins, K. D. Glazebrook and R. R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, §7.4 and §8. doi:10.1002/9780470980033
• J. C. Gittins, Bandit processes and dynamic allocation indices, J. R. Stat. Soc. B 41 (1979), 148–177. doi:10.1111/j.2517-6161.1979.tb01068.x

Motivation

Gittins index policies are optimal for a single server choosing among alternative bandit processes, and the achievable region method of Bertsimas and Niño-Mora (Math. Oper. Res. 1996) explains why: when the performance vectors of a scheduling system satisfy generalized conservation laws, the region they fill is a polytope whose optimal vertex is an index priority. Most real systems have several servers working in parallel, and for them the conservation laws fail. Glazebrook and Wilkinson (Ann. Appl. Probab. 2000) observed that $M$ parallel machines are close to a single machine working at $M$ times the speed, where the laws do hold, and turned that closeness into explicit bounds on how much an index policy can lose. Section 5.7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), presents that analysis for the simple family of alternative bandit processes (SFABP). Its first quantitative output is an upper bound on the optimal return, Corollary 5.20. This bound is the reference point against which the index heuristics of the rest of the section are measured.

This mission continues the public series Multi-armed Bandit Allocation Indices I–VI. Mission IV of that series formalized the single-machine achievable region theory of Chapter 5: Lemma 5.1, Theorems 5.5 and 5.10, and the identity of the adaptive greedy indices with Gittins indices.

Setting

There are $n$ arms. Arm $b$ has a finite state space $E_b$; the $E_b$ are disjoint, and their union $E = \{1, \dots, N\}$ is the set of job types. One transition kernel $P$ on $E$ moves an arm when it is processed. Each $E_b$ is closed under $P$, and $P$ is irreducible on each $E_b$. Time is discrete, rewards are discounted by $a^t$ with $0 < a < 1$, and processing a job of type $i$ earns $r_i$. There are $M$ identical machines, $1 \le M \le n$. At each time $t = 0, 1, 2, \dots$ a policy $\pi$ chooses, on the basis of the history, a set of exactly $M$ arms. Each chosen arm makes one transition and the others are frozen. From the initial state-vector $k$, the performance $x_i^\pi(k)$ is the expected total discounted number of times a job of type $i$ is processed. The return is $R^\pi(k) = \sum_{i \in E} r_i x_i^\pi(k)$, and $R^{\mathrm{opt}}(k) = \sup_\pi R^\pi(k)$.

The matrix $A = (A_i^S)$ is the single-arm matrix of §5.3, published in the series as conservationCoeff: for $i \in S$, $A_i^S = E[1 + a + \cdots + a^{T_i^S - 1}]$, where $T_i^S \ge 1$ is the number of transitions the chain started at $i$ needs to return to $S$, and $A_i^S = 0$ otherwise. Job types are numbered in ascending order $\nu_1 \le \cdots \le \nu_N$ of the indices produced by the adaptive greedy algorithm $\mathrm{AG}(A, r)$ (IsAdaptiveGreedy, greedyIndex), and $S_i = \{1, \dots, i\}$. Write

$$A^\pi(S, k) = \sum_{i \in E} A_i^S x_i^\pi(k), \qquad A(S, k) = \inf_\pi A^\pi(S, k).$$

Let $\psi_i$ be the number of arms with no job type in $S_i$, let $i_b = \min E_b$, and number the arms so that $i_1 \le \cdots \le i_n$. For each other arm, $T_{k_b}^{S_i}$ is the processing needed to bring it from $k_b$ into $S_i$ for the first time, and $T_k^{S_i}$ is the sum of these over the other arms, which evolve independently.

Formalization targets

Goal: Corollary 5.20 (p. 142)

$$R^{\mathrm{opt}}(k) \le \nu_N \Big(\frac{M}{1-a}\Big) - \Big(\frac{1}{1-a}\Big) \sum_{i = i_{n-M+1}}^{N-1} (\nu_{i+1} - \nu_i)(M - \psi_i)\, E\Big[a^{T_k^{S_i}/(M - \psi_i)}\Big].$$

Milestones

• Eq. (5.21) in the form of p. 139: $r_j = \nu_N - \sum_{i=j}^{N-1} (\nu_{i+1} - \nu_i) A_j^{S_i}$.
• Eq. (5.25): for every policy, $R^\pi(k) = \nu_N \frac{M}{1-a} - \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i) A^\pi(S_i, k)$.
• Lemma 5.19(ii): if $\psi_i \ge M$ then $A(S_i, k) = 0$.
• Lemma 5.19(i): if $M - 1 \ge \psi_i$ then $A(S_i, k) \ge \frac{M - \psi_i}{1 - a} E\big[a^{T_k^{S_i}/(M - \psi_i)}\big]$.
• Eq. (5.27): $R^{\mathrm{opt}}(k) - R^\pi(k) \le \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i)\big[A^\pi(S_i, k) - A(S_i, k)\big]$.

The goal keeps the book's constants. Eq. (5.27) is a companion bound from the same identity.

Significance

The bound is explicit and computable from single-arm quantities: the AG indices and the laws of first-entry times. Subtracting from it the exact return of a concrete policy gives a certified suboptimality gap without solving the parallel-machine dynamic program, which has no index solution. The book uses it in exactly this way. With the exact return (5.30)–(5.31) of the heuristic $\pi_G^*$, it shows that $\pi_G^*$ loses $O(1-a)$, and in the limit $a \to 1$ that $\pi_G^*$ is average-overtaking optimal (Theorem 5.25).

All of these results are proved in the book and in Glazebrook and Wilkinson (2000). None is machine-checked. The series so far covers only the single-machine theory, and there is no parallel-machine bandit model on Prove2Me. This mission supplies that model and states the first link of the chain: from conservation-law algebra to a bound for a system that does not satisfy the conservation laws.

Difficulty

The identity (5.25) is algebra once the policy processes exactly $M$ arms in every period. The difficulty is the lower bound on $A(S_i, k)$. The obvious idea, which works for one machine, is to minimize $A^\pi(S_i, k)$ by giving priority to job types outside $S_i$. On $M$ machines such a policy cannot keep every machine busy outside $S_i$, and the minimizing policy is not known, so $A(S_i, k)$ has no closed form and must be bounded below over all history-dependent policies at once. The bound has to hold uniformly: it must account for each arm's processing both before and after its first visit to $S_i$, with arms frozen for random lengths of time in between. The printed proof also contains a step whose last inequality goes the wrong way (finding F2). The lemma is true, but the printed chain of inequalities cannot be followed literally.

Formalization scope

Job types are Fin (N + 1), so the book's $N$ is Lean's N + 1 and the book's type $i$ is the Lean index i - 1. Sums over $i = 1, \dots, N - 1$ run over i : Fin N, with $\nu_{i+1}$ = ν i.succ, $\nu_i$ = ν i.castSucc and $S_i$ = Finset.Iic i.castSucc. The arms are Fin n, and arm : Fin (N + 1) → Fin n assigns job types to arms. One kernel on the disjoint union replaces the book's per-arm matrices $P^b$, and IsArmFamily states closedness and irreducibility. A policy (ParallelPolicy n N M) is a sequence of Markov kernels from histories to Boolean selection vectors with exactly $M$ true entries. The law of the history is built by composition, and the performance is a discounted sum of expected per-period occupation counts. $R^{\mathrm{opt}}$ and $A(S, k)$ are a real supremum and infimum over all policies. The class is nonempty because $1 \le M \le n$, and both families are bounded, so neither takes a junk value. $E[a^{T/m}]$ is an integral against the product of the single-arm chain laws, with a real exponent and $a^\infty = 0$. The numbering by AG indices is two hypotheses: the identity permutation is an output of $\mathrm{AG}(A, r)$, and $\nu$ is monotone. The arm numbering is a function lowest with lowest b $= i_b$ and lowest monotone.

Unit conversions: none. Section 5.7 is written in discrete time with discount factor $a$, the convention of the series' published definitions, so every constant is the book's.

Correction of the setup: the book assumes "the number of parallel servers $M$ exceeds the number of arms $n$" (p. 139). The rest of the section needs the opposite (finding F1): for instance, the arm index $n - M + 1$ in Corollary 5.20 is not positive when $M > n$. Every item assumes $1 \le M \le n$.

Trivializing formalizations ruled out: $A(S_i, k)$ is not a hypothesis or an abstract GCL quantity. It is the infimum over an explicitly constructed, nonempty class of parallel-machine policies, so the goal cannot be discharged by assuming the conservation laws for the $M$-machine system (which fail). The theorems do not allow $M > n$, where the policy class is empty and the supremum would take the junk value $0$.

Out of scope: the branching-bandit bounds of §5.5 (Theorems 5.12 and 5.13). They need a continuous-time branching-bandit model whose GCL property the book only cites. Also out of scope are Theorem 5.11 (priority classes) and the $O(\cdot)$ results 5.21–5.23 and Theorem 5.25.

Reusable infrastructure: the parallel-machine SFABP model (Def_AllocationIndices_Branching_Parallel) serves the remaining results of §5.7. Lemmas on the law of a frozen arm's trajectory under an arbitrary policy are welcome contributions.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, §5.3 and §5.7. https://doi.org/10.1002/9780470980033
• K. D. Glazebrook, D. J. Wilkinson, Index-based policies for discounted multi-armed bandits on parallel machines, Annals of Applied Probability 10 (2000), 877–896. https://doi.org/10.1214/aoap/1019487512
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21 (1996), 257–306. https://doi.org/10.1287/moor.21.2.257

Motivation

Ellipsoids are the simplest convex bodies that can approximate an arbitrary convex set to within a factor depending only on the dimension. They are used for exactly that in control (reachable sets of linear systems), robust optimization (uncertainty sets) and the ellipsoid method. A linear system $x(t+1)=Ax(t)+Bu(t)$ with $\|u(t)\|_2\le1$ illustrates the need. Its reachable set grows by an arithmetic sum at every step, so an ellipsoidal description of it requires approximating a sum of ellipsoids by a single ellipsoid, recursively and cheaply.

Timeline. Fritz John (1948) proved that every convex body has a unique maximal-volume inscribed ellipsoid and a unique minimal-volume circumscribed one, each within a factor $n$ ($\sqrt n$ for symmetric bodies) of the body; the circumscribed case goes back to Löwner. Boyd, El Ghaoui, Feron and Balakrishnan (1994) gave semidefinite programs whose solutions are ellipsoids that provably contain a sum of ellipsoids. Nesterov (1998) and Ye (1999) proved a $\pi/2$ approximation bound for semidefinite relaxations of quadratic maximization with commuting constraint matrices. Ben-Tal and Nemirovski (2001), Lecture 4, §4.9, combine the last two: the semidefinite outer ellipsoid of a sum of ellipsoids has volume at most $(\pi/2)^{n/2}$ times that of the smallest one.

Setting

All objects live in $\mathbb R^n$, with $u^Tu=\sum_ju_j^2$.

• An ellipsoid is a set $E(A,c)=\{Au+c \mid u^Tu\le1\}$ with $A\in\mathbb R^{n\times q}$. It is full-dimensional if it can be written with $A$ square and $\operatorname{Det}A\ne0$.
• Volume is normalized: $\operatorname{Vol}(G)$ is the Lebesgue measure of $G$ divided by that of the unit Euclidean ball. Then $\operatorname{Vol}(E(A,c))=|\operatorname{Det}A|$ and $\operatorname{Vol}(W[Z])=(\operatorname{Det}Z)^{-1/2}$, where $W[Z]=\{x \mid x^TZx\le1\}$ for $Z\succ0$.
• A solid is a closed, bounded, convex set with nonempty interior.
• Fix positive definite $B_1,\dots,B_m$ and the centred ellipsoids $W_i=W[B_i]$. Their arithmetic sum is $W=W_1+\dots+W_m=\{w_1+\dots+w_m \mid w_i\in W_i\}$.
• Let $B^i$ be the $(mn)\times(mn)$ block-diagonal matrix whose only nonzero $n\times n$ diagonal block is the $i$-th, equal to $B_i$. Let $M[Z]$ be the $(mn)\times(mn)$ matrix of $m^2$ blocks, all equal to $Z$.
• The semidefinite program

$$\max_{t,Z,\lambda}\Big\{t \;\Big|\; t\le\operatorname{Det}^{1/n}(Z),\ \sum_{i=1}^m\lambda_iB^i\succeq M[Z],\ \lambda\ge0,\ Z\succeq0,\ \sum_{i=1}^m\lambda_i=1\Big\}\qquad(\tilde O)$$

produces, from each feasible solution with $t>0$, an ellipsoid $W[Z]\supseteq W$.

Formalization targets

Goal: Proposition 4.9.5

Let $(t_*,Z_*,\lambda_*)$ be any optimal solution of $(\tilde O)$. Let $Z_{**}\succ0$ be such that $W[Z_{**}]$ is the smallest-volume full-dimensional ellipsoid containing $W$. Then

$$\operatorname{Vol}(W[Z_*])\le\Big(\frac\pi2\Big)^{n/2}\operatorname{Vol}(W[Z_{**}]).$$

This is the book's ratio $\vartheta=\operatorname{Vol}(W[Z_*])/\operatorname{Vol}(W[Z_{**}])\le(\pi/2)^{n/2}$ in product form.

Milestones

1. (D): if every $X\succeq0$ with $\operatorname{Tr}(B^iX)\le1$ for all $i$ has $\operatorname{Tr}(M[Z]X)\le1$, then $W\subseteq W[Z]$.
2. Proposition 4.9.4: feasible solutions of $(\tilde O)$ with $t>0$ give $Z\succ0$, $W\subseteq W[Z]$ and $\operatorname{Vol}(W[Z])\le t^{-n/2}$. Optimal solutions give the smallest such volume.
3. Proposition 4.10.5 (Nesterov–Ye): for commuting $B_i$, strictly feasible constraints $x^TB_ix\le d_i$ and $A\succeq0$, the semidefinite value satisfies $F^*\le\frac\pi2f^*$, and the dual is solvable.
4. Theorem 4.9.1 (Löwner–Fritz John) for solids, both the inscribed and the circumscribed ellipsoid, with factors $n$ and $\sqrt n$.
5. Proposition 4.9.3: containment of $E(Z,z)$ ($Z\in\mathbb R^{n\times q}$, $q\ge1$) in a full-dimensional ellipsoid is equivalent to a linear matrix inequality in one scalar.
6. Lemma 4.9.1: $|\operatorname{Det}(S+C)|\ge\operatorname{Det}S$ for $S\succ0$ and $C$ skew-symmetric.
7. Proposition 4.9.6: the inner program $(\tilde I)$ gives ellipsoids contained in $W$ of volume at least $t^n$. Optimal solutions give the largest such volume.

Significance

The goal is a quantitative guarantee for a tractable surrogate. Computing the smallest ellipsoid containing a sum of ellipsoids is believed hard when $m$ is part of the input. A single semidefinite program gives an ellipsoid within a factor $\sqrt{\pi/2}\approx1.253$ in average linear size, uniformly in $n$ and $m$. The reachable-set recursion of the motivating example therefore loses at most a fixed factor per step. Proposition 4.10.5 is also the textbook instance of a constant-factor semidefinite relaxation bound for quadratic maximization, used well beyond this chapter.

All results are proved in the book, except Theorem 4.9.1 (Exercise 4.71) and Proposition 4.10.5 (Exercise 4.58 from Exercise 4.38). Some ellipsoid results already exist as Lean statements on Prove2Me, in the Boyd–Vandenberghe convex optimization series: existence, uniqueness and $1/n$-rounding of the Löwner–John ellipsoid of a finite point set. None of the statements here is formalized there. In particular, nothing exists for general solids, the inscribed ellipsoid, the $\sqrt n$ symmetric factor, sums of ellipsoids, or the Nesterov–Ye bound.

Difficulty

The goal's statement is short, but its proof crosses several fields. The obvious idea, comparing $W[Z_*]$ with $W[Z_{**}]$ directly, fails: $W[Z_{**}]$ is in general not of the form produced by $(\tilde O)$, since $(\tilde O)$ only reaches ellipsoids certified by a semidefinite relaxation. Closing that gap requires the full Nesterov–Ye bound $\pi/2$ for a quadratic maximization over the product of the $W_i$. That bound is itself a substantial theorem, which the book proves only through a chain of exercises. Mathlib has volumes, determinants and positive semidefinite matrices. It has no Löwner–John theory for convex bodies, no Schur-complement LMI calculus for block matrices over sum types, and no semidefinite duality.

The book's Proposition 4.9.6 is false as printed. Its constraint $t\le(\operatorname{Det}\cdot)^{1/n}$ admits every $t\le0$. For $n=2$, $A_1=I$, $X_1=0$, $t=-10$, the ellipsoid is $\{0\}$ while $t^n=100$. A corrected variant adds $t\ge0$.

Formalization scope

Vectors are Fin n → ℝ, and matrices are Matrix (Fin n) (Fin q) ℝ. $\succeq0$ and $\succ0$ are Mathlib's PosSemidef and PosDef, which include symmetry. The unit ball is written with the dot product, because Mathlib's metric ball on Fin n → ℝ is a cube. Volume is Mathlib's volume divided by the volume of the Euclidean unit ball, valued in $[0,\infty]$, so flat ellipsoids have volume $0$. $\operatorname{Det}^{1/n}$ is Real.rpow. The $(mn)\times(mn)$ block matrices are indexed by Fin m × Fin n. Optimal values appear only as explicit predicates: optimal = feasible with maximal objective, least upper bound, attained minimum.

In the goal, $W[Z_{**}]$ enters through hypotheses: $Z_{**}\succ0$, $W\subseteq W[Z_{**}]$, and no full-dimensional ellipsoid with any centre that contains $W$ has smaller volume. These hypotheses are satisfiable, by Theorem 4.9.1 and the central symmetry of $W$, so the goal is not vacuous. Volume is the measure-theoretic volume, not a formula in $\operatorname{Det}$ assumed as a definition: a formalization that defines the volume of $W[Z]$ as $(\operatorname{Det}Z)^{-1/2}$ for every $Z$ would not be the book's statement.

Two variants accompany the faithful statements. The first, [Corrected] Proposition 4.9.6, adds $t\ge0$, following finding F1. A Lean disproof of the printed statement on the instance above exists locally. The second, [Strengthened] Proposition 4.9.5, drops the minimality of $W[Z_{**}]$ (finding F2): the printed proof uses only $Z_{**}\succ0$ and $W\subseteq W[Z_{**}]$. Proofs of either variant, and disproofs of the printed Proposition 4.9.6, are welcome.

A complete development needs: Lebesgue volume of linear images ($|\operatorname{Det}|$ scaling); Schur complements for symmetric block matrices; semidefinite weak and strong duality, at least for the strictly feasible case; simultaneous diagonalization of commuting symmetric matrices; and the $\pi/2$ relaxation bound itself. The last four are reusable across the series' Lecture 4 missions.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001, §4.9 and §4.10.5. https://doi.org/10.1137/1.9780898718829
• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays Presented to R. Courant, Interscience, 1948, 187–204. https://doi.org/10.1007/978-3-0348-0439-4_9
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9 (1998), 141–160. https://doi.org/10.1080/10556789808805690
• Y. Ye, Approximating quadratic programming with bound and quadratic constraints, Mathematical Programming 84 (1999), 219–226. https://doi.org/10.1007/s10107980012a

Motivation

Many combinatorial and nonconvex problems can be written as the maximization or minimization of a quadratic form under quadratic constraints. Such problems are NP-hard in general, but each has a semidefinite relaxation: a convex problem over positive semidefinite matrices, solvable to any accuracy in polynomial time, whose optimal value bounds the original one. The relaxation is useful exactly to the extent that this bound is tight, and the quality of the bound is measured by an explicit approximation ratio.

Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001), develops this theory from first principles and proves the two classical ratios. The history it follows:

• N. Z. Shor (1987) introduced the semidefinite relaxation scheme for quadratically constrained problems that §4.3.1 describes.
• M. X. Goemans and D. P. Williamson (J. ACM 42, 1995, doi:10.1145/227683.227684) proved that for MAXCUT with nonnegative weights the semidefinite relaxation is within a factor $0.87856\ldots$ of the maximum cut.
• Yu. Nesterov (1998, doi:10.1080/10556789808805690) proved that for the maximization of any positive semidefinite quadratic form over the vertices of the cube $\{-1,1\}^n$ the relaxation is within a factor $2/\pi$.
• Nesterov and Y. Ye, and A. Nemirovski, C. Roos and T. Terlaky (doi:10.1007/s101070050100), extended such bounds to systems of quadratic inequalities, with factors $\pi/2$ (commuting constraints) and $2\ln(2\sum_i \operatorname{Rank} B_i)$ (general convex constraints).

This mission formalizes the book's statements of these results.

Setting

Let $A$ be a real symmetric $n\times n$ matrix and let $S_n$ be the set of vectors $x \in \mathbb R^n$ with every coordinate equal to $+1$ or $-1$. The quadratic sign problem (4.3.17) is

$$\mathrm{OPT} = \max_{x\in S_n} x^TAx,$$

and its semidefinite relaxation (4.3.18) is

$$\mathrm{SDP} = \max\{\operatorname{Tr}(AX) : X = X^T \succeq 0,\ X_{ii} = 1,\ i = 1,\dots,n\},$$

where $X \succeq 0$ means that $X$ is symmetric positive semidefinite. Every $x \in S_n$ gives the feasible matrix $X = xx^T$, which is why $\mathrm{SDP} \ge \mathrm{OPT}$. For a matrix $X$, $\operatorname{asin}[X]$ denotes the matrix with entries $\operatorname{asin}(X_{ij})$.

The MAXCUT problem (4.3.14) with weights $a_{ij} = a_{ji} \ge 0$ is $\max\{\tfrac14\sum_{i,j}a_{ij}(1 - x_ix_j) : x_i^2 = 1\}$, with relaxation (4.3.15) $\max\{\tfrac14\sum_{i,j}a_{ij}(1 - X_{ij}) : X = X^T \succeq 0,\ X_{ii} = 1\}$. The constant $\alpha = 0.87856\ldots$ is the largest $\alpha$ with $\operatorname{acos}(x)/\pi \ge \alpha\cdot\tfrac12(1 - x)$ for all $x \in [-1, 1]$.

The general quadratically constrained problem (4.3.5) minimizes $f_0(x) = x^TA_0x + 2b_0^Tx + c_0$ subject to $f_i(x) = x^TA_ix + 2b_i^Tx + c_i = 0$, $i = 1, \dots, m$. Its Lagrangian lower bound (4.3.9) and Shor's relaxation (4.3.11) are semidefinite programs built from the bordered matrices $\bar A_i = \begin{pmatrix} c_i & b_i^T\\ b_i & A_i\end{pmatrix}$.

Finally, the setting (SL.??) of the exercises takes a system $x^TB_ix \le d_i$, $i = 1,\dots,m$, with $d_i \ge 0$, the value $f^* = \max\{x^TAx : x^TB_ix \le d_i\}$, the relaxation value $F^* = \max\{\operatorname{Tr}(AX) : \operatorname{Tr}(B_iX) \le d_i,\ X \succeq 0\}$, and the dual (SDD) $\min\{\sum_i\lambda_id_i : \sum_i\lambda_iB_i \succeq A,\ \lambda \ge 0\}$.

Formalization targets

Goal: Nesterov's theorem (Theorem 4.3.2, p. 173)

For every positive semidefinite $A$,

$$\mathrm{SDP} \ge \mathrm{OPT} \ge \frac{2}{\pi}\,\mathrm{SDP} \qquad \Big[\tfrac2\pi = 0.6366\ldots\Big].$$

The constant $2/\pi$ is the book's, stated exactly.

Milestones

1. Simple lemma (p. 163): $x^TAx + 2b^Tx + c \ge 0$ for all $x$ if and only if $\begin{pmatrix} c & b^T\\ b & A\end{pmatrix} \succeq 0$.
2. Proposition 4.3.1 (p. 163): the optimal value of (4.3.9) is at most that of (4.3.5).
3. Proposition 4.3.2 (p. 164): the optimal value of Shor's relaxation (4.3.11) is at most that of (4.3.5).
4. Theorem 4.3.1 (p. 171, Goemans–Williamson): $\mathrm{OPT} \le \mathrm{SDP}$ and $\alpha\cdot\mathrm{SDP} \le \mathrm{OPT}$ for MAXCUT, $\alpha = 0.87856\ldots$.
5. Lemma 4.3.1 (p. 174): for every feasible $X$ of (4.3.18), $\mathrm{OPT} \ge \frac2\pi\sum_{i,j}a_{ij}\operatorname{asin}(X_{ij})$, and consequently $\mathrm{OPT} \ge \frac2\pi\max\{\operatorname{Tr}(A\operatorname{asin}[X]) \mid X \succeq 0,\ X_{ii} = 1\}$ (4.3.19).
6. Nesterov's observation (p. 174): $\operatorname{asin}[X] \succeq X$ for every positive semidefinite $X$ with $|X_{ij}| \le 1$.
7. Proposition 4.10.5 (pp. 314–315, Nesterov–Ye): if the $B_i$ commute, the system is strictly feasible, some nonnegative combination of the $B_i$ is positive definite and $A \succeq 0$, then $f^* \ge 0$, (SDD) is solvable with optimal value $F^*$, and $F^* \le \frac\pi2 f^*$.
8. Proposition 4.10.6 (p. 315, Nemirovski–Roos–Terlaky): if $B_i \succeq 0$, $d_i > 0$ and $\sum_iB_i \succ 0$, then $f^* \ge 0$, (SDD) is solvable with optimal value $F^*$, and $F^* \le 2\ln\big(2\sum_{i=1}^m\operatorname{Rank}(B_i)\big)f^*$.

Significance

Nesterov's theorem was the first constant-factor guarantee for semidefinite relaxation of a quadratic program whose objective is not a cut function, and it holds for every positive semidefinite form, including those arising in graph partitioning and in robust optimization. Together with the Goemans–Williamson theorem it underlies the matrix cube theorem and the approximate S-lemma later in the book, and the general logarithmic bound of Proposition 4.10.6 is the template for many approximation results in robust and chance-constrained optimization.

All statements of this mission are proved in the literature. On Prove2Me, a Goemans–Williamson statement exists in another form (the expected value of Gaussian rounding against the integer optimum, with constant $0.878$), and a constant-factor bound for the same objects as the goal exists with a much weaker constant ($2K$ with $K \le 288$, via Grothendieck's inequality). Neither the factor $2/\pi$ nor the exact constant $0.87856\ldots$ nor the bounds of Propositions 4.10.5–4.10.6 has a machine-checked statement or proof. Formalizing them also yields reusable infrastructure: optimal values of semidefinite programs as explicit predicates, the elliptope $\{X \succeq 0, X_{ii} = 1\}$, and entrywise matrix functions.

Difficulty

The upper bounds ($\mathrm{SDP} \ge \mathrm{OPT}$, Propositions 4.3.1–4.3.2) are the routine part. The lower bounds compare a continuous relaxation with a discrete optimum, and the book's constants ($2/\pi$, $0.87856\ldots$, $\pi/2$, $2\ln(2\sum_i\operatorname{Rank}B_i)$) leave no slack: an argument that loses any constant factor proves a different theorem. No feasible matrix of the relaxation is in general close to a rank-one matrix $xx^T$ with $x \in S_n$, so the obvious idea of reading a sign vector off an optimal $X$ directly gives no factor at all. The objects involved also go beyond what Mathlib packages: optimal values of semidefinite programs, entrywise transcendental functions of matrices, and, for Propositions 4.10.5–4.10.6, duality between (SDP) and (SDD).

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $X \succeq 0$ is Mathlib's Matrix.PosSemidef, which includes symmetry. The $(n+1)\times(n+1)$ matrices of §4.3.1 are indexed by Unit ⊕ Fin n. Optimal values are never a bare sSup: a maximization's optimal value enters as the hypothesis that a real number is the least upper bound of the objective over the feasible set, and these sets are nonempty and bounded, so the hypotheses are satisfiable for every instance. The optimal values of §4.3.1, which can be $\pm\infty$, are infima and suprema in EReal. The constant $0.87856\ldots$ is defined as the exact infimum $\inf_{-1\le x<1} 2\operatorname{acos}(x)/(\pi(1-x))$, never a decimal. The ratio $1 \ge \mathrm{OPT}/\mathrm{SDP} \ge 0.87856\ldots$ of (4.3.16) is stated in product form, $\mathrm{OPT} \le \mathrm{SDP}$ and $\alpha\cdot\mathrm{SDP} \le \mathrm{OPT}$: with Lean's convention $x/0 = 0$, a ratio would make the all-zero-weight instance meaningless, and the product form rules out that trivialization. The book's standing conditions (symmetric data; $d_i \ge 0$ in (SL.??)) are explicit hypotheses.

Contributions welcome: compactness of the elliptope $\{X \succeq 0,\ X_{ii} = 1\}$ and attainment of SDP values, rotation-invariant measures on spheres in Fin n → ℝ, entrywise functions of positive semidefinite matrices (Mathlib has the Schur product theorem, Matrix.PosSemidef.hadamard), and conic duality for (SDP)/(SDD). These are reusable well beyond this chapter.

Beyond the paper. One sharpness probe accompanies the goal: Nesterov's theorem with "$A \succeq 0$" weakened to "$A$ symmetric". It is false (finding F3: for $n = 1$, $A = (-1)$, $\mathrm{OPT} = \mathrm{SDP} = -1$ and $-\tfrac2\pi \le -1$ fails); its disproof is the sought outcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM/MPS, 2001, §4.3 and §4.10. doi:10.1137/1.9780898718829
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145. doi:10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9 (1998), 141–160. doi:10.1080/10556789808805690
• A. Nemirovski, C. Roos, T. Terlaky, On maximization of quadratic form over intersection of ellipsoids with common center, Mathematical Programming 86 (1999), 463–473. doi:10.1007/s101070050100