Optimization

Motivation

Car dealers, electronics retailers and office suppliers sell products whose prices and features are set upstream by manufacturers, and bundle each product with a service of their own: maintenance, repairs or a warranty. The dealer's short-term problem is then purely combinatorial. Which products should be carried, and which of them should come with a long rather than a short service? Longer service makes a product more attractive to consumers but costs the dealer more per unit sold, and the cost per unit of service time depends on the product's quality.

Wang, Ke and Cui (SSRN 3766191, accepted at Manufacturing & Service Operations Management) study price, quality and service decisions under multinomial logit (MNL) and nested logit demand. Section 5.2 of the paper treats the dealer's problem and shows that its solution has a two-threshold structure. This mission formalizes that result, Theorem 5, together with the steps of its proof in the Online Supplement.

The single-service version of the question is classical: under MNL demand with fixed prices, the profit-maximizing assortment consists of the products with the highest margins, a revenue-ordered (here: markup-ordered) assortment (Talluri & van Ryzin 2004). Theorem 5 extends this to two service options per product, where the choice is between three actions for each product (not offered, short service, long service) and the margin of each action differs.

Setting

There are products $\mathcal N=\{1,\dots,N\}$. Product $i$ has a fixed price $p_i$ and quality $q_i$, a quality sensitivity $\alpha_i$, a service utility per unit time $s_i$, a unit production cost $c_iq_i^2$, and a service cost per unit time $a_i-b_iq_i$. Two service durations are available: a short one $t_s$ and a long one $t_l$.

The dealer chooses two disjoint sets $S_l,S_s\subseteq\mathcal N$: products in $S_l$ are offered with service duration $t_l$, products in $S_s$ with $t_s$, and the others are not offered. A product $i$ offered with duration $t$ has attraction $\exp(\alpha_iq_i-p_i+ts_i)$ and markup $p_i-c_iq_i^2-t(a_i-b_iq_i)$. Under MNL demand with an outside option, product $i\in S_l$ is bought with probability

$$d_i(\mathbf p,\mathbf q;S_l,S_s)=\frac{\exp(\alpha_iq_i-p_i+t_ls_i)}{1+\sum_{j\in S_l}\exp(\alpha_jq_j-p_j+t_ls_j)+\sum_{j\in S_s}\exp(\alpha_jq_j-p_j+t_ss_j)},$$

and similarly with $t_s$ for $i\in S_s$ (eq. (12)). The dealer's expected profit, with market size one, is

$$\Pi^s(\mathbf p,\mathbf q;S_l,S_s)=\sum_{i\in S_l}\big[p_i-c_iq_i^2-t_l(a_i-b_iq_i)\big]d_i+\sum_{i\in S_s}\big[p_i-c_iq_i^2-t_s(a_i-b_iq_i)\big]d_i ,$$

and problem (13) is to maximize $\Pi^s$ over disjoint pairs $(S_l,S_s)$.

Two orderings of products appear in the answer. The short-service markup is $z_i=p_i-c_iq_i^2-t_s(a_i-b_iq_i)$. The adjusted markup is

$$x_i=(p_i-c_iq_i^2)-A_i\,(a_i-b_iq_i),\qquad A_i=\frac{t_l\exp(t_ls_i)-t_s\exp(t_ss_i)}{\exp(t_ls_i)-\exp(t_ss_i)} .$$

A markup-ordered assortment is a set of the products with the highest values of $z_i$; an adjusted markup-ordered set is a set of the products with the highest values of $x_i$.

Formalization targets

Goal: Theorem 5

Assume $t_s<t_l$, $s_i>0$ and $a_i-b_iq_i\ge0$ for all $i$. There are thresholds $\theta,\theta'$ such that, with $S_{i^*}=\{i:z_i\ge\theta\}$ and $S_{j^\natural}=\{i:x_i\ge\theta'\}$,

$$S_{j^\natural}\subseteq S_{i^*}\quad\text{and}\quad \Pi^s(\mathbf p,\mathbf q;S_l,S_s)\le\Pi^s\big(\mathbf p,\mathbf q;S_{j^\natural},\,S_{i^*}\setminus S_{j^\natural}\big)\ \text{ for all disjoint }(S_l,S_s).$$

Part (a) of the paper (a markup-ordered assortment is an optimal offer set) and part (b) (long service on an adjusted markup-ordered subset of it, short service on the rest) are one statement about the same $S_{i^*}$.

Milestones from the proof (Online Supplement p. 8)

1. (EC.11). For disjoint $(S_l,S_s)$, $r=\Pi^s(S_l,S_s)$ if and only if $r=\sum_{i\in S_l}h^l_i(r)+\sum_{i\in S_s}h^s_i(r)$, where $h^l_i(r)=[y_i-r]\exp(\alpha_iq_i-p_i+t_ls_i)$, $h^s_i(r)=[z_i-r]\exp(\alpha_iq_i-p_i+t_ss_i)$ and $y_i=p_i-c_iq_i^2-t_l(a_i-b_iq_i)$.
2. The fixed point. $H(r)=\max_{S_l,S_s}\{\sum_{S_l}h^l_i(r)+\sum_{S_s}h^s_i(r)\}=\sum_i\max\{h^l_i(r),h^s_i(r),0\}$; $H$ is non-increasing; $r=H(r)$ has a unique root $r^*$, and $r^*$ is the optimal value of (13).
3. Breakpoints. $x_i,y_i,z_i$ are the roots of $h^l_i=h^s_i$, $h^l_i=0$, $h^s_i=0$, and $x_i\le y_i\le z_i$.
4. Piecewise form. $h_i=h^l_i$ on $r\le x_i$, $h^s_i$ on $x_i<r\le z_i$, $0$ on $r>z_i$.
5. Level sets at $r^*$. $S_l=\{x_i\ge r^*\}$ and $S_s=\{z_i\ge r^*\}\setminus S_l$ is an optimal pair with profit $r^*$.

Significance

Problem (13) has $3^N$ feasible pairs. Theorem 5 reduces the search to at most $O(N^2)$ pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin $x_i$, which charges each unit of service cost at the rate $A_i>t_l$ rather than at $t_l$. The paper's managerial reading is that high-margin products go with long service, as with retailers that attach longer warranties to expensive items.

The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified two-service extension of the MNL revenue-ordered assortment theorem, and the fixed-point reduction (milestones 1 and 2) is a reusable device for MNL assortment problems with several options per product.

Difficulty

