Convex Optimization

Motivation

Many problems in convex optimization, variational inequalities, mechanics, traffic equilibrium and signal processing reduce to finding a zero of a monotone operator on a Hilbert space. Frequently that operator is a sum $A + L^*\circ B\circ L$ of a monotone operator and a monotone operator composed with a linear map and its adjoint, and one also wants the solution of an associated dual inclusion. The prototype is Fenchel–Rockafellar duality: with $A=\partial f$ and $B=\partial g$, the pair of problems is $\min_x f(x)+g(Lx-r)-\langle x\mid z\rangle$ and $\min_v f^*(z-L^*v)+g^*(v)+\langle v\mid r\rangle$.

Before this paper, splitting methods for the primal problem needed $B$ to be single-valued and smooth (forward–backward, or Tseng's forward–backward–forward method), or needed the resolvent of $L^*\circ B\circ L$, which has no closed form in terms of $B$ and $L$ in general. Briceño-Arias and Combettes (arXiv:1011.5517, SIAM J. Optim. 2011) observed that the primal–dual pair is equivalent to a single inclusion on the product space involving a maximally monotone operator plus a bounded skew linear operator. Applying an inexact forward–backward–forward method to that inclusion gives the first algorithm that solves the primal and dual inclusions simultaneously and uses $A$, $B$ and $L$ separately. Later primal–dual methods, including those of Combettes–Pesquet (2012), Vũ (2013) and Condat (2013), build on this construction.

Setting

Let $\mathcal H$ and $\mathcal G$ be real Hilbert spaces. A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns to each point a subset; its graph is $\{(x,u)\mid u\in Mx\}$, its inverse $M^{-1}$ has graph $\{(u,x)\mid u\in Mx\}$, and $\operatorname{zer}M=\{x\mid 0\in Mx\}$. $M$ is monotone if $\langle x-y\mid u-v\rangle\ge0$ whenever $u\in Mx$, $v\in My$, and maximally monotone if no monotone operator has a strictly larger graph. For $\gamma>0$ the resolvent $J_{\gamma M}=(\mathrm{Id}+\gamma M)^{-1}$ is then an everywhere-defined single-valued map.

Problem 1.1. Let $A:\mathcal H\to2^{\mathcal H}$ and $B:\mathcal G\to2^{\mathcal G}$ be maximally monotone, $L:\mathcal H\to\mathcal G$ bounded linear, $z\in\mathcal H$, $r\in\mathcal G$. Solve the primal inclusion

$$z\in Ax+L^*B(Lx-r)\qquad(1.2)$$

and the dual inclusion

$$-r\in -LA^{-1}(z-L^*v)+B^{-1}v.\qquad(1.3)$$

Their solution sets are $\mathcal P$ and $\mathcal D$.

Problem 1.2. On the Hilbert direct sum $\mathcal K=\mathcal H\oplus\mathcal G$ set

$$M:(x,v)\mapsto(-z+Ax)\times(r+B^{-1}v),\qquad S:(x,v)\mapsto(L^*v,-Lx),$$

and find a zero of $M+S$.

The algorithm (3.1) of the paper, for step sizes $\gamma_n$ and error sequences $a_{i,n},b_{i,n},c_{i,n}$, reads

$$\begin{aligned}y_{1,n}&=x_n-\gamma_n(L^*v_n+a_{1,n}), & y_{2,n}&=v_n+\gamma_n(Lx_n+a_{2,n}),\\ p_{1,n}&=J_{\gamma_nA}(y_{1,n}+\gamma_nz)+b_{1,n}, & p_{2,n}&=J_{\gamma_nB^{-1}}(y_{2,n}-\gamma_nr)+b_{2,n},\\ q_{1,n}&=p_{1,n}-\gamma_n(L^*p_{2,n}+c_{1,n}), & q_{2,n}&=p_{2,n}+\gamma_n(Lp_{1,n}+c_{2,n}),\\ x_{n+1}&=x_n-y_{1,n}+q_{1,n}, & v_{n+1}&=v_n-y_{2,n}+q_{2,n}.\end{aligned}$$

Formalization targets

Goal: Theorem 3.1

Assume $L\neq0$, $z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$, all six error sequences absolutely summable, $\varepsilon\in\,]0,1/(\|L\|+1)[$ and $\gamma_n\in[\varepsilon,(1-\varepsilon)/\|L\|]$. Then for some $\bar x\in\mathcal P$ and $\bar v\in\mathcal D$ with $z-L^*\bar v\in A\bar x$ and $\bar v\in B(L\bar x-r)$:

$$x_n-p_{1,n}\to0,\quad v_n-p_{2,n}\to0,\qquad x_n,\,p_{1,n}\rightharpoonup\bar x,\quad v_n,\,p_{2,n}\rightharpoonup\bar v,$$

and the convergence of $x_n,p_{1,n}$ (resp. $v_n,p_{2,n}$) is strong if $A$ is uniformly monotone at $\bar x$ (resp. $B^{-1}$ at $\bar v$).

Milestones

1. Lemma 2.1: $\alpha_{n+1}\le\alpha_n-\beta_n+\varepsilon_n$ with nonnegative terms and summable $\varepsilon_n$ implies $(\alpha_n)$ converges and $\sum\beta_n<\infty$. Covered by the proved platform theorem GradErrors.Deterministic.lemma_1 (Bertsekas–Tsitsiklis), of which it is the special case $Y=\alpha\ge0$, so that the alternative $Y_t\to-\infty$ cannot occur.
2. Lemma 2.2: a quasi-Fejér sequence whose sequential weak cluster points lie in $C$ converges weakly to a point of $C$.
3. Theorem 2.5(i)–(ii): for $A$ maximally monotone and $B$ monotone and $\beta$-Lipschitz with $\operatorname{zer}(A+B)\ne\varnothing$, the inexact forward–backward–forward iteration has $\sum\|x_n-p_n\|^2<\infty$, $\sum\|y_n-q_n\|^2<\infty$, and $x_n,p_n\rightharpoonup\bar x\in\operatorname{zer}(A+B)$.
4. Proposition 2.7(i)–(iv): $M$ and $M+S$ are maximally monotone; $S$ is bounded linear with $S^*=-S$ and $\|S\|=\|L\|$; $J_{\gamma M}(x,v)=(J_{\gamma A}(x+\gamma z),J_{\gamma B^{-1}}(v-\gamma r))$.
5. Proposition 2.8: $\operatorname{zer}(M+S)$ is a closed convex subset of $\mathcal P\times\mathcal D$, and $z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$, $\mathcal P\ne\varnothing$, $\operatorname{zer}(M+S)\ne\varnothing$, $\mathcal D\ne\varnothing$ and $-r\in\operatorname{ran}(-L\circ A^{-1}\circ(z-L^*\cdot)+B^{-1})$ are equivalent.

Significance

Theorem 3.1 gives a method that handles two arbitrary maximally monotone operators coupled by an arbitrary bounded linear map, with only resolvent evaluations of $A$ and $B^{-1}$ (computed in parallel) and forward applications of $L$ and $L^*$. It tolerates summable errors in every step and variable step sizes, and it produces a primal and a dual solution simultaneously, assuming only that the primal problem is solvable. The paper derives from it, as instances, methods for sums of composite operators (Theorem 3.8) and for Fenchel–Rockafellar-type composite minimization (Section 4).

The theorem is proved in the literature. This mission formalizes it, which in turn requires a machine-checked inexact forward–backward–forward theorem (Theorem 2.5) and the structural facts about the monotone+skew reformulation (Propositions 2.7, 2.8). These intermediate results are reusable for the descendants of this algorithm. No machine-checked proof of Theorem 3.1, of Theorem 2.5, or of the quasi-Fejér Lemma 2.2 is known to the mission's authors. On Prove2Me, CondatPD.FB.lemma_4_4 (inexact forward–backward with a cocoercive operator) and CondatPD.FB.theorem_3_1 (Condat's primal–dual method) concern related algorithms; CondatPD.PPA.A_maximal_monotone is an open subdifferential special case of Proposition 2.7(iii).

