All missions

Motivation

Firms that sell durable goods compete on price, on product quality and on the services bundled with the product: a factory warranty, free maintenance, technical support. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of all three when consumers choose among the firm's products according to a multinomial logit (MNL) model. Their first result (Theorem 1, the subject of mission I of this series) is that when each product may receive its own service duration, every optimal duration is the shortest or the longest allowed.

In practice many firms do not differentiate service across products: every Apple product, for example, comes with the same one-year factory warranty. The paper's Section 3 therefore studies a benchmark in which one uniform service duration is attached to all products, and compares it with differentiated service to measure the value of service differentiation. Theorem 3, the goal of this mission, says that the extreme-duration structure survives the uniformity constraint.

The pricing side builds on a line of work on multi-product pricing under logit demand. Hanson and Martin (1996) showed that the MNL profit is not jointly concave in prices; Li and Huh (2011) and Gallego and Wang (2014) showed that, nevertheless, optimal markups (price minus cost) are equal across the products of a firm under the MNL and nested logit models.

Setting

A firm sells $N$ products, $\mathcal N=\{1,\dots,N\}$. For product $i$:

• $\alpha_i$ is the consumers' sensitivity to quality, $s_i$ the utility of service per unit time;
• $c_iq_i^2$ is the unit production cost at quality $q_i$, with $c_i>0$;
• $a_i-b_iq_i$ is the expected service cost per unit time, with base cost $a_i$ and a marginal effect $b_i$ of quality on service cost that may be positive, negative or zero.

The firm chooses prices $\mathbf p$, qualities $\mathbf q$ and service durations $\mathbf t$. Under the MNL choice model (2) a consumer buys product $i$ with probability

$$d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\frac{\exp(\alpha_iq_i-p_i+t_is_i)}{1+\sum_{j\in\mathcal N}\exp(\alpha_jq_j-p_j+t_js_j)},$$

the $1$ being the no-purchase option. With unit market size, the total expected profit (3) is

$$\Pi(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\sum_{i\in\mathcal N}\big[p_i-c_iq_i^2-t_i(a_i-b_iq_i)\big]\,d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N).$$

Service durations lie in an interval $[t_s,t_l]$, the shortest and longest durations the firm may offer.

The uniform-duration problem (7) adds the constraint $t_i=t$ for all $i$:

$$\max_{\mathbf p,\mathbf q,\;t\in[t_s,t_l]}\ \Pi\big(\mathbf p,\mathbf q,(t,\dots,t);\mathcal N\big).$$

Formalization targets

Goal: Theorem 3 (p. 15)

$$\exists\,t^*\in\{t_s,t_l\},\ \exists\,\mathbf p^*,\mathbf q^*:\quad \Pi\big(\mathbf p,\mathbf q,(t,\dots,t)\big)\le\Pi\big(\mathbf p^*,\mathbf q^*,(t^*,\dots,t^*)\big) \quad\forall\,t\in[t_s,t_l],\ \mathbf p,\mathbf q\in\mathbb R^N .$$

Problem (7) has an optimal solution whose uniform duration is an endpoint. The goal says nothing about the optimal prices, qualities or profit value; those belong to the milestones.

