Optimization

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.

Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective

where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.

Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.

Motivation

The joint replenishment problem (JRP) is a basic model of inventory coordination: several items are ordered from one supplier, each item pays its own ordering and holding costs, and an additional item-independent joint ordering cost rewards ordering the items at common times. Two accounting conventions are studied. In the periodic JRP (also called the general integer model; see the survey of Goyal and Satir, 1989) the joint cost is charged at every point of a common grid, whether or not an item is ordered there; in the aperiodic JRP it is charged only at actual order times.

For decades the literature produced heuristics and enumerative algorithms for the JRP without a polynomial-time exact algorithm and without evidence that none exists. Schulz and Telha (arXiv:2007.09045v1; published in Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard) showed that already the two-item problem is at least as hard as integer factorization, in both variants. For the periodic JRP the paper notes (p. 10): "No hardness results were previously known for the periodic JRP."

Timeline, as recorded in the paper (pp. 4–5):

• 2011: Schulz and Telha announce that the two-item aperiodic JRP is at least as hard as integer factorization (Theorem 1(a)).
• 2018: Cohen-Hillel and Yedidsion prove that the aperiodic JRP with an arbitrary number of items is strongly NP-hard.
• 2020: the preprint arXiv:2007.09045v1 adds the periodic case (Theorem 1(b), via Lemma 2, the subject of this mission) and, assuming the Riemann hypothesis, NP-hardness of the two-item periodic JRP under randomized reductions (Theorem 2).

Setting

An item with ordering cost $K \ge 0$ and holding cost $H \ge 0$, replenished every $q$ time units, where $q$ is a positive integer, has the EOQ cost

In the two-item periodic JRP, item $i \in \{1,2\}$ has parameters $(K_i, H_i)$ and an integer period $q_i \ge 1$, and a joint ordering cost $K_0 > 0$ is incurred every $\rho$ time units, where $\rho$ divides both periods. At an optimum $\rho = \gcd(q_1,q_2)$, and the problem is to minimize objective (3) of the paper,

An optimal solution is a pair of positive integers whose value is at most the value of every pair of positive integers.

Given a natural number $M$, the instance of Lemma 2 is

with objective written $\mathrm{JRP}_M$ and item 2's cost $\mathrm{EOQ}_2(q) = K_2/q + H_2 q$. Fixing $q_2 = M$ leaves the single-variable problem (4):

An odd composite number is an odd integer $M > 1$ that is not prime.

Formalization targets

Goal: Lemma 2 (p. 11)

For every odd composite $M$: the coefficients of the instance above satisfy $K_0 > 0$ and are natural numbers at most $M^5$; the instance has an optimal solution; and every optimal solution $(q_1,q_2)$ satisfies

The goal does not say which non-trivial divisor $\gcd(q_1,M)$ is: optimal solutions need not be unique (for $M = 15$ both $q_1 = 3$ and $q_1 = 5$ are optimal).

Milestones (proof of Lemma 2, pp. 11–12)

1. For $q_2 \ne M$: $\mathrm{EOQ}_2(q_2) \ge \mathrm{EOQ}_2(M \pm 1) = \mathrm{EOQ}_2(M) + \frac{H_2}{M\pm 1} \ge \mathrm{EOQ}_2(M) + M$.
2. For $q_2 \ne M$: $\mathrm{JRP}_M(q_1,q_2) > M + \mathrm{EOQ}_2(M) + 1 = \mathrm{JRP}_M(M,M)$.
3. With $q_2 = M$ the instance reduces to problem (4): $\mathrm{JRP}_M(q_1,M) = \mathrm{EOQ}_2(M) + \frac{M}{\gcd(q_1,M)} + q_1$.
4. An odd composite $M$ has a divisor $p$ with $3 \le p \le M/3$.
5. For such $p$: $\frac{M}{\gcd(p,M)} + p \le \frac{2M}{3}$.
6. If $\gcd(q,M) = 1$ or $\gcd(q,M) = M$, then $\frac{M}{\gcd(q,M)} + q \ge M$.

Significance

The result. Lemma 2 says that an exact solver for the two-item periodic JRP, applied to an instance whose coefficients have size $O(\log M)$, returns a pair from which a non-trivial divisor of $M$ is read off as $\gcd(q_1, M)$. Repeating on the factors yields the full factorization, so a polynomial-time algorithm for the two-item periodic JRP would give a polynomial-time algorithm for integer factorization (Theorem 1(b), p. 12). Since the security of RSA-type cryptosystems rests on the belief that factoring is hard, the lemma explains why exact algorithms for even two items have not been found. Section 3 of the paper extends the same construction to a reduction from a range-divisor problem that is NP-complete under randomized reductions, assuming the Riemann hypothesis; that extension is a separate mission of this series.