The profit is a ratio of sums, so exchanging one product's service changes every choice probability, and pairwise exchange arguments do not directly compare assortments. The naive idea of ranking products by a single margin fails: the long-service margin $y_i$ and the short-service margin $z_i$ order products differently, and the long service also raises the product's attraction. Neither ordering alone decides which products get long service. The adjusted markup $x_i$ is the breakpoint at which long and short service become equally profitable, and the three breakpoints $x_i\le y_i\le z_i$ must line up for the threshold structure to hold. This ordering uses $a_i-b_iq_i\ge0$: with a negative service cost the long service can be optimal for a product whose adjusted markup is below that of a product left unserved, and part (b) fails.

Formalization scope

• Products are Fin N (0-based); $N=0$ is allowed. All parameters $\alpha,a,b,c,s,p,q$ are arbitrary real vectors and $t_s,t_l$ real numbers; prices and qualities are fixed data, not decisions.
• The outside option is the constant $1$ in the denominator. The MNL formula is the definition; its derivation from Gumbel utilities is cited, not formalized.
• Decisions are pairs of Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.
• "Markup-ordered" and "adjusted markup-ordered" are upper level sets $\{i: z_i\ge\theta\}$, $\{i:x_i\ge\theta'\}$ with real thresholds. Each is a prefix of every decreasing relabelling, so no tie-break is fixed; the empty and the full set are allowed.
• The model's standing assumptions are explicit hypotheses wherever they are used: $t_s<t_l$ (shortest and longest duration), $s_i>0$ (service utility) and $a_i-b_iq_i\ge0$ (service cost). The first two make $A_i$ well defined; $A_i$ is a total Lean function that returns $0$ when its denominator vanishes, a value no statement relies on. No sign is imposed on $b_i$ or $c_i$.
• Trivializing formalizations are ruled out: the statement has two service levels (a single level would be the Talluri–van Ryzin theorem), uses level sets rather than a fixed relabelling with strict orders, ties the long-service set to the same offered set in (a) and (b) instead of using independent existentials, and states the three hypotheses rather than leaving them implicit.
• Definitions: the MNL choice probabilities and profit (12)–(13), and the auxiliary functions $h^l_i,h^s_i,h_i,H$, $A_i$, $x_i$. Proofs of the milestones need only finite sums, max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.

Selected references

• Ruxian Wang, Chenxu Ke, Shiliang 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 — DOI of the published version: https://doi.org/10.1287/msom.2020.0947
• Kalyan Talluri, Garrett van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• Daniel McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.

Motivation

A firm that sells durable products with an attached service (a warranty, a maintenance plan, a support contract) chooses three things for each product: its price, its quality, and how long the service lasts. Wang, Ke and Cui (SSRN 3766191, Manufacturing & Service Operations Management, 2022) study this joint decision when consumers choose among the products according to a discrete choice model. Under the multinomial logit (MNL) model they show that every product's optimal service duration is either the shortest or the longest available, so that the products split into a short-service group and a long-service group.

That conclusion suggests a different model of the consumer. In business procurement, and more generally when the buyer first decides how long a product will be used, the consumer plausibly chooses a service duration first and a product second. The two-stage nested logit (NL) model (Ben-Akiva 1973; McFadden 1980) captures exactly this: the two service groups become nests, and products within a nest are closer substitutes than products in different nests. Section 4 of the paper asks whether the MNL structure of optimal qualities and prices survives in this model. This mission formalizes its answer, Theorem 4.

Price optimization under the nested logit model has a substantial literature. For prices alone, the optimal prices within a nest share one markup and the problem reduces to a one-dimensional fixed point (Li & Huh 2011; Gallego & Wang 2014). Theorem 4 adds quality as a decision, with production cost quadratic in quality and service cost depending on quality.

Setting

There are two nests $x\in\{s,l\}$. Nest $x$ contains $m_x$ products $i=1,\dots,m_x$, and every product of nest $x$ is sold with the same fixed service duration $t_x$. Product $i$ of nest $x$ has parameters $\alpha_{xi}$ (quality sensitivity), $a_{xi}$ (base service cost per unit time), $b_{xi}$ (marginal effect of quality on service cost), $c_{xi}>0$ (production-cost coefficient) and $s_{xi}$ (service utility per unit time). The firm chooses a price $p_{xi}$ and a quality $q_{xi}$ for every product.

The total attractiveness of nest $x$ is $e_x=\sum_{i=1}^{m_x}\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})$. With upper-level scale parameter $\mu_1\ge 1$ (the nest coefficient is $1/\mu_1$; the lower-level scale is normalized to $1$), a consumer chooses nest $x$ with probability

$$d_x(\mathbf p,\mathbf q)=\frac{e_x^{1/\mu_1}}{1+e_s^{1/\mu_1}+e_l^{1/\mu_1}},$$

buys nothing with the remaining probability, and, having chosen nest $x$, picks product $i$ with probability $d_{i|x}=\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})/e_x$. The probability of buying product $i$ of nest $x$ is $d_{xi}=d_x\,d_{i|x}$. The markup of a product is its price minus production cost $c_{xi}q_{xi}^2$ minus service cost $t_x(a_{xi}-b_{xi}q_{xi})$, and the firm's expected profit (market size one) is

$$\Pi_M(\mathbf p,\mathbf q)=\sum_{x\in\{s,l\}}\sum_{i=1}^{m_x}\bigl[p_{xi}-c_{xi}q_{xi}^2-t_x(a_{xi}-b_{xi}q_{xi})\bigr]\,d_{xi}(\mathbf p,\mathbf q).$$

The firm maximizes $\Pi_M$ over all real price and quality vectors. When $\mu_1=1$ the model is the MNL model.

Formalization targets

Goal: Theorem 4

Let $q^\dagger_{xi}=(\alpha_{xi}+t_xb_{xi})/(2c_{xi})$. The equation

$$r=\sum_{x\in\{s,l\}}\mu_1\Bigl(\sum_{i=1}^{m_x}\exp\bigl(\alpha_{xi}q^\dagger_{xi}-c_{xi}q^{\dagger2}_{xi}-t_x(a_{xi}-b_{xi}q^\dagger_{xi})+t_xs_{xi}-r-\mu_1\bigr)\Bigr)^{1/\mu_1}$$

has a unique real solution $r^\dagger$. With $p^\dagger_{xi}=\mu_1+r^\dagger+c_{xi}q^{\dagger2}_{xi}+t_x(a_{xi}-b_{xi}q^\dagger_{xi})$,