Difficulty

The obvious route, applying a known splitting method directly to $A_1+A_2$ with $A_2=L^*\circ B\circ(L\cdot-r)$, fails: $A_2$ need not be maximally monotone, and its resolvent cannot be computed from that of $B$. The reformulation on $\mathcal K$ avoids this, but at a cost. $M+S$ is not a subdifferential, $S$ is not cocoercive (it is skew, so $\langle Sx\mid x\rangle=0$), and forward–backward theory does not apply; one needs the forward–backward–forward method with Lipschitz, merely monotone $S$. Proving that method's convergence with errors requires quasi-Fejér analysis in a possibly infinite-dimensional space, where bounded sequences only have weakly convergent subsequences and the limit must be identified through the maximal monotonicity of $M+S$, whose graph is sequentially closed in the weak–strong topology. The strong convergence clauses (iii)–(iv) need a further estimate, since uniform monotonicity of $A$ at $\bar x$ does not by itself control the coupled iterate.

Formalization scope

• Hilbert spaces are [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]; set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity (no proper monotone extension of the graph), zer, the resolvent predicate IsResolvent, weak convergence WeakTendsto ($\langle u_n,y\rangle\to\langle u,y\rangle$ for all $y$), opInv and opAdd are imported from published platform definitions.
• $\mathcal K=\mathcal H\oplus\mathcal G$ is WithLp 2 (H × G), whose inner product is $\langle x\mid x'\rangle+\langle v\mid v'\rangle$; the plain product would carry the sup norm.
• Resolvents are given maps with the resolvent property, one per iteration since $\gamma_n$ varies: JA n satisfies $\gamma_n^{-1}(w-J^A_nw)\in A(J^A_nw)$ for all $w$, and likewise for $B^{-1}$. For maximally monotone operators and $\gamma_n>0$ such maps exist (Minty's theorem) and are unique, so quantifying over them is the paper's statement. Proposition 2.7(iv) is stated as "the product map is a resolvent of $\gamma M$", which is the equality by uniqueness.
• "Absolutely summable" is Summable (fun n => ‖a n‖); indices start at $0$; $\|L\|$ is the operator norm and $L\ne0$ is kept, so the step-size window is nonempty.
• "$S\in\mathcal B(\mathcal K)$" is the existence of a continuous linear operator equal to $S$ pointwise, whose adjoint is its negative and whose norm is $\|L\|$.
• "Uniformly monotone at $x$" (Lemma 2.4(i)) uses a nondecreasing $\phi:[0,\infty[\to[0,+\infty]$ vanishing only at $0$, compared in EReal, against every point of the graph. It is neither strong monotonicity nor uniform monotonicity on a set.
• Lemma 2.1 is not restated: the mission references the proved platform theorem GradErrors.Deterministic.lemma_1, of which it is a special case.
• A trivializing formalization is ruled out. The resolvents are constrained by their defining property (an unconstrained map would make the goal false), the existence hypothesis is the paper's only one ($z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$, not a dual solution or a zero of $M+S$), and the hypotheses are satisfiable ($\mathcal H=\mathcal G=\mathbb R$, $A=B=0$, $L=\mathrm{Id}$ is a checked instance).

The mission needs Minty-type facts (existence of resolvents), demiclosedness of maximally monotone graphs, sums of a maximally monotone and a Lipschitz monotone operator, and quasi-Fejér/Opial arguments in Hilbert space. None of these is in Mathlib in this form, and all are reusable beyond this mission. Contributions toward any of the milestones, or toward this general infrastructure, are welcome.

Selected references

• L. M. Briceño-Arias, P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, arXiv:1011.5517v1 (2010); SIAM J. Optim. 21 (2011) 1230–1250. https://arxiv.org/abs/1011.5517v1 , https://doi.org/10.1137/10081602X
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38 (2000) 431–446. https://doi.org/10.1137/S0363012998338806
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
• D. P. Bertsekas, J. N. Tsitsiklis, Gradient convergence in gradient methods with errors, SIAM J. Optim. 10 (2000) 627–642. https://doi.org/10.1137/S1052623497331063
• P. L. Combettes, J.-C. Pesquet, Primal-dual splitting algorithm for solving inclusions with mixtures of composite, Lipschitzian, and parallel-sum type monotone operators, Set-Valued Var. Anal. 20 (2012) 307–330. https://doi.org/10.1007/s11228-011-0191-y
• B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38 (2013) 667–681. https://doi.org/10.1007/s10444-011-9254-8
• L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158 (2013) 460–479. https://doi.org/10.1007/s10957-012-0245-9

Motivation

Second-order cone programming (SOCP) minimizes a linear function over the intersection of an affine subspace with a product of Lorentz cones. It contains convex quadratically constrained programs, robust linear programs with ellipsoidal uncertainty, and many norm-minimization problems, and it is solved in practice by primal–dual interior-point methods. At each iteration such a method computes a search direction from a linearized, symmetrized form of the complementarity conditions; the symmetrization depends on a scaling matrix $G$, and different choices of $G$ give different directions. The two directions used in practice are the HKM direction (Helmberg–Rendl–Vanderbei–Wolkowicz, Kojima–Shindoh–Hara, Monteiro) and the NT direction (Nesterov–Todd).

A desirable property of a search direction is scale invariance: if the problem is transformed by an automorphism of the cone, the direction computed for the transformed problem is the image of the original direction. A scale-invariant method behaves identically on all problems related by such a change of coordinates, so its behaviour does not depend on an arbitrary choice of coordinates within each cone.

Timeline. Tsuchiya (1999, Optim. Methods Softw. 11 & 12, pp. 141–182; reference [27] of the paper) proved that the HKM and NT directions for SOCP are scale invariant, with a two-page argument for each. Tütüncü, Toh and Todd (2003), in the paper that describes the solver SDPT3 version 3.0, derived closed forms for the blocks $(\mathcal E_i)^{-1}\mathcal F_i$ of the Schur complement matrix ((23) for HKM, (29) for NT) and used them to give a short proof of Tsuchiya's result (their Proposition 1).

Setting

There are $n_q$ second-order cone blocks. Block $i$ has dimension $q_i \ge 1$, and a vector $x_i \in \mathbb R^{q_i}$ is split into its first coordinate $x_i^0$ and the rest $x_i^1$. The cone is $K_q^{q_i} = \{x : x^0 \ge \|x^1\|_2\}$, and with $\bar J = \operatorname{diag}(1, -I)$ and $J = -\bar J$, the function $\gamma(x) = \sqrt{(x^0)^2 - \langle x^1, x^1 \rangle} = \sqrt{x^\top \bar J x}$ is defined on the cone.

The data are matrices $A_i \in \mathbb R^{q_i \times m}$, a vector $b \in \mathbb R^m$ and vectors $c_i \in \mathbb R^{q_i}$. The primal problem minimizes $\sum_i \langle c_i, x_i \rangle$ subject to $\sum_i A_i^\top x_i = b$ and $x_i \in K_q^{q_i}$; the dual maximizes $b^\top y$ subject to $A_i y + z_i = c_i$ and $z_i \in K_q^{q_i}$.

The arrow matrix of $v$ is $\operatorname{Arw}(v) = \begin{pmatrix} v^0 & (v^1)^\top \\ v^1 & v^0 I \end{pmatrix}$. Given an interior iterate $(x, y, z)$ and a scaling block $G_i$, set

$$\mathcal E_i = \operatorname{Arw}(G_i^{-1} z_i)\, G_i, \qquad \mathcal F_i = \operatorname{Arw}(G_i x_i)\, G_i^{-1}, \qquad T_{G_i}(x_i, z_i) = \operatorname{Arw}(G_i x_i)(G_i^{-1} z_i).$$

With $\mu = \langle x, z \rangle / n_q$ and a centering parameter $\sigma$, a search direction $(\Delta x, \Delta y, \Delta z)$ solves the Newton system

$$A_i \Delta y + \Delta z_i = c_i - z_i - A_i y, \qquad \sum_i A_i^\top \Delta x_i = b - \sum_i A_i^\top x_i, \qquad \mathcal E_i \Delta x_i + \mathcal F_i \Delta z_i = \sigma\mu\, e_1 - T_{G_i}(x_i, z_i).$$

The HKM direction takes $G_i$ from the explicit formula (19) in $z_i$; the NT direction takes $G_i$ from (20)–(21) in $x_i$ and $z_i$.

The automorphism group $\mathcal G_i$ of $K_q^{q_i}$ consists of the invertible linear maps $F$ with $F K_q^{q_i} = K_q^{q_i}$; these are exactly the matrices with $F^\top \bar J F = \lambda^2 \bar J$ for some $\lambda > 0$ and $F_{00} > 0$. Scaling by $F = \operatorname{diag}(F_1, \dots, F_{n_q})$ sends the data and iterate to $\hat A_i = F_i^{-1} A_i$, $\hat b = b$, $\hat c_i = F_i^{-1} c_i$, $\hat x_i = F_i^\top x_i$, $\hat y = y$, $\hat z_i = F_i^{-1} z_i$.

Formalization targets

Goal: Proposition 1 (p. 11)

For either direction (HKM or NT), every interior iterate, every $\sigma$, and every choice of $F_i \in \mathcal G_i$,

$$(\Delta x, \Delta y, \Delta z) \text{ solves the Newton system for } (A, b, c; x, y, z) \iff (F^\top \Delta x,\ \Delta y,\ F^{-1} \Delta z) \text{ solves it for } (\hat A, \hat b, \hat c; \hat x, \hat y, \hat z).$$

Milestones

In attack order: the identities (31) for $F$ with $F^\top \bar J F = \bar J$; the Schur complement reduction (10)–(15); $\operatorname{Arw}(G_i^{-1} z_i) = I$ for HKM; the HKM closed forms (23) and (24)–(25); the right-hand-side formula (28) for both directions; the HKM invariance step of the proof; the NT identities $G_i x_i = G_i^{-1} z_i$ and (29); the NT block formula (30); and the NT invariance step of the proof.

Significance

The proposition shows that SDPT3's two second-order-cone directions do not depend on how each cone is coordinatized. The closed forms (23), (24), (29) and (30) are what SDPT3 uses to assemble the Schur complement matrix: they show that each block is a diagonal matrix plus a low-rank term, which is the basis for its sparse and Sherman–Morrison–Woodbury handling of large cones.

The result is proved twice in the literature (Tsuchiya 1999 and this paper). As far as is known, neither proof has been machine-checked, and no formal library contains the HKM or NT scalings, the arrow matrix of the Jordan algebra of the Lorentz cone, or its automorphism group. This mission produces those definitions and a checked proof. The printed proof assumes $F_i^\top \bar J F_i = \bar J$, that is $\lambda = 1$; the goal covers the whole group $\mathcal G_i$, so a complete formalization also closes the case $\lambda \ne 1$, where (31) and the remark that $\omega_i$ is unchanged no longer hold as printed.

Difficulty

Every step is linear algebra, but none is a one-line rewrite. The inverse of $\mathcal E_i$ appears everywhere, so one first needs invertibility of $G_i$ and $\mathcal E_i$ for interior iterates, and the HKM and NT scalings must be shown to satisfy $G_i e_1 = z_i$ and $G_i x_i = G_i^{-1} z_i$ respectively, which are identities involving $\gamma$, square roots and the denominators $\gamma(z) + z^0$ and $1 + t^0$. Transporting the Newton system directly through $F$ fails: $\mathcal E_i$ and $\mathcal F_i$ are built from $G_i$, which is not equivariant in an obvious way, and the HKM scaling at $\hat z_i$ is not $F_i^{-1} G_i$. For $\lambda \ne 1$, the quantities $\gamma$, $\omega$ and $t$ scale by powers of $\lambda$, and these factors must be tracked until they cancel.

Formalization scope

A block of dimension $q_i$ is Fin (d i + 1) → ℝ, so $q_i = d_i + 1 \ge 1$; $x_i^0$ is index 0 and $x_i^1$ the indices Fin.succ j. Mathlib's norm on this type is the sup norm, so every Euclidean quantity is written through $\bar J$. Interior points are encoded by $x^0 > 0$ and $(x^0)^2 - \langle x^1, x^1 \rangle > 0$. Matrix inverses are Matrix.inv, which is $0$ on singular input; the milestones that invert a matrix state its invertibility.

Standing assumptions: the problem is a pure SOCP ($n_s = n_l = 0$); the iterate is interior; $\mu = \langle x, z \rangle / n_q$. The paper's assumption that $A$ has full row rank is dropped, because the goal is stated for solution sets of the Newton system and needs no uniqueness. $\mathcal G_i$ is encoded algebraically (positive multiples of orthochronous Lorentz transformations) rather than as $\{F : F K = K\}$, so that the goal does not require the classification of cone automorphisms. The goal assumes nothing about the scaled iterate; its interiority is a consequence.

The Newton system is defined by its raw rows with $\mathcal E_i$, $\mathcal F_i$ from (8) and $G_i$ from (19)/(21). A formalization that defined the direction through the closed forms (23)/(29), or defined $G_i$ implicitly by $G_i e_1 = z_i$ or $G_i x_i = G_i^{-1} z_i$, would make the goal nearly definitional and is ruled out.

Reusable infrastructure: the arrow matrix and $\gamma$ of the Lorentz cone, the HKM and NT scalings, and the algebra of Lorentz transformations. Contributions toward any milestone, and alternative proofs of the goal that bypass the milestones, are welcome.

Selected references

• R. H. Tütüncü, K. C. Toh, M. J. Todd, Solving semidefinite-quadratic-linear programs using SDPT3, Mathematical Programming 95 (2003) 189–217. https://doi.org/10.1007/s10107-002-0347-5
• T. Tsuchiya, A convergence analysis of the scaling-invariant primal-dual path-following algorithms for second-order cone programming, Optimization Methods and Software 11 & 12 (1999) 141–182 (reference [27] of the SDPT3 paper; no stable link recorded).
• F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003) 3–51. https://doi.org/10.1007/s10107-002-0339-5
• Yu. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods in convex programming, Mathematics of Operations Research 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1

Why the Nesterov–Todd scaling of a second-order cone matters

Conic quadratic (second-order cone) programs are solved in practice by primal-dual interior-point methods. Each iteration solves a Newton system for the central-path equations, and for non-polyhedral cones that system is only guaranteed to be well posed after the problem is scaled: the primal point $x$ and the dual slack $s$ are transformed by a matrix $\Theta W$ chosen from the current iterate. Among the scalings analysed by Monteiro and Tsuchiya (2000), the best complexity bounds are obtained with the Nesterov–Todd (NT) scaling of Nesterov and Todd (1997), which maps $x$ and $s$ to the same point.

Andersen, Roos and Terlaky (2003) describe the conic quadratic interior-point solver of MOSEK. Their Lemma 4.2 gives the NT scaling in closed form for each of the three cone types they use. It is what makes the NT direction cheap: each cone block of $W$ is determined by one vector $w$, and $W$, $W^2$ and their inverses can be applied in time linear in the dimension. For the quadratic cone the formula goes back to Tsuchiya (1999); the paper re-derives it and extends it to the rotated quadratic cone.

Setting

Fix one cone block of dimension $d$. Coordinates are $x = (x_1,\dots,x_d)$, $x_{k:d}$ denotes the subvector of coordinates $k,\dots,d$, and $\|\cdot\|$ is the Euclidean norm. The block is one of

• the positive half-line $\mathbb R_+$ ($d=1$), with $T = Q = 1$;
• the quadratic cone $K^q = \{x : x_1 \ge \|x_{2:d}\|\}$ ($d\ge1$), with $T = I$ and $Q = \operatorname{diag}(1,-1,\dots,-1)$;
• the rotated quadratic cone $K^r = \{x : 2x_1x_2 \ge \|x_{3:d}\|^2,\ x_1,x_2\ge0\}$ ($d\ge2$), with $T$ the identity except for the leading block $\tfrac1{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$, and $Q$ the matrix with $Q_{12} = Q_{21} = 1$, $Q_{jj} = -1$ for $j\ge3$, and zeros elsewhere.

A scaling matrix (Definition 3.3) is a symmetric positive definite $W$ with $WQW = Q$. For $\theta>0$ the scaled points are $\bar x = \theta W x$ and $\bar s = (\theta W)^{-1}s$. The pair $(\theta, W)$ is an NT scaling of $(x, s)$ when $\bar x = \bar s$, equation (28); equivalently $s = \theta^2W^2x$, equation (29).

Formalization targets

Goal: Lemma 4.2 (p. 15)

For $x, s$ in the interior of the cone:

1. every NT scaling satisfies

$$\theta^2 = \sqrt{\frac{s^TQs}{x^TQx}};\qquad(30)$$

2. with this $\theta$ and

$$w = \frac{\theta^{-1}s + \theta Qx}{\sqrt2\sqrt{x^Ts + \sqrt{x^TQx\,s^TQs}}},\qquad(32)$$

the following matrices $W$ make $(\theta, W)$ an NT scaling: $W = \theta^{-1}(X^{-1}S)^{1/2}$ for $\mathbb R_+$;

$$W = \begin{bmatrix} w_1 & w_{2:d}^T\\ w_{2:d} & I + \frac{w_{2:d}w_{2:d}^T}{1+w_1}\end{bmatrix} = -Q + \frac{(e_1+w)(e_1+w)^T}{1+e_1^Tw}\qquad(31)$$

for $K^q$; and

$$W = -Q + \frac{(Te_1+w)(Te_1+w)^T}{1+e_1^TTw}\qquad(34)$$

for $K^r$. In the last two cases $W^2 = -Q + 2ww^T$, equations (33) and (35).

Milestones

Lemma 3.3 i)–iii) (scaling preserves $x^Ts$ and rescales $x^TQx$, $s^TQs$ by $\theta^{\pm2}$); (30) on its own; the normalization $w_1^2 - \|w_{2:d}\|^2 = 1$ and the square (62) of the arrow form (31); positivity of the radicand of (32); the identity $2\theta^2(w^Tx)^2 = x^Ts + \sqrt{x^TQx\,s^TQs}$ and the formula (32); for the rotated cone, the transport (63) by $T$, the identities $\hat\theta = \theta$ and $\hat w = Tw$, and $TWT = \hat W$. Two companions: Lemma 4.3, $(\theta W)^{-2} = \theta^{-2}QW^2Q$, and Lemma 3.3 iv), that a scaling maps the cone and its interior onto themselves.

