All missions

Motivation

Firms that sell durable goods set three things at once: a price, a quality level, and the length of an ancillary service that comes free with the product, such as a warranty. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study these joint decisions under multinomial logit (MNL) demand. For a monopolist offering several products they show (their Theorem 1) that each service duration is extreme (the shortest or the longest allowed), each quality is set product by product, and all markups are equal.

A natural question is whether that structure survives competition. In practice, quality and warranty terms are long-term strategic choices while prices react to rivals; if competition changed the optimal qualities and durations, the monopoly analysis would say little about real markets. Section 2.4 of the paper answers the question for an oligopoly of $N$ single-product firms. This mission formalizes that answer, Theorem 2.

Setting

There are $N$ firms; firm $i \in \mathcal N = \{1, \dots, N\}$ sells product $i$. Product $i$ has a quality sensitivity $\alpha_i$, a base service cost per unit time $a_i$, a marginal effect $b_i$ of quality on service cost (of either sign, or zero), a production-cost coefficient $c_i > 0$ (cost $c_i q_i^2$), and a service utility per unit time $s_i$. Firm $i$ chooses a price $p_i$, a quality $q_i$ and a service duration $t_i \in [t_s, t_l]$.

A consumer buys product $i$ with the MNL choice probability

$$d_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N) = \frac{\exp(\alpha_i q_i - p_i + t_i s_i)}{1 + \sum_{j \in \mathcal N} \exp(\alpha_j q_j - p_j + t_j s_j)},$$

where the $1$ is the outside (no-purchase) option. The payoff of firm $i$ is its markup times its market share:

$$\Pi_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N) = \big[p_i - c_i q_i^2 - t_i(a_i - b_i q_i)\big]\, d_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N).$$

A Nash equilibrium is a profile $(\mathbf p, \mathbf q, \mathbf t)$ with every $t_i \in [t_s, t_l]$ such that no firm can raise $\Pi_i$ by changing its own triple $(p_i, q_i, t_i)$, jointly, to any other triple with duration in $[t_s, t_l]$. The monopolistic case is problem (4): one firm maximizes $\sum_i \Pi_i$ over all prices and qualities in $\mathbb R^N$ and durations in $[t_s, t_l]^N$. Finally, the duration index of product $i$ is

$$\varphi_i(t) = \frac{b_i^2 t^2}{4 c_i} + \Big(s_i - a_i + \frac{\alpha_i b_i}{2 c_i}\Big) t .$$

Formalization targets

Goal: Theorem 2

Assume $c_i > 0$ for all $i$, $t_s < t_l$, and $\varphi_i(t_s) \ne \varphi_i(t_l)$ for all $i$. Then

$$\exists!\, (\mathbf p^o, \mathbf q^o, \mathbf t^o) \text{ Nash equilibrium}, \qquad \mathbf t^o = \mathbf t^*,\quad \mathbf q^o = \mathbf q^*,\quad p_i^o \le p_i^* \ (i \in \mathcal N)$$

for every optimal solution $(\mathbf p^*, \mathbf q^*, \mathbf t^*)$ of the monopolist's problem, which exists. The goal compares with any monopoly optimum and does not presuppose the monopoly formulas of Theorem 1.

Milestones

The proof in the Online Supplement (pp. 2–3) passes through the following statements, which are the mission's milestones:

1. (EC.1): a firm's profit is the unique root $r_i$ of $r_i(1 + \sum_{j \ne i} e^{\cdot}) = [\text{markup}_i - r_i]\, e^{\alpha_i q_i - p_i + t_i s_i}$;
2. (EC.2): $p_i \mapsto [\text{markup}_i - r_i]\, e^{\alpha_i q_i - p_i + t_i s_i}$ is unimodal with peak at markup $r_i + 1$;
3. (EC.3): in every equilibrium $q_i = (\alpha_i + t_i b_i)/(2c_i)$ and $t_i$ maximizes $\varphi_i$ on $[t_s, t_l]$;
4. the price root $\varphi_i(A)$ of the first-order condition exists, is unique, and decreases in the aggregate $A$;
5. the aggregate equation has a unique root $A^o$, and the price competition has the unique equilibrium $p_i^o = \varphi_i(A^o)$;
6. $\varphi_i(A) \le A + k_i$ when $A$ exceeds firm $i$'s attraction by at least one;
7. $A^o \ge m^*$, the root of $m = 1 + \sum_i \exp(\alpha_i q_i - c_i q_i^2 - t_i(a_i - b_i q_i - s_i) - m)$;
8. $p_i^o = \varphi_i(A^o) \le m^* + c_i q_i^2 + t_i(a_i - b_i q_i)$.

