Convex Optimization

Motivation

Two-stage stochastic linear programs choose a first-stage decision $x$ before a random parameter is revealed and a recourse decision $w$ afterwards. The classical model assumes the distribution of the random data is known. In practice it is estimated, and often only its first two moments are trusted. The minimax (distributionally robust) approach hedges against this ambiguity by minimizing the worst-case expected cost over all distributions consistent with the known information; it goes back to Žáčková (1966) and Dupačová (1987). A second concern is risk: a decision maker who is not risk neutral evaluates the random second-stage cost through a nondecreasing convex disutility, not through its mean.

Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine both: the distribution of the second-stage data is known only through its mean and second-moment matrix, and the second-stage cost is passed through a piecewise-linear convex disutility. For the case where the randomness is in the objective of the second-stage problem, they show that the resulting minimax problem is exactly a single semidefinite program of polynomial size. This mission formalizes that result, Theorem 2.1 of the paper, and the steps of its proof.

Setting

The first-stage feasible region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge 0\}$ for $A\in\mathbb R^{m_1\times n}$, $b\in\mathbb R^{m_1}$, with first-stage cost vector $c\in\mathbb R^n$. Given a recourse matrix $W\in\mathbb R^{r\times d}$, a technology matrix $T\in\mathbb R^{r\times n}$ and $h\in\mathbb R^r$, the recourse set of $x$ is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge 0\}$. For an objective vector $q\in\mathbb R^d$, the second-stage cost is the value of a linear program,

$$\mathcal Q(q,x)=\min_{w}\ q'w\quad\text{s.t.}\quad Ww=h-Tx,\ w\ge 0 .$$

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$, a nondecreasing convex piecewise-linear function; $K=1$, $\alpha_1=1$, $\beta_1=0$ is the risk-neutral case.

The objective $\tilde q$ of the second stage is random, the right-hand side $h$ is constant. The moment class $\mathcal P$ consists of all probability distributions of $\tilde q$ on $\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$. The problem studied is

$$Z=\min_{x\in X}\Big(c'x+Z(x)\Big),\qquad Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big]. \tag{2}$$

The inner supremum is an infinite-dimensional linear program over distributions (the paper's (5)). Its dual (6) is the semi-infinite program

$$Z_D(x)=\min_{Y,y,y_0}\ Q\cdot Y+\mu'y+y_0\quad\text{s.t.}\quad q'Yq+q'y+y_0\ge\mathbb U(\mathcal Q(q,x))\ \ \forall q\in\mathbb R^d,$$

over symmetric $Y$, where $Q\cdot Y=\sum_{i,j}Q_{ij}Y_{ij}$. The paper's standing assumptions are: $X$ is nonempty and bounded (Assumption 1); complete recourse (Assumption 2); $\{\pi\in\mathbb R^r : W'\pi\le q\}\neq\emptyset$ for all $q$ (Assumption 3); and $Q-\mu\mu'\succ 0$ (Assumption 4).

Formalization targets

Goal: Theorem 2.1

Under the assumptions, with $M_k=\begin{pmatrix}Y&\frac12(y-\alpha_k w_k)\\ \frac12(y-\alpha_k w_k)'&y_0-\beta_k\end{pmatrix}$,

$$Z=Z_{\mathrm{SDP}}=\min_{x,Y,y,y_0,w_k}\ c'x+Q\cdot Y+\mu'y+y_0\ \ \text{s.t.}\ \ M_k\succeq 0,\ Ww_k+Tx=h,\ w_k\ge0\ (k=1,\dots,K),\ Ax=b,\ x\ge 0, \tag{7}$$

and, for every $x\in X$, $Z(x)$ equals the value of the program (8) obtained from (7) by fixing $x$. The Lean goal also asserts that both $Z$ and $Z_{\mathrm{SDP}}$ are genuine greatest lower bounds of their sets of objective values.

Milestones, in the order the proof uses them

1. Weak duality $Z(x)\le Z_D(x)$ (§2.1, p. 583).
2. Strong duality $Z(x)=Z_D(x)$ under Assumption 4 (§2.1, p. 583, citing Isii).
3. Any $(Y,y,y_0)$ satisfying the $k$-th constraint $(\mathcal C_k)$ of (6) has $Y\succeq 0$.
4. Under Assumption 3, $X(x)$ is bounded and convex.
5. The minimax exchange $\inf_q\max_{w\in X(x)}=\max_{w\in X(x)}\inf_q$ for $q'Yq+q'y+y_0-\alpha_kq'w-\beta_k$.
6. $(\mathcal C_k)$ holds iff a single $w_k\in X(x)$ satisfies the inequality for every $q$.
7. The matrix inequality form: a quadratic $[q;1]'M[q;1]$ is nonnegative for all $q$ iff $M\succeq 0$ (a published, proved theorem, referenced).
8. The dual (6) and the semidefinite program (8) have the same objective values (p. 584).

Significance

Theorem 2.1 turns a minimax problem over an infinite-dimensional set of distributions, with a nonlinear risk measure applied to an LP value function, into one semidefinite program whose size is polynomial in $n$, $d$, $r$ and $K$. Off-the-shelf interior-point solvers then compute the risk-averse minimax decision, and the dual of (8) yields an explicit worst-case distribution (Theorem 2.2, formalized in the companion mission). The paper contrasts this with Delage and Ye's ellipsoid-method result, which covers a larger class of functions but gives no single compact program, and with the random right-hand-side case, which it shows to be NP-hard.

The result is proved in the paper; nothing here is open mathematics. As far as a search of the platform shows, none of it is formalized: no moment-problem duality theorem, no reformulation of a distributionally robust two-stage program, and no instance of the S-lemma-type step "$\forall q\ \exists w$ becomes $\exists w\ \forall q$" exist in machine-checked form. A complete development would provide the moment-problem strong duality for a specific continuous integrand with linear growth, which other distributionally robust optimization results reuse.

Difficulty

The obvious argument dualizes the moment problem and then substitutes the formula for $\mathcal Q$. Two steps resist this. First, strong duality for the moment problem is not a finite-dimensional LP fact: it needs the moment vector $(\mu,Q)$ to lie in the interior of the moment cone, and passing from that to "no duality gap" requires a separation argument in an infinite-dimensional space together with integrability of the integrand under every distribution with finite second moments. Second, constraint (6) is a "for every $q$ there is a $w$" statement, because $\mathcal Q(q,x)$ is a minimum over $w$. Replacing it with one $w_k$ that works for all $q$ is not a formal manipulation: it needs $Y\succeq 0$, which is not a constraint of (6) but a consequence of it, then a minimax theorem with the compact side $X(x)$, then attainment of the outer maximum. Both the boundedness of $X(x)$ and the convexity in $q$ are derived, not assumed.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ; indices $k$ run over Fin K with $K\ge 1$. The paper's letter $p$ denotes both the dimension of $q$ and the LP dual vector; here the dimension is $d$ and dual vectors are $\pi$. Distributions are probability measures with square-integrable coordinates (the platform's MomentDRO.Conf moment objects), not the densities written in (5). Every printed min/max is a real infimum/supremum of the set of objective values; attainment is not claimed except where a statement says so. $\mathcal Q(q,x)$ is a real infimum and is only used where $X(x)\neq\emptyset$ and Assumption 3 hold, which make it finite. Positive semidefiniteness is Matrix.PosSemidef on matrices indexed by Fin d ⊕ Fin 1. The minimax exchange is stated in EReal, since $\inf_q$ can be $-\infty$.