$$\Pi_M(\mathbf p,\mathbf q)\le\Pi_M(\mathbf p^\dagger,\mathbf q^\dagger)=r^\dagger\quad\text{for all }(\mathbf p,\mathbf q),$$

and $(\mathbf p^\dagger,\mathbf q^\dagger)$ is the only maximizer.

Milestones

The milestones follow the paper's proof in the Online Supplement:

1. (EC.5): at an optimal price vector, every product $i$ of nest $x$ has markup $1+r/\mu_1+(1-1/\mu_1)r_x$, where $r$ is the profit and $r_x$ the nest's average markup; so markups are constant within a nest.
2. (EC.6): with a common markup $\rho_x$ per nest, the profit is $\sum_x\rho_x d_x(\boldsymbol\rho,\mathbf q)$; at the optimal markups, $\rho_x-\mu_1=r$ for each nonempty nest.
3. (EC.7): for every $r$, the right-hand side above, as a function of $\mathbf q$, is maximized exactly at $\mathbf q^\dagger$.
4. (EC.8): that right-hand side is strictly decreasing in $r$, so the fixed-point equation has exactly one root.

Significance

The result. Theorem 4 has two consequences. First, each product's optimal quality depends only on its own parameters and its nest's service duration, not on any other product, although all products are substitutes. At this quality, the marginal production and service cost of quality equals the consumer's marginal utility from it. Second, every product in both nests carries the same markup, $\mu_1+r^\dagger$: the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with $m_s+m_l$ prices reduces to finding the root of a single monotone function. Proposition 7 of the paper uses these closed forms to compare consumer surplus with and without quality control under the NL model.

Formalizing it. The paper's proof writes down first-order conditions and assumes an optimum exists. The goal here is global optimality and uniqueness over all real prices and qualities, which the paper does not prove. A complete formalization needs the existence of the maximizer or a direct upper bound, together with the first-order identities. The related platform item DLevelNestedLogit.Pricing.stationary_point_iff (Li et al. 2015) characterizes stationary points of the price-only revenue in a $d$-level nested logit model. It has no costs and no quality, and it is not used here. No result of this mission has a machine-checked proof yet.

Difficulty

The profit $\Pi_M$ is not concave in prices (under the nested logit model, concavity is known only after a change of variables to market shares, Li & Huh 2011), so a first-order condition does not by itself certify a global maximum. The paper's argument shows only that any optimum satisfies the stated formulas. For a global result, the critical points must be shown to coincide with the maximizers, and the profit must be bounded above by $r^\dagger$ everywhere, including at decisions where markups differ across products of a nest or are negative. The two reductions, to nest markups and then to the scalar $r$, are only valid at the optimum and have to be carried out with that in mind. The exponent $1/\mu_1\le 1$ makes $e_x^{1/\mu_1}$ concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.

Formalization scope

• Nests are a two-element type Nest (s, l). Products of nest $x$ are Fin (m x), 0-based. Nests may be empty: an empty nest has $e_x=0$, $0^{1/\mu_1}=0$, and contributes nothing.
• The outside option is the "$1+$" in the denominator of $d_x$, not a nest.
• Durations $t_s,t_l$ are fixed data, not decisions, with no order assumed between them. The nests are fixed.
• Prices and qualities range over all of $\mathbb R$. The model's normalization $q\ge 0$ is not imposed, as in the paper's own formula.
• Standing hypotheses: $\mu_1\ge 1$ (general; $\mu_1=1$ is allowed but is not the only case) and $c_{xi}>0$. No sign is imposed on $\alpha,a,b,s$.
• Powers are Real.rpow of nonnegative sums of exponentials.
• "Optimal" means a global maximizer over all real vectors. The milestones that the paper derives from first-order conditions are stated as properties of a global maximizer.
• The price formula $p^\dagger$ takes $r$ as an argument, and the theorem must identify $r=r^\dagger$.

The following versions are trivializing and are excluded: $\mu_1=1$ only (the MNL case), a single nest, first-order conditions in place of global optimality, fixed qualities, or an optimum defined by the paper's formula.

The definitions (Model, MarkupProblem, Optimum) are self-contained and can be reused for other nested logit pricing results. Contributions are welcome on each milestone, on a sorry-free derivative of $\Pi_M$ in $p_{xi}$, and on an existence result for the maximizer.

Selected references

• Y. Wang, J. 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 — DOI https://doi.org/10.1287/msom.2020.0947
• M. Ben-Akiva, Structure of Passenger Travel Demand Models, PhD thesis, Massachusetts Institute of Technology, 1973 (no stable link; cited as in the source's bibliography).
• D. McFadden, Econometric Models for Probabilistic Choice Among Products, Journal of Business 53(3), S13–S29, 1980. https://doi.org/10.1086/296093
• 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 (cited as in the source's bibliography; link not verified in this session).

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model facility location, pooling, max-cut, trust-region steps and robust optimization problems, and every $\{0,1\}$ integer program can be written as one; in general they are NP-hard. The standard tractable approach is the Shor semidefinite relaxation, which lifts $x$ to the matrix $xx^\top$ and relaxes the rank-one condition to positive semidefiniteness. A recurring question is when this relaxation loses nothing: when its optimal value equals that of the QCQP (SDP tightness), and, more strongly, when its projected epigraph equals the convex hull of the QCQP's epigraph (convex hull exactness). The second property also describes the convex hull of the nonconvex feasible set's epigraph, which is useful in branch-and-bound and cutting-plane methods.

Timeline. The S-lemma (Yakubovich, 1971) gives SDP tightness for one inequality constraint, and Fujie and Kojima (1997) recorded the dual description of the SDP value used below. For the trust-region subproblem and its generalization, convex hull descriptions of the epigraph were given by Ho-Nguyen and Kılınç-Karzan (2017) and by Wang and Kılınç-Karzan (arXiv:1907.08843, 2019). Beck (2007) and Beck, Drori and Teboulle (2012) gave SDP tightness results for quadratic matrix programs. Wang and Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (arXiv:1911.09195v3, Math. Program. 2021), introduced a general framework based on the faces of a dual set $\Gamma$ and proved convex hull and tightness results for polyhedral $\Gamma$ and for QCQPs with large quadratic eigenvalue multiplicity. This mission formalizes the paper's first convex hull theorem (Theorem 1, p. 13) and the framework it rests on.

Setting

Fix $N$ variables and $m\ge1$ constraints, the first $m_I$ inequalities and the remaining $m_E=m-m_I$ equalities. Each function is

$$q_i(x)=x^\top A_ix+2b_i^\top x+c_i,\qquad A_i\in\mathbb S^N,\ b_i\in\mathbb R^N,\ c_i\in\mathbb R,\quad i=0,\dots,m.$$

The QCQP (1) is $\mathrm{Opt}=\inf\{q_0(x): q_i(x)\le0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\}$, and its epigraph is $\mathcal D=\{(x,t): x\text{ feasible},\ q_0(x)\le2t\}$.

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 SDP relaxation (3) minimizes $\langle Q_0,Y\rangle$ over $X\in\mathbb S^N$ with $Y\succeq0$ and the constraints $\langle Q_i,Y\rangle\le0$ or $=0$; its value is $\mathrm{Opt}_{\mathrm{SDP}}$ and its projected epigraph is $\mathcal D_{\mathrm{SDP}}=\{(x,t):\exists X,\ (x,X)\text{ feasible},\ \langle Q_0,Y\rangle\le2t\}$ (4). Always $\mathrm{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}\ge\mathrm{Opt}_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ let $A(\gamma)=A_0+\sum_i\gamma_iA_i$, and similarly $b(\gamma)$, $c(\gamma)$ 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)\succeq0,\ \gamma_i\ge0\ \text{for } i\le m_I\}.$$

