Optimization

Motivation

In high-dimensional linear regression the number of unknown coefficients $M$ may be much larger than the number of observations $n$, and the coefficient vector can only be recovered because it is assumed to be sparse: few of its entries are non-zero. Two convex estimators dominate this setting: the Lasso of Tibshirani (1996), an $\ell_1$-penalized least-squares estimator, and the Dantzig selector of Candès and Tao (2007), which minimizes the $\ell_1$ norm subject to a bound on the correlation between the residual and the columns of the design. Both are used routinely in statistics, signal processing and machine learning, and their rates of convergence determine how many observations suffice to estimate a sparse vector.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009) analysed the two estimators side by side under a single, weak condition on the design, the restricted eigenvalue (RE) assumption. This mission formalizes their rates for the Dantzig selector, Theorem 7.1 of the paper.

Timeline. Candès and Tao (Ann. Statist. 35, 2007) introduced the Dantzig selector and bounded its $\ell_2$ error under a uniform uncertainty principle on the design. Bickel, Ritov and Tsybakov (2009) replaced that condition by the RE assumptions, which are implied by it (their Lemma 4.1), and obtained $\ell_p$ bounds for every $1\le p\le2$ and a prediction bound, with explicit constants. Later work (van de Geer and Bühlmann, EJS 2009) compared RE with the compatibility condition and other design conditions.

Setting

Observations follow the linear model

$$y=X\beta^*+w,$$

where $X\in\mathbb R^{n\times M}$ is a deterministic design matrix, $n\ge1$, $M\ge2$, $\beta^*\in\mathbb R^M$ is unknown, and $w=(W_1,\dots,W_n)$ has independent $\mathcal N(0,\sigma^2)$ coordinates with $\sigma>0$. The columns are normalized: every diagonal element of the Gram matrix $X^TX/n$ equals 1.

For $\beta\in\mathbb R^M$, $J(\beta)=\{j:\beta_j\ne0\}$ is its support and $\mathcal M(\beta)=|J(\beta)|$ its sparsity; $\beta^*$ satisfies $\mathcal M(\beta^*)\le s$ for an integer $1\le s\le M$. Norms are $|\delta|_p=(\sum_j|\delta_j|^p)^{1/p}$ and $|v|_2^2=\sum_iv_i^2$; for an index set $J$, $\delta_J$ keeps the coordinates of $\delta$ in $J$ and sets the others to 0, and $J^c$ is the complement of $J$.

With a tuning level $r=A\sigma\sqrt{\log M/n}$, $A>\sqrt2$, the Dantzig selector is any minimizer

$$\hat\beta_D\in\arg\min_{\beta\in\Lambda}|\beta|_1,\qquad \Lambda=\Big\{\beta\in\mathbb R^M:\ \Big|\tfrac1nX^T(y-X\beta)\Big|_\infty\le r\Big\}.$$

The cone condition at an index set $J_0$ with constant $c_0>0$ is $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$. Assumption RE$(s,c_0)$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Assumption RE$(s,m,c_0)$ is the same with $|\delta_{J_{01}}|_2$ in the denominator, where $J_{01}=J_0\cup J_1$ and $J_1$ collects the $m$ largest $|\delta_j|$ outside $J_0$; it is used for $s\le m$, $s+m\le M$.

Formalization targets

Goal: Theorem 7.1

With probability at least $1-M^{1-A^2/2}$, every Dantzig selector satisfies

$$|\hat\beta_D-\beta^*|_1\le\frac{8A}{\kappa^2(s,1)}\,\sigma s\sqrt{\frac{\log M}{n}},\qquad |X(\hat\beta_D-\beta^*)|_2^2\le\frac{16A^2}{\kappa^2(s,1)}\,\sigma^2s\log M,$$

and, on the same event, if RE$(s,m,1)$ holds, simultaneously for all $1<p\le2$,

$$|\hat\beta_D-\beta^*|_p^p\le2^{p-1}\,8\Big\{1+\sqrt{\tfrac sm}\Big\}^{2(p-1)}s\Big(\frac{A\sigma}{\kappa^2(s,m,1)}\sqrt{\frac{\log M}{n}}\Big)^p .$$

Milestones

In the order the proof of the paper uses them:

1. The noise event $\mathcal B=\bigcap_j\{|\frac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P\{\mathcal B^c\}\le M^{1-A^2/2}$ (proof of Lemma B.3).
2. Lemma B.3, (B.9): for any $\beta$ satisfying the Dantzig constraint, $\delta=\hat\beta_D-\beta$ satisfies the cone condition at $J(\beta)$ with $c_0=1$.
3. (B.25): on $\mathcal B$, $\beta^*\in\Lambda$, $\frac1n|X^TX\delta|_\infty\le2r$, and $\frac1n|X\delta|_2^2\le4r\sqrt s\,|\delta_{J_0}|_2$.
4. (B.26): under RE$(s,1)$, $\frac1n|X\delta|_2^2\le16r^2s/\kappa^2$ and $|\delta_{J_0}|_2\le4r\sqrt s/\kappa^2$.
5. (B.27): on the cone, $|\delta|_1\le(1+c_0)\sqrt s\,|\delta_{J_0}|_2$.
6. (B.28): on the cone, $|\delta|_2\le(1+c_0\sqrt{s/m})\,|\delta_{J_{01}}|_2$.
7. (B.29): under RE$(s,m,1)$, $|\delta|_2^2\le16(1+\sqrt{s/m})^2(r\sqrt s/\kappa^2)^2$.
8. Interpolation: $\sum_ja_j\le b_1$, $\sum_ja_j^2\le b_2$, $a_j\ge0$ imply $\sum_ja_j^p\le b_1^{2-p}b_2^{p-1}$ for $1<p\le2$.

Significance

The result. Theorem 7.1 shows that, up to the factor $\log M$, the Dantzig selector estimates an $s$-sparse vector as well as least squares would if the support were known: the prediction error $\frac1n|X(\hat\beta_D-\beta^*)|_2^2$ is of order $\sigma^2s\log M/n$, and the $\ell_p$ errors are of order $s^{1/p}\sigma\sqrt{\log M/n}$. The bounds hold for any $M$, including $M\gg n$, provided only that RE holds, and every constant is explicit. The paper's Theorem 7.2 gives the same rates for the Lasso; comparing the two is the paper's main message.

Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has not been machine-checked. A complete formal proof would provide: a verified Gaussian maximal inequality for the noise event, the deterministic cone and RE arithmetic that underlies essentially all $\ell_1$-regularized estimation theory, and a reusable $\ell_1$–$\ell_2$ interpolation lemma. Most milestones are deterministic and independent of the probability layer.

Difficulty

The obvious argument — compare $\hat\beta_D$ with $\beta^*$ in Euclidean norm using the smallest eigenvalue of $X^TX/n$ — fails because that eigenvalue is 0 whenever $M>n$. The proof must instead show that the error vector lies in a cone on which $X$ is injective in a quantitative sense, and this uses the optimality of $\hat\beta_D$ (not just feasibility) together with the event $\mathcal B$ on which $\beta^*$ itself is feasible. The $\ell_p$ bound needs a second, stronger condition RE$(s,m,1)$ and a control of the tail of the error outside the $m$ largest coordinates. On the formal side, handling the non-uniqueness of the minimizer, real powers with exponent $p-1$ or $2-p$, and the union over $M$ Gaussian tails with the exact constant $M^{1-A^2/2}$ all need care.

Formalization scope

Vectors are functions Fin M → ℝ, the design is Matrix (Fin n) (Fin M) ℝ; the paper's dictionary of functions enters only through $X$. The unit diagonal of $X^TX/n$ is a hypothesis, not a normalization performed in the proof. The noise is W : Fin n → Ω → ℝ on a probability space, measurable, mutually independent, each of law $\mathcal N(0,\sigma^2)$; $\log$ is the natural logarithm. The Dantzig selector is a predicate (feasible and of minimal $\ell_1$ norm among feasible vectors), and every result is stated for every minimizer. RE$(s,c_0)$ and RE$(s,m,c_0)$ are stated through a witness $\kappa$ (a number with the defining lower-bound property); $\kappa(s,c_0)$ is the largest witness and the bounds decrease in $\kappa$, so the statements are equivalent to the paper's while avoiding the value of a real infimum over an empty set. Two witnesses are kept apart: $\kappa$ for RE$(s,1)$ in (7.4)–(7.5), $\kappa'$ for RE$(s,m,1)$ in (7.6). Ties in the choice of the $m$ largest coordinates are handled by quantifying over every admissible $J_1$. The probability statement asserts one measurable event $E$ with $\mathbb P(E)\ge1-M^{1-A^2/2}$ on which all three bounds hold for every minimizer, every admissible $m$, every witness $\kappa'$ and every $p$.

The event $E$ is fixed before the minimizer is quantified, so a formalization in which the event depends on $\hat\beta_D$, or in which RE is a hypothesis about the random error vector rather than the design, would be a different (weaker) statement and is not accepted. The deterministic milestones (B.26)–(B.29) take the conclusion of (B.25) as a hypothesis; they are true for every vector satisfying their hypotheses and are not restricted to the event.

A complete development needs Gaussian tail bounds and a union bound (Mathlib's gaussianReal), finite Hölder-type inequalities for real exponents, and elementary sorting arguments for the tail outside $J_{01}$. The cone, RE and interpolation lemmas are reusable for the Lasso (Theorem 7.2, a sister mission) and beyond. Proofs of any milestone are welcome independently.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• S. van de Geer, P. Bühlmann, On the conditions used to prove oracle results for the Lasso, Electron. J. Statist. 3, 1360–1392, 2009. https://doi.org/10.1214/09-EJS506

Motivation

Two estimators dominate sparse high-dimensional regression, where the number $M$ of candidate regressors can far exceed the sample size $n$. The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an $\ell_1$ penalty. The Dantzig selector (Candès and Tao, 2007) minimises the $\ell_1$ norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.

Setting

Let $f_1,\dots,f_M$ be real functions (the dictionary) on a set $\mathcal Z$, and $Z_1,\dots,Z_n\in\mathcal Z$ fixed design points, with $n\ge1$ and $M\ge2$. The design matrix is $X=(f_j(Z_i))\in\mathbb R^{n\times M}$. Observations are $Y_i=f(Z_i)+W_i$, where $f$ is an unknown function and $W_1,\dots,W_n$ are independent $\mathcal N(0,\sigma^2)$ with $\sigma>0$. Write $y=(Y_i)$, $\boldsymbol f=(f(Z_i))$ and $w=(W_i)$, so $y=\boldsymbol f+w$.

The empirical norm of $g$ is $\|g\|_n=(\tfrac1n\sum_i g(Z_i)^2)^{1/2}$. Every column has $\|f_j\|_n\neq0$, and $f_{\max}=\max_j\|f_j\|_n$. For $\beta\in\mathbb R^M$, $f_\beta=\sum_j\beta_jf_j$ has value vector $X\beta$. The support is $J(\beta)=\{j:\beta_j\ne0\}$ and the sparsity is $\mathcal M(\beta)=|J(\beta)|$. For $J\subseteq\{1,\dots,M\}$, $\delta_J$ agrees with $\delta$ on $J$ and vanishes elsewhere.

Fix $r>0$. The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(Y_i-f_\beta(Z_i)\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j| .$$

With $D=\mathrm{diag}(\|f_1\|_n^2,\dots,\|f_M\|_n^2)$, the Dantzig constraint is $|\tfrac1nD^{-1/2}X^\top(y-X\beta)|_\infty\le r$. The Dantzig selector $\hat\beta_D$ is any vector of smallest $|\beta|_1=\sum_j|\beta_j|$ that satisfies it. The estimators are $\hat f_L=f_{\hat\beta_L}$ and $\hat f_D=f_{\hat\beta_D}$.

Assumption RE$(s,c_0)$ with $1\le s\le M$, $c_0>0$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\ \frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Throughout, $r=A\sigma\sqrt{\log M/n}$, where $\log$ is the natural logarithm.

Formalization targets

Goal: Theorem 5.1

Assume RE$(s,1)$ with $1\le s\le M$, and let $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution with $\mathcal M(\hat\beta_L)\le s$ and every Dantzig selector satisfy

$$\Big|\,\|\hat f_D-f\|_n^2-\|\hat f_L-f\|_n^2\,\Big|\le16A^2\,\frac{\mathcal M(\hat\beta_L)\sigma^2}{n}\,\frac{f_{\max}^2}{\kappa^2(s,1)}\,\log M .$$

Milestones

The proof uses one probabilistic event and two one-sided deterministic inequalities.

1. The Lasso satisfies the Dantzig constraint (2.3).
2. The noise event $\mathcal A=\bigcap_j\{2|\tfrac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$ (B.4).
3. On $\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_L)|_\infty\le 3rf_{\max}/2$ (Lemma B.1, (B.2)).
4. The Dantzig error lies in the cone $|\delta_{J_0^c}|_1\le|\delta_{J_0}|_1$ (Lemma B.3, (B.9)).
5. On the larger event $\mathcal B\supseteq\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_D)|_\infty\le 2rf_{\max}$ (Lemma B.3, (B.10)).
6. $\|\hat f_D-f\|_n^2\le\|\hat f_L-f\|_n^2+16f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal B$ (B.15).
7. $\|\hat f_L-f\|_n^2\le\|\hat f_D-f\|_n^2+9f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal A$ (B.17).

Further result: Theorem 5.2

Assume $\|f_j\|_n=1$ for all $j$ and RE$(s,5)$. With probability at least $1-M^{1-A^2/8}$, whenever $\mathcal M(\hat\beta_D)\le s$,

$$\|\hat f_L-f\|_n^2\le10\|\hat f_D-f\|_n^2+81A^2\,\frac{\mathcal M(\hat\beta_D)\sigma^2}{n}\,\frac{\log M}{\kappa^2(s,5)} .$$

Significance

The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate $\mathcal M(\hat\beta_L)\sigma^2\log M/n$ of a sparse regression with $\mathcal M(\hat\beta_L)$ parameters. The bound carries a factor $f^2_{\max}/\kappa^2(s,1)$ that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating $f$ to the dictionary.

Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, $16A^2$ and the thresholds $2\sqrt2$ and $M^{1-A^2/8}$, which appear in all later analyses.

Difficulty

Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives $\pm\tfrac2n\delta^\top X^\top(\boldsymbol f-X\hat\beta)$ plus $\tfrac1n|X\delta|_2^2$ with $\delta=\hat\beta_L-\hat\beta_D$. A crude bound on the cross term, $|\delta|_1\cdot|X^\top(\cdot)|_\infty$, yields an error proportional to $|\delta|_1$. This does not produce the sparse rate unless $|\delta|_1$ is controlled by $|X\delta|_2$. That control needs $\delta$ to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector $\hat\beta_L$. The restricted eigenvalue condition must therefore hold uniformly over supports of size at most $s$; a condition for one fixed support does not suffice. The probabilistic part is a union bound over $M$ Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.

Formalization scope

The dictionary and the design points enter every statement only through $X$ and $\boldsymbol f$, so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and $f$ is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and $y=f+W(\omega)$. The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as $|\tfrac1n\sum_iX_{ij}(y_i-(X\beta)_i)|\le r\|f_j\|_n$. The Lasso penalty and the Dantzig constraint are weighted by $\|f_j\|_n$, and the Dantzig objective $|\beta|_1$ is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.

RE$(s,c_0)$ is stated through a witness: a real $\kappa>0$ with $\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ on the cone, for all $|J_0|\le s$. The paper's $\kappa(s,c_0)$ is attained, so it is the largest witness. Every bound decreases in $\kappa$, so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least $p$" becomes the existence of a measurable event $E$ with $\mathbb P(E)\ge p$ on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition $\mathcal M(\hat\beta_L)\le s$ is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events $\mathcal A$ and $\mathcal B$ as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every $A>0$, which is stronger than the paper's $A>2\sqrt2$ and still true.

The goal cannot be made vacuous. For $A>2\sqrt2$ the probability bound $1-M^{1-A^2/8}$ is positive. Lasso solutions exist because $r>0$ and every $\|f_j\|_n>0$, and Dantzig selectors exist because the Lasso is feasible. RE$(s,1)$ with $\kappa=1$ holds for $X=\sqrt n\,I$.

A complete development needs:

• subgradient optimality for the weighted Lasso;
• a Gaussian tail bound $\mathbb P(|\eta|\ge t)\le e^{-t^2/2}$ together with the law of a weighted sum of independent Gaussians;
• Cauchy–Schwarz on supports;
• the quadratic bound $bx-x^2\le b^2/4$.

The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095 ; doi:10.1214/08-AOS620
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Stat. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008

Motivation

The continuous-review $(Q, r)$ policy — order a fixed quantity $Q$ whenever the inventory position falls to the reorder point $r$ — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).

Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.

Setting

Demands arrive at rate $\lambda>0$ and orders arrive after a fixed leadtime $L>0$. Each order costs $K>0$; holding and backorder costs accrue at rates $h>0$ and $p>0$ per unit per unit time. The leadtime demand $D$ is a nonnegative random variable with $E(D)=\lambda L$. The inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y)=E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$.