As printed, Assumptions 2 and 3 contradict each other whenever $r\ge1$: complete recourse produces a nonzero $u\ge0$ with $Wu=0$, and Assumption 3 at $q=-u$ is then infeasible. A statement assuming both would be vacuous. The formalization therefore uses what the proof of Theorem 2.1 uses: Assumption 3 for all $q$, and $X(x)\neq\emptyset$ for every $x\in X$ in place of Assumption 2. The hypotheses of the goal are satisfiable (e.g. $W=1$, $T=0$, $h=0$, $X=\{0\}$, $\mu=0$, $Q=1$). Program (7) is defined as one joint program over $(x,Y,y,y_0,w_1,\dots,w_K)$, never through $Z_D(x)$, so the goal is not strong duality plus unfolding.

Needed infrastructure: integrability of LP value functions under second-moment distributions, the moment-problem strong duality, Sion's minimax theorem (available in Mathlib and on the platform), and the bordered-matrix characterization of nonnegative quadratics (already proved on the platform). Proofs of any milestone, and reusable lemmas about LP value functions, are welcome.

Selected references

• D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
• K. Isii, On the sharpness of Chebyshev-type inequalities, Annals of the Institute of Statistical Mathematics, 185–197, 1963 (reference [15] of the paper; volume as printed there). https://doi.org/10.1287/moor.1100.0445
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
• E. Delage, 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
• J. Dupačová, The minimax approach to stochastic programming and an illustrative application, Stochastics 20(1):73–88, 1987. https://doi.org/10.1080/17442508708833436

Motivation

The trust-region subproblem asks for the minimum of a quadratic function over a Euclidean ball,

$$(Q_1)\qquad \min\Big\{\tfrac12 x^TAx + b^Tx : \|x\|\le r\Big\},$$

with $A$ a real symmetric $n\times n$ matrix that may be indefinite. It is solved at every iteration of a trust-region method for nonlinear optimization (Moré and Sorensen 1983; Conn, Gould and Toint 2000), so a method for it is used many thousands of times in a single run. Classical methods based on factorizations of $A + \lambda I$ do not scale to large sparse problems.

Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) apply to $(Q_1)$ their DCA, a general algorithm for d.c. programs (minimizing a difference of two convex functions). For a suitable splitting of the objective, one DCA iteration is a matrix–vector product followed by a scaling onto the ball. This mission formalizes the convergence theorem for that iteration (Theorem 4.1 of the paper), together with the general DCA convergence results it is derived from (Theorem 3.7 and the Appendix).