Formalizing it. The result is proved in the paper, and the proof is short. To our knowledge it has no machine-checked proof. This mission produces a Lean statement of the reduction's correctness with the explicit instance, and its proof together with the intermediate steps of the paper's argument. One printed step needs a correction (milestone 4, see below), which a machine-checked proof makes explicit.

Difficulty

Two points need care. First, the claim concerns every optimal solution of a problem over all pairs of positive integers, so it needs both a global lower bound for every pair with $q_2 \ne M$ and the existence of an optimum, which the paper does not state: the objective must be shown to attain its infimum over an infinite discrete domain. Second, the step separating non-trivial from trivial greatest common divisors depends on a divisor of a specific size: the printed claim "a non-trivial divisor $p$ with $3 \le p < M/3$" is false for $M = 9$, whose only non-trivial divisor is $3 = M/3$. The corrected bound $p \le M/3$ still gives the value $2M/3 < M$ that the argument needs, but only because $M \ge 9$ for every odd composite $M$. A direct convexity argument for item 2 alone does not finish the proof: item 1's cost and the joint cost interact through $\gcd(q_1,q_2)$, which is not convex in either variable.

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 1(b); polynomial running time is not formalized. Theorem 1(b) itself, the recursion that turns one divisor into a full factorization, primality testing, and the treatment of even $M$ (p. 10) are not stated.

Conventions committed to:

• Periods are natural numbers cast to $\mathbb{R}$, and every optimality notion and every milestone ranges over positive periods only, because in Lean $K/0 = 0$ and $\gcd(0, M) = M$.
• Costs are real numbers; the coefficients of the instance are natural-number expressions in $M$.
• Objective (3) is the model and is defined directly; the derivation $\rho = \gcd(q_1,q_2)$ (p. 10, with $B = 1$) is not formalized.
• "Odd composite" is encoded as Odd M ∧ 1 < M ∧ ¬ M.Prime.
• "The size of the coefficients is at most $5\log(M)$" is stated as "every coefficient is at most $M^5$".

Disclosed differences from the printed lemma: the goal names the explicit instance of the proof's first sentence instead of "there is an instance" (a stronger statement); it adds the existence of an optimal solution, so that "every optimal solution satisfies …" is not vacuous; and milestone 4 uses $p \le M/3$ in place of the printed $p < M/3$. Milestones 1–3 and 6 are stated for every $M$ with $M \ge 2$ (or every $M$), which contains the paper's case. A formalization with an existential instance, an unattained or empty set of optima, or periods allowed to be $0$ would make the goal trivial or wrong; all three are excluded.

Infrastructure: the definitions (EOQ cost, objective (3), optimality over positive integer pairs) are short and local to this mission; the same objects appear in the companion missions of this series under their own namespaces. Mathlib supplies Nat.gcd, Nat.minFac and Nat.minFac_sq_le_self. Proofs of any milestone are welcome independently; the existence of an optimum is the one ingredient not present among the milestones.

Selected references

• A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv preprint, 2020. https://arxiv.org/abs/2007.09045v1 (published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024).
• S. K. Goyal and A. T. Satir, Joint replenishment inventory control: Deterministic and stochastic models, European Journal of Operational Research 38(1):2–13, 1989. https://doi.org/10.1016/0377-2217(89)90463-3
• T. Cohen-Hillel and L. Yedidsion, The periodic joint replenishment problem is strongly NP-hard, Mathematics of Operations Research 43(4):1269–1289, 2018. https://doi.org/10.1287/moor.2017.0904
• F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2):135–136, 152, 1913; reprinted in Operations Research 38(6):947–950, 1990. https://doi.org/10.1287/opre.38.6.947
• M. Agrawal, N. Kayal and N. Saxena, PRIMES is in P, Annals of Mathematics 160(2):781–793, 2004. https://doi.org/10.4007/annals.2004.160.781

Motivation

Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is

where $F$ collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier $\lambda>0$. The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.

Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.

Setting

All matrices are real. For a symmetric matrix $A$, $A \geqslant 0$ ($A>0$) means positive semidefinite (definite), and $A \leqslant B$ means $B-A\geqslant0$; the notation includes symmetry. $A^\dagger$ is the Moore–Penrose pseudo-inverse and $\bar F^{1/2}$ the positive semidefinite square root of $\bar F\geqslant0$.