Assumption 1: the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$. Assumption 3: $\Gamma$ is polyhedral. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$. A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$ and semidefinite otherwise, with shared zero eigenspace $\mathcal V(\mathcal F)=\{v: A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. Finally $\operatorname{aff\,dim}$ denotes affine dimension.

Formalization targets

Goal: Theorem 1 (p. 13)

Under Assumptions 1 and 3, if every semidefinite face $\mathcal F$ of $\Gamma$ satisfies $\dim\mathcal V(\mathcal F)\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$, then

$$\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}\qquad\text{and}\qquad\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}}$ with definite $\mathcal F(\hat x)$ lies in $\mathcal D$.
4. Observation 1 (p. 10): under Assumption 1, a face of affine dimension $m$ is definite.
5. Lemma 4 (p. 10): under Assumptions 1, 2 and the decomposition condition (7), the two conclusions of Theorem 1 hold.
6. Lemma 8 (p. 13): under Assumption 3, $\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))$ when the supremum is finite.
7. Lemma 7 (p. 13): under the hypotheses of Theorem 1, condition (7) holds.

Companions

Lemma 6 (p. 11: $\dim\mathcal V(\mathcal F)\ge k$ for the quadratic eigenvalue multiplicity $k$), Theorem 2 (p. 15: the hypothesis of Theorem 1 with $k$ in place of $\dim\mathcal V(\mathcal F)$), and Corollaries 1–4 (pp. 16–18: convex quadratic programs, one constraint, $b_i=0$, scalar quadratic forms with $m\le N$).

Significance

The result. Theorem 1 gives a checkable sufficient condition, stated on the faces of a polyhedral dual set, under which the Shor relaxation is exact in the strongest sense: it describes $\mathrm{conv}(\mathcal D)$, so the SDP value equals the QCQP value and, by Remark 7, $\mathrm{conv}(\mathcal D)$ is second-order cone representable. Through Lemma 6 it becomes Theorem 2, the symmetry condition $k\ge\operatorname{aff\,dim}\{b(\gamma)\}+1$; its corollaries recover the convex hull results for the trust-region subproblem and its generalization and give new ones for simultaneously diagonalizable and "Swiss cheese" problems. The sharpness of the bound is shown in §4.3 of the paper.

Formalizing it. The theorem is proved in the paper; nothing in it is machine-checked. A formal proof needs strong conic duality for the SDP in Lemma 1, the Minkowski–Weyl decomposition in Lemma 8, and the face-by-face decomposition argument of Lemma 7. These pieces are shared with the paper's SDP tightness result (Theorem 3), which uses Lemmas 1–3 and 8 again.

Difficulty

The obvious attempt is to take $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$, recover a rank-one solution of the SDP, and read off a point of $\mathcal D$. This fails because an optimal $Y$ need not have rank one, and a rank-reduction step can leave the feasible set of a nonconvex constraint. The paper instead moves $(\hat x,\hat t)$ along a direction $v$ in the shared zero eigenspace of the face $\mathcal F(\hat x)$, and must show that both endpoints of the move stay in $\mathcal D_{\mathrm{SDP}}$ while the face strictly grows in affine dimension. Controlling the endpoints needs finiteness of the relevant family of quadratic functions, which is where polyhedrality enters; without it (§4.3) the argument and the theorem fail. Lemma 1 also needs a strong duality theorem for semidefinite programs with a minimax step, neither of which is elementary in Lean.

Formalization scope

The Lean development lives in the namespace QCQPTightness.ConvHull. A QCQP is a structure with symmetric $A_0, A_i$, vectors $b_0,b_i$, scalars $c_0,c_i$ and a count $m_I\le m$; constraints are indexed by Fin m, constraint $i$ being an inequality exactly when $i<m_I$. Conventions:

• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, never real infima; points of $\mathbb R^{N+1}$ are pairs $(x,t)$, and $\mathrm{conv}$ is convexHull ℝ.
• Faces of $\Gamma$ are nonempty convex extreme subsets; the page's convention $\operatorname{aff\,dim}\emptyset=-1$ makes the empty face irrelevant, while Lean's affine dimension of $\emptyset$ would be $0$.
• "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t$" is written $\forall\gamma\in\Gamma,\ q(\gamma,x)\le2t$; "a convex combination of points with property $P$" is membership in the convex hull of the set of such points; the unit sphere is $v^\top v=1$.
• The goal carries exactly the paper's hypotheses plus its standing assumption $m\ge1$ (p. 1); Assumption 2 is not assumed because Assumption 3 implies it.
• Lemma 8 is printed with "$\mathcal F_r(\hat x)$ is the face of $\Gamma_e$"; it is formalized with $\Gamma_r$, as the proof and Lemma 7 use it.

A trivializing formalization would assume condition (7), the decomposition of Lemma 8, or any property of $\mathcal F(\hat x)$ in the goal; the goal assumes none of these, and the dimension hypothesis is satisfiable with semidefinite faces present (for $q_0=-x^2$, $q_1=x^2-1$, the face $\{\gamma_1=1\}$ is semidefinite with $\dim\mathcal V=1$).