Timeline (as recorded in the paper's introduction):

• 1978: J. F. Toland develops the duality theory of d.c. optimization (J. Math. Anal. Appl. 66 (1978)).
• 1988: Pham Dinh and Elbernoussi introduce the DCA based on this duality, in its subgradient form (reference [23] of the paper, Trends in Mathematical Optimization, Birkhäuser).
• 1994: Le Thi's thesis and the authors' Rouen research report develop the DCA's convergence theory and large-scale implementations (references [7], [27] of the paper).
• 1998: the present paper specializes the DCA to $(Q_1)$, proves Theorem 4.1, and gives a restarting procedure that reaches a global solution.

Setting

Let $X = \mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For a function $\theta:X\to\mathbb R\cup\{+\infty\}$, $\operatorname{dom}\theta = \{x:\theta(x)<+\infty\}$, and $\Gamma_0(X)$ is the set of proper, lower semicontinuous, convex functions. For $\theta\in\Gamma_0(X)$ the conjugate is $\theta^*(y) = \sup_x\{\langle x,y\rangle-\theta(x)\}$, and the subdifferential at $x\in\operatorname{dom}\theta$ is $\partial\theta(x) = \{y : \theta(z)\ge\theta(x)+\langle z-x,y\rangle\ \forall z\}$. The function $\theta$ is $\rho$-convex ($\rho\ge0$) if $\theta-\frac\rho2\|\cdot\|^2$ is convex.

A d.c. program is $(P)\ \alpha = \inf\{g(x)-h(x): x\in X\}$ with $g,h\in\Gamma_0(X)$, under the convention $+\infty-(+\infty)=+\infty$ and the standing inclusions $\operatorname{dom}g\subset\operatorname{dom}h$, $\operatorname{dom}h^*\subset\operatorname{dom}g^*$. Its dual objective is $h^*(y)-g^*(y)$. The simplified DCA builds two sequences from $x^0\in\operatorname{dom}g$:

$$y^k\in\partial h(x^k),\qquad x^{k+1}\in\partial g^*(y^k).$$

For $(Q_1)$ let $E = \{x:\|x\|\le r\}$ ($r>0$), $\chi_E$ its indicator, and $f(x) = \frac12x^TAx+b^Tx+\chi_E(x)$. Fix $\rho>0$ with $\rho I-A$ positive semidefinite and split $f = g-h$ as in (16):

$$g(x) = \tfrac12\rho\|x\|^2+b^Tx+\chi_E(x),\qquad h(x) = \tfrac12x^T(\rho I-A)x.$$

The resulting DCA starts at any $x^0\in\mathbb R^n$ and, with $w^k = (\rho I-A)x^k-b$, sets $x^{k+1} = w^k/\rho$ if $\|w^k\|\le\rho r$ and $x^{k+1} = r\,w^k/\|w^k\|$ otherwise; equivalently $x^{k+1} = P_E\big(x^k-\frac1\rho(Ax^k+b)\big)$. A Kuhn–Tucker point of $(Q_1)$ is an $x^*$ with some $\lambda^*\ge0$ such that $(A+\lambda^*I)x^* = -b$, $\lambda^*(\|x^*\|-r)=0$ and $\|x^*\|\le r$.

Formalization targets

Goal: Theorem 4.1 (p. 491)

For every run of the DCA,

$$f(x^{k+1})\le f(x^k)-\tfrac12(\rho+\lambda)\|x^{k+1}-x^k\|^2,\qquad \lambda = \lambda_{\min}(\rho I-A),$$

$f(x^k)$ decreases to a limit $\alpha'\ge\alpha$, $\|x^{k+1}-x^k\|\to0$, and every limit point of $\{x^k\}$ is a Kuhn–Tucker point.

Milestones

In attack order:

1. (P_k): $\partial g^*(y)$ is the set of minimizers of $g-\langle\cdot,y\rangle$.
2. (18)–(19): the DCA step solves (18), is the projection (19), and is a simplified-DCA step for (16).
3. Proposition A.1(i): $(g-h)(x^{k+1})\le(h^*-g^*)(y^k)-\frac{\rho_2}2\|dx^k\|^2\le(g-h)(x^k)-\frac{\rho_1+\rho_2}2\|dx^k\|^2$, with its equality case.
4. Corollary A.2(i)–(ii): the same descent with the dual decrements.
5. Lemma A.3: continuity of $h$ along sequences with bounded subgradients.
6. Theorem 3.7(i): the descent with maxima of the four weighted steps.
7. Theorem 3.7(iii): if $\alpha$ is finite, both objectives converge to a common $\beta\ge\alpha$, the steps vanish, and the Fenchel–Young gaps tend to $0$.
8. Theorem 3.7(iv): with bounded iterates, limit points pair into $(x^*,y^*)\in[\partial g^*(y^*)\cap\partial h^*(y^*)]\times[\partial g(x^*)\cap\partial h(x^*)]$.
9. The moduli of (16): $\rho(g)=\rho$ and $\rho(h)=\rho-\lambda_n$.
10. (20): $\partial h(x^*)\subset\partial g(x^*)$ if and only if $x^*$ is a Kuhn–Tucker point.

The equality case of Theorem 3.7(i) and Theorem 3.7(ii) (the dual descent) are included as further draft theorems.

Significance

Theorem 4.1 makes the DCA a descent method for $(Q_1)$ whose accumulation points satisfy the first-order conditions. That property is what the paper's restarting procedure (§4.2) builds on: at a Kuhn–Tucker point that is not a global minimizer, one eigenvector computation gives a better feasible point, and the DCA reaches a global solution after at most $2m+2$ restarts, where $m$ is the number of distinct negative eigenvalues of $A$. Theorem 3.7 is the convergence theorem for the DCA on general d.c. programs, used throughout the later DCA literature.

All of these results are proved in the paper. As far as is known, none of them has a machine-checked proof: Mathlib has convex conjugates and subdifferentials in pieces, but no d.c. duality, no DCA and no analysis of the trust-region subproblem. This mission produces that development: a statement layer for d.c. programming with extended values, a formal proof of the general descent and criticality theorem, and its specialization to $(Q_1)$.

Difficulty

Every inequality of the analysis runs over $\mathbb R\cup\{+\infty\}$. The differences $g-h$ and $h^*-g^*$ need the paper's convention $+\infty-(+\infty)=+\infty$, and the finiteness of each value along a run has to be derived from the standing inclusions. The hard step is the passage to limit points in Theorem 3.7(iv). Lower semicontinuity of $g$, $g^*$ and $h$ gives only one-sided inequalities at a limit point, while the theorem asserts equalities of values there. The naive argument of passing to the limit in $y^k\in\partial h(x^k)$ and $x^{k+1}\in\partial g^*(y^k)$ fails, because $x^{k+1}$ and $x^k$ need not have the same limit unless $\rho_1+\rho_2>0$. For $(Q_1)$ the specialization needs boundedness of the iterates, finiteness of $\alpha$, and the subdifferential of the indicator of the ball. None of these is a hypothesis of Theorem 4.1, so each must be proved from the run.

Formalization scope

$X$ is EuclideanSpace ℝ (Fin n). Extended values are EReal, and every d.c. difference is dcSub g h x, equal to $+\infty$ when $g(x)=+\infty$ and to $g(x)-h(x)$ otherwise, because Mathlib's EReal has $\top-\top=\bot$. $\Gamma_0$, subgradients and the conjugate come from published platform definitions (IsProperClosedConvex, IsSubgradient, CondatPD.FinDim.conj). The modulus of strong convexity is never defined as a supremum. Statements take explicit constants $\rho_1,\rho_2,\rho_1^*,\rho_2^*$ with "$f_i$ is $\rho_i$-convex", which is what the paper requires of them. Hypotheses "$\rho(g)+\rho(h)>0$" become $\rho_1+\rho_2>0$. The matrix $A$ is a self-adjoint continuous linear operator. "$\lambda$ is the smallest eigenvalue of $\rho I-A$" is encoded by quantifying over every $\mu$ with $\rho I-A\succeq\mu I$. A limit point is a cluster point. The objective $f$ is $+\infty$ outside $E$, and the run starts from an arbitrary $x^0$, as on the page. Statements involving $dy^{k-1}$ are for $k\ge1$. Theorem 3.7(iv)'s limit identity is stated along a common convergent subsequence, as in its proof.

Ruled out: the goal is stated for the explicit iteration a)/b) of p. 490, never for an abstract run assumed to satisfy Theorem 3.7, and it carries no hypothesis of boundedness, finite $\alpha$ or convergence. A run predicate that no sequence satisfies would make everything vacuous, and a sanity file exhibits concrete runs.