Quadratic matrix inequalities. A symmetric $\Pi \in \mathbb S^{q+r}$ is partitioned into blocks $\Pi_{11}$ ($q\times q$), $\Pi_{12}$, $\Pi_{21}$, $\Pi_{22}$ ($r\times r$). Its solution sets are

and $\mathcal Z_r^+(\Pi)$ is defined in the same way with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and the class $\boldsymbol\Pi_{q,r}$ consists of the $\Pi$ with $\Pi_{22}\leqslant0$, $\Pi\,|\,\Pi_{22}\geqslant0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Petersen's data. Fix $C\in\mathbb R^{n\times n}$ symmetric, $E\in\mathbb R^{n\times p}$, $\bar F\in\mathbb R^{q\times q}$ with $\bar F\geqslant0$, and $G\in\mathbb R^{q\times n}$. The uncertainty set is $\mathcal F=\{F\in\mathbb R^{p\times q}: F^\top F\leqslant\bar F\}$. Display (4.17) defines

In this proposition the letters $q,r$ of the QMI section become $n,p$, so $\mathcal Z_p(N)\subseteq\mathbb R^{p\times n}$.

Formalization targets

Goal: Proposition 4.16 (Petersen's lemma)

(a) The robust strict inequality holds if and only if a single multiplier exists:

(b) If $E\neq0$, $\bar F>0$ and $G\neq0$, the same equivalence holds with $\leqslant 0$ in place of $<0$ on both sides.

Milestones

1. Lemma A.1 (p. 26): $A^\top A\leqslant B^\top B$ if and only if $A=SB$ for some contraction $S$ ($S^\top S\leqslant I$); the strict version under full column rank of $B$; and $S=AB^\dagger$ is such a factor.
2. Set identity (p. 17): $\{FG: F\in\mathcal F\}=\{S\bar F^{1/2}G: S^\top S\leqslant I\}=\{H: H^\top H\leqslant G^\top\bar FG\}$.
3. Reformulation (4.17) (p. 17): the strict robust inequality is $\mathcal Z_p(N)\subseteq\mathcal Z_p^+(M)$, the non-strict one is $\mathcal Z_p(N)\subseteq\mathcal Z_p(M)$, and $N\in\boldsymbol\Pi_{n,p}$ with $N_{22}<0$.
4. Theorem 4.10 (strict matrix S-lemma, p. 13): for $N\in\boldsymbol\Pi_{q,r}$ with $N_{22}<0$, $\mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)$ iff $M-\alpha N>0$ for some $\alpha\geqslant0$.
5. Theorem 4.7 (matrix S-lemma, p. 12): for $N\in\boldsymbol\Pi_{q,r}$ with a positive eigenvalue, $\mathcal Z_r(N)\subseteq\mathcal Z_r(M)$ iff $M-\alpha N\geqslant0$ for some $\alpha\geqslant0$.
6. Schur-complement step (p. 17): for $\alpha>0$, $M-\alpha N>0$ iff $-C-\alpha G^\top\bar FG-\alpha^{-1}EE^\top>0$, together with the non-strict analogue.
7. Slater condition (p. 17): $\bar F>0$ and $G\neq0$ imply that $N$ has a positive eigenvalue.

Significance

The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair $(M,N)$ of (4.17), and the hypotheses $E\neq0$, $\bar F>0$, $G\neq0$ of the non-strict version become exactly the Slater condition of Theorem 4.7.

Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).

Difficulty

The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with $\leqslant 0$ is false without a Slater-type condition, and the formal statement has to carry $E\neq0$, $\bar F>0$ and $G\neq0$ exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of $F$. The quantifier over $\mathcal F$ must first become a QMI in $H=FG$, which is what Lemma A.1 provides.

Formalization scope

Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. $X<0$ is (−X).PosDef and $X\leqslant0$ is (−X).PosSemidef; both include symmetry, as the paper's notation does. $F^\top F\leqslant\bar F$ is (F̄ − FᵀF).PosSemidef. The multiplier $\lambda$ is required positive, so $\lambda^{-1}$ is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix $N$. "Full column rank" is B.rank = q.

Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because $A^\top A<B^\top B$ already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").

A trivializing formalization is excluded. The quantifier in the goal ranges over every $F\in\mathbb R^{p\times q}$ with $F^\top F\leqslant\bar F$, not over a fixed $F$ or over $H$. Part (b)'s extra hypotheses are not added to part (a), and the sanity instance $n=p=q=1$, $C=-3$, $E=G=\bar F=1$ satisfies every hypothesis and both multiplier conditions at $\lambda=1$.