Infrastructure needed: SDP strong duality (the platform has ConvexOptimization.sdp_strong_duality), the Minkowski–Weyl theorem for polyhedra, faces of convex sets and affine dimension. Proofs of any milestone, of the companions, and reusable lemmas about faces of spectrahedra are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Math. Program. (2021); arXiv:1911.09195v3. 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, J. Global Optim. 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
• A. Beck, Quadratic matrix programming, SIAM J. Optim. 17 (2007) 1224–1238. https://doi.org/10.1137/05064816X
• N. Ho-Nguyen, F. Kılınç-Karzan, A second-order cone based approach for solving the trust-region subproblem and its variants, SIAM J. Optim. 27 (2017) 1485–1512. https://doi.org/10.1137/16M1065197
• A. L. Wang, F. Kılınç-Karzan, The generalized trust region subproblem: solution complexity and convex hull results, arXiv:1907.08843 (2019). https://arxiv.org/abs/1907.08843
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

Why the image function matters for ADMM

The alternating direction method of multipliers (ADMM) solves problems of the form $\min_{x,z} f(x)+g(z)$ subject to $Ax+Bz=b$. Themelis and Patrinos (arXiv:1709.05747v4, SIAM J. Optim. 30(1):149–181, 2020) show that, for nonconvex $f$ and $g$, ADMM is the Douglas–Rachford splitting method applied to a reformulated problem whose second term is the image function $\varphi_2=(Bg)$, $(Bg)(s)=\inf\{g(z)\mid Bz=s\}$. Their convergence theory for DRS requires the nonsmooth term to be proper and lower semicontinuous (Assumption IIa4), so whether $(Bg)$ inherits lower semicontinuity from $g$ decides whether the theory applies to a given ADMM instance.

Image functions, also called epi-compositions or infimal post-compositions, are classical objects of variational analysis (Rockafellar and Wets, Variational Analysis; Bauschke and Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces; Auslender and Teboulle, Asymptotic Cones and Functions). For convex $g$ the question of when $(Bg)$ is closed has a long history through recession functions; Section 5.4.1 of the paper gives a characterization that needs no convexity.

Setting

Let $\overline{\mathbb R}=\mathbb R\cup\{+\infty\}$. For $g:\mathbb R^n\to\overline{\mathbb R}$ the domain is $\operatorname{dom}g=\{z\mid g(z)<\infty\}$; $g$ is lower semicontinuous (lsc) if its epigraph is closed, and level bounded if every set $\{z\mid g(z)\le\alpha\}$, $\alpha\in\mathbb R$, is bounded.

Fix a matrix $B\in\mathbb R^{p\times n}$. The image function of $g$ under $B$ (Definition 5.1) is

$$(Bg)(s)=\inf_{z\in\mathbb R^n}\{g(z)\mid Bz=s\},\qquad s\in\mathbb R^p,$$

with values in $[-\infty,+\infty]$. Its domain is $B\operatorname{dom}g$: outside that set the infimum is over values $+\infty$ only.

Condition (5.5) at a point $\bar z\in\operatorname{dom}g$ compares the best value of $g$ on the affine fibre $\bar z+\ker B$ with the values of $g$ far away along directions that $B$ nearly annihilates:

$$\liminf_{\substack{\|d\|\to\infty\\ Bd\to0}} g(\bar z+d)\;\ge\;\inf_{d\in\ker B} g(\bar z+d).$$

The right side equals $(Bg)(B\bar z)$.

Formalization targets

Goal: Theorem 5.11, on $B\operatorname{dom}g$

For every lsc $g:\mathbb R^n\to\overline{\mathbb R}$ and every $B\in\mathbb R^{p\times n}$,

$$(Bg)\ \text{is lsc at every } \bar s\in B\operatorname{dom}g\quad\Longleftrightarrow\quad (5.5)\ \text{holds at every } \bar z\in\operatorname{dom}g.$$

Milestones

1. The right side of (5.5) is $(Bg)(B\bar z)$.
2. The "if" direction: (5.5) on $\operatorname{dom}g$ gives lower semicontinuity of $(Bg)$ at every point of $B\operatorname{dom}g$.
3. The "only if" direction: lower semicontinuity of $(Bg)$ on $B\operatorname{dom}g$ forces (5.5) on $\operatorname{dom}g$.

Companion results

• The "In particular" clause of Theorem 5.11, as printed: if $g$ is lsc and level bounded, then $(Bg)$ is lsc on all of $\mathbb R^p$.
• The properness clause of Proposition 5.10: if $g$ is proper and lsc and, for some $\beta>0$, $\min_z\{g(z)+\frac\beta2\|Bz-s\|^2\}$ is attained for every $s$, then $(Bg)$ is proper.

Significance

Theorem 5.11 turns Assumption IIa4, a property of a derived function, into a checkable condition on $g$ and $B$. Its level-bounded corollary covers every lsc $g$ with bounded sublevel sets, and the characterization explains why the pathological example (5.4) of the paper, in which $g$ is even $C^1$, fails: a minimizing sequence on the fibre escapes to infinity while $B$ applied to it converges. Combined with the convergence theorem for ADMM in the same paper (Theorem 5.6), this identifies the ADMM instances to which the tight DRS stepsize theory applies.

The theorem is proved in the paper. As far as is known, no machine-checked proof of it, or of any closedness criterion for image functions, exists in Lean or in Mathlib. A formalization fixes the exact range of the equivalence, which the printed statement gets wrong (see Formalization scope), and supplies reusable infrastructure: the image function in EReal, and liminfs along the filter "$\|d\|\to\infty$, $Bd\to0$".

Difficulty

Lower semicontinuity of $(Bg)$ at $\bar s$ asks that values of $g$ on fibres $\{Bz=s\}$, $s\to\bar s$, not drop below $(Bg)(\bar s)$. The natural argument picks near-minimizers $z_k$ on these fibres and passes to a limit; this works only when the $z_k$ stay bounded, and nothing in lsc of $g$ alone prevents them from escaping to infinity. The difficulty is to account exactly for the unbounded case, which must be compared with the fibre through $\bar s$ by a translation $z_k-\bar z$, and that requires a point $\bar z\in\operatorname{dom}g$ with $B\bar z=\bar s$. The converse requires turning a failure of (5.5), stated as a filter liminf, into a sequence witnessing the failure of lower semicontinuity.

Formalization scope