Significance

The result. Lemma 4.2 turns the NT scaling, defined implicitly by (28), into explicit data: one scalar $\theta$ and one vector $w$ per cone. Combined with Lemma 4.3 it shows that every product with $W$, $W^2$ or their inverses in the scaled Newton system (27) is a rank-one correction of a signature matrix, which is what the paper's implementation relies on. The rotated-cone formula (34) is the paper's own addition and is what lets rotated cones be handled natively instead of through a change of variables.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist, and the platform has no formalization of second-order-cone scalings. The work is the matrix algebra of the Lorentz group — the signature matrix $Q$, the matrices with $WQW = Q$, and their action on $K^q$ and $K^r$ — which is reusable for every second-order-cone algorithm.

Difficulty

Most of the items are finite-dimensional identities, but they are identities between block matrices of arbitrary size with entries that are nested square roots, and they hold only on the interior of the cone, where the radicands are positive. The derivation in the paper runs backwards: it assumes $W$ has the shape (31) and solves for $w$, taking a square root without fixing its sign. The goal asks for the forward direction — that the displayed $\theta$, $w$, $W$ do satisfy (28) and $W\succ0$ — which needs the normalization $w^TQw = 1$, positive definiteness of $-Q + (e_1+w)(e_1+w)^T/(1+w_1)$, and, for the rotated cone, the reduction to the quadratic cone through $T$ with $TT = I$ and $TQ^rT = Q^q$.