For order quantity $Q>0$ and reorder point $r$, the long-run average cost is

$$c(Q,r)=\frac{\lambda K+\int_r^{r+Q}G(y)\,dy}{Q}.$$

Let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and define $H(Q)=G(r(Q))$ for $Q>0$, $H(0)=G(y^0)$, and $C(Q)=c(Q,r(Q))$. The optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^*=C(Q^*)$. Write $H_0(Q)=H(Q)-G(y^0)$ and

$$C_0(Q)=\frac{\lambda K+\int_0^Q H_0(y)\,dy}{Q},$$

the controllable cost, so that $C(Q)=G(y^0)+C_0(Q)$; $C^*_0=C_0(Q^*)$. The constant $G(y^0)$ is the newsboy cost.

The EOQ model is the same construction with demand constant at $\lambda L$: $G_d(y)=h(y-\lambda L)^+ + p(\lambda L-y)^+$, with functions $H_d$, $C_d$, optimal quantity $Q^*_d=\sqrt{2\lambda K(h+p)/(hp)}$ and optimal cost $C^*_d=C_d(Q^*_d)$.

Formalization targets

Goal: Theorem 3 (p. 97)

$$C^*_0\le\frac{Q^*_d}{Q^*}\,C^*_d,\qquad C^*_d\le C^*\le G(y^0)+\frac{Q^*_d}{Q^*}\,C^*_d.$$