Needed infrastructure: the Fenchel–Young equality and its equality case for $\Gamma_0$ functions in EReal, subdifferential inversion $y\in\partial g(x)\iff x\in\partial g^*(y)$, strong-convexity versions of the subgradient inequality, and the normal cone of a Euclidean ball. These are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• Pham Dinh Tao and Le Thi Hoai An, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM J. Optim. 8(2):476–505, 1998. https://doi.org/10.1137/S1052623494274313
• J. F. Toland, Duality in nonconvex optimization, J. Math. Anal. Appl. 66(2):399–415, 1978. https://doi.org/10.1016/0022-247X(78)90243-3
• J. J. Moré and D. C. Sorensen, Computing a trust region step, SIAM J. Sci. Statist. Comput. 4(3):553–572, 1983. https://doi.org/10.1137/0904038
• A. R. Conn, N. I. M. Gould and Ph. L. Toint, Trust-Region Methods, SIAM, 2000. https://doi.org/10.1137/1.9780898719857
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Why local minimizers of d.c. programs matter

A d.c. program minimizes a difference of two convex functions,

$$\alpha = \inf\{g(x) - h(x) : x \in \mathbb R^n\},$$

with $g$ and $h$ proper, lower semicontinuous and convex. Every twice continuously differentiable function is d.c. on compact convex sets, so the class covers most smooth nonconvex optimization, and it includes the trust-region subproblem $\min\{\tfrac12 x^\top A x + b^\top x : \|x\| \le r\}$ that motivates the paper of Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998) 476–505). Global minimization of a d.c. function is NP-hard in general, so practical algorithms, in particular the DCA of the same authors, compute local minimizers and critical points. The theory of local optimality is therefore what those algorithms can actually certify.

D.c. programs come with a dual program built from conjugate functions, $\inf\{h^*(y) - g^*(y) : y \in \mathbb R^n\}$, which has the same optimal value. Toland (J. Math. Anal. Appl. 66 (1978)) showed that global solutions correspond under this duality. For local solutions the correspondence is subtler, and §3.2 of the paper gives conditions under which a local minimizer of the primal produces one of the dual. Toland's earlier version required $g^*$ to be differentiable on the whole space; Corollary 3.5 of the paper needs only a condition at the single point $y^*$.

Setting

Let $X = \mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$; the dual space $Y$ is identified with $X$. Functions take values in $\mathbb R \cup \{+\infty\}$. $\Gamma_0(X)$ is the set of proper lower semicontinuous convex functions. For $\theta \in \Gamma_0(X)$:

• the effective domain is $\operatorname{dom}\theta = \{x : \theta(x) < +\infty\}$;
• the conjugate is $\theta^*(y) = \sup\{\langle x, y\rangle - \theta(x) : x \in X\}$;
• the subdifferential at $x_0 \in \operatorname{dom}\theta$ is $\partial\theta(x_0) = \{y : \theta(x) \ge \theta(x_0) + \langle x - x_0, y\rangle\ \forall x\}$, empty outside $\operatorname{dom}\theta$; $\operatorname{dom}\partial\theta$ is the set where it is nonempty.

Differences are taken under the convention $+\infty - (+\infty) = +\infty$. Throughout, $g, h \in \Gamma_0(X)$ satisfy the standing inclusions

$$\operatorname{dom} g \subset \operatorname{dom} h, \qquad \operatorname{dom} h^* \subset \operatorname{dom} g^*. \tag{3}$$

A point $x^*$ is a local minimizer of $g - h$ if $g(x^*) - h(x^*)$ is finite and there is a neighbourhood $U$ of $x^*$ with $g(x^*) - h(x^*) \le g(x) - h(x)$ for all $x \in U$ (display (4) of the paper); under the convention this is the same as requiring it for $x \in U \cap \operatorname{dom} g$. It is a critical point if $\partial g(x^*) \cap \partial h(x^*) \ne \emptyset$. The set $\mathcal P_l = \{x^* : \partial h(x^*) \subset \partial g(x^*)\}$ collects the points satisfying the classical necessary condition. "Local minimizer of $h^* - g^*$" is the same definition applied to the dual pair $(h^*, g^*)$.

Formalization targets

Goal: Corollary 3.5 (p. 485)

Let $x^* \in \operatorname{dom} g$ have an open neighbourhood $U$ with $g(x) - h(x) \ge g(x^*) - h(x^*)$ for all $x \in U \cap \operatorname{dom} g$, and let $y^* \in \partial h(x^*)$. If

