Optimization

Motivation

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$. Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$'s resource; agent $i$ has $b_i>0$ units. The problem is

$$\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.$$

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$, a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$; its value is $Z=\sum_jc_{i_jj}$. Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$, $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$. The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$. For $i\in I'$ the binary knapsack problem

$$\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}$$

chooses the cheapest set of tasks to move off agent $i$; call its optimal value $z^*_i$. The knapsack bound is

$$\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .$$

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

$$\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.$$

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$, counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

$$\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},$$

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR$_\lambda$) is a lower bound on (P) (p. 95); (PR$_\lambda$) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$'s part into (PK$_i$), $p_j=c_{2j}-c_{1j}$, and agent $i$'s part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR$_L$) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR$_L$), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR$_\lambda$), the reduction of each agent's subproblem to (PK$_i$), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR$_\lambda$) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR$_\lambda$)" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR$_\lambda$) and (P) can fall below LB), and $m\ge2$. All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR$_\lambda$) value, or that restricts the (PR$_\lambda$) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR$_L$) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$" is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

• G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
• M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

Motivation

Retailers of seasonal goods sell at a full price first and mark down later. Customers who know this can wait for the markdown, and a firm that always has stock left for the markdown teaches them to wait. One remedy is to stock less than the low-price market would absorb, so that a customer who waits risks not getting the good at all. Liu and van Ryzin (Management Science 54(6), 2008) model this capacity rationing as a two-period game between a monopolist who chooses a stocking quantity and risk-averse customers who choose when to buy, and they characterize exactly when rationing is worth its cost in lost sales. The paper belongs to the revenue-management literature on strategic customers, where the firm's decision must anticipate the customers' best response to it.

Setting

A firm announces a price $p_1$ for period 1 and a lower price $p_2<p_1$ for period 2 and buys $C$ units at unit cost $\alpha<p_2$ before sales start; there is no replenishment. A market of $N>0$ customers, each wanting one unit, has valuations $v$ drawn independently from a distribution $F$; from §3 on, $F$ is uniform on $[0,\bar U]$.

Period-2 requests are filled at random with probability $q$, the fill rate, which customers anticipate correctly. Every customer has the same utility $u$: strictly increasing, concave, twice differentiable, with $u(0)=0$; from §3 on, $u(x)=x^\gamma$ with $0<\gamma<1$ (smaller $\gamma$ means more risk aversion). A customer with valuation $v$ buys in period 1 exactly when

$$v\ge p_1\quad\text{and}\quad u(v-p_1)\ge q\,u(v-p_2).$$

The threshold $v(q)$ separates early buyers from waiters.

Under the §3 assumptions, a cutoff $v\in[p_1,\bar U]$ is induced by the fill rate $q(v)=((v-p_1)/(v-p_2))^\gamma$ and the stocking quantity $C(v)=\frac{N}{\bar U}(\bar U-v+(v-p_2)q(v))$. The firm's profit from a segmented market is

$$\Pi(v)=\frac{N}{\bar U}\left((p_1-\alpha)(\bar U-v)+(p_2-\alpha)(v-p_2)\left(\frac{v-p_1}{v-p_2}\right)^\gamma\right),\tag{6}$$

and the profit from serving everybody at the low price is $\Pi^{NS}=(p_2-\alpha)\frac{N}{\bar U}(\bar U-p_2)$. The firm's optimal profit is the larger of $\Pi^0=\max_{p_1\le v\le\bar U}\Pi(v)$ and $\Pi^{NS}$. The first-order condition of (6) is

$$\left(\frac{v-p_1}{v-p_2}\right)^\gamma\left(1+\frac{\gamma(p_1-p_2)}{v-p_1}\right)-\frac{p_1-\alpha}{p_2-\alpha}=0,\tag{7}$$

with root $v^0>p_1$, and the critical valuation bound is

$$U_c=\frac{(p_2+\gamma(p_1-\alpha))v^0-p_2(p_1+\gamma(p_2-\alpha))}{v^0-p_1+\gamma(p_1-p_2)}.\tag{8}$$

In Lean these objects are IsCustomerUtility, buysEarly, cutoff (module LiuVanRyzin.Model) and fillRate, capacity, segProfit, lowPriceProfit, focLHS, criticalU (module LiuVanRyzin.PowerModel).

Formalization targets

Goal: Proposition 3 (p. 1122)

If $\bar U\ge U_c$, rationing is optimal: $v^0\in[p_1,\bar U]$, $v^0$ maximizes $\Pi$ on $[p_1,\bar U]$, and $\Pi(v^0)\ge\Pi^{NS}$. If $\bar U<U_c$, serving the whole market at the low price is optimal:

$$\Pi(v)\le\Pi^{NS}\qquad\text{for all }v\in[p_1,\bar U].$$

The goal fixes no constants; it is the paper's dichotomy, stated with its own (7) and (8).

Milestones, in attack order