A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959v3
• I. R. Petersen, A stabilization algorithm for a class of uncertain linear systems, Systems & Control Letters 8 (1987) 351–357 (reference [35] of the paper).
• I. R. Petersen and C. V. Hollot, A Riccati equation approach to the stabilization of uncertain linear systems, Automatica 22 (1986) 397–411 (reference [36] of the paper).
• A. Bisoffi, C. De Persis and P. Tesi, Data-driven control via Petersen's lemma, preprint, 2021. https://arxiv.org/abs/2109.12175
• H. J. van Waarde, M. K. Camlibel and M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022) 162–175 (reference [54] of the paper).

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model trust-region subproblems, robust least squares, max-cut and many problems in signal processing and control. They are NP-hard in general, so practice relies on convex relaxations, and the standard one is the Shor semidefinite (SDP) relaxation. The SDP relaxation lifts $N$ variables to an $(N+1)\times(N+1)$ positive semidefinite matrix, which is expensive for large $N$.

For an important subclass, the simultaneously diagonalizable QCQPs (SD-QCQPs), a much cheaper relaxation is available: after a change of variables all quadratic forms are diagonal, and the products $x_j^2$ can be relaxed by $N$ new variables $y_j \ge x_j^2$. This is a second-order cone (SOCP) relaxation, studied by Ben-Tal and den Hertog (2014) and Locatelli (2016) for the trust-region problem with additional constraints and related problems. Whether one may use the SOCP relaxation in place of the SDP relaxation without losing anything, for the optimal value and for the convex-hull description, is the question settled here.

This mission formalizes Proposition 1 of A. L. Wang and F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (Math. Program., 2021; arXiv:1911.09195v3), §4.2.1 and App. A, together with Lemma 9 of §4.2.

Setting

A QCQP (1) in $N$ variables has data $A_i \in \mathbb{S}^N$, $b_i \in \mathbb{R}^N$, $c_i \in \mathbb{R}$ for $i \in [\![0,m]\!]$, with $m \ge 1$ constraints of which the first $m_I$ are inequalities. Writing $q_i(x) = x^\top A_i x + 2 b_i^\top x + c_i$,

The SDP relaxation (3) uses $Q_i = \begin{pmatrix} c_i & b_i^\top \\ b_i & A_i\end{pmatrix}$ and the lifted variable $Y = \begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix}$ with $X \in \mathbb{S}^N$:

Its projected epigraph $\mathcal{D}_{\mathrm{SDP}}$ (4) is the set of $(x,t) \in \mathbb{R}^{N+1}$ for which some $X$ satisfies these constraints together with $\langle Q_0, Y\rangle \le 2t$.

A family $\{A_i\}_{i\in[\![0,m]\!]}$ is simultaneously diagonalizable (SD) if there is an invertible $U$ with every $U^\top A_i U$ diagonal (Definition 4); an SD-QCQP is a QCQP whose matrices are SD (Definition 5). Changing variables by $U$ gives a diagonal QCQP (10): $A_i = \mathrm{Diag}(a_i)$ with $a_i \in \mathbb{R}^N$, so $q_i(x) = \langle a_i, x^2\rangle + 2\langle b_i, x\rangle + c_i$ with $(x^2)_j = x_j^2$. For it, the SOCP relaxation (11) is

and $\mathcal{D}_{\mathrm{SOCP}}$ (12) is the set of $(x,t)$ for which some $y$ satisfies these constraints and $\langle a_0,y\rangle + 2\langle b_0,x\rangle + c_0 \le 2t$.

The dual set is $\Gamma = \{\gamma \in \mathbb{R}^m : A_0 + \sum_i \gamma_i A_i \succeq 0,\ \gamma_i \ge 0\ \forall i \in [\![m_I]\!]\}$.

Formalization targets

Goal: Proposition 1 (p. 21)

For a diagonal QCQP (10),

No regularity assumption is made; both values may be $+\infty$ or $-\infty$.

Milestones (App. A, pp. 34–35)

1. If $\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0$, then $X \succeq xx^\top$ and $X_{jj} \ge x_j^2$.
2. $\mathcal{D}_{\mathrm{SDP}} \subseteq \mathcal{D}_{\mathrm{SOCP}}$.
3. If $y_j \ge x_j^2$ for all $j$, the matrix $X$ with diagonal $y$ and off-diagonal entries $x_jx_k$ satisfies $\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0$.
4. $\mathcal{D}_{\mathrm{SOCP}} \subseteq \mathcal{D}_{\mathrm{SDP}}$.