$$y^* \in \operatorname{int}(\operatorname{dom} g^*) \quad\text{and}\quad \partial g^*(y^*) \subset U, \tag{12}$$

then $y^*$ is a local minimizer of $h^* - g^*$.

Milestones (in the order of the paper's proof)

1. Theorem 3.2(i) (p. 484): a local minimizer $x^*$ of $g - h$ lies in $\mathcal P_l$.
2. Inverse subgradients (proof of Corollary 3.5, p. 485): $y^* \in \partial h(x^*) \cap \partial g(x^*)$ gives $x^* \in \partial g^*(y^*) \cap \partial h^*(y^*)$.
3. Upper semicontinuity of $\partial g^*$ (proof of Corollary 3.5, p. 485): under (12) with $U$ open, $y^*$ has a neighbourhood $V \subset \operatorname{int}(\operatorname{dom} g^*)$ with $\partial g^*(y) \subset U \cap \operatorname{dom} g$ for every $y \in V$.
4. Theorem 3.2(ii) (p. 484): if $y^* \in \partial g(x^*) \cap \partial h(x^*)$, $U$ is a neighbourhood of $x^*$ with $U \cap \operatorname{dom} g \subset \operatorname{dom}\partial h$, and every $x \in U \cap \operatorname{dom} g$ has some $y \in \partial h(x)$ with

$$h^*(y) - g^*(y) \ge h^*(y^*) - g^*(y^*),$$

then $g(x) - h(x) \ge g(x^*) - h(x^*)$ on $U \cap \operatorname{dom} g$, and $x^*$ is a local minimizer.

Companion statements

• Corollary 3.3 (p. 485): if $x^* \in \operatorname{dom} g$ and $\partial h(x) \cap \partial g(x^*) \ne \emptyset$ for all $x \in U \cap \operatorname{dom} g$, then $x^*$ is a local minimizer, with the inequality on all of $U \cap \operatorname{dom} g$.
• Corollary 3.4 (p. 485): if $x^* \in \operatorname{int}(\operatorname{dom} h)$ and $\partial h(x^*) \subset \operatorname{int}(\partial g(x^*))$, then $x^*$ is a strict local minimizer.
• The differentiable case of (12) (pp. 485–486): in the setting of the goal, if $g^*$ is differentiable at $y^*$ then $\partial g^*(y^*) = \{x^*\}$ and (12) holds.

Significance

Corollary 3.5 lets a local solution of the primal d.c. program be read off as a local solution of the dual one. This matters when the dual program is easier to handle locally, and it is the local counterpart of the global duality of Theorem 3.1. Theorem 3.2(ii), which the authors present as new, is a sufficient condition for primal local optimality stated through the dual objective. Corollaries 3.3 and 3.4 are the sufficient conditions on which the convergence analysis of the DCA rests: they explain when the critical points that the DCA reaches are in fact local minimizers, for instance when $h$ is polyhedral.

These results have been proved on paper since 1997–1998 and are not open. To our knowledge none of them has a machine-checked proof. Formalizing them produces the local optimality theory of d.c. programming on top of an extended-real convex analysis layer (conjugates, subdifferentials, the convention $+\infty - (+\infty) = +\infty$), which the sibling missions of this series (global optimality, the DCA for the trust-region subproblem) can reuse.

Difficulty

Theorem 3.2 and Corollaries 3.3–3.4 are short arguments built on the Fenchel–Young inequality and its equality case. The obstacle in the goal is that the dual application of Theorem 3.2(ii) needs its hypothesis on a whole neighbourhood $V$ of $y^*$, while (12) is a condition at the single point $y^*$. Bridging this requires the upper semicontinuity of the subdifferential of $g^*$ at an interior point of its domain. That rests on two facts: $g^*$ is continuous and locally bounded there, and the subdifferential is locally bounded with closed graph. Neither is in Mathlib for extended-real functions. The dual application also needs $(h^*, g^*)$ to satisfy the standing assumptions, which needs biconjugation $g^{**} = g$ for $g \in \Gamma_0$, again in the extended-real setting. A first attempt that works only with finite-valued convex functions does not apply: $g^*$ is typically $+\infty$ outside a bounded set.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n) and values are EReal. $\Gamma_0$, $\partial$ and the conjugate are the published definitions ThreeOpSplitting.ConvexRates.IsProperClosedConvex, InertialFB.IFB.IsSubgradient and CondatPD.FinDim.conj (an EReal supremum over all of $X$). The subgradient predicate requires the base point to lie in the domain, as the paper does.
• The paper's $g(x) - h(x)$ is the function dcSub, which returns $+\infty$ whenever $g(x) = +\infty$. Mathlib's EReal subtraction is not used for it, because Mathlib sets $\top - \top = \bot$, and that would make every point outside $\operatorname{dom} g$ a global minimizer with value $-\infty$.
• "Local minimizer" includes the finiteness of $g(x^*) - h(x^*)$ (Mathlib's IsLocalMin is not used), and the goal's conclusion includes the finiteness of $h^*(y^*) - g^*(y^*)$.
• The standing assumptions $g, h \in \Gamma_0$ and (3) are the structure DCStanding and are a hypothesis of every item.
• Disclosed deviations:
  • In the goal and in milestone 3, $U$ is open. The page says "a neighborhood", but its proof needs an open set containing $\partial g^*(y^*)$.
  • Corollary 3.3 adds $x^* \in \operatorname{dom} g$. Without it the hypothesis is vacuous when $U \cap \operatorname{dom} g = \emptyset$, and the conclusion fails.
  • "$g^*$ differentiable at $y^*$" is stated through a real function that agrees with $g^*$ near $y^*$.
• The goal assumes nothing about $V$, the upper semicontinuity of $\partial g^*$, Theorem 3.2 or the relation $x^* \in \partial g^*(y^*)$. Those appear only as milestones.
• Infrastructure that would be reusable beyond this mission, and contributions that are welcome:
  • Fenchel–Young equality for EReal-valued $\Gamma_0$ functions;
  • biconjugation $g^{**} = g$;
  • continuity of a convex function on the interior of its domain;
  • local boundedness and upper semicontinuity of the subdifferential.

Selected references

• Pham Dinh Tao, Le Thi Hoai An, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM J. Optim. 8(2) (1998) 476–505. https://doi.org/10.1137/S1052623494274313
• J. F. Toland, Duality in nonconvex optimization, J. Math. Anal. Appl. 66 (1978) 399–415. https://doi.org/10.1016/0022-247X(78)90243-3
• Pham Dinh Tao, Le Thi Hoai An, Convex analysis approach to d.c. programming: theory, algorithms and applications, Acta Math. Vietnam. 22(1) (1997) 289–355.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Primal-dual interior-point methods are the standard algorithms for linear, second-order-cone and semidefinite programming. Their best-known variants keep the iterates in a narrow neighbourhood of the central path and take short or moderately long steps whose length is fixed in advance. Practical codes instead take long steps and recentre only when needed. Nesterov and Todd (SIAM J. Optim. 8 (1998) 324–364) developed a common theory of primal-dual methods for all self-scaled cones, the class that contains the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products. Section 7 of that paper analyses a predictor-corrector method whose neighbourhood is defined by the functional proximity measure $\gamma_F$, the conic version of the Tanabe–Todd–Ye potential. The predictor may move arbitrarily far from the central path, as measured by $\gamma_F$, and a Newton corrector brings the iterate back.

Timeline:

• 1994: Nesterov and Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, develop self-concordant barriers and logarithmically homogeneous barriers.
• 1997: Nesterov and Todd, Self-scaled barriers and interior-point methods for convex programming (Math. Oper. Res. 22 (1997) 1–42), introduce self-scaled barriers and the scaling point.
• 1998: the paper of this mission proves the symmetric primal-dual estimates and the complexity of the functional-proximity predictor-corrector method (Theorem 7.1).

Setting

Let $E=\mathbb R^n$ with the Euclidean inner product, and let $K\subseteq E$ be a closed convex cone that is pointed and has nonempty interior. Its dual cone is $K^*=\{s:\langle s,x\rangle\ge0\ \forall x\in K\}$. A $\nu$-self-concordant logarithmically homogeneous barrier $F$ for $K$ is a self-concordant function on $\operatorname{int}K$ that tends to $+\infty$ at the boundary and satisfies $(F'(x)h)^2\le\nu\langle F''(x)h,h\rangle$ and $F(\tau x)=F(x)-\nu\ln\tau$. Its conjugate is $F_*(s)=\sup\{-\langle s,x\rangle-F(x):x\in\operatorname{int}K\}$. $F$ is self-scaled if, for all $w,x\in\operatorname{int}K$, $F''(w)x\in\operatorname{int}K^*$ and $F_*(F''(w)x)=F(x)-2F(w)-\nu$. For $x\in\operatorname{int}K$ and $s\in\operatorname{int}K^*$, the scaling point $w\in\operatorname{int}K$ satisfies $F''(w)x=s$.

The problem is $\min\{\langle c,x\rangle:Ax=b,\ x\in K\}$ with dual $\max\{\langle b,y\rangle:A^*y+s=c,\ s\in K^*\}$, where $A:E\to\mathbb R^m$ is surjective. A triple $(x,y,s)$ is strictly feasible if $x\in\operatorname{int}K$, $s\in\operatorname{int}K^*$ and both equality constraints hold. With $\mu(x,s)=\langle s,x\rangle/\nu$ the functional proximity measure is

$$\gamma_F(x,s)=F(x)+F_*(s)+\nu\ln\mu(x,s)+\nu\ \ge0,$$

and it vanishes exactly on the central path. The neighbourhood is $\mathcal F(\beta)=\{(x,y,s)\ \text{strictly feasible}:\gamma_F(x,s)\le\beta\}$. The affine-scaling direction $(p_x,p_y,p_s)$ solves $F''(w)p_x+p_s=s$, $Ap_x=0$, $A^*p_y+p_s=0$. The centering direction $(d_x,d_y,d_s)$ solves the same system with right-hand side $s+\mu(x,s)F'(x)$. One Newton step moves by $-\alpha(d_x,d_y,d_s)$, with $\alpha=1/(1+\gamma_\infty+\bar\sigma)$, where $\gamma_\infty$ is the uniform proximity measure and $\bar\sigma=\max\{\sigma_x(d_x),\sigma_s(d_s)\}$.

One iteration of Algorithm 7.1 starts from $(x,y,s)\in\mathcal F(\beta)$. It takes the largest predictor step $\alpha$ along the affine-scaling direction with $\gamma_F=\beta+\Delta$, then applies Newton steps until the iterate is back in $\mathcal F(\beta)$.

Formalization targets

Goal: Theorem 7.1

Let $\beta=\kappa-\ln(1+\kappa)$ with $\kappa\in(0,1)$ and $\Delta>0$. There are constants $\omega_1,\omega_2>0$, depending only on $\Delta$ and $\kappa$, such that one iteration of Algorithm 7.1 on any self-scaled cone satisfies

$$\langle s_+,x_+\rangle\le(1-\alpha)\langle s,x\rangle,\qquad \frac{\alpha^2}{1-\alpha}\ge\frac{\omega_1}{\nu},\qquad \frac{\alpha^2}{1-\alpha}\ge\frac{\omega_2}{|p_x|_x\,\|p_s\|_s}\ge\frac{\omega_2}{\sqrt\nu\,|p_x|_x\,|p_s|_s},$$

and the corrector reaches $\mathcal F(\beta)$ after $N\le\lceil\Delta/(\bar\tau-\ln(1+\bar\tau))\rceil$ Newton steps, where $\bar\tau=\tfrac12\sqrt{3\beta/(1+\beta)}$. The constants are left existential, as on the page.

Milestones

In the paper's order, the milestones are:

• the σ-identities at the scaling point (Lemma 3.4);
• the norm comparison $|a|_b\le\|a\|_b\le\sqrt\nu|a|_b$ (Proposition 3.5);
• the third-derivative bounds (Theorem 3.8) and the parallelogram rule (Theorem 3.11);
• the barrier form of $\gamma_F$ (Lemma 3.12);
• the relations between the proximity measures (Theorem 4.2, (4.28)) and the comparison of metrics at $x$, $s$, $w$ (Lemma 4.3);
• the properties of the affine-scaling direction (Lemma 5.2) and the exact change of $\gamma_F$ along it (Theorem 5.3, Lemma 5.4);
• the properties of the centering direction (Lemma 5.6) and the decrease of $\gamma_F$ per Newton step (Theorem 5.7).

Significance

Theorem 7.1 gives an $O(\sqrt\nu\ln(\langle s_0,x_0\rangle/\epsilon))$ iteration bound for a method whose predictor neighbourhood $\mathcal F(\beta+\Delta)$ can be as wide as desired, with a bounded number of corrector steps per iteration. Inequality (7.3) also lets the step adapt to the problem: in the paper's normalisation the predictor step is at least of the order of the square root of the maximal feasible step. The same bounds apply to the narrow-neighbourhood predictor-corrector method of Section 6. One theorem covers linear, second-order-cone and semidefinite programming, with no reformulation through matrices.

The result is proved in the paper. No machine-checked proof of it, or of any of the self-scaled-barrier estimates it rests on, is known. Formalizing the proof produces a reusable library of local norms, σ-measures and third-derivative bounds for self-scaled barriers, and of the proximity measures of primal-dual methods.

Difficulty

A naive argument would bound the predictor step with the usual self-concordance estimate $|F'''(x)[p,p,p]|\le2\|p\|_x^3$. That bound loses a factor $\sqrt\nu$ and cannot give (7.2) or (7.3). What is needed is the sharper self-scaled bound (3.14), in which one factor is the smaller norm $|p|_x$. It in turn depends on the cone being self-scaled: $F'''(x)[v]$ must be negative semidefinite for $v\in K$, and the scaling point must exist. The other obstacle is that the change of $\gamma_F$ along the affine-scaling direction must be computed exactly, not just estimated. That is the parallelogram rule (Theorem 3.11), an identity special to self-scaled barriers. The corrector bound needs a lower bound on the Newton decrement that holds uniformly outside $\mathcal F(\beta)$, which (4.28) supplies.

Formalization scope

• Spaces. The dual space $E^*$ is identified with $E$ through the inner product. Which local norm is meant is carried by the function used:

  • lnorm G v u and dnorm G v u, with $G=F$ or $G=F_*$;
  • sigma C c u $=\min\{\beta\ge0:\beta c-u\in C\}$, with the cone $C$ and the centre $c$ fixed by the paper's four cases.

  Each two-form measure uses its first printed form.

• Standing assumptions. Every statement assumes that $K$ is a proper cone and that $F$ is a $\nu$-self-scaled barrier, and it also states $\nu\ge1$, which the paper derives. The barrier includes explicit nondegeneracy of $F''$, which also follows from the other axioms. The conjugate is a supremum over $\operatorname{int}K$ and is only evaluated on $\operatorname{int}K^*$. Assumptions (2.4)–(2.5) are implied by the strictly feasible points that the statements start from.

• Scaling points, directions and steps are predicates given by their defining equations; nothing is computed by inverting a matrix.

• Corrections to the page. Two printed slips are corrected, and both are disclosed:

  • the predictor point of Algorithm 7.1 is $(x-\alpha p_x,y-\alpha p_y,s-\alpha p_s)$;
  • (7.4) is stated with a ceiling, since $N\ge1$ while the printed right-hand side can be below $1$.

• Ruling out trivial versions. The goal does not assume any of the following; they are milestones, not hypotheses:

  • the identity (7.5);
  • the bounds of Lemma 5.4;
  • the decrease of Theorem 5.7;
  • the gap identity (5.9).

  The constants $\omega_1,\omega_2$ are quantified before the cone, the barrier and the data, so they cannot depend on them. The predictor step is the largest step whose whole segment stays strictly feasible.

• Out of scope. No self-scaled barrier, existence of scaling points (T*3.2 of [NT97]), or result of Nesterov–Nemirovskii is formalized here. These and the central-path duality theorem (Theorem 4.1) are external results. Proofs that build them are welcome, as is a non-vacuity witness for the goal on the orthant of $\mathbb R^2$.

Selected references

• Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
• Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Math. Oper. Res. 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• O. Güler, Barrier functions in interior point methods, Math. Oper. Res. 21 (1996) 860–885. https://doi.org/10.1287/moor.21.4.860

Motivation

Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector $\bar y$ exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal $\bar y$ does not tell where the primal optimum is, because the minimizers of $x \mapsto L_0(x, \bar y)$ over $X$ typically include points that are not optimal and not even feasible. A linear program is the extreme case: $L_0(\cdot, \bar y)$ is then often constant.

The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for $r > 0$, minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for $L_0$ has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.

Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian $L_r$ below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.

Setting

Let $E$ be a real vector space, $X \subseteq E$ a nonempty convex set, and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex functions. The problem is

$$\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \quad\text{subject to } f_i(x) \le 0,\ i = 1, \dots, m.$$

A point is feasible if it lies in $X$ and satisfies the constraints. The optimal value "inf in (P)" is the infimum of $f_0$ over the feasible points, an element of $[-\infty, +\infty]$. An optimal solution is a feasible $\bar x$ with $f_0(\bar x) \le f_0(x)$ for every feasible $x$.

For $y \in \mathbb R^m$ (no sign restriction), $\theta(t) = \max\{0, t\}$ and $r > 0$, the penalty Lagrangian is

$$L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big].$$

The ordinary Lagrangian is $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ for $y \ge 0$, and $-\infty$ otherwise. The dual objectives are $g_r(y) = \inf_{x \in X} L_r(x, y)$ and $g_0(y) = \inf_{x \in X} L_0(x, y)$. Problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$.

• A dual optimal solution is a maximizer $\bar y$ of $g_r$ with $g_r(\bar y) > -\infty$.
• (P) is normal if the dual optimal value $\sup g_0$ equals the optimal value of (P).
• $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ if $-\infty < \inf_{x \in X} L_r(x, \bar y) = \inf$ in (P).
• $(\bar x, \bar y)$ is a saddle point of $L_r$ if $\bar x \in X$ and $L_r(\bar x, y) \le L_r(\bar x, \bar y) \le L_r(x, \bar y)$ for all $x \in X$, $y \in \mathbb R^m$.

In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.

Formalization targets

Goal: Theorem 3.5 (p. 362)

Assume (P) is normal, $\bar y$ is a dual optimal solution, and $r > 0$. Then for every $\bar x \in E$

$$\bar x \text{ is optimal for (P)} \iff \bar x \in X \text{ and } L_r(\bar x, \bar y) \le L_r(x, \bar y) \ \ \forall x \in X.$$

Milestones (attack order)

1. §3 after (3.17), pp. 361–362: for $r > 0$, $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ iff $\bar y$ is optimal for $(D_r)$ and (P) is normal.
2. §3, p. 362: for $r > 0$, $(\bar x, \bar y)$ is a saddle point of $L_r$ iff $\bar x$ is optimal for (P) and $\bar y$ is a Kuhn–Tucker vector.
3. Corollary 3.4, $r > 0$ (p. 362): $L_r$ and $L_0$ have the same Kuhn–Tucker vectors and the same saddle points, and the saddle points of $L_r$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions

$$\bar y_i \ge 0,\ f_i(\bar x) \le 0,\ \bar y_i f_i(\bar x) = 0\ (\forall i), \qquad \bar x \in \operatorname{argmin}_X \Big(f_0 + \sum_i \bar y_i f_i\Big).$$

4. Corollary 3.4, $r = 0$: the saddle points of $L_0$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions.
5. Proof of Theorem 3.5, pp. 362–363: if $\bar y$ is optimal for $(D_r)$ and $\bar x \in X$ minimizes $L_r(\cdot, \bar y)$ over $X$, then $\nabla_y L_r(\bar x, \bar y) = 0$ and $\bar y$ maximizes $L_r(\bar x, \cdot)$ over $\mathbb R^m$.

Significance

The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of $L_r(\cdot, \bar y)$ over $X$ solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function $g_r$ over $\mathbb R^m$, then minimize $L_r(\cdot, \bar y)$ over $X$. For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, $L_r$ behaves exactly like $L_0$.

Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on $\mathbb R^n$ (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.

Difficulty

The "if" direction is the substantive one. A minimizer $\bar x$ of $L_r(\cdot, \bar y)$ is not known to be feasible; feasibility must come from maximality of $\bar y$ in the dual. The natural argument for $L_0$ breaks at exactly this point: $L_0(\bar x, \cdot)$ is affine on the orthant, and minimality in $x$ gives no information about $\nabla_y$. For $L_r$ the link is the differentiability of the dual function $g_r$ with $\nabla g_r(\bar y) = \nabla_y L_r(\bar x, \bar y)$ (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so $\pm\infty$ must be handled at each step.

Formalization scope

• $E$ is a bare real vector space (AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.
• $X$ is a Set E. Each statement assumes the paper's standing hypothesis (p. 358): $X$ convex and nonempty, $f_0, \dots, f_m$ convex on $X$.
• The $f_i$ are total functions E → ℝ, and only their values on $X$ enter. Constraint indices are Fin m (0-based), with $f_0$ a separate argument.
• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m).
• $g_r$, $g_0$, $L_0$, the optimal value of (P) and the dual optimal value are EReal-valued. An infeasible (P) has value $+\infty$, and $g_0 = -\infty$ off $y \ge 0$.
• $r > 0$ is an explicit hypothesis wherever the paper has it. Theorem 3.5 is false for $r = 0$ (p. 363), and the Lean expression Lr at $r = 0$ is not $L_0$.
• "Dual optimal solution" in Theorem 3.5 is read as optimal for $(D_r)$ with the same $r$, with $g_r(\bar y) > -\infty$ (the convention of p. 361). The paper's reading, optimal for $(D_0)$, is equivalent by Theorem 3.2, which is posed in mission 1 of this series.
• "$\bar x$ minimizes $L_r(\cdot, \bar y)$ over $X$" includes $\bar x \in X$. The equivalence is stated for every $\bar x \in E$. No sign condition is imposed on $\bar y$: nonnegativity is a consequence of dual optimality, not a hypothesis.
• Saddle points are taken over $X \times \mathbb R^m$ (Rockafellar's Convex Analysis, §36). For $L_0$ they are taken in the extended reals.
• Trivializing readings ruled out: normality is neither dropped nor replaced by existence of an optimal solution or by Slater's condition, and the minimization on the right of Theorem 3.5 is never over a set containing points outside $X$.

The solver needs the representation $L_r(x, y) = \min_u\{F_r(x, u) + u \cdot y\}$, weak duality, the envelope formula and differentiability of $g_r$ (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.

Selected references

• R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.