Milestones (the paper's proof, pp. 29–30)

1. (24). At a fixed uniform duration $t$, the root $r(t)$ of

$$r=\sum_{i\in\mathcal N}\exp\Big(\frac{b_i^2t^2}{4c_i}+\Big(s_i-a_i+\frac{\alpha_ib_i}{2c_i}\Big)t+\frac{\alpha_i^2}{4c_i}-r-1\Big)$$

is unique, and it is the optimal profit over prices and qualities, attained at $q_i=(\alpha_i+tb_i)/(2c_i)$, $p_i=1+r+c_iq_i^2+t(a_i-b_iq_i)$. 2. $\partial r/\partial t$. $r(t)$ is differentiable with $r'(t)=\sum_iA_iG_i/(1+\sum_iG_i)$. 3. The numerator. $\sum_iA_iG_i$ has nonnegative derivative. 4. Quasi-convexity. $r(t)$ is quasi-convex in $t$. 5. (25). The root equation is equivalent to $r=y(t)/\exp(1+r)$ with $y(t)=\sum_i\exp(\cdot)$, so $r(t)$ increases with $y(t)$. 6. Convexity of $y$. $y$ is convex in $t$.

Milestones 2–4 and 5–6 are the paper's two routes from (24) to Theorem 3. A further item states the universal reading of Theorem 3 (every optimal uniform duration is $t_s$ or $t_l$) under $t_s<t_l$ and the non-degeneracy assumption that some product has $b_i\ne0$ or $a_i\ne s_i$.

Significance

Theorem 3 is the basis of the paper's Section 3. It shows that a firm restricted to one service policy should still go to an extreme, and it makes the uniform benchmark a comparison of two candidate durations. Comparing that benchmark with Theorem 1's differentiated optimum measures the value of service differentiation, which the paper reports numerically. Equation (24) also gives the optimal profit at every uniform duration as the root of a scalar equation, which is the form any sensitivity analysis in $t$ starts from.

On the formal side, the paper's results are proved on paper but, as far as is known, none is machine-checked. The mission requires formalizing the reduction of the joint MNL price–quality problem to a scalar fixed point (the equal-markup property of Li and Huh, extended to quality), an implicit-function derivative and a Cauchy–Schwarz step, or alternatively a convexity argument. The equal-markup reduction is shared with missions I and VI of this series.

Difficulty

The obvious argument fails at the first step: the MNL profit is not jointly concave in the price vector (Hanson and Martin 1996), let alone in prices, qualities and the duration together, so "maximize a concave function and check the endpoints" does not apply. The extreme-point structure holds only after prices and qualities have been optimized out, and that requires knowing the optimal profit at each $t$ exactly: as the root of (24), a fixed-point equation in which $r$ appears on both sides. The global optimality in (24) is itself the hard part, since a first-order condition alone does not give a global maximum of a non-concave function on $\mathbb R^{2N}$.

Formalization scope

Conventions committed to in Lean:

• Products are Fin N, 0-based; $N=0$ is allowed. The outside option is the constant $1$ in the MNL denominator, not a product.
• Parameters $\alpha,a,b,c,s:\texttt{Fin N}\to\mathbb R$, with only $c_i>0$ assumed; no sign on $b_i$, and $b_i=0$ is allowed.
• Prices and qualities range over all of $\mathbb R^N$. The model's normalization $q_i\in[0,a_i/b_i)$ (p. 8) is not imposed, matching the paper's derivation of $q_i=(\alpha_i+tb_i)/(2c_i)$ by a first-order condition.
• A uniform duration is the constant vector fun _ => t; the goal assumes $t_s\le t_l$.
• "Optimal" means a global maximizer; existence of an optimum is part of the goal's conclusion.
• The goal is the existential reading of Theorem 3. The universal reading is false in the degenerate case $b_i=0$, $a_i=s_i$ for all $i$, where the optimal profit does not depend on $t$, and is stated separately with that case excluded.
• The root $r(t)$ is not a definition: milestones quantify over any function $R$ with $R(t)=\sum_iG_i(R(t),t)$ for every $t$, which (24) shows is unique.

These formalizations would trivialize the goal and are ruled out: a single product (then Theorem 3 is Theorem 1(a)); qualities fixed rather than chosen; a duration vector $t\in[t_s,t_l]^N$ instead of one shared $t$; and an existential statement in which $t^*$ may be any point of $[t_s,t_l]$.

The definitions needed are the MNL choice probability and profit, plus the scalar functions $G_i$, $A_i$ and $y$ of the proof. Mathlib's QuasiconvexOn, ConvexOn, HasDerivAt and Finset.sum_mul_sq_le_sq_mul_sq cover the rest. A proof of (24), the global optimality of equal markups and per-product quality under MNL, would be reusable across the whole series. Contributions to any milestone are welcome.

Selected references

• R. Wang, C. Ke, S. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022; accepted manuscript SSRN 3766191. https://ssrn.com/abstract=3766191, https://doi.org/10.1287/msom.2020.0947
• H. Li, W. T. Huh, Pricing multiple products with the multinomial logit and nested logit models: concavity and implications, Manufacturing & Service Operations Management 13(4) 549–564, 2011. https://doi.org/10.1287/msom.1110.0344
• G. Gallego, R. Wang, Price optimization and competition for multi-products under the nested logit model with product-differentiated price coefficients, Operations Research 62(2) 450–461, 2014. https://doi.org/10.1287/opre.2013.1249
• W. Hanson, K. Martin, Optimizing multinomial logit profit functions, Management Science 42(7) 992–1003, 1996. https://doi.org/10.1287/mnsc.42.7.992
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, Academic Press, 1974. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf

Motivation

Dynamic pricing asks a seller to post prices to a stream of customers and learn demand from purchase decisions alone. Luo, Sun and Liu study the contextual version in which a customer's valuation is linear in a covariate vector plus noise with an unknown distribution (arXiv:2109.07340v2; Mathematics of Operations Research, 2024). Their DIP policy estimates the linear part, discretizes the remaining price residual, and then runs an upper-confidence-bound rule on the discretized problem. Because the linear part is only estimated, the discretized problem is not an ordinary linear bandit: its reward parameter drifts from period to period by an amount controlled by the estimation error. The paper calls this a perturbed linear bandit (PLB) and proves an upper bound for it whose dominant extra term is linear in the perturbation size times the horizon.

This mission formalizes the matching statement: no algorithm can avoid that linear term. It is the paper's Proposition 2 (p. 22), proved in its Appendix A (pp. 44–46).

Setting

Fix a dimension $d$. A perturbed linear bandit with perturbation constant $C_p$ consists of parameters $\xi_1,\xi_2,\ldots\in\mathbb R^d$, finite action sets $\mathcal A_1,\mathcal A_2,\ldots\subset\mathbb R^d$ and noise variables $\eta_1,\eta_2,\ldots$, with $\|\xi_s-\xi_t\|_\infty\le C_p$ for all periods $s,t$. In period $t$ an algorithm $\mathcal A^*$ sees the action set $\mathcal A_t$ and the history of its past actions and rewards, plays $A_t\in\mathcal A_t$, and observes the reward

$$Z_t=\langle\xi_t,A_t\rangle+\eta_t .$$

The algorithm may randomize. The parameters $\xi_t$ are never observed.

For a central parameter $\tilde\xi\in\mathbb R^d$ the paper defines the parameter set

$$PB(\tilde\xi,C_p)=\{\xi\in\mathbb R^d:\ \|\xi-\tilde\xi\|_\infty\le C_p/2\},$$

so any sequence in $PB(\tilde\xi,C_p)$ has perturbation at most $C_p$.

The PLB regret over $T_0$ periods compares each action with the best action of the current period:

$$R^{PLB}_{T_0}(\mathcal A^*)=\sum_{t=1}^{T_0}\Big(\max_{a\in\mathcal A_t}\langle\xi_t,a\rangle-\langle\xi_t,A_t\rangle\Big)\ \ge 0 .$$

The expectation $\mathbb E$ is over the algorithm's randomness and the noise.

Formalization targets

Goal: Proposition 2 (p. 22)

For every $\tilde\xi$ with positive entries (and $d\ge2$) there is $C_0>0$ depending only on $\tilde\xi$ such that for every $C_p\ge0$ with $C_p/2<\min_i\tilde\xi_i$ and every algorithm $\mathcal A^*$ there are parameters $\xi_t\in PB(\tilde\xi,C_p)$ and action sets $\mathcal A_t$ with

$$\mathbb E\big(R^{PLB}_{T_0}(\mathcal A^*)\big)\ \ge\ C_0\,C_p\,T_0\qquad\text{for all }T_0\ge1 .$$

The formal statement also records that the constructed instance is a PLB with perturbation $C_p$, that its action sets are nonempty, and that every action has a single nonzero entry with $|\langle\xi_t,a\rangle|\le1$, which places the hard instance inside the class covered by the paper's upper bound (Lemma 3, Conditions 1 and 3).

Milestones

1. Two-point construction (proof of Proposition 2, p. 44). With $C=C_p/2$, two coordinates $j_u\ne j_v$, $u=\tilde\xi_{j_u}$, $v=\tilde\xi_{j_v}$, actions $U=e_{j_u}/(u+C)$, $V=e_{j_v}/(v+C)$ and parameters $\xi_u,\xi_v$ obtained from $\tilde\xi$ by moving the two coordinates by $\mp C$, $\pm C$:

$$\xi_u,\xi_v\in PB(\tilde\xi,C_p),\qquad\langle\xi_u,U\rangle=\tfrac{u-C}{u+C}\le1=\langle\xi_v,U\rangle,\qquad\langle\xi_v,V\rangle=\tfrac{v-C}{v+C}\le1=\langle\xi_u,V\rangle .$$

2. Per-period bound (pp. 45–46). If $u\le v$, $A$ is a random action in $\{U,V\}$, and $\xi_t=\xi_u$ when $P(A=U)\ge1/2$ and $\xi_t=\xi_v$ otherwise, then

$$\mathbb E(r_t)\ \ge\ C_0C_p,\qquad C_0=\frac1{4v}.$$

Significance

The result. Lemma 3 of the paper bounds the regret of its M-LinUCB algorithm on a PLB by a $\sqrt{T_0}$-type term plus $2a_{\max}C_pT_0$. Proposition 2 shows that the second term is not an artefact of the analysis: an adversary who may move the parameter inside a box of width $C_p$ forces every algorithm to pay order $C_pT_0$. In the pricing application the perturbation is proportional to the estimation error $\|\hat\theta-\theta_0\|_1$ of the linear part, so the lower bound explains why the paper's pricing regret bound (Theorem 1) carries a term linear in the accumulated estimation error. The result also separates the PLB from the zero-perturbation linear bandit, where $\tilde O(\sqrt{T_0})$ regret is achievable.

Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof requires an explicit model of randomized, history-dependent algorithms interacting with an adversarially chosen but deterministic parameter sequence, which the mission supplies. The model and the two-point construction are reusable for other two-hypothesis lower bounds in linear and contextual bandits.

Difficulty

The obvious argument fixes one hard instance and shows that every algorithm suffers on it. That fails: for a fixed parameter sequence, an algorithm that always plays the optimal action of that sequence has zero regret. The instance must therefore be chosen after the algorithm, and it must be chosen period by period, because the law of the period-$t$ action depends on the rewards of periods $1,\dots,t-1$, which depend on the parameters already chosen. The parameters must nevertheless be deterministic: the adversary may react to the law of the algorithm's action, not to its realization. Making this recursive construction precise, together with the measurability needed for "the probability that $A_t=U$" to be meaningful, is the main formal work. The arithmetic of each period is elementary.

A second point concerns the dimension: the construction needs two distinct coordinates, and for $d=1$ the statement fails, since every parameter in $PB(\tilde\xi,C_p)$ is then positive and playing the largest action has zero regret.

Formalization scope

• Model. Arms are coordinates Fin d (0-based); periods are 1-based. Vectors are Fin d → ℝ, and $\|\cdot\|_\infty$ is Mathlib's sup norm on that type. Action sets are finite sets (Finset). The maximum over an empty action set is set to $0$; every statement requires nonempty action sets.
• Algorithms. An algorithm is a decision rule that maps a sample point $\omega$ of a probability space (its internal randomness), the past actions and rewards, and the current action set to an action of that set; it is jointly measurable in $\omega$ and the history. The trajectory $(A_t,Z_t)$ is defined recursively from the rule, the parameters, the action sets and the noise. Since the rule sees all of $\omega$, it may also depend on the noise; this only enlarges the class over which the lower bound holds.
• Noise. The goal quantifies over every measurable noise process. The paper's PLB asks for conditionally sub-Gaussian noise; since $\eta\equiv0$ is allowed, the formal statement is stronger than the printed existence statement, and the paper's proof uses no property of the noise.
• Instance. The parameters and action sets are deterministic and are chosen after the algorithm, the probability space and the noise. The constant $C_0$ is chosen after $\tilde\xi$ and before $C_p$, the algorithm and $T_0$, which is the formal content of "only dependent on $\tilde\xi$".
• Added hypotheses. $d\ge2$ (necessary, see above) and $C_p\ge0$ (otherwise $PB(\tilde\xi,C_p)$ is empty).
• Expectation. Expected regret is the lower Lebesgue integral of the nonnegative regret, so no integrability convention can make the bound hold vacuously. The bound is positive whenever $C_p>0$; a formalization in which the expectation could collapse to a default value, or the algorithm class could be empty, is ruled out (the class contains every fixed-choice rule).
• Source. The source is the arXiv v2 preprint (6 March 2023); the paper's proofs are in its Appendix A.

Contributions welcome: proofs of the two milestones, the measurability of the recursively defined actions, and the summation step from the per-period bound to the goal.

Selected references

• Y. Luo, W. W. Sun, Y. Liu, Distribution-Free Contextual Dynamic Pricing, Mathematics of Operations Research, 2024. Preprint arXiv:2109.07340v2; DOI 10.1287/moor.2023.1369.
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS, 2011. link
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

Motivation

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

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

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

Setting

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

$$\mathrm{Opt} = \inf_{x\in\mathbb{R}^N} \bigl\{ q_0(x) : q_i(x) \le 0,\ i \in [\![m_I]\!];\ q_i(x) = 0,\ i \in [\![m_I+1,m]\!] \bigr\}.$$

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

$$\mathrm{Opt}_{\mathrm{SDP}} = \inf_{x, X} \bigl\{ \langle Q_0, Y\rangle : \langle Q_i, Y\rangle \le 0,\ i \in [\![m_I]\!];\ \langle Q_i, Y\rangle = 0,\ i \in [\![m_I+1,m]\!];\ Y \succeq 0 \bigr\}.$$

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

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

$$\mathrm{Opt}_{\mathrm{SOCP}} = \inf_{x, y\in\mathbb{R}^N} \bigl\{ \langle a_0,y\rangle + 2\langle b_0,x\rangle + c_0 : \langle a_i,y\rangle + 2\langle b_i,x\rangle + c_i \le 0 \text{ or } = 0;\ y_j \ge x_j^2\ \forall j \bigr\},$$

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

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

Formalization targets

Goal: Proposition 1 (p. 21)

For a diagonal QCQP (10),

$$\mathcal{D}_{\mathrm{SOCP}} = \mathcal{D}_{\mathrm{SDP}} \qquad\text{and}\qquad \mathrm{Opt}_{\mathrm{SOCP}} = \mathrm{Opt}_{\mathrm{SDP}}.$$

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

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

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

Companion: Lemma 9 (p. 19)

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Why SDP exactness for QCQPs matters

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as max-cut, Boolean least squares, the trust-region subproblem and its generalizations, and robust least squares, and it is NP-hard in general. The standard convex approach is the Shor semidefinite relaxation: lift $x$ to the matrix $Y=\begin{pmatrix}1&x^\top\\x&X\end{pmatrix}\succeq 0$ and linearize. The relaxation always gives a lower bound $\mathrm{Opt}_{\mathrm{SDP}}\le\mathrm{Opt}$. When the bound is exact, the nonconvex problem is solved by one semidefinite program, and an optimizer of the QCQP can be read off the SDP solution.

Earlier exactness results cover special structure: problems with a single constraint (the S-lemma), diagonal QCQPs under sign conditions (Burer–Ye 2019), and the extended trust-region problem under a perturbation condition (Locatelli 2016). A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195, Math. Program. 2021) give a single framework that produces sufficient conditions for both exactness ($\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$) and the stronger convex-hull property ($\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}$). Both kinds of condition are stated through the faces of a dual object $\Gamma$. This mission formalizes the exactness result for polyhedral $\Gamma$, Theorem 3 of §5.