Companion: Lemma 9 (p. 19)

For any SD-QCQP, $\Gamma$ is polyhedral.

Significance

The result. Proposition 1 transfers every SDP-tightness and convex-hull criterion to the SOCP relaxation of an SD-QCQP. The paper's main theorems give sufficient conditions for $\mathrm{conv}(\mathcal{D}) = \mathcal{D}_{\mathrm{SDP}}$ and for $\mathrm{Opt} = \mathrm{Opt}_{\mathrm{SDP}}$ under the assumption that $\Gamma$ is polyhedral; Lemma 9 shows this assumption holds for every SD-QCQP, and Proposition 1 then gives the same conclusions for an SOCP with only $N$ additional variables and $N$ convex quadratic constraints instead of an $(N+1)\times(N+1)$ semidefinite matrix (Remark 12). The value identity was first recorded by Locatelli (2016); the set identity is, according to the authors, new in the paper.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces Lean definitions of the QCQP, its Shor relaxation, its projected epigraph and the lifted SOCP relaxation that are shared with the other missions of this series on the same paper, and a checked transfer from SDP to SOCP relaxations that downstream tightness results can use.

Difficulty

The argument is short on paper; the formal work is in the matrix bookkeeping. The inclusion $\mathcal{D}_{\mathrm{SDP}} \subseteq \mathcal{D}_{\mathrm{SOCP}}$ needs a Schur complement for a block matrix whose top-left block is the scalar $1$, in the block indexing $\mathrm{Fin}\,1 \oplus \mathrm{Fin}\,N$, and the identity $\langle \mathrm{Diag}(a), X\rangle = \langle a, \mathrm{diag}(X)\rangle$ inside a trace of block products. The reverse inclusion needs an explicit lifted matrix, and its positive semidefiniteness is a global property of an $(N+1)\times(N+1)$ matrix that the coordinatewise inequalities $y_j \ge x_j^2$ do not give entry by entry. The value identity is an identity of infima in the extended reals, where either side may be $\pm\infty$, so real arithmetic on the values is not available.

Formalization scope

• A QCQP is a structure QCQP N m with symmetric $A_0, A_i$, vectors $b_0, b_i$, scalars $c_0, c_i$ and $m_I \le m$. Constraint $i : \mathrm{Fin}\ m$ is the paper's constraint $i+1$, an inequality iff $i < m_I$.
• $\mathrm{Opt}_{\mathrm{SDP}}$ and $\mathrm{Opt}_{\mathrm{SOCP}}$ are infima in EReal, so infeasibility gives $+\infty$ and unboundedness $-\infty$. $\langle Q, Y\rangle$ is $\operatorname{tr}(QY)$, and $X$ in the SDP is symmetric.
• Diagonal, not SD. The paper states Proposition 1 "for any SD-QCQP", but $\mathcal{D}_{\mathrm{SOCP}}$ and $\mathrm{Opt}_{\mathrm{SOCP}}$ are defined only after the change of variables, which §4.2.1 assumes throughout. The goal and milestones 2 and 4 therefore take vectors $a_0, a_i$ and the hypothesis $A_0 = \mathrm{Diag}(a_0)$, $A_i = \mathrm{Diag}(a_i)$. Lemma 9 is stated for SD-QCQPs, with invertibility of $U$ as IsUnit U.
• The goal keeps the standing assumption $m \ge 1$ (p. 1); the milestones and Lemma 9 drop it, which makes them stronger. No Assumption 1 is made anywhere.
• No trivializing reading: $\mathcal{D}_{\mathrm{SOCP}}$ is defined directly from (12) with a vector $y$, not through matrices or through $\mathcal{D}_{\mathrm{SDP}}$, so the goal is a genuine comparison of two different feasible sets.
• Polyhedral means a finite intersection of closed halfspaces.
• Needed infrastructure: Schur complements of block matrices (Mathlib's Matrix.fromBlocks positive-semidefiniteness results), traces of block products, and EReal infima. A reusable lemma "$\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0 \iff X - xx^\top \succeq 0$" is welcome beyond this mission.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming, 2021. arXiv:1911.09195v3, doi:10.1007/s10107-020-01589-9
• A. Ben-Tal, D. den Hertog, Hidden conic quadratic representation of some nonconvex quadratic optimization problems, Mathematical Programming 143:1–29, 2014 (reference [8] of the paper).
• M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6):1141–1151, 2016 (reference [37] of the paper).
• N. Z. Shor, Dual quadratic estimates in polynomial and boolean programming, Annals of Operations Research 25:163–168, 1990 (reference [47] of the paper).