Formalization scope

• Per block. Every statement is made for one cone block. $\Theta$ and $W$ are block diagonal (pp. 11–12), so this is the paper's statement block by block. The cone type is the parameter kind : ConeKind, and vectors are Fin d → ℝ.
• Index base and norms. The paper's $x_1$ is coordinate 0. $\|x_{2:d}\|^2$ is written as a sum of squares (tailSq x 1); Mathlib's norm on Fin d → ℝ, which is the sup norm, is never used.
• Interiors. The interiors are given by strict inequalities. The paper never defines $\operatorname{int}(K)$ concretely; these coincide with the topological interiors.
• Added hypotheses. All are disclosed in the items:
  • the dimension conventions ($d=1$ for $\mathbb R_+$, $d\ge1$ for $K^q$, $d\ge2$ for $K^r$), which the paper leaves implicit;
  • $\theta>0$ in Definition 3.3, which the paper calls positive definite on p. 24;
  • $1+w_1>0$ wherever the page divides by $1+w_1$;
  • $w^Tx>0$ for the last step of the derivation of (32), where the page silently fixes this sign.
• Inverses. The matrix inverse is Mathlib's total inverse. The NT predicate always contains $W\succ0$, so (28) never reads the junk value of a singular inverse.
• Reading of Lemma 4.2. The lemma names $\theta$ and $W$ without quantifying them. The goal states (30) for every NT scaling and asserts that the displayed formulas are an NT scaling. It does not claim that the NT scaling is unique, which the paper does not prove.
• Ruling out a trivial formalization. Stating only (30) would allow a version that holds vacuously if no NT scaling existed. Part 2 of the goal is what excludes this, and a sanity check exhibits $\theta = 1$, $W = I$ at $x = s = e_1$ in $K^q$ for $d=2$.