• $\mathbb R^n$ and $\mathbb R^p$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p); $B$ is a continuous linear map between them. Every dimension, including $0$, is allowed.
• $\overline{\mathbb R}$ is EReal, and $g$ is assumed never to take the value $-\infty$. The image function is the EReal infimum $\inf_{z,\ Bz=s} g(z)$, which may be $-\infty$ and is $+\infty$ off $B\operatorname{dom}g$. Properness of $g$ is not assumed in the goal: if $\operatorname{dom}g=\emptyset$ both sides hold.
• Lower semicontinuity at a point is Mathlib's LowerSemicontinuousAt, the neighbourhood form of the page's sequential level-set criterion.
• The liminf in (5.5) is taken in the complete lattice $[-\infty,+\infty]$ along the meet of the cobounded filter ($\|d\|\to\infty$) and the preimage under $B$ of the neighbourhood filter of $0$. When no such $d$ exist (e.g. $B$ injective) the filter is trivial, the liminf is $+\infty$, and (5.5) holds, as an empty liminf does on the page.
• Correction. As printed, Theorem 5.11 asserts lsc of $(Bg)$ everywhere, and its "if" direction is then false. Take $n=2$, $p=1$, $B=[1\ 0]$, and $g$ the indicator of the closed set $\{(x,y):x>0,\ xy\ge1\}$. Condition (5.5) holds at every $\bar z\in\operatorname{dom}g$, since its right side is $0$ and $g\ge0$; but $(Bg)(s)=0$ for $s>0$ and $+\infty$ for $s\le0$, so $(Bg)$ is not lsc at $0$. The proof begins "given $\bar s\in\operatorname{dom}(Bg)$" and covers exactly $B\operatorname{dom}g$; both directions establish the corrected equivalence, which is the goal. The "In particular" clause is true as printed and is stated with lsc everywhere. The lsc clause of Proposition 5.10 fails for the same reason and is not formalized.
• Assumption IIa2 enters Proposition 5.10 only through the solvability of $\min_z\{g(z)+\frac\beta2\|Bz-s\|^2\}$ for every $s$.
• A trivializing formalization is ruled out: the goal assumes only lsc of $g$ and linearity of $B$, as on the page, and is not restricted to proper or level-bounded $g$ (that is the separate companion).
• Contributions welcome: proofs of the milestones, a general Mathlib-style lemma that the infimum of an lsc function over the fibres of a linear map is lsc on its domain under (5.5), and the closedness of image functions under level-boundedness.

Selected references

• A. Themelis, P. Patrinos, Douglas–Rachford splitting and ADMM for nonconvex optimization: tight convergence results, SIAM J. Optim. 30(1):149–181, 2020. Preprint arXiv:1709.05747v4. https://arxiv.org/abs/1709.05747, https://doi.org/10.1137/18M1163993
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998 (corrected printings 2009, 2011). https://doi.org/10.1007/978-3-642-02431-3
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• A. Auslender, M. Teboulle, Asymptotic Cones and Functions in Optimization and Variational Inequalities, Springer, 2003 (cited as 2002 in the paper). https://doi.org/10.1007/b97594

Motivation

Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an $L$-smooth convex function $f$ with function values decreasing at the rate $O(L/k^2)$. That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODE $\ddot X+\frac3t\dot X+\nabla f(X)=0$ reproduces the $O(1/t^2)$ function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.

Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the $O(\sqrt s)$ terms of the limit, where $s$ is the step size. The resulting high-resolution ODEs contain a gradient-correction term $\sqrt s\,\nabla^2 f(X)\dot X$, which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time $t$ decays like $1/t^3$, while the low-resolution ODE gives only $1/t^2$. Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).

Setting

Let $f:\mathbb R^n\to\mathbb R$ have gradient $\nabla f$ and Hessian $\nabla^2 f$. For $L>0$, the class $\mathcal F^1_L(\mathbb R^n)$ consists of the differentiable $f$ with

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle,\qquad \|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|\qquad(x,y\in\mathbb R^n).$$

The class $\mathcal F^2_L(\mathbb R^n)$ is its subclass of twice continuously differentiable functions whose Hessian is Lipschitz continuous. A minimizer $x^\star$ of $f$ is fixed.

Given a step size $s>0$, put $t_0=1.5\sqrt s$. The high-resolution ODE of NAG-C (1.12) is

$$\ddot X(t)+\frac3t\dot X(t)+\sqrt s\,\nabla^2 f(X(t))\dot X(t)+\Big(1+\frac{3\sqrt s}{2t}\Big)\nabla f(X(t))=0\qquad(t\ge t_0),$$

with $X(t_0)=x_0$ and $\dot X(t_0)=-\sqrt s\,\nabla f(x_0)$. The analysis uses the Lyapunov function (4.1)

$$\mathcal E(t)=t\Big(t+\frac{\sqrt s}{2}\Big)\big(f(X)-f(x^\star)\big)+\frac12\big\|t\dot X+2(X-x^\star)+t\sqrt s\,\nabla f(X)\big\|^2 .$$

With $s=0$ it reduces to the Lyapunov function of Su, Boyd and Candès.

Formalization targets

Goal: Theorem 5 (p. 21)

For every $f\in\mathcal F^2_L(\mathbb R^n)$, every step size $s>0$, and every solution $X$ of (1.12),

$$\inf_{t_0\le u\le t}\|\nabla f(X(u))\|^2\le\frac{(12+9sL)\,\|x_0-x^\star\|^2}{2\sqrt s\,(t^3-t_0^3)}\qquad\text{for all }t>t_0 .$$

With $s=1/L$ this is $O(\sqrt L/t^3)$. The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.

Milestones (pp. 22–23)

1. The exact derivative of $\mathcal E$ along (1.12) (first display of the proof of Lemma 4.1, p. 23).
2. Lemma 4.1, (4.2): $\frac{d\mathcal E}{dt}\le-\big[\sqrt s\,t^2+(\frac1L+\frac s2)t+\frac{\sqrt s}{2L}\big]\|\nabla f(X)\|^2$ for $t\ge t_0$.
3. The integrated form: $\int_{t_0}^t\big[\sqrt s\,u^2+(\frac1L+\frac s2)u+\frac{\sqrt s}{2L}\big]\|\nabla f(X(u))\|^2\,du\le\mathcal E(t_0)-\mathcal E(t)\le\mathcal E(t_0)$.
4. (4.3): the infimum is at most $\mathcal E(t_0)$ divided by $\sqrt s(t^3-t_0^3)/3+(\frac1L+\frac s2)(t^2-t_0^2)/2+\frac{\sqrt s}{2L}(t-t_0)$.
5. $\mathcal E(t_0)\le 3s\cdot\frac L2\|x_0-x^\star\|^2+2\|x_0-x^\star\|^2$, from the initial conditions.
6. (4.4): the same bound as (4.3) with numerator $(2+1.5sL)\|x_0-x^\star\|^2$. Keeping only the cubic term of the denominator gives Theorem 5.