All three inequalities are part of the goal. The weaker remark after the proof, $C^*_d\le C^*\le C^*_d+G(y^0)$, drops the factor $Q^*_d/Q^*$ and is not the goal.

Milestones

1. Eq. (7): $C(Q)=\big(\lambda K+\int_0^Q H(y)\,dy\big)/Q$ for $Q>0$.
2. Eq. (8): $Q>0$ is optimal iff $H(Q)=C(Q)$.
3. Eqs. (13)–(15): $C(Q)=G(y^0)+C_0(Q)$, and $H_0(Q^*)=C_0(Q^*)$.
4. Lemma 6: $A(Q)=QH(Q)-\int_0^QH$ is increasing and convex; $Q=Q^*$ iff $A(Q)=\lambda K$; $Q^*$ increases and $r^*$ decreases in $K$.
5. Eqs. (18), (20): $H_d(Q)=\frac{hp}{h+p}Q$, and $Q^*_d$ is the EOQ optimum.
6. Lemma 8: $\int_0^QH\ge\tfrac12QH(Q)\ge A(Q)\ge\tfrac12QH_0(Q)\ge\int_0^QH_0$, with equalities for deterministic demand.
7. Eq. (22): $G_d(y)\le G(y)$ for all $y$.

Significance

Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by $Q^*_d/Q^*$. Combined with $Q^*_d\le Q^*$ (Theorem 2 of the paper), the gap $C^*-C^*_d$ is at most the newsboy cost $G(y^0)$, independent of $K$, so the EOQ cost is a good proxy when $K$ is large relative to $G(y^0)$. The same machinery yields the paper's Theorem 5, that using $Q^*_d$ in the stochastic model costs at most $1/8$ more than the optimum.