A complete development needs:

• the cone definitions and the matrices $T$, $Q$;
• Mathlib's Matrix.PosDef and Matrix.inv;
• elementary real square-root algebra.

Lemmas about $\{W : W\succ0,\ WQW = Q\}$ (closure under products and inverses, invariance of $K^q$) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for positive definiteness of (31).

Selected references

• E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; authors' preprint of 18 Dec 2000. https://doi.org/10.1007/s10107-002-0349-3
• Yu. E. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1) (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
• R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88(1) (2000) 61–83. https://doi.org/10.1007/PL00011378
• T. Tsuchiya, A convergence analysis of the scaling-invariant primal-dual path-following algorithms for second-order cone programming, Optimization Methods and Software 11–12 (1999) 141–182. https://doi.org/10.1080/10556789908805750
• F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003) 3–51. https://doi.org/10.1007/s10107-002-0339-5

Motivation

Many operations models contain terms of the form $E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$: expected shortfall or overflow of an affine function of an uncertain vector. Inventory and newsvendor costs, penalties for violated soft constraints, and the Conditional Value-at-Risk of a linear decision rule all reduce to it. In practice the distribution $\mathbb P$ of the uncertainty is rarely known; what is known are a few descriptive statistics, such as a range for the mean and an estimate of the covariance. Distributionally robust optimization then replaces the expectation by its supremum over every distribution consistent with that information.