A companion item states Corollary 4.2 (p. 24): $f(X(t))-f(x^\star)\le\frac{(4+3sL)\|x_0-x^\star\|^2}{t(2t+\sqrt s)}$ for $t>t_0$.

Significance

Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives $\min_{i\le k}\|\nabla f(x_i)\|^2$ to zero at the rate $O(L^2/k^3)$. Combining the $O(1/t^2)$ function-value rate with $\|\nabla f\|^2\le 2L(f-f^\star)$ gives only $O(L/t^2)$. Previously known $O(L^2/k^3)$ rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor $\|\nabla f(X)\|^2$ in Lemma 4.1 comes from the term $t\sqrt s\,\nabla f(X)$ in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the $1/t^3$ rate (p. 23).

The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.

Difficulty

The obvious route goes through the function-value rate and the inequality $\|\nabla f\|^2\le2L(f-f^\star)$. It loses a factor of $t$ and yields only $1/t^2$. The cubic rate needs a Lyapunov function whose derivative contains a term proportional to $t^2\|\nabla f(X)\|^2$. Proving the derivative identity requires differentiating $t\mapsto\nabla f(X(t))$ through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle+\frac1{2L}\|\nabla f(X)\|^2$ of $L$-smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on $[t_0,t]$, and compare an infimum with a weighted average.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, and $\nabla^2 f(x)v$ is the Fréchet derivative of the gradient map applied to $v$.
• The classes $\mathcal F^1_L$ and $\mathcal F^2_L$ are stated in the first-order form printed on p. 8. The Hessian's Lipschitz constant is existential, since the paper fixes none.
• The minimizer $x^\star$ is a hypothesis $f(x^\star)\le f(z)$ for all $z$. The paper presupposes it exists.
• The step size is any $s>0$; there is no condition $s\le1/L$.
• A solution of (1.12) is a pair $(X,V)$ with $X(t_0)=x_0$ and $V(t_0)=-\sqrt s\,\nabla f(x_0)$. For every $t\ge t_0$, $X$ has derivative $V(t)$ and $V$ has the derivative prescribed by (1.12), both relative to $[t_0,\infty)$.
• Every statement quantifies over all solutions. Existence and uniqueness (the paper's Proposition 2.2) are not assumed.
• The infimum $\inf_{t_0\le u\le t}$ ranges over the points of the interval $[t_0,t]$. Statements involving it hold for $t>t_0$, as on the page.
• Derivative bounds assert that the derivative exists.
• The integral bound asserts integrability of its integrand.

Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is $\le 0$); the velocity is not tied to $\dot X$; the goal is stated at $t=t_0$ (where Lean divides by $0$); or derivatives are written with deriv, which is $0$ where a function is not differentiable. The statements here avoid all of these.

Infrastructure. A complete development needs:

• the chain rule for $\nabla f\circ X$ along a path;
• the co-coercivity inequality for $L$-smooth convex functions;
• the fundamental theorem of calculus for one-sided derivatives on $[t_0,t]$;
• the mean-value comparison of an infimum with a weighted average.

The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Math. Program. (2021), DOI 10.1007/s10107-021-01681-8. https://arxiv.org/abs/1810.08907
• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, J. Mach. Learn. Res. 17(153), 2016. https://arxiv.org/abs/1503.01243
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27, 1983. https://www.mathnet.ru/eng/dan46009
• Y. Nesterov, How to make the gradients small, Optima 88, 2012. http://www.mathopt.org/Optima-Issues/optima88.pdf
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Math. Program. 156, 2016. https://arxiv.org/abs/1310.3787
• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020. https://arxiv.org/abs/1907.10536

Why a high-resolution ODE for the heavy-ball method

Polyak's heavy-ball method and Nesterov's accelerated gradient method for strongly convex functions (NAG-SC) are the two classical momentum methods of smooth convex optimization. With step size $s$ and momentum $\alpha=(1-\sqrt{\mu s})/(1+\sqrt{\mu s})$ they differ only by a gradient-correction term, yet NAG-SC is accelerated for every $\mu$-strongly convex, $L$-smooth objective while the heavy-ball method can fail to converge outside the quadratic case (Lessard, Recht & Packard 2016). The classical continuous-time limit cannot see this difference: as $s\to0$ both methods converge to the same low-resolution ODE $\ddot X+2\sqrt\mu\,\dot X+\nabla f(X)=0$ (Su, Boyd & Candès 2016 treat the convex analogue).

Shi, Du, Jordan & Su (2018/2021) keep the $O(\sqrt s)$ terms of the limit and obtain high-resolution ODEs, one per method, which do distinguish the two algorithms. This mission formalizes their convergence theorem for the high-resolution ODE of the heavy-ball method (Theorem 2 of arXiv:1810.08907v3). A companion mission in the same series treats the high-resolution ODE of NAG-SC (Theorem 1), whose only difference is a Hessian-driven damping term $\sqrt s\,\nabla^2 f(X)\dot X$.

Setting

Work in $\mathbb R^n$ with the standard inner product $\langle\cdot,\cdot\rangle$ and Euclidean norm $\|\cdot\|$. A function $f:\mathbb R^n\to\mathbb R$ belongs to $\mathcal F^1_L(\mathbb R^n)$ if $L>0$, $f$ is differentiable and convex in the form $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle$, and $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$. It belongs to $\mathcal S^1_{\mu,L}(\mathbb R^n)$ if moreover $0<\mu\le L$ and

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2\quad\text{for all }x,y,$$

and to $\mathcal S^2_{\mu,L}(\mathbb R^n)$ if in addition $f$ is twice continuously differentiable with a Lipschitz-continuous Hessian. Write $x^\star$ for the minimizer of $f$.

Given a step size $s>0$ and an initial point $x_0$, the high-resolution ODE of the heavy-ball method is

$$\ddot X(t)+2\sqrt\mu\,\dot X(t)+\bigl(1+\sqrt{\mu s}\bigr)\nabla f(X(t))=0,\qquad X(0)=x_0,\quad \dot X(0)=-\frac{2\sqrt s\,\nabla f(x_0)}{1+\sqrt{\mu s}},\tag{1.10}$$

for $t\ge0$. The initial velocity matches the first step of the discrete method. The paper's Lyapunov function is