1. Proposition 1 (p. 1120): for every $q\in[0,1)$ the threshold $v(q)\ge p_1$ exists and is unique, for a general utility.
2. Proposition 2 (p. 1120): $v(q)$ is strictly increasing in $q$, and convex if $u'''\ge 0$.
3. Proposition 5 (p. 1123): $C(v)$ and $q(v)$ are strictly increasing on $[p_1,\bar U]$, so choosing $C$ is the same as choosing $v$ or $q$.
4. §3.1, root of (7) (p. 1122): the left side of (7) strictly decreases on $v>p_1$ and changes sign, so $v^0$ exists and is unique.
5. Lemma 1 (p. 1122): $\Pi$ is strictly concave on $v\ge p_1$; its maximizer on $[p_1,\bar U]$ is $v^0$ if $v^0\le\bar U$, and $\bar U$ otherwise.
6. §3.1, bounds (p. 1122): $U_c$ decreases in $v^0$, $p_1<v^0<p_1+\gamma(p_2-\alpha)$, and $p_1+\gamma(p_2-\alpha)<U_c<p_1+p_2-\alpha$.

Significance

Proposition 3 answers the paper's central question: whether a firm facing strategic, risk-averse customers should deliberately under-stock. The answer depends on a single number, $U_c$, which depends on prices, cost and risk aversion but not on the market size, and it is compared with the top of the valuation range. Corollary 1, the $\gamma\to1$ limits of Proposition 4, and the comparative statics of Propositions 6–8 on how the optimal fill rate moves with $p_1$, $p_2$ and $\gamma$ are all read off from it. The bounds of milestone 6 turn it into sufficient conditions stated in the primitives alone.

The results are proved in the paper's e-companion (Online Appendix C). No machine-checked proof of any of them is known. Formalizing them gives a verified instance of a pattern that recurs throughout revenue management: a customer best response (a threshold), a reduction of the firm's problem to one scalar decision, a concavity argument, and a comparison of two regimes.

Difficulty

Most of the work is analysis of real powers with a moving base. $\Pi$ contains $(v-p_2)\bigl((v-p_1)/(v-p_2)\bigr)^\gamma$, whose derivative blows up at $v=p_1$, so its concavity on the closed half-line $[p_1,\infty)$ is not a routine second-derivative computation at the endpoint. The regime comparison in Proposition 3 is not implied by Lemma 1: Lemma 1 locates the segmented optimum, but whether it beats $\Pi^{NS}$ depends on $\bar U$, which enters $\Pi$ both through the prefactor $N/\bar U$ and through $\bar U-v$. The equivalence of that comparison with $\bar U\ge U_c$ requires eliminating $(v^0-p_1)/(v^0-p_2)$ with (7).

For Propositions 1–2 the utility is general: the threshold is defined by an inequality between $u(v-p_1)$ and $q\,u(v-p_2)$, and neither its monotonicity in $q$ nor its convexity under $u'''\ge0$ follows from a closed form. Only for $x^\gamma$ is there one.

Formalization scope

All quantities are real numbers. The utility of Propositions 1–2 is a function $u:\mathbb R\to\mathbb R$ that is strictly increasing, concave and continuous on $[0,\infty)$, twice differentiable on $(0,\infty)$, with $u(0)=0$. The threshold $v(q)$ is defined as the infimum of the set of early buyers, not assumed. Powers are Real.rpow; every power-model statement stays on $v\ge p_1$, or on $v>p_1$ where $(v-p_1)^{-1}$ appears. $\Pi$ is written in the closed form (6). The root $v^0$ is a binder constrained by $v^0>p_1$ and (7), and milestone 4 shows such a root exists. "Increases" in Propositions 2 and 5 is read as strictly increasing.

Hypotheses the paper uses without stating them, added here:

• $0\le p_2<\bar U$ in the goal. The uniform law gives $N\bar F(p_2)=\frac N{\bar U}(\bar U-p_2)$ only for $p_2\in[0,\bar U]$, and it makes $\bar U>0$.
• $p_1\le\bar U$ in the second part of Lemma 1, because (6) maximizes over the interval $[p_1,\bar U]$.
• Continuity of $u$ at $0$ in Propositions 1–2. The paper's "twice differentiable" implies it for any utility differentiable at $0$, and $x^\gamma$ satisfies it.
• In Proposition 2, "nonnegative third derivative" is read as $u\in C^3(0,\infty)$ with $u'''\ge0$ there.

The goal cannot be trivialized: $v^0$ is pinned to the root of (7), part 2 quantifies over every $v\in[p_1,\bar U]$, and the optimum is compared with $\Pi^{NS}$ exactly as the paper defines optimality.

Contributions are welcome at every level. Useful ones include the real-power calculus lemmas behind milestones 3–6, a proof of Propositions 1–2 for general concave utilities, and reusable facts about thresholds defined by single-crossing inequalities.

Selected references

• Q. Liu, G. van Ryzin, Strategic Capacity Rationing to Induce Early Purchases, Management Science 54(6):1115–1131, 2008. https://doi.org/10.1287/mnsc.1070.0832
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer, 2004. https://doi.org/10.1007/b139000

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_i x_i F_i \succeq 0$. When the data $F_i$ are uncertain, El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) proposed to optimize against the worst case over a norm-bounded family of perturbations: the robust SDP. Their Theorem 3.1 shows that, for unstructured ("full") perturbations, the robust SDP is itself an SDP in the enlarged variable $(x,\tau)$. Section 4 of the paper then asks what robustification does to the solution. Nominal SDPs are often ill-posed: the optimal set can be a whole face, and optimal points can jump under small data changes. Section 4 shows that, under explicit hypotheses, the robust problem has a unique solution with quadratic growth, which is the sense in which the paper describes robustness as a regularization of SDPs. This mission formalizes that result, Theorem 4.2.

Setting

Fix natural numbers $m, n, p, q$, matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$ (symmetric), $R_0, \dots, R_m \in \mathbb{R}^{q\times n}$, $L \in \mathbb{R}^{n\times p}$, and an objective vector $c \in \mathbb{R}^m$, $c \neq 0$. Write $F(x) = F_0 + \sum_{i=1}^m x_iF_i$ and $R(x) = R_0 + \sum_{i=1}^m x_iR_i$.

With full perturbations, uncertainty level $\rho = 1$ and $D = 0$ (the standing choices of §4), the robust SDP is the SDP

$$\text{minimize } c^Tx \quad\text{subject to}\quad \mathcal{F}(x,\tau) = \begin{bmatrix} F(x) - \tau LL^T & R(x)^T \\ R(x) & \tau I\end{bmatrix} \succeq 0 \tag{15}$$

in the variables $y = (x,\tau) \in \mathbb{R}^m \times \mathbb{R}$. A point is feasible if $\mathcal{F}(x,\tau) \succeq 0$ (symmetric positive semidefinite) and optimal if it is feasible and minimizes $c^Tx$ over all feasible $(x',\tau')$. The solution is the pair $(x,\tau)$.

The paper's hypotheses (§4.1):

• H1 (Slater): $\mathcal{F}(x,\tau) \succ 0$ for some $(x,\tau)$.
• H2 (inf-compactness): every sublevel set $\{(x,\tau)\ \text{feasible} : c^Tx \le M\}$ is bounded.
• H3(a): the nullspace of the pencil $\lambda R_0 + \sum_i x_iR_i$ is one and the same proper subspace $N \subsetneq \mathbb{R}^n$ for every $(\lambda,x) \neq (0,0)$.
• H3(b): for every $x$ the stacked matrix $\begin{bmatrix} L^T \\ R(x)\end{bmatrix}$ has full column rank.

For $\tau > 0$ put $G(x,\tau) = F(x) - \tau LL^T - \frac{1}{\tau}R(x)^TR(x)$, the Schur complement of the block $\tau I$ in $\mathcal{F}(x,\tau)$.

The quadratic growth condition (QGC) holds at an optimal point $y^\star = (x^\star,\tau^\star)$ if there are $\alpha, \varepsilon > 0$ with

$$c^Tx \ \ge\ c^Tx^\star + \alpha\,\|y - y^\star\|^2 \qquad \text{for every feasible } y = (x,\tau),\ \|y - y^\star\| < \varepsilon .$$

Formalization targets

Goal: Theorem 4.2 (p. 39)

Under $c \neq 0$, symmetry of the $F_i$, H1, H2, H3(a) and H3(b):

$$\bigl(\forall\, y^\star \text{ optimal for (15)}:\ \text{QGC holds at } y^\star\bigr)\quad\text{and}\quad \exists!\, y = (x,\tau) \text{ optimal for (15)} .$$

Both halves are stated; uniqueness is of the pair $(x,\tau)$, and existence is part of the claim.

Milestones, in the order the paper's proof uses them

1. §4.1 (p. 38): H3(a) implies $R(x) \neq 0$ for every $x$.
2. §4.2 (p. 39): under H3(a), every feasible $\tau$ is positive; in particular $\tau_{\mathrm{opt}} > 0$.
3. §4.2, Eq. (16): for $\tau > 0$, $\mathcal{F}(x,\tau) \succeq 0 \iff G(x,\tau) \succeq 0$.
4. Appendix A (p. 49): at every optimal $(x,\tau)$ there is a dual matrix $Z \succeq 0$, $Z \neq 0$, with $\operatorname{Tr} ZG(x,\tau) = 0$, $\operatorname{Tr} Z\,\partial G/\partial x_i = c_i$ and $\tau^2\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z$.
5. Appendix A (p. 49): H3(b) rules out $\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z = 0$ for $Z \succeq 0$, $Z \neq 0$, hence $\operatorname{Tr}R(x)^TR(x)Z > 0$.
6. Appendix A (pp. 49–50): under H3(a), with $\tau > 0$, $Z \succeq 0$ and $\operatorname{Tr}R(x)^TR(x)Z > 0$, the Hessian of the Lagrangian $c^Tx - \operatorname{Tr} Z\,G(x,\tau)$ is positive definite.

Significance

The result. Theorem 4.2 turns the robust SDP into a well-posed problem: a unique solution with quadratic growth. Quadratic growth is the property from which the paper's Hölder-stability results (Theorem 4.3, Corollaries 4.1–4.2) follow through the perturbation theory of Bonnans, Cominetti and Shapiro, and it is what justifies using the robust SDP as a regularization of ill-conditioned SDPs (§5.4). The remark after the theorem notes a geometric reading: the growth holds for every objective, so the boundary of the robust feasible set contains no facets.

Formalizing it. The theorem has a published proof (Appendix A), which relies on a second-order sufficient condition for nonlinear SDPs cited from Bonnans, Cominetti and Shapiro. There is no machine-checked proof of it or of any second-order optimality result for SDPs that we know of. A formalization provides a complete account of the dual attainment, complementarity and second-order steps for this concrete problem class, and it checks the paper's computations; one of them, the intermediate display for the second derivative in Appendix A, has a factor error in its cross term that does not affect the conclusion.

Difficulty

The feasible set of (15) is a spectrahedron, and linear objectives over spectrahedra do not in general have unique minimizers, since optimal faces can be flat. Uniqueness therefore cannot come from convexity alone. It has to come from curvature of the boundary at the optimum, and that curvature is carried only by the nonlinear term $\frac{1}{\tau}R(x)^TR(x)$ of the Schur complement, which is degenerate along some directions. Positive definiteness of the Hessian must be recovered from the structural hypotheses H3(a) and H3(b), which interact with a dual matrix $Z$ that is known only to exist. The natural first attempt is to use $\tau > 0$ and the positive semidefiniteness of $Z$ directly. That attempt fails: the second derivative is $\operatorname{Tr} Z\,\mathcal{R}^T\mathcal{R}$ for a direction-dependent matrix $\mathcal{R}$, which vanishes on the kernel of $Z$, so it is not positive without H3(a) relating the kernels of all members of the pencil. Dual attainment and complementarity for (15) also have to be established, and the local second-order bound then has to be converted into a statement about every nearby feasible point.

Formalization scope

• Representation. Data are bundled in RobustSDP.Uniqueness.SDPData m n p q; decision points are pairs y : (Fin m → ℝ) × ℝ; the coefficient Fs i, i : Fin m, is the paper's $F_{i+1}$. $\succeq 0$ and $\succ 0$ are Mathlib's Matrix.PosSemidef and Matrix.PosDef, which include symmetry, as the paper's notation does.
• Conventions fixed. §4's standing choices $D = 0$ and $\rho = 1$ are built into (15). The standing assumptions $c \neq 0$ and symmetric $F_i$ (p. 33) are explicit hypotheses. H2 is read as bounded sublevel sets of the feasible set in $(x,\tau)$; the paper's wording ("any unbounded sequence of feasible points produces an unbounded sequence of objectives") is meant in this sense, as its claim that H1 and H2 give existence of optimal points shows. H3(b)'s full column rank is injectivity of $\xi \mapsto (L^T\xi, R(x)\xi)$. The QGC uses the Euclidean norm on $\mathbb{R}^{m+1}$ in its local form, which is equivalent to the paper's $o(\|y - y_{\mathrm{opt}}\|^2)$ form. It is stated for (15) rather than for the paper's reformulation (16), with which (15) coincides near the optimum because $\tau_{\mathrm{opt}} > 0$. The auxiliary constraint $\tau \ge 0.99\,\tau_{\mathrm{opt}}$ of (16) is not formalized. $G$ uses Lean's τ⁻¹, which is $0$ at $\tau = 0$, so every statement about $G$ assumes $\tau > 0$ or $\tau \ne 0$.
• No trivializing reading. The goal cannot be satisfied by stating only uniqueness of $x$, by reading H2 as "the objective is bounded below", or by reading H3(a) as "$R(x) \neq 0$". The statement quantifies over the pair $(x,\tau)$, and both the quadratic growth and the existence and uniqueness halves are required. The hypotheses are jointly satisfiable: for example $m = 1$, $n = p = 2$, $q = 4$, $F(x) = \mathrm{diag}(3+x, 3-x)$, $L = I_2$, $R(x) = [1; x]\otimes I_2$ and $c = 1$.
• Infrastructure. A complete development needs Schur complements for positive semidefinite block matrices (available in Mathlib), strong duality with dual attainment for inequality-form SDPs under Slater's condition (ConvexOptimization.sdp_strong_duality on the platform, in another Mathlib environment), existence of minimizers on closed bounded sets, second derivatives of matrix-valued maps, and a local second-order argument for convex problems. The duality and second-order parts can be reused beyond this mission. Contributions to any milestone, or alternative proofs that avoid the general Bonnans–Cominetti–Shapiro theory, are welcome.

Selected references

• L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
• J. F. Bonnans, R. Cominetti and A. Shapiro, Sensitivity analysis of optimization problems under second order regular constraints, Math. Oper. Res. 23(4), 806–831, 1998 (the paper's reference [10]). https://doi.org/10.1287/moor.23.4.806
• A. Shapiro, First and second order analysis of nonlinear semidefinite programs, Math. Programming Ser. B 77, 301–320, 1997. https://doi.org/10.1007/BF02614439
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A variational inequality asks for a point $x$ of a set $K\subseteq\mathbb R^n$ at which a vector field $f$ makes a non-obtuse angle with every feasible direction: $(x'-x)^T f(x)\ge 0$ for all $x'\in K$. It is the common form of the first-order optimality condition of a constrained optimization problem, of complementarity problems in mathematical programming, and of equilibrium conditions in traffic networks and economics. Two generalizations are standard in operations research. In a quasi-variational inequality the constraint set depends on the unknown, $K=K(x)$, as in generalized Nash games where each player's feasible set depends on the other players' choices. In a generalized variational inequality the vector field is set-valued, $y\in f(x)$, as when $f$ is the subdifferential of a nonsmooth convex function.

D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the problem that combines both, the generalized quasi-variational inequality (GQVI), and proved existence theorems for it. Their §5 gives a second route to existence, independent of the set-valued fixed point theory of their §3: a solution is a fixed point of a map built from Euclidean projections, and for single-valued continuous $f$ the Brouwer fixed point theorem produces one. The characterization of solutions as projection fixed points, for the generalized variational inequality, is due to Fang and Peterson (reference [11] of the paper, a 1979 University of Maryland Baltimore County research report). This mission formalizes that projection route.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^Ty$ and norm $\|x\|$. A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a subset $K(x)\subseteq\mathbb R^n$; a point-to-point mapping $f$ assigns a vector $f(x)$.

The GQVI. Given point-to-set mappings $K$ and $f$, $\mathrm{GQVI}(K,f)$ asks for vectors $x$ and $y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^Ty\ge 0\ \text{ for all } x'\in K(x).$$

Such a pair is a solution. For a point-to-point $f$ one takes $y=f(x)$: find $x\in K(x)$ with $(x'-x)^Tf(x)\ge0$ for all $x'\in K(x)$.

Projection. For a set $S$ and a point $z$, the projection $P_S(z)=\operatorname{sol}\min_{x\in S}\|x-z\|$ is the nearest point of $S$ to $z$. For nonempty closed convex $S$ it exists and is unique.

Semicontinuity of point-to-set mappings (Berge). $K$ is upper semicontinuous at $x$ if for every open $G\supseteq K(x)$ there is a neighbourhood $N$ of $x$ with $K(x')\subseteq G$ for $x'\in N$; lower semicontinuous at $x$ if for every open $G$ meeting $K(x)$ there is a neighbourhood $N$ of $x$ with $K(x')\cap G\ne\emptyset$ for $x'\in N$; continuous if both. "On a set $C$" means at every point of $C$, with neighbourhoods relative to $C$.

Formalization targets

Goal: Theorem 5.2 (p. 220)

Let $f$ be continuous on a nonempty compact convex set $C$, and let $K$ be a continuous mapping on $C$ whose values $K(x)$, $x\in C$, are nonempty, closed, convex and contained in $C$. Then there is $x$ with

$$x\in K(x),\qquad (x'-x)^Tf(x)\ge 0\quad\text{for all }x'\in K(x).$$

Milestone: Lemma 5.1 (p. 220)

If $K$ is continuous at $x_0$ and every $K(x)$ is nonempty, closed and convex, then for every $y_0$ the map

$$(x,y)\longmapsto p(x,y)=P_{K(x)}(y)$$

is continuous at $(x_0,y_0)$.

Milestone: Theorem 5.1 (p. 220)

If every $K(x)$ is closed and convex, then for every pair $(x^*,y^*)$

$$(x^*,y^*)\ \text{solves}\ \mathrm{GQVI}(K,f)\iff x^*=P_{K(x^*)}(x^*-y^*)\ \text{and}\ y^*\in f(x^*).$$

The Brouwer fixed point theorem is already on the platform (AGT.brouwer_fixed_point) and is included as a reference item, as is the Hilbert-space nearest-point theorem VectorSpaceOpt.min_distance_convex_set.

Significance

Theorem 5.2 is the existence theorem for quasi-variational inequalities with a moving convex constraint set and a continuous single-valued field, under compactness. With $K$ constant it is the Hartman–Stampacchia theorem (Acta Math. 115 (1966) 271–310), the basic existence result for finite-dimensional variational inequalities, and so it also covers existence of equilibria of generalized Nash games whose shared constraints satisfy the continuity hypotheses. The paper notes that Theorem 5.2 also follows from its Corollary 3.1, which rests on the Eilenberg–Montgomery fixed point theorem; the projection route needs only Brouwer.

Theorem 5.1 matters beyond this existence result: it turns the GQVI into a fixed-point equation, which is the basis of projection algorithms for variational inequalities and of the contraction argument of the paper's Theorem 5.3. Lemma 5.1, continuity of the projection onto a continuously moving closed convex set, is a stability result used throughout parametric optimization.

All three statements were proved in 1982. None has a machine-checked proof on the platform or in Mathlib, which has neither a projection onto a general closed convex set as a function of the set nor any variational inequality. The work of this mission is to formalize the known proofs.

Difficulty

Theorem 5.1 is a direct consequence of the variational characterization of the nearest point of a convex set. The substance lies in Lemma 5.1 and in adapting it to the goal. The projection depends on the set $K(x)$, not only on the point, and continuity of $K$ is a statement about sets, given by two separate semicontinuity conditions that each control only one side of the convergence. Neither alone suffices: upper semicontinuity without lower lets $K(x)$ shrink abruptly and the nearest point jump; lower without upper lets limits of nearest points fall outside $K(x_0)$. The limit points of the projections must also be kept bounded, which needs the nonemptiness near $x_0$.

A second difficulty is that the goal assumes continuity of $K$ only on $C$, with neighbourhoods relative to $C$, while Lemma 5.1 is stated for continuity at a point of $\mathbb R^n$. Applying the lemma to the composite map $x\mapsto P_{K(x)}(x-f(x))$ on $C$ therefore requires either a relative version of the lemma or a reduction; the lemma cannot be quoted verbatim.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with its Euclidean norm, never the sup-norm space Fin n → ℝ. Point-to-set mappings are functions into Set. The solution predicate is IsGQVISolution K f x y; a point-to-point $f$ enters as fun z => {f z}. Upper and lower semicontinuity are Mathlib's UpperHemicontinuousAt/On and LowerHemicontinuousAt/On; "continuous on $C$" is both, relative to $C$.

The projection is IsProj S z p (nearest-point predicate) and proj S z, which returns a nearest point when one exists and the junk value $z$ otherwise. Theorem 5.1 uses the relational form, so no junk value enters when $K(x^*)=\emptyset$. Lemma 5.1 assumes every $K(x)$ nonempty, closed and convex, so proj is always the true projection there.

Two hypotheses implicit in the paper are explicit:

1. Closed values in Theorem 5.2. The paper uses Berge's definitions, under which upper semicontinuous mappings have compact values, and its proof uses that each $K(x)$ is closed. The Lean statement assumes $K(x)$ closed for $x\in C$; without it the theorem is false ($C=[0,1]$, $K(x)\equiv(0,1)$, $f\equiv1$).
2. Nonempty values in Lemma 5.1. The projection function $p(x,y)=P_{K(x)}(y)$ is defined only for nonempty $K(x)$; the Lean statement assumes $K(x)\ne\emptyset$ for all $x$.

A formalization in which the projection is merely "some point of $K(x)$", or ignores the distance, would make the reverse direction of Theorem 5.1 false and Lemma 5.1 meaningless; a GQVI whose test points range over $C$ instead of $K(x)$ would turn Theorem 5.2 into a plain variational inequality on $C$. Both are excluded by the definitions above.

A complete development needs the nearest-point characterization on closed convex sets (available in Mathlib and on the platform), sequential characterizations of upper and lower hemicontinuity for closed-valued mappings in $\mathbb R^n$, continuity of the projection onto a moving convex set, and Brouwer's theorem (a platform reference). The hemicontinuity lemmas and the projection-continuity lemma are reusable for the other missions of this series and for parametric optimization in general. Proofs of Lemma 5.1 and Theorem 5.1, a relative-to-$C$ version of Lemma 5.1, and a proof of Brouwer's theorem are all welcome.

Selected references

• D. Chan and J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. C. Fang and E. L. Peterson, Generalized variational inequalities, Mathematics Research Report No. 79-10, Department of Mathematics, University of Maryland Baltimore County, October 1979 (cited by Chan and Pang as [11]; no online copy).
• P. Hartman and G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
• C. Berge, Topological Spaces, The Macmillan Company, New York, 1963 (definitions of upper and lower semicontinuity of point-to-set mappings).

Motivation

Infinite-horizon optimal control problems with nonnegative costs (Strauch's negative dynamic programming, the positive-cost counterpart of Blackwell's positive model) are among the settings where the standard tools of discounted dynamic programming fail: there is no contraction, costs may be infinite, and the value-iteration algorithm started from zero may converge to the wrong limit. Strauch showed in 1966 that under these assumptions the limit of value iteration can lie strictly below the optimal cost (Strauch 1966). Bertsekas (1977) recast the deterministic, stochastic and minimax versions of these problems as one abstract problem about a monotone mapping $H$, and proved Bellman's equation, optimality criteria for stationary policies, and conditions for convergence of the dynamic programming algorithm at that level of generality (Bertsekas 1977). This framework became the basis of the "abstract dynamic programming" theory developed later in Bertsekas and Shreve (1978) and Bertsekas (2013, 2022).

This mission formalizes the part of the paper that works under the uniform increase assumption, culminating in the paper's compactness condition for convergence of value iteration.

Setting

A model consists of a nonempty state space $S$, a control space $C$, for each $x\in S$ a nonempty constraint set $U(x)\subseteq C$, a mapping $H:S\times C\times F\to[-\infty,+\infty]$, where $F$ is the set of functions $J:S\to[-\infty,\infty]$ ordered pointwise, and a terminal function $\bar J\in F$ with $\bar J(x)>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for $u\in U(x)$.

A selector is $\mu:S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors, and $\{\mu,\mu,\dots\}$ is stationary. Define

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$ $$J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J)(x),\qquad J^*(x)=\inf_\pi J_\pi(x),\qquad J_\infty(x)=\lim_{N\to\infty}T^N(\bar J)(x).$$

$J^*$ is the optimal value function and $J_\infty$ the limit of the dynamic programming algorithm. A policy is optimal if $J_\pi=J^*$.

Assumption I is $\bar J(x)\le H(x,u,\bar J)$ for all $x$ and $u\in U(x)$. Assumption I.1 says that $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $\bar J$. Assumption I.2 says there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+re)\le H(x,u,J)+\alpha r$ for $r>0$ and $J\ge\bar J$, where $e\equiv1$. For the convergence analysis the paper introduces, for $k\ge1$, the sets $C_k=\{(x,u,\lambda)\mid u\in U(x),\ H[x,u,T^{k-1}(\bar J)]\le\lambda\}$ with $\lambda$ real, their projections $P(C_k)$ on $(x,\lambda)$ through admissible $u$, and the closure $\overline{P(C_k)}$ obtained by adding limits of real sequences $\lambda_n$ at fixed $x$.

Formalization targets

Goal: Proposition 12

Let I, I.1, I.2 hold, let $C$ be a Hausdorff topological space, and suppose there is $\bar k$ such that $U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ is compact for every $x$, real $\lambda$ and $k\ge\bar k$. Then

$$P\Bigl(\bigcap_{k\ge1}C_k\Bigr)=\bigcap_{k\ge1}\overline{P(C_k)},\qquad J_\infty=T(J_\infty)=T(J^*)=J^*,$$

and there exists an optimal stationary policy.

Milestones

In attack order: Proposition 2 ($J_N=T^N(\bar J)$ for the $N$-stage problem); Proposition 4 ($\varepsilon$-optimal policies, stationary when $\alpha<1$); Proposition 5 (Bellman's equation $J^*=T(J^*)$ and minimality of $J^*$ among $T$-excessive functions above $\bar J$); Corollary 5.1 (the same for $J_\mu$); Proposition 7 ($\{\mu^*,\mu^*,\dots\}$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$); Proposition 10 ($J_\infty\le T(J_\infty)\le T(J^*)=J^*$, with equality throughout iff $J_\infty=T(J_\infty)$); Lemma 2 ($\overline{P(C_k)}=E[T^k(\bar J)]$, the epigraph); Proposition 11 (convergence of value iteration is equivalent to interchanging projection and intersection); Lemma 3 (a function with compact real sublevel sets attains its minimum).

Significance

The result. Proposition 12 gives a checkable condition, compactness of sublevel sets of the one-stage costs, under which value iteration started at $\bar J$ converges to the optimal cost and an optimal stationary policy exists, in any model covered by the abstract framework: deterministic and stochastic control with nonnegative costs, minimax control, and problems with state constraints encoded by infinite costs. Without such a condition the algorithm can stall below $J^*$ even in one-dimensional deterministic problems. Propositions 5 and 7 are the abstract form of the classical Bellman equation and optimality criterion for positive-cost problems.

Formalizing it. The results are proved in the paper. The platform's existing dynamic programming results are finite-state, real-valued and contraction-based; none covers extended-real costs, general state spaces, or the uniform increase regime. This mission would produce a machine-checked abstract DP layer over EReal in which the Bellman equation, the stationary-policy criterion and the convergence conditions are proved once for every model satisfying the assumptions. No machine-checked proof of these results is known.

Difficulty

The obvious argument for $J_\infty=J^*$ interchanges a limit in $N$ with an infimum over policies. Under Assumption I the iterates increase, and a limit of infima of an increasing family can be strictly smaller than the infimum of the limits; the paper's own example in Section 1 shows it. Monotone convergence arguments therefore do not apply. The paper converts the interchange into a statement about projections of the sets $C_k$ and closes the gap with a compactness argument, which requires handling infinite values carefully: epigraphs are taken over real $\lambda$ only, and states where the value is $+\infty$ are treated separately. Proposition 4, on which Bellman's equation rests, needs a selection of nearly optimal policies state by state and a geometric control of the errors through I.2.

Formalization scope

Functions in $F$ are S → EReal. Policies are sequences ℕ → Selector, where a selector is a function with $\mu(x)\in U(x)$ for all $x$. The composition $T_{\mu_0}\cdots T_{\mu_{N-1}}$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ and $J_\infty$ are limUnder atTop of their defining sequences. Every statement assumes Assumption I, under which these sequences are nondecreasing and the limits exist. $T$ takes the infimum over $U(x)$ only and $J^*$ over admissible policies only. Both $S$ and each $U(x)$ are nonempty. $\lambda$ ranges over $\mathbb R$, and the closure $\overline{\,\cdot\,}$ is the sequential closure in $\lambda$ at fixed $x$, not a topological closure on $S\times\mathbb R$. The sets $C_k$ are used only for $k\ge1$. I.2 is parameterized by its scalar $\alpha$. Proposition 4's second part refers to the $\alpha$ for which I.2 is assumed.

Repairs of the page. Lemma 3 is false as printed. On $\mathbb N$ with the cofinite topology every subset is compact, yet $f(n)=-n$ has no minimum. It also fails for $U=\emptyset$. The mission states Lemma 3 for a Hausdorff space $C$ and nonempty $U$, and Proposition 12 for a Hausdorff control space. Proposition 12 is also false as printed: with $S=\{0\}$, $C=U(0)=\mathbb N$ cofinite, $\bar J(0)=0$ and $H(0,u,J)=J(0)+1/(u+1)$, all hypotheses hold but no stationary policy is optimal and (70) fails. Proposition 11(b)'s parenthetical "(equivalently there exists an optimal stationary policy)" holds only together with $J_\infty=J^*$ (the paper cites an example with an optimal stationary policy and $J_\infty\neq J^*$). It is stated in that joint form, never as an equivalence between condition (68) and the bare existence of an optimal stationary policy.

Trivializing readings ruled out. An empty constraint set would make $T\equiv+\infty$ and the policy set empty, so every Bellman identity would hold trivially. The model therefore requires $U(x)\neq\emptyset$. The goal's three conclusions, (70), the chain of equalities and the optimal stationary policy, are all required, so a formalization that states only one of them is not the goal.

Needed infrastructure: monotone limits in EReal, infima over sets, and compactness in Hausdorff spaces (Mathlib's Cantor intersection theorem). The definitions (model, assumptions, epigraph sets) can be reused for the companion mission under Assumption D and for later abstract DP developments. Proofs of any milestone are welcome, as are reusable lemmas on monotone EReal sequences.

Selected references

• D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. http://web.mit.edu/dimitrib/www/abstractdp.html

Motivation

Conic quadratic programs (second-order cone programs) minimize a linear objective subject to linear constraints and constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. They model robust linear programs with ellipsoidal uncertainty, truss topology design, contact problems with Coulomb friction, and convex quadratically constrained quadratic programs. In theory they are no harder than linear programs of the same size; in practice, linear programming software handles far larger instances than conic quadratic solvers did at the time of writing (Ben-Tal & Nemirovski 2001, pp. 193–195). This raises a question about geometry rather than algorithms: can a second-order cone be replaced by a polyhedral cone of moderate size without losing much accuracy?

The obvious answer — circumscribe the cone by a polyhedral cone with many facets — fails: the number of facets must grow exponentially in the dimension, even for constant accuracy. Ben-Tal and Nemirovski showed that auxiliary variables change the picture completely: a projection of a polyhedral cone can approximate the Lorentz cone with size only $O(k\ln(1/\varepsilon))$. The construction is now standard; it underlies, for instance, the lifted linear-programming branch-and-bound algorithm for mixed-integer conic quadratic programs of Vielma, Ahmed & Nemhauser 2008.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The $(k+1)$-dimensional Lorentz cone is

$$L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.$$

Fix $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map

$$\Pi(y,t,u):\mathbb R^k\times\mathbb R\times\mathbb R^{p}\to\mathbb R^{q}$$

such that

1. if $(y,t)\in L^k$, there is $u\in\mathbb R^p$ with $\Pi(y,t,u)\ge0$ (componentwise);
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Equivalently, the polyhedral cone $\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone lying between $L^k$ and its $(1+\varepsilon)$-extension. The size of the approximation is $p+q$: the number of auxiliary variables plus the number of linear inequalities (an equation counts as two).

The construction in the paper uses a tower of variables: for $k=2^\theta$, the coordinates $y_1,\dots,y_k$ form generation $0$, each consecutive pair of generation $\ell-1$ has a successor in generation $\ell$ ($y_i^\ell$ has parents $y_{2i-1}^{\ell-1},y_{2i}^{\ell-1}$), and the single variable of generation $\theta$ is $t$. It also uses an explicit linear system (8) in variables $\xi^j,\eta^j$, $j=0,\dots,\nu$, with trigonometric coefficients $\cos(\pi/2^{j+1})$, $\sin(\pi/2^{j+1})$, $\tan(\pi/2^{\nu+1})$, whose accuracy is $\delta(\nu)=1/\cos(\pi/2^{\nu+1})-1$.

Formalization targets

Goal: Theorem 1.1

There is an absolute constant $C$ such that for every positive integer $k$ and every $\varepsilon\in(0,1]$, $L^k$ admits a polyhedral $\varepsilon$-approximation with

$$p_k+q_k\le C\,k\ln\frac{2}{\varepsilon}.$$

The constant is not fixed; the goal asserts only the order of growth, which is what the paper claims.

Milestones

1. §2, Eq. (5). For $k=2^\theta$, $\theta\ge1$: $(y,t)$ extends to a tower solving $\sqrt{[y_{2i-1}^{\ell-1}]^2+[y_{2i}^{\ell-1}]^2}\le y_i^\ell$ for all $i,\ell$ if and only if $\|y\|_2\le t$.
2. §2, Eqs. (6)–(7). Placing polyhedral $\varepsilon_\ell$-approximations of $L^2$ on every level of the tower yields a polyhedral approximation of $L^k$ with $1+\varepsilon=\prod_{\ell=1}^\theta(1+\varepsilon_\ell)$.
3. Proposition 2.1 (i), (ii) and Eq. (9). System (8) is a polyhedral $\delta(\nu)$-approximation of $L^2$, and $\delta(\nu)=O(4^{-\nu})$.
4. Proof of Theorem 1.1, system (10), property 3. System (8) with parameter $\nu_\ell$ on level $\ell$ of the tower approximates $L^{2^\theta}$ with quality $\beta=\prod_{\ell=1}^\theta 1/\cos(\pi/2^{\nu_\ell+1})-1$.
5. Proof of Theorem 1.1, choice of $\nu_\ell$. With $\nu_\ell=\lfloor c\,\ell\ln(2/\varepsilon)\rfloor$: $\beta\le\varepsilon$ and $\sum_\ell 2^{\theta-\ell}\nu_\ell\le C\,2^\theta\ln(2/\varepsilon)$.

Significance

The theorem shows that conic quadratic constraints are, up to a factor logarithmic in the accuracy, no more expensive to express as linear constraints than they are in their native form. Consequences listed in the paper include approximating convex quadratically constrained quadratic programs, robust counterparts of linear programs with ellipsoidal uncertainty, and problems with low-dimensional cones (Coulomb friction, $k\le3$; truss design, $k\le2$) by linear programs of comparable size. Together with the matching lower bound of §3 of the same paper (a separate mission of this series), it pins down the size of the best polyhedral approximation up to constants. The recursive halving of dimensions through the tower of 3-dimensional cones is a reusable device for other rotation-invariant cones.

The result is proved in the paper; as far as is known it has not been machine-checked. This mission produces a formal proof of the construction, including the trigonometric estimate $\delta(\nu)=O(4^{-\nu})$ and the explicit linear encoding with its size count. Explicit values of the absolute constants are welcome as additional results.

Difficulty

The planar estimate is the core. Part (ii) of Proposition 2.1 must hold for every solution of the inequality system (8), not only for the solution one would write down for a given point of $L^2$; an argument that tracks only the intended solution proves part (i) and nothing about part (ii). The accuracy must also come out as $1/\cos(\pi/2^{\nu+1})-1$, geometric in $\nu$; a bound that decays only polynomially in $\nu$ would give size $\mathrm{poly}(1/\varepsilon)$ instead of $\ln(1/\varepsilon)$. The naive idea of approximating $L^k$ directly by tangent hyperplanes is ruled out by the exponential facet count mentioned above; the auxiliary variables are indispensable. The second difficulty is bookkeeping: packaging $k-1$ copies of system (8) on a tower of depth $\theta=\log_2 k$ into a single linear map, counting its variables and inequalities exactly, handling $k$ that is not a power of two, and summing the accuracies so that the total size is $O(k\ln(2/\varepsilon))$ rather than $O(k\ln k\ln(1/\varepsilon))$.

Formalization scope

• Vectors of $\mathbb R^k$ are Fin k → ℝ. The norm $\|y\|_2$ is written out as eucNorm y = Real.sqrt (∑ i, y i ^ 2); the norm Mathlib attaches to Fin k → ℝ is the sup norm, under which the cone would be polyhedral and the theorem trivial.
• A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ) and $\ge0$ is the componentwise order. Linearity is essential: with an arbitrary map, $\Pi(y,t)=t-\|y\|_2$ would be an exact approximation with $p=0$, $q=1$. Affine maps are not allowed either; the paper's approximations are homogeneous.
• The paper's absolute constants $O(1)$ are existential constants quantified before $k$, $\varepsilon$ and $\theta$. The goal requires $k\ge1$ and $\varepsilon\in(0,1]$, as in the paper; $\ln$ is Real.log.
• System (8) and system (10) are stated as propositions with the absolute values written out; their parameters $\nu$, $\nu_\ell$ are required to be positive integers, as in the paper (at $\nu=0$ the coefficient $\tan(\pi/2)$ would be evaluated as $0$ by Lean).
• Tower variables are indexed Y ℓ i with 0-based i, so the parents of Y ℓ i are Y (ℓ-1) (2i) and Y (ℓ-1) (2i+1); the milestones on (6)–(7) and (10) are stated on solution sets rather than on an explicit linear map. The size counts of (10) (properties 1–2) are not separate milestones; the arithmetic milestone on $\nu_\ell$ records the bound on $\sum_\ell 2^{\theta-\ell}\nu_\ell$ to which they reduce.
• $\delta(\nu)=O(1/4^\nu)$ is stated as $\exists C>0,\ \forall\nu\ge1,\ \delta(\nu)\le C/4^\nu$.

A complete development needs: elementary trigonometry of $\pi/2^{j}$ (available in Mathlib), rotations in the plane, finite products and sums over $\{1,\dots,\theta\}$, and a way to assemble many small linear systems into one linear map with an exact count of rows and columns. The last piece, and the tower of variables with the reduction from arbitrary $k$ to a power of two, are reusable for other lifted polyhedral approximations. Contributions of any milestone, of explicit linear encodings of (8) and (10), and of the extension from $k=2^\theta$ to all $k$ are welcome.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• J. P. Vielma, S. Ahmed and G. L. Nemhauser, A lifted linear programming branch-and-bound algorithm for mixed-integer conic quadratic programs, INFORMS Journal on Computing 20(3):438–450, 2008. https://doi.org/10.1287/ijoc.1070.0256
• A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829