The question goes back to Scarf (1958), who solved a single-product newsvendor problem against the worst distribution with known mean $\mu$ and variance $\sigma^2$, using the fact that $\sup E(X^+) = \tfrac12\big(\mu + \sqrt{\mu^2 + \sigma^2}\big)$ over such laws; Gallego and Moon (1993) simplified the argument. El Ghaoui, Oks and Oustry (2003) obtained conic representations of worst-case Value-at-Risk under mean and covariance information, and Delage and Ye (2010) studied stochastic programs with uncertain mean and covariance. Goh and Sim (2010) use bounds of this kind inside a general framework for linear optimization under uncertainty with recourse: after a piecewise-linear decision rule is introduced, every expectation in the reformulated problem is of the form above, and the framework needs a tractable, ideally exact, value for its worst case. Section 5.2 of the paper provides it when the information consists of a set containing the mean and the exact covariance.

Setting

A primitive uncertainty $\tilde z \in \mathbb R^{N}$ is represented through a segregated uncertainty $\tilde\zeta \in \mathbb R^{N_E}$, $N_E \ge N$, and a fixed matrix $F \in \mathbb R^{N\times N_E}$ and vector $g \in \mathbb R^{N}$ with $\tilde z = F\tilde\zeta + g$ (equation (9) of the paper). The paper notes that $F$ has full row rank. Write $n = N_E$.