Setting

Fix $N\ge 0$ variables and $m\ge 1$ constraints, of which the first $m_I$ are inequalities and the remaining $m_E=m-m_I$ equalities. For $i=0,\dots,m$ let $q_i(x)=x^\top A_ix+2b_i^\top x+c_i$ with $A_i$ symmetric. The QCQP is

$$\mathrm{Opt}=\inf_{x\in\mathbb R^N}\{q_0(x) : q_i(x)\le 0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\},$$

and its epigraph is $\mathcal D=\{(x,t) : q_0(x)\le 2t,\ x\text{ feasible}\}$. With $Q_i=\begin{pmatrix}c_i&b_i^\top\\b_i&A_i\end{pmatrix}$, the SDP relaxation minimizes $\langle Q_0,Y\rangle$ over $Y=\begin{pmatrix}1&x^\top\\x&X\end{pmatrix}\succeq0$ with $\langle Q_i,Y\rangle\le 0$ or $=0$. Its value is $\mathrm{Opt}_{\mathrm{SDP}}$, and its projected epigraph $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some $X$ is feasible with $\langle Q_0,Y\rangle\le 2t$.

For multipliers $\gamma\in\mathbb R^m$ put $A(\gamma)=A_0+\sum_i\gamma_iA_i$, $b(\gamma)=b_0+\sum_i\gamma_ib_i$, and the Lagrangian $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual object is