Significance

The result. Theorem 2 says that the quality and service rules of the monopoly are robust to competition: each firm sets quality where marginal consumer utility equals marginal cost, and offers the shortest or the longest service, regardless of what its rivals do. Only prices respond to competition, and they fall. The proof also shows that the competitive aggregate $A^o$ exceeds the monopolist's, so more consumers buy and consumer surplus $\log A^o$ is higher than under monopoly. Uniqueness makes comparative statics well defined.

Formalizing it. The theorem is proved in the paper and, to our knowledge, not formalized anywhere. A formal proof requires the MNL price-competition equilibrium argument (existence and uniqueness through a one-dimensional aggregate), which is a standard tool in operations management and industrial organization (Anderson, de Palma and Thisse 1992) and has independent reuse value. Making the argument precise also exposes two points the paper leaves implicit: the tie case in the duration choice, and the domain on which the bound $\varphi_i(A) \le A + k_i$ holds.

Difficulty

The game is not concave: $\Pi_i$ is not concave in firm $i$'s own strategy $(p_i, q_i, t_i)$ (its best attainable value is convex in the duration $t_i$, which is why durations end up extreme), and strategies are unbounded in price and quality, so the standard existence theorems for concave games with compact strategy sets do not apply. Writing down the first-order conditions and solving them produces candidates, but it shows neither that a candidate is a global best response nor that no other equilibrium exists. Uniqueness also fails without the no-indifference condition (see below).

Formalization scope

• Products are indexed by Fin N (0-based); $N$ is arbitrary. The outside option is the 1 + in the denominator, not an element of Fin N.
• Prices and qualities are unconstrained reals. The paper's normalization $q_i \in [0, a_i/b_i)$ (p. 8) is not imposed, because Theorem 1's quality formula and the proof ignore it. Durations lie in $[t_s, t_l]$ for equilibrium profiles, deviations and the monopoly problem alike.
• A Nash equilibrium is defined through the published general pure-strategy Nash equilibrium notion (CarbonDoubleCount.Planner.IsPureNash) with Function.update: deviations are unilateral and joint in $(p_i, q_i, t_i)$, not coordinate by coordinate.
• Optimality in the monopoly problem means global maximality over the feasible set, never a first-order condition.
• Added hypothesis. $\varphi_i(t_s) \ne \varphi_i(t_l)$ for every $i$. If $\varphi_i(t_s) = \varphi_i(t_l)$, firm $i$ has two best responses giving it the same profit and the same attraction, hence the same payoffs to all rivals; both are equilibria and "unique" is false. The paper's proof picks one endpoint "depending on the comparison" and does not treat ties.
• "Lower prices" is stated as $p_i^o \le p_i^*$, as the paper's proof concludes; for $N = 1$ the two problems coincide.
• The price root $\varphi_i(A)$ is defined on the region $p > k_i$, $\exp(w_i - p) < A$ where the first-order condition is increasing in $p$; it takes Lean's junk value only for $A \le 0$, where no statement uses it.

Formalizations that do not count: a price-only game with qualities and durations fixed at the monopoly values (that is the paper's reduction, not the theorem); a two-firm version; an equilibrium notion checked one coordinate at a time; or an equilibrium assumed rather than proved to exist.

A complete development needs real analysis of one-variable functions (monotonicity, the intermediate value theorem, maximization of $x e^{-x}$-type functions) and finite sums. The pure-Nash definition and the MNL price-competition milestones (4–8) are reusable beyond this paper. Proofs of any milestone, and alternative arguments for the price-equilibrium uniqueness, are welcome.

Selected references

• Y. Wang, J. Ke, Y. 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
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992. https://doi.org/10.7551/mitpress/2450.001.0001
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, Academic Press, 1974.

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.

Motivation

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as binary programs, max-cut, the trust-region subproblem and many problems in signal processing and control. A standard convex approximation is the Shor semidefinite programming (SDP) relaxation, which replaces the rank-one matrix $xx^\top$ by a positive semidefinite matrix $X \succeq xx^\top$. The relaxation always gives a lower bound; the question studied by Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2020, doi:10.1007/s10107-020-01589-9) is when it is tight, either in the sense of objective values or in the stronger sense that the relaxation describes the convex hull of the problem's epigraph.