The distributional information is:

• a set $\hat{\mathcal V} \subseteq \mathbb R^{n}$ known to contain the mean $\hat\zeta = E_{\mathbb P}(\tilde\zeta)$ (the mean is uncertain, its "support" is $\hat{\mathcal V}$);
• the exact covariance $\Sigma \in \mathbb R^{N \times N}$ of the primitive vector $\tilde z$.

The family is

$$\mathbb F_2 = \Big\{\mathbb P :\ \hat\zeta = E_{\mathbb P}(\tilde\zeta) \in \hat{\mathcal V},\ E_{\mathbb P}\big(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F'\big) = \Sigma\Big\}.$$

For $r^0 \in \mathbb R$ and $r \in \mathbb R^{n}$ the worst-case expected positive part is $\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$, and the bound of (22) is

$$\pi^2(r^0, r) = \inf_{y:\, F'y = r}\ \sup_{\hat\zeta \in \hat{\mathcal V}} \Big\{ \tfrac12 (r^0 + r'\hat\zeta) + \tfrac12 \sqrt{(r^0 + r'\hat\zeta)^2 + y'\Sigma y} \Big\}.$$

Following the paper (p. 909), an infeasible minimization has value $+\infty$; all values are in $[-\infty, +\infty]$.

Formalization targets

Goal: Theorem 2 (p. 910)

For $F$ of full row rank, $\Sigma$ positive semidefinite and $\hat{\mathcal V}$ nonempty,

$$\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^2(r^0, r) \qquad \text{for all } r^0, r.$$

This is an exact identity; it contains no constants that later work could improve.

Milestones

1. Upper-bound part of Theorem 2: $\sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^2(r^0, r)$, with no hypotheses.
2. Remark after Theorem 2: for $\Sigma \succeq 0$, $f(u) = \tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y}$ is nondecreasing in $u$.
3. (23): for $\Sigma \succeq 0$ and $\hat{\mathcal V} \neq \emptyset$,

$$\pi^2(r^0, r) = \inf_{u,\, y}\Big\{\tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y} :\ r^0 + \sup_{\hat\zeta \in \hat{\mathcal V}} r'\hat\zeta \le u,\ F'y = r\Big\}.$$