The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous $(Q,r)$ model as a whole — optimal reorder points, the one-variable reduction through $H$, and the area function $A$ — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.

Difficulty

The middle inequality compares minima of two different functions: $C_d\le C$ pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of $C$ as a minimum over $r$. The outer inequalities depend on Lemma 8, whose proof uses convexity of $H$ and a slope comparison $H'\le H_d'$ (Lemmas 4 and 7). The paper argues these through first and second derivatives of $r(Q)$ and $G$, which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of $Q^*$ is asserted in the paper without a separate argument.

Formalization scope

Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary $G:\mathbb R\to\mathbb R$ and instantiated at the stochastic $G$ and at $G_d$. A structure QRModel holds the parameters, the demand distribution $\mu$ (a probability measure on $\mathbb R$) and the standing assumptions.

Conventions committed to:

• Positivity of $\lambda,L,K,h,p$; $D\ge0$ almost surely; $D$ integrable with $E(D)=\lambda L$; $G$ has a unique minimizer (p. 90). No density is assumed.
• $r(Q)$ is a chosen minimizer of $c(Q,\cdot)$ over $\mathbb R$, not a solution of $G(r)=G(r+Q)$; $y^0$ is a chosen minimizer of $G$. Both use junk value $0$ when no minimizer exists, which never happens under the assumptions.
• $H(0)=G(y^0)$; statements about $H$ and $A$ are on $[0,\infty)$, about $c$, $C$, $C_0$ for $Q>0$.
• "Optimal order quantity" means $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$; the goal takes any such $Q^*$ and Lemma 6 states that exactly one exists, so the goal is not vacuous.
• $C^*_d$ is $C_d(Q^*_d)$, with $Q^*_d$ the explicit formula (20); milestone 5 proves it is the EOQ optimum. $C^*_0$ is $C_0(Q^*)$, which equals $\min_{Q>0}C_0$ by (13).
• "Increasing" in Lemma 6 is read strictly, as the proof gives. Lemma 8 is stated for $Q\ge0$; "deterministic" means $\mu$ is the Dirac mass at $\lambda L$.