Why projection methods for variational inequalities

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with $F$ a gradient), of saddle-point problems (with $F$ the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of $F$ and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.

The classical such method, the projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$, does not converge for merely monotone $F$. Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of $F$ per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of $F$ per step, evaluating $F$ at the reflected point $2x_n-x_{n-1}$ instead of at $x_n$. This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, let $C\subseteq H$ be closed and convex, and let $F:H\to H$. The metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$. The variational inequality (1.1) is

with solution set $S$. The paper's standing assumptions for this result are

• (C1) $S\neq\emptyset$;
• (C2*) $F$ is strongly monotone with modulus $m>0$: $\langle F(x)-F(y),x-y\rangle\ge m\|x-y\|^2$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz with constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 chooses $x_0=y_0\in H$ and a step $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and iterates

The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.

Formalization targets

Goal: Theorem 3.3 (p. 6)

Under (C1), (C2*), (C3) and $0<\lambda<(\sqrt2-1)/L$, every run of Algorithm 3.1 converges to the solution $z$ of (1.1) at least R-linearly:

The goal fixes neither $\gamma$ nor $M$; the proof produces them from $\lambda$, $L$ and $m$, but the theorem asserts only the shape of the rate.

Milestones

In attack order:

1. Uniqueness (p. 6): under (C2*) the solution set has at most one point.
2. The identity for $\|y_n-z\|^2$ (p. 6, via Lemma 2.5): $\|y_n-z\|^2=2\|x_n-z\|^2-\|x_{n-1}-z\|^2+2\|x_n-x_{n-1}\|^2\ge2\|x_n-z\|^2-\|x_{n-1}-z\|^2$.
3. (3.8) (p. 7): the strong-monotonicity estimate at $y_n$ with a free modulus $m_1\in(0,m]$.
4. (3.2) (p. 4): $\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\|x_{n+1}-x_n\|^2-2\lambda\langle F(y_n),x_{n+1}-z\rangle$.
5. (3.4) (p. 5): $2\lambda\langle F(y_{n-1}),y_n-x_{n+1}\rangle\le\|x_{n+1}-x_n\|^2-\|x_n-y_n\|^2-\|x_{n+1}-y_n\|^2$, $n\ge2$.
6. (3.5) (p. 5): the Lipschitz estimate of $2\lambda\langle F(y_n)-F(y_{n-1}),y_n-x_{n+1}\rangle$.
7. (3.9) (p. 7): the two-step recursion $a_{n+1}+b_{n+1}\le(1-2\alpha)a_n+\alpha a_{n-1}+\beta b_n$ in the iterates, with $\beta=\max\{\lambda L/(1-\sqrt2\lambda L),\tfrac12\}$.
8. Lemma 2.8 (p. 3): a nonnegative pair of sequences satisfying that recursion for all $\alpha\in(0,\alpha_0)$ has $a_n\le\gamma^nM$.

Significance

The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy $\varepsilon$ in $O(\log(1/\varepsilon))$ iterations with one projection each, which matters when projecting onto $C$ dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.

Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of $n$ and the positivity of $M$ implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.

Difficulty

The natural first attempt, a contraction $\|x_{n+1}-z\|\le q\|x_n-z\|$ (Q-linear convergence), is not what the paper proves and is not available: the reflected point $y_n$ depends on $x_{n-1}$, so the error at step $n+1$ is controlled only by the errors at steps $n$ and $n-1$, together with auxiliary terms $\|x_n-y_{n-1}\|^2$ and $\langle F(z),x_{n-1}-z\rangle$. Strong monotonicity is applied at $y_n$, not at $x_n$, and $\|y_n-z\|^2$ can be smaller than $\|x_n-z\|^2$; the lower bound $2\|x_n-z\|^2-\|x_{n-1}-z\|^2$ may even be negative. The step range $\lambda<(\sqrt2-1)/L$ is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of $\gamma$ and $\delta$, to yield a geometric bound.

Formalization scope

• $H$ is a general real inner product space, complete where a projection is used ([CompleteSpace H]); it is never specialized to $\mathbb R^n$.
• $P_C$ is defined by choice as a nearest point, returning its argument when none exists; every statement using it assumes $C$ closed, convex and nonempty (through $z\in C$, $C\neq\emptyset$, or (C1)), so the junk value is never reached.
• Runs of Algorithm 3.1 are infinite sequences without the stopping rule; a stopped run continues as a constant sequence. $x_0$ is any point of $H$, as in the paper, so statements that need $x_{n-1}\in C$ are stated for $n\ge2$.
• (C2*) and (C3) are required on all of $H$ with real constants $m>0$, $L>0$ (not LipschitzWith, whose $\mathbb R_{\ge0}$ constant admits $L=0$). (C1) stays in the goal: it is the paper's assumption and its only source of $C\neq\emptyset$.
• R-linear convergence means domination by $M\gamma^n$ with $0<\gamma<1$ and $M>0$; a goal allowing $\gamma=1$, $\gamma=0$ or only an $O(\cdot)$ bound would be a different and weaker (or trivially false) statement and is ruled out. The goal does not mention the auxiliary sequences $a_n,b_n$, the constants $\beta,m_1,\alpha_0$, or Lemma 2.8.
• Departures from the page are recorded in each item's Formalization Note: the ranges $n\ge1$/$n\ge2$, the range $n\ge1$ of (2.1) in Lemma 2.8, the proof's "Lemma 2.1" that means Lemma 2.8, and "$m_1$ arbitrary in $(0,m)$" where the argument uses $(0,m]$.
• The projection theorem (existence and characterization of the nearest point) is the published Proved theorem VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.

Selected references

• Yu. Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, SIAM J. Optim. 25(1), 2015. arXiv:1502.04968v1. https://arxiv.org/abs/1502.04968 , https://doi.org/10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12, 747–756, 1976.
• P. Tseng, On linear convergence of iterative methods for the variational inequality problem, J. Comput. Appl. Math. 60, 237–252, 1995.
• L. D. Popov, A modification of the Arrow–Hurwicz method for finding saddle points, Math. Notes 28, 845–848, 1980.
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148, 318–335, 2011.

Motivation

Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.

The plain projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$ does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.

Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be closed and convex, and let $F:H\to H$ be a mapping. For $z\in H$, the metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$ (it exists when $C$ is nonempty). The variational inequality (1.1) asks for $x^*\in C$ with

and $S$ denotes its solution set. The standing assumptions are:

• (C1) $S$ is nonempty;
• (C2) $F$ is monotone: $\langle F(x)-F(y),x-y\rangle\ge0$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz continuous with a constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 (projected reflected gradient method). Fix a step size $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and a starting point $x_0=y_0\in H$, and iterate

The point $y_{n+1}$ is the reflection of $x_n$ through $x_{n+1}$. A sequence $(x_n)$ converges weakly to $x^*$, written $x_n\rightharpoonup x^*$, if $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$.

Formalization targets

Goal: Theorem 3.2 (p. 5)

Under (C1)–(C3), for $0<\lambda<(\sqrt2-1)/L$ and every run of Algorithm 3.1 there is $x^*\in S$ with

Milestones

In the order the proof uses them:

1. Lemma 2.1 (i), p. 3: $\langle P_Mx-x,\,y-P_Mx\rangle\ge0$ for $y\in M$ (already proved on the platform, referenced).
2. Lemma 2.1 (ii), p. 3: $\|P_Mx-y\|^2\le\|x-y\|^2-\|x-P_Mx\|^2$ for $y\in M$.
3. Lemma 3.1, p. 4: for $z\in S$ and $n\ge2$,

4. (3.6), p. 5: the descent inequality $a_{n+1}\le a_n-b_n$ with $a_n=\|x_n-z\|^2+\lambda L\|x_n-y_{n-1}\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ and $b_n=(1-\lambda L(1+\sqrt2))\|x_n-x_{n-1}\|^2$.
5. Lemma 2.7, p. 3: nonnegative sequences with $a_{n+1}\le a_n-b_n$ have $(a_n)$ bounded and $b_n\to0$.
6. Proof of Theorem 3.2, pp. 5–6: $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$ and $\|x_{n+1}-y_n\|\to0$.
7. Lemma 2.2 (Minty), p. 3: for continuous monotone $F$, $x^*\in S$ iff $x^*\in C$ and $\langle F(y),y-x^*\rangle\ge0$ for all $y\in C$.
8. (3.7), p. 6: every weak cluster point of $(x_n)$ lies in $S$.
9. Proof of Theorem 3.2, p. 6: for each $z\in S$, $\|x_n-z\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ converges.
10. Lemma 2.3 (Opial), p. 3: if $x_n\rightharpoonup x$ and $y\ne x$, then $\liminf\|x_n-x\|<\liminf\|x_n-y\|$.

Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ($S$ is closed and convex), and the characterization of $S$ as the zeros of the projected residual $r(x,y)=\|y-P_C(x-\lambda F(y))\|+\|x-y\|$ (§3, p. 4).

Significance

The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of $F$ per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating $F$ is expensive, and keeps the cost of projections at one when projecting onto $C$ is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.

Difficulty

The naive Lyapunov function $\|x_n-z\|^2$ is not monotone along the iteration: because $F$ is evaluated at the reflected point $y_n$ rather than at $x_n$, the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound $(\sqrt2-1)/L$ is what the decrease requires. As a consequence, $\|x_n-z\|$ itself is not known to converge, so the standard Opial lemma ("if $\|x_n-z\|$ converges for every $z\in S$ and all weak cluster points lie in $S$, then $x_n$ converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.

Formalization scope

• $H$ is an arbitrary real inner product space with [CompleteSpace H] in every statement that needs completeness; it is never specialised to $\mathbb R^n$, where weak and norm convergence coincide.
• Weak convergence is stated elementarily: $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$. Subsequences are $x\circ\varphi$ with $\varphi$ strictly increasing.
• The projection $P_C(z)$ is defined by choice as a nearest point, with the junk value $z$ when none exists. Every statement that uses it assumes $C$ closed, convex and nonempty (directly or through $S\ne\emptyset$ or $z\in S$), and a companion item certifies that it is then the metric projection.
• (C2) and (C3) are imposed on all of $H$, as in the paper; $L$ is a real number with $L>0$, and the step range $0<\lambda<(\sqrt2-1)/L$ is strict on both sides.
• Runs of Algorithm 3.1 carry no stopping rule: a run reaching a solution $x_n=y_n\in S$ stays constant, so infinite runs subsume stopped ones. The starting point $x_0$ is any point of $H$, not necessarily in $C$; for this reason Lemma 3.1 and (3.6) are stated for $n\ge2$, which is the range the proof of Theorem 3.2 uses.
• Opial's inequality is stated with liminfs in $[0,\infty]$, where they are always defined.
• A trivializing formalization is ruled out: the goal assumes exactly (C1)–(C3), closedness and convexity of $C$ and the step range, and concludes weak convergence to a point of $S$; it does not assume boundedness of the iterates, a starting point in $C$, finite dimension, or any of the intermediate estimates.

Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.

Selected references

• Yu. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1) (2015), 502–520. arXiv:1502.04968, doi:10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2) (2000), 431–446. doi:10.1137/S0363012998338806
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148 (2011), 318–335. doi:10.1007/s10957-010-9757-3
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967), 591–597. doi:10.1090/S0002-9904-1967-11761-0
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5