$$\mathcal E(t)=\bigl(1+\sqrt{\mu s}\bigr)\bigl(f(X)-f(x^\star)\bigr)+\frac14\|\dot X\|^2+\frac14\bigl\|\dot X+2\sqrt\mu\,(X-x^\star)\bigr\|^2.\tag{3.3}$$

Formalization targets

Goal: Theorem 2 (p. 14)

For $f\in\mathcal S^2_{\mu,L}(\mathbb R^n)$, every step size $0<s\le1/L$, and every $t\ge0$,

$$f(X(t))-f(x^\star)\le\frac{7\,\|x_0-x^\star\|^2}{2s}\,e^{-\sqrt\mu\,t/4}.$$

Milestones

1. The estimate (B.1), p. 50: $\mathcal E\le(1+\sqrt{\mu s})(f(X)-f(x^\star))+\frac34\|\dot X\|^2+2\mu\|X-x^\star\|^2$.
2. The derivative identity of App. B.1, p. 50: along (1.10),

$$\frac{d\mathcal E}{dt}=-\sqrt\mu\Bigl[\|\dot X\|^2+\bigl(1+\sqrt{\mu s}\bigr)\langle\nabla f(X),X-x^\star\rangle\Bigr].$$

3. Lemma 3.2, p. 14: for every $s>0$, $\dfrac{d\mathcal E}{dt}\le-\dfrac{\sqrt\mu}{4}\mathcal E$.
4. The integrated decay, p. 14: $\mathcal E(t)\le e^{-\sqrt\mu t/4}\mathcal E(0)$.
5. The explicit-coefficient bound, p. 14: for $s\le1/L$,

$$f(X)-f(x^\star)\le\left[\frac12+\frac{3}{(1+\sqrt{\mu s})^3}+\frac{2(\mu s)}{1+\sqrt{\mu s}}\right]\frac{\|x_0-x^\star\|^2e^{-\sqrt\mu t/4}}{s}.$$

6. The coefficient inequality, p. 14: for $0<\mu s\le1$, the bracket above is $<7/2$.

Significance

The result. Theorem 2 gives a linear rate $e^{-\sqrt\mu t/4}$ for the heavy-ball ODE with an explicit constant, valid for every $\mathcal S^2_{\mu,L}$ objective and every step size up to $1/L$. Read next to Theorem 1 (rate $e^{-\sqrt\mu t/4}$, constant $2/s$ for the NAG-SC ODE), it shows that at the continuous level both high-resolution ODEs converge at the accelerated rate; the paper locates the difference between the two discrete methods in the discretization, where only the gradient correction of NAG-SC lets the Lyapunov argument survive (its Theorems 3 and 4 and §3.3). The Lyapunov function (3.3) is the NAG-SC function (2.4) with the $\sqrt s\,\nabla f(X)$ term removed, and the two coincide at $s=0$.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a checked chain from the ODE to the rate: a one-sided derivative computation along a trajectory in $\mathbb R^n$, a differential inequality, a Grönwall-type integration, and a closed-form estimate of $\mathcal E(0)$ from the initial conditions and $L$-smoothness. The derivative computation and the Grönwall step reuse directly in the companion missions on the NAG-SC and NAG-C high-resolution ODEs.

Difficulty

The algebra is short; the formal difficulty is analytic. The derivative of $t\mapsto f(X(t))$ must be obtained by the chain rule from a one-sided derivative of $X$ at $t=0$ and $f$'s differentiability, and the derivative of the two squared norms from those of $X$ and $V=\dot X$. Passing from Lemma 3.2 to $\mathcal E(t)\le e^{-\sqrt\mu t/4}\mathcal E(0)$ is a comparison argument for a function known only to have one-sided derivatives on $[0,\infty)$; the naive route through $\frac{d}{dt}\bigl(e^{\sqrt\mu t/4}\mathcal E\bigr)\le0$ requires a monotonicity theorem for functions with derivatives within a half-line. Finally, the estimate of $\mathcal E(0)$ needs $f(x_0)-f(x^\star)\le\frac L2\|x_0-x^\star\|^2$ and $\|\nabla f(x_0)\|\le L\|x_0-x^\star\|$, both consequences of $L$-smoothness and $\nabla f(x^\star)=0$ that must be derived from the class definition, and the constant $7/2$ needs a one-variable inequality in $\sqrt{\mu s}\in(0,1]$.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, and $\nabla^2f(x)$ is fderiv ℝ (gradient f) x. The classes $\mathcal F^1_L$, $\mathcal S^1_{\mu,L}$, $\mathcal S^2_{\mu,L}$ are structures carrying the paper's first-order inequalities (§1.4, p. 8), with $0<\mu\le L$; the Lipschitz constant of the Hessian is existential, as the paper fixes none. The minimizer is a point $x^\star$ with $f(x^\star)\le f(z)$ for all $z$.

A solution of (1.10) is a pair of curves $X,V:\mathbb R\to\mathbb R^n$ with $X(0)=x_0$, $V(0)=-2\sqrt s\,\nabla f(x_0)/(1+\sqrt{\mu s})$, $V(t)$ the derivative of $X$ and $-2\sqrt\mu V(t)-(1+\sqrt{\mu s})\nabla f(X(t))$ the derivative of $V$ at every $t\ge0$, both taken within $[0,\infty)$; values for $t<0$ play no role. The theorems quantify over every such solution. Existence and uniqueness (the paper's Propositions 2.1–2.2) are not assumed, and no a priori bound on $X$ or $V$ is added. Derivative claims assert that the derivative exists and has the stated value or bound, so a statement cannot hold merely because a derivative is undefined. The goal states the decay of $f(X(t))-f(x^\star)$ with the printed constant $7/(2s)$; it does not assume any decay of $\mathcal E$, and an ODE predicate in which $V$ is not the derivative of $X$ would be a different, trivial statement.

All drafts live in the namespace HighResODE.HeavyBallODE, with one definitions file (classes, ODE, Lyapunov function). Contributions are welcome at every milestone; a general lemma "$\varphi'\le-c\,\varphi$ within $[0,\infty)$ implies $\varphi(t)\le e^{-ct}\varphi(0)$" and the $L$-smoothness estimates around a minimizer are reusable well beyond this mission.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, Mathematical Programming (2021); cited here in its preprint version arXiv:1810.08907v3. https://arxiv.org/abs/1810.08907
• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, Journal of Machine Learning Research 17 (2016). https://arxiv.org/abs/1503.01243
• L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM Journal on Optimization 26 (2016). https://arxiv.org/abs/1408.3595
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5