A formalization in which $C^*_d$ were an arbitrary number, or $Q^*$ an arbitrary positive real, would make the goal false or empty; both are tied to the model above.

Needed infrastructure: existence of minimizers of convex coercive functions on $\mathbb R$, differentiation of parametric integrals $\int_{r(Q)}^{r(Q)+Q}G$, and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• P. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

Motivation

Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).

M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.

Timeline:

• 1980s–1990s: Lagrangian (Slater-type) duality for SDP, with strong duality under strict feasibility (see e.g. the surveys of Vandenberghe and Boyd, SIAM Rev. 38 (1996)).
• 1981: Borwein and Wolkowicz, facial reduction for general convex programs, which regularizes a problem by passing to the minimal face containing the feasible set; not of polynomial size in the SDP data (J. Math. Anal. Appl. 83 (1981)).
• 1997: Ramana, the ELSD, an explicit polynomial-size dual with zero gap and dual attainment for every SDP.
• 1997: Ramana, Tunçel and Wolkowicz relate the ELSD to facial reduction (SIAM J. Optim. 7 (1997)).

Setting

Let $n, m$ be natural numbers, $\mathcal M_n$ the space of real $n\times n$ matrices, and $\mathcal S_n\subseteq\mathcal M_n$ the symmetric ones. On $\mathcal M_n$ the inner product is $A\bullet B = \sum_{i,j}A_{ij}B_{ij}$. For symmetric $A$, $A\succeq 0$ means $A$ is positive semidefinite. The data are symmetric $Q_0, Q_1,\dots,Q_m\in\mathcal S_n$ and $c\in\mathbb R^m$. The primal SDP is

$$(\mathrm P)\qquad \sup\ c^{\mathsf T}x\quad\text{s.t.}\quad Q(x) := Q_0-\sum_{i=1}^m x_iQ_i\succeq 0 ,$$

with feasible region $G = \{x\mid Q(x)\succeq 0\}$, a spectrahedron. Define $Q^*:\mathcal M_n\to\mathbb R^m$ by $Q^*(U) = (U\bullet Q_i)_{i=1}^m$ and write $Q^\#(U) = 0$ for "$Q_0\bullet U = 0$ and $Q^*(U) = 0$".

For $k\ge 1$ let $\mathcal C_k$ be the set of tuples $(U_i, W_i)_{i=1}^k$ of real $n\times n$ matrices with $W_0 = 0$ and, for $i = 1,\dots,k$,

$$Q^\#(U_i+W_{i-1}) = 0,\qquad U_i\succeq W_iW_i^{\mathsf T}.$$

The $W_i$ need not be symmetric. $\mathcal U_k$ and $\mathcal W_k$ are the sets of last components $U_k$ and $W_k$; $\mathcal W_0 = \{0\}$. The ELSD is

$$\inf\ (U+W)\bullet Q_0\quad\text{s.t.}\quad Q^*(U+W) = c,\quad W\in\mathcal W_m,\quad U\succeq 0,$$