4. Tightness part of Theorem 2: $\pi^2(r^0, r) \le \sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ under the goal's hypotheses.

Significance

Theorem 2 says that the deterministic problem (22) evaluates the worst case exactly, not merely bounds it. Through (23) it becomes a second-order cone program whenever $\hat{\mathcal V}$ is conic representable, so distributionally robust constraints and objectives with mean–covariance information can be handed to an off-the-shelf conic solver without loss. In the paper, $\pi^2$ is one of three building blocks (with the mean–support bound $\pi^1$ and the directional-deviation bound $\pi^3$) that are combined by infimal convolution into the unified bound of Theorem 4, which in turn prices the deflected linear decision rules of §6. Specialized to $N = n$, $F = I$ and a singleton mean set, it recovers Scarf's mean–variance bound.

The theorem is proved in the paper's online appendix; no machine-checked proof of it, nor of Scarf's bound in this multivariate form, is known to exist. A formalization would certify the exact value, including the cases the printed statement treats only implicitly: $r$ outside the range of $F'$ (both sides $+\infty$), a degenerate quadratic form $y'\Sigma y = 0$, and unbounded mean sets.

Difficulty

The upper bound is a moment inequality and is the easier half. The difficulty is tightness. The supremum over $\mathbb F_2$ is in general not attained, so the proof must exhibit, for every point of $\hat{\mathcal V}$, distributions on $\mathbb R^{n}$ that meet the full covariance constraint on $F\tilde\zeta$ exactly while driving the expected positive part of the single linear functional $r'\tilde\zeta$ to the bound. The constraint fixes $N(N+1)/2$ second moments, not just the variance of $r'\tilde\zeta$, so the scalar extremal laws behind Scarf's bound do not directly give members of $\mathbb F_2$. The case $F'y = r$ infeasible requires showing that the worst case is $+\infty$, i.e. that $\mathbb F_2$ contains distributions with arbitrarily large expectations; this is where the full-rank assumption on $F$ enters.

Formalization scope

The random vector is the identity on Fin n → ℝ and a distribution is a measure P on it. The mean, the covariance matrix and the finite-second-moment condition come from the published definition MomentDRO_Conf_Setting (meanVec, covMat, HasSecondMoments). The covariance condition is $F\,\mathrm{Cov}_{\mathbb P}(\tilde\zeta)\,F' = \Sigma$, which equals the paper's $E_{\mathbb P}(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F')$ by linearity; it constrains the covariance of the primitive vector, an $N \times N$ matrix, not the covariance of $\tilde\zeta$. The positive part is max · 0. The worst case and $\pi^2$ take values in EReal: an infimum over an empty set is $+\infty$ and a supremum over an empty set is $-\infty$, matching the paper's convention for infeasible problems. The paper's "inf" and "sup" are not claimed to be attained.

Readings fixed by this mission, each implicit in the paper:

• Full row rank of $F$ (p. 906, "F has to be full rank"), stated as surjectivity of $x \mapsto Fx$;
• $\Sigma$ positive semidefinite, as a covariance matrix must be;
• $\hat{\mathcal V}$ nonempty.

Each is needed for the equality: without it $\mathbb F_2$ can be empty (worst case $-\infty$) while $\pi^2$ is finite or $+\infty$. No convexity or closedness of $\hat{\mathcal V}$ is assumed; the theorem does not need it. A formalization that takes the infimum in $\mathbb R$ (where an empty infimum is $0$) or states only the inequality $\le$ would trivialize or weaken the theorem and is ruled out.

A complete development needs a Scarf-type mean–variance inequality for $E(X^+)$, constructions of multivariate distributions with a prescribed mean and covariance (Gaussian or finitely supported laws), and the monotonicity and continuity facts behind (23). The scalar inequality and the constructions of distributions with given first two moments are reusable well beyond this mission. Proofs of any milestone, and supporting lemmas on moment-constrained families, are welcome.

Selected references

• J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4), 902–917, 2010. https://doi.org/10.1287/opre.1090.0795
• H. Scarf, A min-max solution of an inventory problem, in K. Arrow (ed.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 201–209, 1958.
• G. Gallego and I. Moon, The distribution free newsboy problem: Review and extensions, Journal of the Operational Research Society 44(8), 825–834, 1993. https://doi.org/10.1057/jors.1993.141
• L. El Ghaoui, M. Oks and F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4), 543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3), 595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• X. Chen, M. Sim, P. Sun and J. Zhang, A linear decision-based approximation approach to stochastic programming, Operations Research 56(2), 344–357, 2008. https://doi.org/10.1287/opre.1070.0441