Earlier exactness results are of two kinds. One kind concerns special structure: one constraint (the S-lemma, the trust-region subproblem), or two constraints under extra conditions. The other kind, due to Beck (Quadratic matrix programming, SIAM J. Optim. 2007, Corollary 4.4), exploits block symmetry: if every quadratic form is of the form $I_k\otimes\mathbb A_i$ with $k \ge m$, the SDP bound equals the optimal value. The paper under formalization recasts both kinds in one framework. Its convex hull results (Theorems 1 and 2) assume that a certain dual set $\Gamma$ is polyhedral, and its Proposition 3 shows that without polyhedrality the convex hull result can fail. This mission is about Theorem 7, which removes the polyhedrality assumption at the price of a larger symmetry parameter.

Setting

Fix $N \ge 1$ variables and $m = m_I + m_E \ge 1$ constraints. For $i\in[\![0,m]\!]$ let $q_i(x) = x^\top A_ix + 2b_i^\top x + c_i$ with $A_i$ a symmetric $N\times N$ matrix, $b_i\in\mathbb R^N$ and $c_i\in\mathbb R$. The QCQP is

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

Its epigraph is $\mathcal D = \{(x,t)\in\mathbb R^N\times\mathbb R : q_0(x)\le 2t,\ x \text{ feasible for (1)}\}$. With $Q_i = \begin{pmatrix} c_i & b_i^\top\\ b_i & A_i\end{pmatrix}$ and $Y = \begin{pmatrix} 1 & x^\top\\ x & X\end{pmatrix}$, the Shor relaxation imposes $Y\succeq0$, $\langle Q_i,Y\rangle\le0$ for inequalities and $\langle Q_i,Y\rangle=0$ for equalities; its projected epigraph $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some symmetric $X$ satisfies these constraints and $\langle Q_0,Y\rangle\le 2t$. Always $\operatorname{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ write $A(\gamma)=A_0+\sum_i\gamma_iA_i$ and $q(\gamma,x) = q_0(x)+\sum_i\gamma_iq_i(x)$, and let $\Gamma = \{\gamma : A(\gamma)\succeq0,\ \gamma_i\ge0\ \forall i\in[\![m_I]\!]\}$. Assumption 1 asks that (1) be feasible and that $A(\gamma^*)\succ0$ for some $\gamma^*$ that is nonnegative on the inequality indices.

The quadratic eigenvalue multiplicity (Definition 3) is the largest integer $k$ such that $N = kn$ and, for every $i\in[\![0,m]\!]$, $A_i = I_k\otimes\mathbb A_i$ for some symmetric $n\times n$ matrix $\mathbb A_i$. Here $I_k\otimes\mathbb A$ is block diagonal with $k$ copies of $\mathbb A$, and for $y\in\mathbb R^k$, $z\in\mathbb R^n$ the vector $y\otimes z\in\mathbb R^N$ has $j$-th block $y_jz$. Every QCQP has multiplicity at least $1$.

Formalization targets

Goal: Theorem 7 (p. 29)

$$\text{Assumption 1 and } k\ge m+2 \quad\Longrightarrow\quad \operatorname{conv}(\mathcal D) = \mathcal D_{\mathrm{SDP}}.$$

Milestones (in the order of the proof)

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}} = \{(x,t) : \sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}} = \min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. $A(\gamma)\succeq0 \iff \mathbb A(\gamma) = \mathbb A_0+\sum_i\gamma_i\mathbb A_i\succeq0$ (p. 29).
3. Under Assumption 1, every $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$ admits $Z\in\mathbb S^n$ with $Z\succeq0$, $q_0(\hat x)+\langle\mathbb A_0,Z\rangle\le2\hat t$, $q_i(\hat x)+\langle\mathbb A_i,Z\rangle\le0$ on inequalities and $=0$ on equalities: the system (17), p. 29.
4. If $k\ge m+2$, for any $\hat x$ and $z$ there is a unit $y\in\mathbb R^k$ with $\langle A_i\hat x+b_i, y\otimes z\rangle = 0$ for all $i\in[\![0,m]\!]$: the system (18), p. 30.
5. If $k\ge m+2$, every $(\hat x,\hat t,Z)$ satisfying (17) has $(\hat x,\hat t)\in\operatorname{conv}(\mathcal D)$ (pp. 29–30).

A supporting item (not a milestone) states the expansion used in the induction step: for $A = I_k\otimes\mathbb A$ with $\mathbb A$ symmetric and unit $y$, $q(\hat x\pm y\otimes z) = q(\hat x)\pm2\langle A\hat x+b,y\otimes z\rangle+\langle\mathbb A,zz^\top\rangle$ (p. 30).