and Weak-ELSD is the same program with $\mathcal W_{m-1}$. For the milestones: the polar $G^\circ = \{y\mid x^{\mathsf T}y\le 1\ \forall x\in G\}$, the algebraic polar $G^* = \{Q^*(U)\mid U\bullet Q_0\le 1,\ U\succeq 0\}$, and $S_k = Q^*(\mathcal W_k)$.

Formalization targets

Goal: Theorem 6 (Duality Theorem)

For all data $(Q_0,\dots,Q_m,c)$:

1. weak duality: $c^{\mathsf T}x\le (U+W)\bullet Q_0$ for $x\in G$ and $(U,W)$ feasible for ELSD or Weak-ELSD;
2. if $G\neq\emptyset$, then $\sup_{x\in G}c^{\mathsf T}x<\infty$ iff ELSD is feasible, iff Weak-ELSD is feasible;
3. if $G\ne\emptyset$ and ELSD (or Weak-ELSD) is feasible, there is $v\in\mathbb R$ with

$$v = \sup_{x\in G}c^{\mathsf T}x = \inf_{\mathrm{ELSD}}(U+W)\bullet Q_0 = \inf_{\mathrm{Weak\text{-}ELSD}}(U+W)\bullet Q_0;$$

4. if $G\ne\emptyset$ and the primal is bounded, ELSD attains $v$.

Milestones

Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation $Q(x)U = Q(x)W = 0$), weak duality over every $\mathcal W_k$, Lemma 10 (nested subspaces), Lemma 13 ($G^\circ = \mathrm{Cl}(G^*)$), Corollary 14, Claims 17 and 16, the central Theorem 12,

$$G^\circ = \{Q^*(U+W)\mid W\in\mathcal W_k,\ U\succeq 0,\ U\bullet Q_0\le 1\}\qquad(0\in G,\ k\ge m-1),$$

the translation invariance of $\mathcal C_k,\mathcal U_k,\mathcal W_k$ (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.

Significance

The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.

The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, $A\bullet B = 0\Rightarrow AB = 0$) and on polars of convex sets.

Difficulty

The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar $G^*$ (Lemma 13 only gives $G^\circ = \mathrm{Cl}(G^*)$). The difficulty is to show that finitely many, and at most $m-1$, corrections by the sets $S_k$ close $G^*+S_k$ (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.

Formalization scope

Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "$\succeq 0$" is Mathlib's PosSemidef (which over ℝ includes symmetry); $A\bullet B$ is the entrywise sum on all of $\mathcal M_n$; $c^{\mathsf T}x$ is the dot product. The data $Q_0,\dots,Q_m$ carry symmetry hypotheses in every statement, as the paper assumes throughout. $\mathcal C_k$ is encoded by sequences $U, W:\mathbb N\to\mathcal M_n$ with $U_0 = W_0 = 0$, so $\mathcal U_0 = \mathcal W_0 = \{0\}$; for $m = 0$ the index $m-1$ is $0$. Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption $0\in G$ is a hypothesis. In Claim 16 the index satisfies $k+1\le m$, the range where $S_{k+1}$ is introduced, and $\dim S_k$ is the rank of the span of $S_k$.

Theorems 20 and 21 are printed with $Q^*(U+W) = 0$; both are false as printed (counterexamples in the items) and are stated with the corrected $Q^*(U+W) = c$ that the paper's derivation from Theorem 6 gives.

Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined $\mathcal W_m$, not the Lagrangian dual or an arbitrary subspace; the $W_i$ range over all of $\mathcal M_n$, not only symmetric matrices (the paper's Example 4 needs a nonsymmetric $W_2$).

Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of $\mathbb R^m$. Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.

Selected references

• M. V. Ramana, An exact duality theory for semidefinite programming and its complexity implications, Mathematical Programming 77 (1997) 129–162. https://doi.org/10.1007/BF02614433
• M. V. Ramana, L. Tunçel, H. Wolkowicz, Strong duality for semidefinite programming, SIAM Journal on Optimization 7 (1997) 641–662. https://doi.org/10.1137/S1052623495288350
• J. M. Borwein, H. Wolkowicz, Regularizing the abstract convex program, Journal of Mathematical Analysis and Applications 83 (1981) 495–530. https://doi.org/10.1016/0022-247X(81)90138-4
• L. Vandenberghe, S. Boyd, Semidefinite programming, SIAM Review 38 (1996) 49–95. https://doi.org/10.1137/1038003
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173