$$\Gamma=\{\gamma\in\mathbb R^m : A(\gamma)\succeq 0,\ \gamma_i\ge 0\ (i\le m_I)\}.$$

A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$, and semidefinite otherwise. A semidefinite face has the shared zero eigenspace $\mathcal V(\mathcal F)=\{v : A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$.

The standing hypotheses are Assumption 1 (the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$) and Assumption 3 ($\Gamma$ is polyhedral). $\mathrm{Proj}_V$ denotes the orthogonal projection onto a subspace $V$.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumptions 1 and 3, suppose that every semidefinite face $\mathcal F$ of $\Gamma$ satisfies

$$0\notin\mathrm{Proj}_{\mathcal V(\mathcal F)}\{b(\gamma):\gamma\in\mathcal F\}.$$

Then every $(x^*,t^*)\in\arg\min_{(x,t)\in\mathcal D_{\mathrm{SDP}}}2t$ lies in $\mathcal D$, and in particular

$$\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Lemma 2 (p. 9): a semidefinite face has a unit vector in $\mathcal V(\mathcal F)$.
3. Lemma 3 (p. 9): under Assumptions 1 and 2, a point of $\mathcal D_{\mathrm{SDP}}$ whose face $\mathcal F(\hat x)$ is definite lies in $\mathcal D$.
4. Lemma 8 (p. 13): for polyhedral $\Gamma$, $\Gamma=\Gamma_e+\mathrm{cone}(\Gamma_r)$ with polytopes $\Gamma_e,\Gamma_r$, and $\mathcal F(\hat x)=\mathcal F_e(\hat x)+\mathrm{cone}(\mathcal F_r(\hat x))$.
5. Separation step of the proof of Theorem 3 (p. 24): on a semidefinite face satisfying the hypothesis, some nonzero $v\in\mathcal V(\mathcal F)$ and $\epsilon>0$ have $v^\top b(\gamma)\le-\epsilon$ for all $\gamma\in\mathcal F$.

Companion: Theorem 4 (p. 25)

If a sequence $h_j\to0$ in $\mathbb R^N$ has $0\notin\mathrm{Proj}_{\mathcal V(\mathcal F)}\{b(\gamma)+h_j:\gamma\in\mathcal F\}$ for every semidefinite face and every $j$, then $\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$.

Significance

Theorem 3 gives exactness without the convex-hull property, and the paper uses it to recover known exactness results: Proposition 5 (p. 28) shows that the hypotheses of the Burer–Ye theorem for diagonal QCQPs imply those of Theorem 3, and Proposition 4 (p. 27) shows that Locatelli's hypotheses for the extended trust-region problem imply those of Theorem 4. The conclusion is also algorithmic: the $x$-block of any optimal lifted matrix of the SDP is optimal for the QCQP, so no rounding is needed. Theorem 4 extends exactness to limits of problems satisfying the condition; Example 4 is a problem where the SDP is exact but $\mathrm{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$.

The results are proved in the paper; none of them has a machine-checked proof. A formalization adds a checked version of the Lagrangian description of the Shor relaxation (Lemma 1), which every SDP-exactness argument for QCQPs uses, and a reusable Minkowski–Weyl decomposition of the faces of a polyhedral dual set (Lemma 8).

Difficulty

The natural attempt is to show directly that an SDP optimizer $(x^*,t^*)$ is feasible for the QCQP. This works when the face $\mathcal F(x^*)$ is definite (Lemma 3), but nothing in the SDP forces that. When the face is semidefinite, the multipliers on it give no curvature in the directions of $\mathcal V(\mathcal F)$. The difficulty is to rule out a semidefinite optimal face using only first-order information about $b(\gamma)$ on that face. The argument must also control every multiplier off the face uniformly, which is where polyhedrality enters, through the finitely many extreme points and rays of Lemma 8. The paper's argument for Theorem 3 uses polyhedrality at exactly this point.

Lemma 1 itself needs conic duality with attainment: strict feasibility of the dual SDP from Assumption 1, and a minimax step to identify the value.

Formalization scope

• A QCQP is a structure QCQP N m with symmetric A₀, A i, vectors b₀, b i, scalars c₀, c i, and mI ≤ m. Constraint i : Fin m is the paper's constraint $i+1$ and is an inequality iff i < mI. The paper's standing assumption $m\ge1$ (p. 1) is a hypothesis of the goal and of Theorem 4.
• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, so infeasibility and unboundedness are representable and no default value enters. "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t$" is written as a bound for every $\gamma\in\Gamma$.
• Faces are nonempty convex extreme subsets of $\Gamma$. The empty face plays no role in the paper.
• The projection is the orthogonal projection in EuclideanSpace ℝ (Fin N), because Fin N → ℝ carries the sup norm.
• "Any optimizer of $2t$ over $\mathcal D_{\mathrm{SDP}}$" is a point of $\mathcal D_{\mathrm{SDP}}$ with $2t^*\le 2t$ for all points of $\mathcal D_{\mathrm{SDP}}$. Existence of an optimizer is not assumed, and $\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$ is stated as a separate conclusion.
• Lemma 8 formalizes $\mathcal F_r(\hat x)$ as a subset of $\Gamma_r$. The page prints $\Gamma_e$, a slip that the proof and its uses correct.
• The goal assumes neither that $\mathcal F(x^*)$ is definite nor any separating vector. Those are milestones, so the goal cannot be closed by restating a hypothesis.

A complete development needs conic (SDP) strong duality with attainment, a Minkowski–Weyl theorem for polyhedra in $\mathbb R^m$, faces of convex sets, strict separation of a point from a closed convex set, and closedness of linear images of polyhedra. All of these are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the optional comparisons with Burer–Ye and Locatelli (Propositions 4, 5) are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming (2021); arXiv:1911.09195v3 (2020). https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4) (1997) 367–380.
• S. Burer, Y. Ye, Exact semidefinite formulations for a class of (random and non-random) nonconvex quadratic programs, Mathematical Programming 181 (2019) 1–17.
• M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6) (2016) 1141–1151.