Significance

The result. Theorem 7 is the convex hull counterpart of Beck's value-exactness result: under Assumption 1 and enough block symmetry, the Shor relaxation does not merely give the right optimal value but describes $\operatorname{conv}(\mathcal D)$ exactly, so every linear objective in $(x,t)$ over the relaxation is exact. It needs neither the polyhedrality of $\Gamma$ nor the attainment Assumption 2 used elsewhere in the paper. Problems with this structure include quadratic matrix programs (Beck 2007), in which the variable is a matrix $X\in\mathbb R^{n\times k}$ and every quadratic form is a trace $\operatorname{tr}(X^\top\mathbb A_iX)$. The companion Theorem 8 (a separate mission of this series) relaxes $k\ge m+2$ to $k\ge m+1$ at the price of intersecting with the optimal hyperplane, and Remark 14 records that the authors conjecture these thresholds are sharp.

The formalization. Theorem 7 is proved in the paper; no machine-checked proof of it, or of the Shor relaxation's convex hull results in general, is known. The milestones isolate the three ingredients of the proof as reusable statements: the dual description of $\mathcal D_{\mathrm{SDP}}$ (Lemma 1, shared with the polyhedral results of the paper), conic duality applied to a Kronecker-structured SDP, and a rank-reduction argument for Kronecker-structured quadratic forms.

Difficulty

The inclusion $\operatorname{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ is immediate; the content is the reverse inclusion. A point of $\mathcal D_{\mathrm{SDP}}$ comes with a matrix $X\succeq xx^\top$, and the naive idea is to decompose $X - xx^\top$ into rank-one pieces and move $x$ along them. In $\mathbb R^N$ this fails in general: moving along an arbitrary direction changes each constraint by a first-order term that cannot be controlled, and Proposition 3 of the paper exhibits a QCQP with $\operatorname{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$. The theorem therefore depends on the Kronecker structure and on the count $k\ge m+2$ in an essential way, and on an exact dual certificate, whose existence needs the strict feasibility of Assumption 1 and a dual attainment theorem for SDPs that is not yet in Mathlib.

Formalization scope

All objects are defined locally in the namespace QCQPTightness.MultHull.

• Variables live in Fin N → ℝ; constraints are indexed by Fin m, the paper's constraint $i+1$ being index $i$, and index $i$ is an inequality iff $i < m_I$. The standing assumption $m\ge1$ (p. 1) is a hypothesis of the goal.
• $\mathrm{Opt}$, $\mathrm{Opt}_{\mathrm{SDP}}$ and $\sup_{\gamma\in\Gamma}q(\gamma,x)$ are taken in EReal, so an empty or unbounded set never produces the junk value of a real infimum. "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t$" is stated as $q(\gamma,x)\le2t$ for all $\gamma\in\Gamma$.
• $\langle Q,Y\rangle$ is $\operatorname{tr}(QY)$; $\succeq0$ and $\succ0$ are Mathlib's PosSemidef and PosDef; $\operatorname{conv}$ is convexHull ℝ in $\mathbb R^N\times\mathbb R$.
• $I_k\otimes\mathbb A$ is Mathlib's Kronecker product, transported to Fin N by $(j,s)\mapsto s+nj$; $y\otimes z$ uses the same map.
• The goal uses the largest $k$ (IsQuadEigMult k) exactly as Definition 3. The milestones are stated for an arbitrary explicit representation $A_i = I_k\otimes\mathbb A_i$, which makes them at least as strong. Milestone 2 carries $k\ge1$, which the paper notes always holds.
• The goal does not assume the existence of a certificate $Z$ for (17): that existence is milestone 3 and is where Assumption 1 is used. A formalization that assumes it, or that drops Assumption 1, states a different theorem.

A complete development needs: SDP strong duality with dual attainment under a Slater condition (the platform's ConvexOptimization.sdp_strong_duality states a related form), the spectral decomposition of a positive semidefinite matrix into rank-one terms, Kronecker product identities for block-diagonal matrices, and the existence of nonzero solutions of underdetermined homogeneous linear systems. The duality and Kronecker lemmas are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming, 2020 (citation basis: arXiv:1911.09195v3). https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• A. Beck, Quadratic matrix programming, SIAM Journal on Optimization 17(4):1224–1238, 2007 (reference [5] of the paper).
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4):367–380, 1997 (reference [26] 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).