Motivation

A chance constraint asks that a decision $x\in\mathbb R^n$ satisfy uncertain inequalities with high probability. In the setting of Zymler, Kuhn and Rustem (Math. Program. 137, 2013), $m$ affine inequalities $y_i^0(x)+y_i(x)^\top\tilde\xi\le0$, whose coefficients depend affinely on $x$, must hold jointly with probability at least $1-\epsilon$. Joint chance constraints appear wherever several safety conditions must hold at once: portfolio and network design, water reservoir operation, production planning under uncertain demand. They are hard for two reasons. Checking feasibility of a fixed $x$ requires a multi-dimensional integral, and the feasible set is typically nonconvex (Prékopa 1995). Moreover the distribution of $\tilde\xi$ is rarely known; often only its mean and covariance can be estimated.

The distributionally robust version requires the constraint for every distribution consistent with the known first and second moments. A standard tractable inner approximation replaces the probability by a worst-case Conditional Value-at-Risk (CVaR) of a single loss. For a joint constraint this needs the $m$ inequalities aggregated into one loss, and the choice of aggregation decides how much is lost.

Timeline. Charnes and Cooper (1959) and Miller and Wagner (1965) introduced chance constraints; Prékopa proved convexity of joint constraints with log-concave right-hand sides. Nemirovski and Shapiro (2006) studied convex (CVaR-type) approximations. El Ghaoui, Oks and Oustry (2003) and Calafiore and El Ghaoui (2006) gave exact SDP and SOCP reformulations of individual robust chance constraints under moment information. Chen, Sim, Sun and Teo (2010) introduced scaling parameters and an SOCP approximation of joint constraints. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR of the scaled max-loss admits an exact LMI representation and that, with the scaling parameters free, it is essentially exact.

Setting

Let $\tilde\xi$ be a random vector in $\mathbb R^k$. Fix $\mu\in\mathbb R^k$ and a positive definite $\Sigma\in\mathbb S^k$, and let $\mathcal P$ be the set of all probability measures on $\mathbb R^k$ with finite second moments, mean $\mu$ and covariance $\Sigma$. The second-order moment matrix is