Optimization

Motivation

Random coordinate descent minimizes a smooth convex function $f:\mathbb R^n\to\mathbb R$ by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.

The basic method RCDM of the paper takes, along coordinate $i$, a step of length $1/L_i$, where $L_i$ is a Lipschitz constant of the $i$-th partial derivative along the $i$-th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.

Setting

Write $\nabla_i f(x)=\partial f/\partial x_i(x)$ and $e_i$ for the $i$-th standard basis vector of $\mathbb R^n$, $n\ge1$. The function $f$ is convex and differentiable, attains its minimum $f^*=f(x^*)$, and its partial derivatives are coordinate-wise Lipschitz with constants $L_i>0$ ((2.2) with one-dimensional blocks):

$$|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le L_i|u|\qquad(x\in\mathbb R^n,\ u\in\mathbb R,\ i=1,\dots,n).$$

The weighted norm and its dual are $\|x\|_1=(\sum_iL_ix_i^2)^{1/2}$ and $\|g\|_1^*=(\sum_ig_i^2/L_i)^{1/2}$ ((2.7) with $\alpha=1$), and

$$R_1(x_0)=\max_x\Big\{\max_{x^*\in X^*}\|x-x^*\|_1:\ f(x)\le f(x_0)\Big\}$$

measures the size of the initial level set, $X^*$ being the set of minimizers.

The random adaptive coordinate descent method RACDM$(x_0)$ (6.1) keeps estimates $\hat L_1,\dots,\hat L_n$, initialised with given lower bounds $L_i^0\in(0,L_i]$. At iteration $k$ it

1. draws $i=i_k$ uniformly from $\{1,\dots,n\}$;
2. sets $x_{k+1}=x_k-\hat L_i^{-1}\nabla_if(x_k)e_i$ and, as long as $\nabla_if(x_k)\cdot\nabla_if(x_{k+1})<0$, doubles $\hat L_i$ and recomputes $x_{k+1}$;
3. halves $\hat L_i$.

The loop test uses only the sign of one partial derivative and never a function value. With $\varphi_k=\mathbb E f(x_k)$ (the expectation over $i_0,\dots,i_{k-1}$) and $N_k$ the number of partial derivatives computed in iterations $0,\dots,k$, Theorem 7 states three facts about this method.

Formalization targets

Goal: Theorem 7, item 2, (6.2)

$$\varphi_k-f^*\ \le\ \frac{8nR_1^2(x_0)}{16+3k},\qquad k\ge0.$$

This is the rate of RCDM$(0,x_0)$, $\varphi_k-f^*\le 2nR_1^2(x_0)/(k+4)$ ((2.14)), with a larger constant.

Milestones

1. (6.4) — started from an estimate $0<\hat L_i\le L_i$, the doubling loop terminates and the accepted estimate satisfies $\hat L_i\le2L_i$.
2. Theorem 7, item 1 — at the beginning of each iteration $\hat L_i\le L_i$ for every $i$.
3. One-step decrease (proof of Theorem 7, p. 19) — $f(x_k)-f(x_{k+1})\ge\frac{3}{8L_{i_k}}(\nabla_{i_k}f(x_k))^2$.
4. Expected decrease (proof of Theorem 7, p. 19) — $f(x_k)-\mathbb E_{i_k}f(x_{k+1})\ge\frac3{8n}(\|\nabla f(x_k)\|_1^*)^2$.
5. Theorem 7, item 3, (6.3) — $N_k\le 2(k+1)+\sum_{i=1}^n\log_2(L_i/L_i^0)$.

Significance

The result shows that the constants $L_i$ in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same $O(nR_1^2(x_0)/k)$ rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.

Difficulty

The analysis of RCDM rests on the one-step bound $f(x)-f(x-L_i^{-1}\nabla_if(x)e_i)\ge(\nabla_if(x))^2/(2L_i)$, which follows from the smoothness of $f$ along the coordinate line. For RACDM the step uses an estimate $\hat L_i$ that may be smaller than $L_i$, and then the same argument gives no decrease at all: a step that is too long can increase $f$. The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because $f$ is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.

Formalization scope

The formalization works with scalar coordinates ($N=n$, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed $0,\dots,n-1$. It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map $g=\nabla f$, wnorm L 1 and wnormDual L 1 are $\|\cdot\|_1$ and $\|\cdot\|_1^*$, and rcdExpect L 0 k is the expectation over $k$ uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over $\mathbb N$), one iteration, the run along an explicit sequence of draws, and the count $N_k$.

The following choices are made explicitly.

• Step 3 of (6.1) is printed "Set $L_{i_k}:=\frac12L_{i_k}$"; it is read as $\hat L_{i_k}:=\frac12\hat L_{i_k}$, as the paper's proof requires. The true constants $L_i$ never change and enter only hypotheses and bounds.
• $R_1(x_0)$ is not computed: the goal takes any $R$ with $\|x-y^*\|_1\le R$ for all $x$ in the level set and all minimizers $y^*$. "$X^*$ nonempty" is a hypothesis; "$X^*$ bounded" follows from the existence of $R$.
• Implicit hypotheses made explicit: $n\ge1$; $L_i^0>0$ and $L_i^0\le L_i$; in the milestones, $0<\hat L_i\le L_i$ on the entry state.
• Convexity is assumed in the statements that need it (the decreases and the rate); (6.4) and items 1 and 3 hold without it and are stated without it.
• $N_k$ counts $d_j+1$ evaluations of $\nabla_{i_j}f$ at iteration $j$ with $d_j$ doublings, the count the paper's proof uses; counting $\nabla_{i_j}f(x_j)$ as well would give $3(k+1)+\sum_i\log_2(L_i/L_i^0)$.

A trivializing encoding is ruled out: the loop count is the least $d$ at which the sign test fails (an arbitrary admissible $d$ would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants $L_i$, not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. Journal version: SIAM J. Optim. 22(2) (2012) 341–362. doi:10.1137/100802001
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (reference [6] of the paper; inequality (2.1.17)). doi:10.1007/978-1-4419-8853-9
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4) (2015) 231–357, §6.4. arXiv:1405.4980

Motivation

A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution acts as an algebraic input to the dynamics. The class contains linear complementarity systems, mechanical systems with unilateral contact and friction, dynamic Nash games and many hybrid engineering models. Pang and Stewart's paper (Math. Program. 113 (2008); author's version hal-01366027v1) set up a unified theory of such systems: existence of solutions, uniqueness, and convergence of numerical time-stepping schemes.

The numerical question is the practical one. A DVI is solved by discretizing time and solving one finite-dimensional variational inequality per step. Whether the discrete trajectories approximate a true solution as the step size shrinks is not automatic: the algebraic variable $u$ can switch discontinuously, so the discrete $u$'s need not converge pointwise. Section 7 of the paper answers this for a semi-implicit Euler scheme applied to the initial-value problem, and the answer is also an existence proof for the DVI.

Setting

Fix $T>0$ and write $\Omega=[0,T]\times\mathbb R^n$. Let $K\subseteq\mathbb R^m$ be a nonempty closed convex set, let $f:\Omega\to\mathbb R^n$, $B:\Omega\to\mathbb R^{n\times m}$, $G:\Omega\to\mathbb R^m$ and $F:\mathbb R^m\to\mathbb R^m$. For $\Phi:\mathbb R^m\to\mathbb R^m$, $\mathrm{SOL}(K,\Phi)$ is the set of $u\in K$ with $(u'-u)^{\mathsf T}\Phi(u)\ge0$ for all $u'\in K$. The initial-value DVI (6.2) is

$$\dot x=f(t,x)+B(t,x)u,\qquad x(0)=x^0,\qquad u\in\mathrm{SOL}(K,G(t,x)+F).$$

The standing assumptions are (A): $f$, $B$ and $G$ are Lipschitz continuous on $\Omega$ (for the metric $|t-t'|+\|x-x'\|$), and (B): $\sigma_B=\sup_\Omega\|B(t,x)\|<\infty$.

A weak solution is a pair $(x,u)$ with $x(0)=x^0$, $u$ integrable on $[0,T]$ with $u(t)\in K$ for almost every $t$, the integral equation $x(t)-x(s)=\int_s^t[f(\tau,x(\tau))+B(\tau,x(\tau))u(\tau)]\,d\tau$ for $0\le s\le t\le T$, and the integral form of the VI,

$$\int_0^T(\tilde u(t)-u(t))^{\mathsf T}[G(t,x(t))+F(u(t))]\,dt\ge0\quad\text{for every continuous }\tilde u:[0,T]\to K.$$

The time-stepping scheme (7.2) uses a step $h=T/N$, grid points $t_{h,i}=ih$, a parameter $\theta\in[0,1]$, and $x^{h,0}=x^0$:

$$x^{h,i+1}=x^{h,i}+h\big[f(t_{h,i+1},\theta x^{h,i}+(1-\theta)x^{h,i+1})+B(t_{h,i},x^{h,i})u^{h,i+1}\big],\quad u^{h,i+1}\in\mathrm{SOL}(K,G(t_{h,i+1},x^{h,i+1})+F),$$

for $i=0,\dots,N-1$. The iterates are turned into functions of time: $\hat x^h$ is the continuous piecewise linear interpolant of the $x^{h,i}$, and $\hat u^h$ is the piecewise constant interpolant equal to $u^{h,i+1}$ on $(t_{h,i},t_{h,i+1}]$.

Formalization targets

Goal: Theorem 7.1 (p. 44)

Suppose the iterates satisfy the uniform bounds (7.5),

$$\|x^{h,i+1}\|\le c_{0,x}+c_{1,x}\|x^0\|,\qquad\|u^{h,i+1}\|\le c_{0,u}+c_{1,u}\|x^0\|,$$

for all small $h$. Then along some $h_\nu\downarrow0$,

$$\hat x^{h_\nu}\to\hat x\ \text{uniformly on }[0,T],\qquad\hat u^{h_\nu}\rightharpoonup\hat u\ \text{weakly in }L^2(0,T).$$

If moreover (a) $F=\Psi\circ E$ with $\Psi$ Lipschitz and $\|Eu^{h,i+1}-Eu^{h,i}\|\le hc_{2,u}$ (7.6), or (b) $F(u)=Du$ with $D$ positive semidefinite, then every such limit pair $(\hat x,\hat u)$ is a weak solution of (6.2).

Milestones

The proof decomposes into the paper's own steps: Lemma 7.1 (the implicit Euler step is uniquely solvable, with the bounds (7.4)); the uniform step bound $\|x^{h,i+1}-x^{h,i}\|\le Lh$, which makes $\{\hat x^h\}$ equicontinuous; the fact that a weak $L^2$ limit of $K$-valued functions is $K$-valued almost everywhere; the integral VI (7.7) under (a); the integral equation (7.8); and the weak lower semicontinuity (7.9) of $u\mapsto\int_0^Tu^{\mathsf T}Du$ for positive semidefinite $D$, which handles (b).

Companion results

Lemma 7.2 (a discrete Gronwall bound giving (7.5) from one-step growth conditions), Lemma 7.3 ((7.5) from linear growth of the VI solutions) and Proposition 7.1 (existence of the iterates for small $h$) are included as further targets: together with Theorem 7.1 they reduce the hypotheses on the iterates to conditions on $(K,F)$.

Significance

Theorem 7.1 is simultaneously a convergence theorem for a practical numerical method and an existence theorem: any scheme with bounded iterates produces, in the limit, a weak solution of the DVI. Combined with Proposition 7.1 and Lemma 7.3 it yields existence for DVIs whose VI part has linearly growing solution sets, including linear complementarity systems with positive semidefinite $D$, without the upper-semicontinuity machinery of differential inclusions. Case (b) covers monotone linear complementarity systems, the class arising in passive electrical networks and frictionless contact.

The results are proved in the paper. None of them is machine-checked. A formalization would produce a reusable Lean account of Euler polygons, equicontinuity estimates for discrete schemes, and weak $L^2$ limits of constrained sequences, all of which recur in the numerical analysis of nonsmooth dynamical systems.

Difficulty

The obvious argument would pass to the limit in each step of the scheme pointwise. This fails because $\hat u^h$ has no pointwise or strong limit in general: only weak $L^2$ compactness is available. The nonlinear term $F(\hat u^h)$ does not commute with weak limits, so the variational inequality cannot be passed to the limit directly. Each of the two cases supplies the missing compactness or convexity: in (a) the bound (7.6) makes $E\hat u^h$ converge uniformly, and in (b) positive semidefiniteness makes the quadratic term weakly lower semicontinuous. Membership $\hat u(t)\in K$ also does not follow from pointwise reasoning and needs convexity of $K$.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin k), inner products $u^{\mathsf T}v$ are ⟪u, v⟫_ℝ, and matrices are continuous linear maps with the operator norm. $\mathrm{SOL}(K,\Phi)$ is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric.

Step sizes are $h=T/N$ with an integer $N\ge1$, so that the grid ends exactly at $T$. "For all $h\in(0,\bar h]$" becomes "for all $N\ge\bar N$", and "$h_\nu\downarrow0$" becomes a strictly increasing sequence of $N$'s. The iterates are a family indexed by $N$ and are hypotheses of the goal; their existence is the separate Proposition 7.1. Weak convergence in $L^2(0,T;\mathbb R^m)$ is tested against every $L^2$ function, and the uniform convergence of $\hat x^h$ is on all of $[0,T]$. Condition (7.6) is imposed for $1\le i\le N-1$, because the paper's convention $u^{h,0}\equiv u^{h,1}$ makes $i=0$ vacuous.

A weak solution carries integrability of both integrands as explicit conditions. Without them a non-integrable pair would satisfy the integral conditions vacuously, since a Lean integral of a non-integrable function is zero. The following readings are also excluded: convergence of the scheme only at grid points; a scheme in which $u^{h,i+1}$ solves the VI at $x^{h,i}$ instead of $x^{h,i+1}$; and a conclusion about one particular subsequence instead of every subsequence along which both limits exist.

A complete development needs: compactness in $C([0,T])$ (Arzelà–Ascoli), weak sequential compactness of bounded sets in $L^2$, Mazur's lemma on convex combinations, and estimates for piecewise linear and piecewise constant interpolants. The last two items are reusable for other time-stepping schemes. Proofs of any milestone, and of auxiliary interpolation lemmas, are welcome.

Out of scope: the weaker Carathéodory assumption (A′), the implicit scheme (7.3), the cited fixed-point theorems 7.2–7.3, and Theorem 7.4 (which combines Theorem 7.1 with the existence results of §6).

Selected references

• J.-S. Pang and D. E. Stewart, Differential variational inequalities, Mathematical Programming 113(2), 345–424, 2008. https://doi.org/10.1007/s10107-006-0052-x ; author's version hal-01366027v1, https://hal.science/hal-01366027v1
• F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543
• D. E. Stewart, Rigid-body dynamics with friction and impact, SIAM Review 42(1), 3–39, 2000. https://doi.org/10.1137/S0036144599360110

Motivation

Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely and successfully applied to nonsmooth functions. Lewis and Overton (Math. Program. 141 (2013) 135–163) study why. A quasi-Newton step needs a step length along each search direction, and on a nonsmooth function the usual line searches have to decide what to do at points where the function is not differentiable. Classical inexact line searches for nonsmooth optimization (Lemaréchal 1981, Wolfe 1975, Mifflin 1977) ask an oracle for a subgradient at such points. Lewis and Overton propose a simpler rule: a trial point at which the objective is not differentiable simply fails the Wolfe test. This mission formalizes the analysis of that line search, §4 of the paper: when an acceptable step exists, when the bisection search finds one, what happens when it does not, and how many trials it takes on a convex function.

Setting

Let $\bar x$ be an iterate of an optimization algorithm and $\bar p$ a search direction. The line search objective is $h(t)=f(\bar x+t\bar p)-f(\bar x)$ for $t\ge0$. Only $h$ enters the analysis.

Assumption 4.1. The function $h$ is absolutely continuous on every bounded interval and bounded below, and

$$h(0)=0,\qquad s=\limsup_{t\downarrow0}\frac{h(t)}{t}<0 .$$

The number $s$ plays the role of the directional derivative $\nabla f(\bar x)^T\bar p$.

Armijo and Wolfe conditions. Fix constants $c_1<c_2$ in $(0,1)$. For $t>0$,

$$A(t):\ h(t)<c_1st, \qquad W(t):\ h\text{ is differentiable at }t\text{ with }h'(t)>c_2s .$$

An Armijo–Wolfe step is a $t>0$ satisfying both.

Algorithm 4.6. Start from $\alpha=0$, $\beta=+\infty$, $t=1$. At each trial: if $A(t)$ fails, set $\beta\leftarrow t$; otherwise, if $W(t)$ fails, set $\alpha\leftarrow t$; otherwise stop. Then set $t\leftarrow(\alpha+\beta)/2$ if $\beta<+\infty$, and $t\leftarrow2\alpha$ otherwise. So the search doubles until $A$ fails and then bisects the bracket $[\alpha,\beta]$. Write $(\alpha_n,\beta_n,t_n)$ for the state before trial $n=0,1,2,\dots$ (lsRun), so $t_0=1$. The search terminates if some trial passes both tests (Terminates).

Formalization targets

Goal: Theorem 4.7 (convergence)

Under Assumption 4.1 and $0<c_1<c_2<1$:

1. a trial step that passes both tests is an Armijo–Wolfe step;
2. the search terminates under the condition

$$\lim_{t\uparrow\bar t}h'(t)\ \text{exists in }[-\infty,+\infty]\ \text{ for all }\bar t>0; \tag{4.8}$$

3. if the search does not terminate, then eventually the brackets $[\alpha_n,\beta_n]$ are finite, nested, halve in length at each trial and each contains a set of nonzero measure of Armijo–Wolfe steps, and they shrink to a step $\tilde t>0$ with

$$h(\tilde t)=c_1s\tilde t\qquad\text{and}\qquad\limsup_{t\uparrow\tilde t}h'(t)\ge c_2s. \tag{4.9}$$

Milestones

• Lemma 4.4. If $A$ holds at $\alpha>0$ and fails at $\beta>\alpha$, and $h$ is absolutely continuous on $[\alpha,\beta]$, then the Armijo–Wolfe steps in $[\alpha,\beta]$ have nonzero measure.
• Theorem 4.5. Under Assumption 4.1, the Armijo–Wolfe steps have nonzero measure.
• The bracket invariant (proof of Theorem 4.7, pp. 147–148). Without termination, eventually $0<\alpha_n$, $\beta_n<\infty$, $A(\alpha_n)$ holds and $A(\beta_n)$ fails.
• Weak lower semismoothness (pp. 148–149). If $h$ is weakly lower semismooth at every $\bar t>0$ and differentiable at every trial step, the search terminates.
• Proposition 4.11 (complexity on a convex function). For convex $h$ the Armijo–Wolfe steps are the points of differentiability in an open interval $I=(b,b+a)$, and with $d=\max\{1+\lfloor\log_2b\rfloor,0\}$ the search tries a step in $I$ after between $d+1$ and $d+1+\max\{d+\lfloor\log_2(1/a)\rfloor,0\}$ trials when $d\ge1$, and at most $1+\max\{1+\lfloor\log_2(1/a)\rfloor,0\}$ trials when $d=0$.

Significance

Theorem 4.7 is the convergence guarantee for the line search used by the BFGS implementation analysed in the rest of the paper. It isolates the only failure mode: a derivative that oscillates as $t$ increases to a limit point, which condition (4.8) excludes. The paper notes that (4.8) holds for every semi-algebraic $h$, so the search terminates on the functions met in practice. The same line search is the one whose trial sequence produces the binary-expansion behaviour of the secant method in §5. Theorem 4.5 shows that an acceptable step exists on a set of positive measure, which is why a sampling line search is not defeated by the null set of nondifferentiable points. Proposition 4.11 bounds the work per line search on convex functions.

All statements are proved in the paper. None has been formalized; there is no line search for nonsmooth functions on Prove2Me or in Mathlib. A formalization checks the measure-theoretic argument (absolute continuity and the fundamental theorem of calculus for Lebesgue integrals), the bookkeeping of the bisection, and the complexity count, where the printed upper bound turns out to be false for $b<1$.

Difficulty

The obvious proof of termination fails: on a nonsmooth function the bisection can land on a kink at every trial, and the paper's §4.2 constructs a convex $h$ where it does. Termination therefore cannot follow from Assumption 4.1 alone, and both the existence of acceptable steps and the convergence of the brackets have to be argued through measure: Lemma 4.4 needs the fundamental theorem of calculus for absolutely continuous functions and a supremum argument over almost-everywhere inequalities. The non-termination analysis has to combine the bracket invariant with Lemma 4.4 on every late bracket and with a limit argument for (4.9). The complexity bound needs a careful count of doubling and bisection trials, including the regime $b<1$ where no doubling occurs.

Formalization scope

The objective is h : ℝ → ℝ; only its values on $[0,\infty)$ enter. Lebesgue measure is volume with values in $[0,\infty]$, and "nonzero measure" is volume S ≠ 0. Limits superior and inferior are computed in EReal. The upper bound $\beta$ is in WithTop ℝ, with $\top=+\infty$. Stopping freezes the state of lsRun. Mathlib's deriv is $0$ at nondifferentiable points, so the Wolfe condition, condition (4.8) and (4.9) all state differentiability explicitly.

Deviations from the page, each disclosed in the item's Formalization Note:

• Lemma 4.4 adds the standing $0<c_1<c_2<1$ and $s<0$, which its statement omits and its proof uses.
• Condition (4.8) is read as differentiability on a left neighbourhood of $\bar t$ plus existence of the limit, as the proof on p. 148 uses it.
• (4.9) takes the $\limsup$ over points of differentiability left of $\tilde t$; an empty such set would give $-\infty$, so the bound is not vacuous.
• Weak lower semismoothness restricts the paper's subgradient sequences to derivatives at points of differentiability (no Clarke subdifferential in Mathlib). This weakens the hypothesis and strengthens the theorem; the paper's argument proves it unchanged.
• Proposition 4.11. The printed upper bound is false for $b<1$: for $s=-1$, $c_1=0.6$, $c_2=0.9$ and the convex piecewise linear $h$ with slopes $-1$ on $[0,\frac12]$ and $-0.2$ on $[\frac12,10]$, the interval is $I=(\frac12,1)$, the bound is $2$, and the search needs $3$ trials. The bound for $d=0$ is replaced by $1+\max\{1+\lfloor\log_2(1/a)\rfloor,0\}$. The case $a=+\infty$ cannot occur under Assumption 4.1, and a trial at a kink inside $(b,b+a)$ counts as reaching $I$.

Algorithm 4.6 is encoded as the literal state machine; a definition of the search as "some Armijo–Wolfe step" or as an arbitrary nested sequence of brackets would make the goal trivial and is ruled out. The Wolfe condition includes differentiability; without it every kink would pass, since $0>c_2s$.

A complete development needs absolute continuity (AbsolutelyContinuousOnInterval, with almost-everywhere differentiability and the fundamental theorem of calculus, both in Mathlib), the mean value theorem, and facts about one-sided derivatives of convex functions. Lemma 4.4 and the bracket invariant are reusable for other bracketing line searches. Contributions of the milestones in order, of proofs of the definitions' basic properties (all trial steps are positive, the brackets are monotone), and of the §4.2 non-termination example are welcome.

Selected references

• A. S. Lewis, M. L. Overton, Nonsmooth optimization via quasi-Newton methods, Math. Program. Ser. A 141 (2013) 135–163. https://doi.org/10.1007/s10107-012-0514-2
• C. Lemaréchal, A view of line-searches, in: Optimization and Optimal Control, Lecture Notes in Control and Information Sciences 30, Springer, Berlin, 1981, pp. 59–78 (reference [26] of the paper).
• P. Wolfe, A method of conjugate subgradients for minimizing nondifferentiable functions, Math. Programming Study 3 (1975) 145–173 (reference [51] of the paper).
• R. Mifflin, An algorithm for constrained optimization with semismooth functions, Math. Oper. Res. 2 (1977) 191–207. https://doi.org/10.1287/moor.2.2.191

Motivation

A differential variational inequality (DVI) couples an ordinary differential equation for a state $x(t)$ with a finite-dimensional variational inequality that the algebraic variable $u(t)$ must solve at every instant. The class contains complementarity systems from contact mechanics and electrical circuits with diodes, linear complementarity systems from control theory, differential Nash games, and the first-order optimality conditions of optimal control problems with inequality constraints. J.-S. Pang and D. E. Stewart introduced the unified framework in Differential variational inequalities, Math. Program. 113 (2008) (author's version, hal-01366027), and Section 6 of that paper settles the first question any such model raises: when does the initial-value problem have a solution on a whole prescribed time interval?

Before this work, existence results for these systems were tied to special structure: linear complementarity systems with "minimal" and "passive" data, or a given initial condition compatible with the complementarity kernel. Theorem 6.1 gives existence for every initial state under five separate conditions on the variational inequality, each describing a different class of DVIs.

Setting

Fix $T>0$ and write $\Omega=[0,T]\times\mathbb R^n$. For a set $K\subseteq\mathbb R^m$ and a map $\Phi:\mathbb R^m\to\mathbb R^m$, the variational inequality $\mathrm{VI}(K,\Phi)$ asks for $u\in K$ with $(u'-u)^T\Phi(u)\ge0$ for all $u'\in K$; its solution set is $\mathrm{SOL}(K,\Phi)$. The initial-value DVI studied here is

$$\dot x=f(t,x)+B(t,x)u,\qquad x(0)=x^0,\qquad u\in\mathrm{SOL}\big(K,\,G(t,x)+F(\cdot)\big),\qquad(6.2)$$

with $K\subseteq\mathbb R^m$ nonempty, closed and convex, $f:\Omega\to\mathbb R^n$, $B:\Omega\to\mathbb R^{n\times m}$, $G:\Omega\to\mathbb R^m$ and $F:\mathbb R^m\to\mathbb R^m$. Two standing assumptions hold throughout: (A) $f$, $B$, $G$ are Lipschitz continuous on $\Omega$; (B) $B$ is bounded on $\Omega$ in operator norm.

A pair $(x,u)$ is a weak solution (in the sense of Carathéodory) on $[0,T]$ if $x(0)=x^0$; $u$ is integrable on $[0,T]$ with $u(t)\in K$ almost everywhere; $x(t)-x(s)=\int_s^t\big(f(\tau,x(\tau))+B(\tau,x(\tau))u(\tau)\big)\,d\tau$ for $0\le s\le t\le T$, with an integrable integrand; and for every continuous $\tilde u:[0,T]\to K$,

$$\int_0^T(\tilde u(t)-u(t))^T\big(G(t,x(t))+F(u(t))\big)\,dt\ \ge\ 0,\qquad(2.4)$$

with an integrable integrand. The existence proof passes through the differential inclusion $\dot x\in\mathbf F(t,x)$ with the set-valued right-hand side

$$\mathbf F(t,x)=\{f(t,x)+B(t,x)u:\ u\in\mathrm{SOL}(K,G(t,x)+F)\}.\qquad(6.4)$$

Further objects: the recession cone $K_\infty$; the dual cone $C^*=\{v:u^Tv\ge0\ \forall u\in C\}$; the VI kernel $\mathcal K(K,D)$, the solution set of $K_\infty\ni v\perp Dv\in(K_\infty)^*$; an R₀ pair $(K,D)$, one with $\mathcal K(K,D)=\{0\}$; a psd-plus matrix $D$, one with $u^TDu\ge0$ for all $u$ and $u^TDu=0\Rightarrow Du=0$; and the linear growth property

$$\sup\{\|u\|:u\in\mathrm{SOL}(K,q+F)\}\le\rho(1+\|q\|).\qquad(6.5)$$

Formalization targets

Goal: Theorem 6.1

Under (A) and (B), if any one of the following holds, then (6.2) has a weak solution on $[0,T]$ for every $x^0\in\mathbb R^n$:

• (a) $F$ continuous and monotone, and $\liminf_{u\in K,\|u\|\to\infty}(u-u^{\mathrm{ref}})^TF(u)/\|u\|^2>0$ for some $u^{\mathrm{ref}}\in K$ (6.6);
• (b) $F=E^T\circ\Psi\circ E$ with $K_\infty\cap\ker E=\{0\}$ and $\Psi$ continuous and strongly monotone on $EK$;
• (c) $0\in K$, $F(u)=Du$ with $D$ positive semidefinite and $(K,D)$ an R₀ pair;
• (d) $K$ a polyhedron containing $0$, $F(u)=Du$ with $D$ positive semidefinite, and $G(\Omega)\subseteq\operatorname{int}\mathcal K(K,D)^*$;
• (e) $K$ a polyhedron containing the origin or no lines, $F=D+\Phi$ with $D$ psd-plus, $(K,D)$ an R₀ pair, and $\Phi$ continuous with $\|\Phi(u)\|\le L_\Phi\|u\|$ (6.10) and $\|\Phi(u)-\Phi(u')\|\le L'_\Phi\|Du-Du'\|$ (6.12) on $K$, for small enough $L_\Phi$, $L'_\Phi$.

Milestones

• Lemma 6.1 (Deimling): an upper semicontinuous differential inclusion with nonempty closed convex values and linear growth has a weak solution on $[0,T]$.
• Lemma 6.2: (6.5) on $G(\Omega)$ makes $\mathbf F$ grow linearly, with constant $\rho_f+\rho\sigma_B(1+\rho_G)$, and upper semicontinuous.
• Lemma 6.3 (Filippov): a measurable selection lemma.
• Proposition 6.1: a weak solution of the inclusion yields a weak solution of the DVI.
• Propositions 6.2–6.5: nonemptiness, convexity and linear growth of the static VI solution sets under (a), (b), (c)–(d), and (e) respectively; Proposition 6.5 carries the explicit bounds $\rho(1+\|q\|)/(1-\rho L_\Phi)$ (6.11) and $L_V\|q^1-q^2\|/(1-L_VL'_\Phi)$ (6.13).

Significance

Theorem 6.1 is the existence result behind the rest of the paper: Sections 7 and 8 prove that time-stepping schemes converge to weak solutions of (6.2), and those results are informative only for problems that have solutions. Condition (d) gives existence for every initial state of linear complementarity systems $\dot x=p+Ax+Bu$, $\mathcal C\ni u\perp q+Cx+Du\in\mathcal C^*$ with $q+C\mathbb R^n\subseteq\operatorname{int}\mathcal K(\mathcal C,D)^*$, where earlier results required passivity or a compatible initial state. Propositions 6.2–6.5 are results on static variational inequalities in their own right: the linear growth of solution sets in the data had not been a focus of VI theory.

The result is proved in the paper, modulo two cited theorems (Deimling's existence theorem for convex-valued differential inclusions and Filippov's measurable selection lemma). None of it is formalized. A Lean development would supply set-valued upper semicontinuity, Carathéodory solutions of differential inclusions, and existence and linear growth theory for VIs on closed convex and polyhedral sets: material with uses well beyond this paper.

Difficulty

The obvious route, solving the VI for $u$ as a function of $(t,x)$ and substituting into the ODE, fails: the solution map $(t,x)\mapsto\mathrm{SOL}(K,G(t,x)+F)$ is in general set-valued and discontinuous, so the resulting right-hand side is neither single-valued nor continuous, and classical ODE existence does not apply. The detour through the differential inclusion (6.4) requires convex values, which hold when $F$ is monotone but must be proved separately in case (e), where $F=D+\Phi$ is not monotone. It also requires linear growth (6.5), which for unbounded $K$ is a genuine statement about the asymptotics of VI solutions and needs a different argument under each of the five conditions: coercivity, a recession-cone condition, the VI kernel, or a fixed-point argument on polyhedra. Finally, Deimling's theorem and Filippov's lemma are substantial results of set-valued analysis that are not in Mathlib.

Formalization scope

Points of $\mathbb R^k$ are EuclideanSpace ℝ (Fin k); matrices are continuous linear maps, $\|B(t,x)\|$ is the operator norm and $E^T$ the adjoint. Data on $\Omega$ are curried functions on $\mathbb R\times\mathbb R^n$ of which only the values on $[0,T]\times\mathbb R^n$ matter, and Lipschitz continuity on $\Omega$ uses the metric $|t-t'|+\|x-x'\|$. $\mathrm{SOL}(K,\Phi)$ is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric. "Monotone" in (a) and Proposition 6.2 means monotone on $K$. The coercivity (6.6) is written in the equivalent form "$(u-u^{\mathrm{ref}})^TF(u)\ge c\|u\|^2$ for $u\in K$ with $\|u\|\ge R$". Upper semicontinuity is the open-neighbourhood form relative to $\Omega$. In Proposition 6.4 (b) the Lipschitz property is stated on the dual cone $\mathcal K(K,D)^*$, where the paper's proof establishes it (the statement prints $\mathcal K(K,D)$). Nonemptiness of $K$, the paper's standing assumption on variational inequalities, is a hypothesis throughout.

The weak-solution definitions carry explicit integrability conditions on the integrands of the integral equation and of (2.4), and (2.4) is required for every continuous $\tilde u$ with values in $K$. A definition without those integrability conditions (a Lean integral of a non-integrable function is zero), a variational condition tested only on constant $\tilde u$, or (A)–(B) replaced by global boundedness of $f$ and $G$ would make the goal a different and weaker statement; none of these is used.

Contributions welcome at every level: proofs of the milestones, a general theory of upper semicontinuous set-valued maps and Carathéodory solutions of differential inclusions, and existence results for variational inequalities via recession cones and degree theory.

Selected references

• J.-S. Pang, D. E. Stewart, Differential variational inequalities, Mathematical Programming 113(2), 345–424, 2008. https://doi.org/10.1007/s10107-006-0052-x; author's version https://hal.science/hal-01366027
• K. Deimling, Multivalued Differential Equations, de Gruyter, 1992. https://doi.org/10.1515/9783110874228
• A. F. Filippov, On certain questions in the theory of optimal control, SIAM J. Control 1(1), 76–84, 1962. https://doi.org/10.1137/0301005
• F. Facchinei, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

Motivation

A manufacturer must commit to production before a retailer knows how much it will buy. In practice the retailer sends a forecast first, and the manufacturer plans against it. When the forecast binds neither party, the retailer has no reason to report it honestly, and the manufacturer has no reason to plan for the market rather than for its own margin. Purchasing managers have described this to Tsay directly, and Lee, Padmanabhan and Whang (1997) document such "phantom ordering" in several case studies.

A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives (Management Science, 1999), models the situation as a two-stage newsvendor game with a demand-information update between production and purchase. Its first result, Proposition 1, is the benchmark the rest of the paper builds on. Even when both parties share the same beliefs about demand, a linear transfer price alone leaves the manufacturer underproducing relative to a central planner, and the supply chain loses expected profit, for every transfer price. That inefficiency motivates the quantity flexibility (QF) contract studied in the remainder of the paper and in the companion mission of this series.

Setting

Costs. The retail price is $p$ and the unit transfer price paid by the retailer to the manufacturer (the EM) is $c$. The unit production cost is $m$, the unit salvage value is $u$ (the same for either party), and the unit goodwill loss on unmet demand is $s$. The paper's standing assumptions (§3.1, p. 1344) are

$$p > c > m > 0,\qquad u < m,\qquad s \ge 0 .$$

Three critical fractiles recur:

$$\kappa_R = \frac{p+s-c}{p+s-u},\qquad \kappa_{EM} = \frac{c-m}{c-u},\qquad \kappa_S = \frac{p+s-m}{p+s-u}.$$

Demand (§3.3). Market demand is $X = \mu + \varepsilon$. The signal $\mu$ has distribution function $\Theta$, which is differentiable and strictly increasing, and finite variance. The error $\varepsilon \sim N(0,\sigma_\varepsilon^2)$ is independent of $\mu$. $F$ is the distribution function of $X$, $\Phi$ is the standard normal distribution function, and $z_\varepsilon = \Phi^{-1}(\kappa_R)$.

Timing (§3.2). The EM produces $Q$ knowing only the prior. Then $\mu$ is observed and the retailer buys $r \le Q$. Then $X$ is realized, and both parties salvage their surplus. Given $\mu$, the retailer's expected profit from purchase $r$ is

$$G(r\mid\mu) = E_{X\mid\mu}\{p\min[X,r] - c\,r - s[X-r]^+ + u[r-X]^+\}. \tag{1}$$

Without commitment the retailer buys $r^*_{NC}(Q,\mu) = \min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$. The EM's expected profit is

$$\pi_{EM,NC}(Q) = (c-u)\,E_\mu\, r^*_{NC}(Q,\mu) - (m-u)\,Q,$$

and the retailer's is $\pi_{R,NC}(Q) = E_\mu\, G(r^*_{NC}(Q,\mu)\mid\mu)$. A central planner producing $Q$ before the signal earns

$$\Pi_{CC}(Q) = E_X\{p\min[X,Q] - s[X-Q]^+ + u[Q-X]^+\} - mQ .$$

Formalization targets

Goal: Proposition 1 (p. 1347)

Let $Q^*_{NC}$ maximize $\pi_{EM,NC}$ and $Q^*_{CC}$ maximize $\Pi_{CC}$. Then, for every transfer price $c$ admitted by the standing assumptions,

$$Q^*_{NC} < Q^*_{CC}\qquad\text{and}\qquad \pi_{R,NC}(Q^*_{NC}) + \pi_{EM,NC}(Q^*_{NC}) < \Pi_{CC}(Q^*_{CC}).$$

Milestones

1. §4, p. 1345. The centralized optimum exists and is unique:

$$Q^*_{CC} = F^{-1}\!\left(\frac{p+s-m}{p+s-u}\right).$$

2. §5.1, (1), p. 1346. The closed form

$$G(r\mid\mu) = (p+s-c)r - s\mu - (p+s-u)E_{X\mid\mu}[r-X]^+ ,$$

and the retailer's optimal purchase under $r \le Q$ is $\min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$. 3. §5.2, p. 1347. The EM's optimal production exists and is unique:

$$Q^*_{NC} = \Theta^{-1}\!\left(\frac{c-m}{c-u}\right) + z_\varepsilon\sigma_\varepsilon .$$

Significance

Proposition 1 shows that sharing demand information does not remove inefficiency. Under common beliefs and with no commitment, no linear transfer price makes the decentralized chain efficient. Adjusting $c$ moves profit between the parties but cannot recover the planner's expected profit. This is the reason the paper studies richer contracts, and the efficiency result for the QF contract (the paper's Proposition 6) is measured against the benchmark $Q^*_{CC}$ defined here.

The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development therefore supplies arguments the published record does not contain. It also exhibits the exact hypotheses the result needs. In particular it covers the degenerate case $\sigma_\varepsilon = 0$, where the signal is perfect. No part of this mission has a prior formal proof. Newsvendor critical-fractile results exist on Prove2Me for single-decision models, but without the production stage and information update used here.

Difficulty

The EM and the planner solve newsvendor problems against different demand laws. The EM faces the retailer's purchase $\mu + z_\varepsilon\sigma_\varepsilon$, while the planner faces $X = \mu + \varepsilon$. Their fractiles are $\kappa_{EM}$ and $\kappa_S$. The obvious comparison, $\kappa_{EM} < \kappa_S$, settles the case $\sigma_\varepsilon = 0$ only. For $\sigma_\varepsilon > 0$ the two quantities are inverse distribution functions of different random variables. $z_\varepsilon$ may be negative, and the planner's distribution is a convolution. A comparison of fractiles alone therefore does not order $Q^*_{NC}$ and $Q^*_{CC}$. The strict profit gap also needs more than optimality of $Q^*_{CC}$: it requires comparing the decentralized system profit at $Q^*_{NC}$ with the planner's profit at the same production, and then using uniqueness of the planner's optimum.

The analytic infrastructure is also substantial. It includes differentiating expectations of piecewise-linear functions under a Gaussian law and under a general prior, continuity and strict monotonicity of a convolution's distribution function, and existence of a root of $F(Q) = \kappa_S$.

Formalization scope

All objects live in the namespace TsayQF.NoCommit, in one definitions file Model.

• Costs are a structure Data with fields $p, c, m, u, s \in \mathbb R$ and the standing assumptions (i)–(iii) as fields. "For any $c$" is quantification over all Data. No sign is imposed on $u$.
• The prior is a probability measure ν on ℝ; $\Theta$ is cdf ν. "Differentiable and invertible" is Differentiable ℝ (cdf ν) together with StrictMono (cdf ν), and "mean and variance" is MemLp id 2 ν.
• The error variance is v : ℝ≥0, so $\sigma_\varepsilon = \sqrt v$ and v = 0 is allowed. The law of $X$ is the pushforward of ν.prod (gaussianReal 0 v) under addition, and given $\mu$ demand has law gaussianReal μ v.
• Inverse distribution functions are not Lean functions here. $z_\varepsilon$ is a real z with hypothesis cdf (gaussianReal 0 1) z = kR D. The milestones state existence of a solution of each fractile equation and characterize the maximizers by it.
• Expectations are Bochner integrals. Finite variance of $\mu$ makes every integrand integrable, so no expectation silently defaults to zero.
• Optimality is IsMaxOn over Set.univ for productions and over Set.Iic Q for the purchase. Productions range over $\mathbb R$; the paper's presumption that $\mu$ and $X$ are almost certainly nonnegative is not imposed, because no result here needs it.
• The goal quantifies over arbitrary maximizers. Milestones 1 and 3 show that maximizers exist, so the goal is not vacuous. A sorry-free sanity file checks the paper's §8 data $(p,c,m,u,s) = (15,10,6,3,0)$ and shows that a normal prior satisfies the hypotheses on $\Theta$.

The goal must not be weakened to non-strict inequalities, and the EM's demand must remain the retailer's purchase $\min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$, not market demand. Either change trivializes the result or changes it. Reusable pieces are the newsvendor critical-fractile characterization for a general continuous strictly increasing distribution, and monotonicity and continuity of the distribution function of a sum of independent variables with one Gaussian summand. Proofs of the milestones as standalone lemmas are welcome.

Selected references

• A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
• H. L. Lee, V. Padmanabhan, S. Whang, The Bullwhip Effect in Supply Chains, Sloan Management Review 38(3):93–102, 1997. https://sloanreview.mit.edu/article/the-bullwhip-effect-in-supply-chains/
• A. V. Iyer, M. E. Bergen, Quick Response in Manufacturer-Retailer Channels, Management Science 43(4):559–570, 1997. https://doi.org/10.1287/mnsc.43.4.559
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7

Motivation

Minimizing the sum of the $k$ largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and $f_k$ is differentiable at $B$ exactly when $\lambda_k(B)>\lambda_{k+1}(B)$; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.

The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point $X$ of $\{X\succeq0: A_i\bullet X=b_i,\ i\le m\}$ satisfies $\operatorname{rank}X(\operatorname{rank}X+1)/2\le m$. This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.

Setting

$\mathcal S^n$ is the space of real symmetric $n\times n$ matrices, $X\succeq0$ means $X$ is symmetric positive semidefinite, and $A\bullet B=\sum_{i,j}a_{ij}b_{ij}$. For $B\in\mathcal S^n$, $\lambda_1(B)\ge\dots\ge\lambda_n(B)$ are its eigenvalues and, for $k\in\{1,\dots,n\}$,

$$f_k(B)=\lambda_1(B)+\dots+\lambda_k(B).$$

The multiplicity $\operatorname{mult}(\lambda_i(B))$ is the largest $p\ge1$ with $\lambda_j(B)=\dots=\lambda_{j+p-1}(B)$ for some $j\le i\le j+p-1$.

A face of a convex set $S$ is a convex $F\subseteq S$ such that $x\in F$, $y,z\in S$, $x=\tfrac12(y+z)$ imply $y,z\in F$; an extreme point is a one-point face; $\dim S$ is the maximal number of affinely independent points of $S$, minus one. Write $t(i)=i(i+1)/2$ and

$$\tau(l,r,s)=\max\{\,i+j:\ t(i)+t(j)\le l,\ i\le r,\ j\le s\,\}.$$

Let $A_0,A_1,\dots,A_m\in\mathcal S^n$ be linearly independent, $A(x)=A_0+\sum_{i=1}^mx_iA_i$, and assume $m\ge1$ and $k<n$ (the standing assumptions of §4). The affine eigenvalue problem is

$$(EV_k)\qquad\min\{f_k(A(x)):\ x\in\mathbb R^m\},$$

and $\Theta$ denotes its set of optimal solutions, a closed convex set. For $B\in\mathcal S^n$ the semidefinite program

$$\min\ kz+I\bullet V\quad\text{s.t.}\quad V,W\succeq0,\quad zI+V-W=B \tag{3.14}$$

has optimal value $f_k(B)$; $\Omega_k(B)$ is its set of optimal solutions $(z,V,W)$.

Formalization targets

Goal: Theorem 4.3

If $x^*$ is an extreme point of $\Theta$ and $m>k(n-k)$, then

$$\lambda_k(A(x^*))=\lambda_{k+1}(A(x^*))\qquad\text{and}\qquad \operatorname{mult}(\lambda_k(A(x^*)))\ \ge\ n-\tau\big(t(n)-m-1,\,k-1,\,n-k-1\big).$$

Milestones

1. Theorem 2.1: on a face $F$ of the primal feasible set, $t(\operatorname{rank}X)\le m+\dim F$; on a face $G$ of the dual feasible set, $t(\operatorname{rank}Z)\le t(n)-m+\dim G$.
2. Theorem 2.2: the multi-block version $\sum_jt(\operatorname{rank}X_j)\le m-q+\dim G$ for programs with $p$ semidefinite blocks and $q$ free variables.
3. Lemmas 3.1, 3.2 and Theorem 3.3: the optimal value of (3.14) and an explicit description of $\Omega_k(B)$ through an eigendecomposition $B=Q\operatorname{Diag}(\lambda)Q^T$.
4. The rank identity of §3: $\operatorname{rank}V+\operatorname{rank}W+\operatorname{mult}(\lambda_k(B))=n$ on $\Omega_k(B)$ when $\lambda_k(B)=\lambda_{k+1}(B)$.
5. Lemma 4.2 and (4.31): $\{x^*\}\times\Omega_k(A(x^*))$ is a face of the feasible set of the lifted SDP (4.26), of dimension $1$ or $0$ according as $\lambda_k>\lambda_{k+1}$ or $\lambda_k=\lambda_{k+1}$.
6. Lemma 4.1: $\Theta$ contains no line, so it has extreme points whenever it is nonempty.

Significance

The theorem says that once the number of free parameters $m$ exceeds $k(n-k)$, the $k$-th and $(k+1)$-st eigenvalues necessarily coincide at extreme optimal solutions, so $f_k\circ A$ is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential $\partial f_k(A(x^*))$, which is $t(\operatorname{mult}(\lambda_k))$. The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.

The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of $f_k$, nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum $f_k$, and the multiplicity bound itself.

Difficulty

Extremality of $x^*$ in $\Theta$ is a statement in the parameter space $\mathbb R^m$ and gives no direct information on the spectrum of $A(x^*)$: perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where $f_k$ is not differentiable. The quantitative bound (4.30) also needs more than the optimal value $f_k(A(x^*))$: it depends on the whole optimal set $\Omega_k(A(x^*))$, on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal $V,W$ to the multiplicity of $\lambda_k$. None of these (faces and dimension of spectrahedra, the semidefinite representation of $f_k$, eigenvalue run lengths) is in Mathlib.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $A\bullet B$ is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and $\lambda_i(B)$ is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with $\dim\emptyset=-1$. All rank bounds are compared in $\mathbb Z$. $\Theta$ is the argmin set $\{x: f_k(A(x))\le f_k(A(y))\ \forall y\}$ and $\Omega_k(B)$ is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.

Hypotheses added relative to the page, each disclosed in its item: $1\le k<n$ in the statements of §3, which mention $\lambda_{k+1}$; $k\ge1$ (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and $\lambda_k(B)=\lambda_{k+1}(B)$ in the rank identity of p. 348, which is false as printed when $\lambda_k(B)>\lambda_{k+1}(B)$ ($n=2$, $k=1$, $B=\operatorname{diag}(2,0)$ gives $3\ne2$) and is used in the paper only in the equal case. The linear independence of $A_0,\dots,A_m$ is kept with $A_0$ included, as on p. 348.

Trivializing formalizations are ruled out: $\Theta$ is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk $0$, $\operatorname{mult}$ is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.

A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of $f_k$ with its optimal set, and convexity facts on $\Theta$. Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.

Selected references

• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23(2), 339–358, 1998. https://doi.org/10.1287/moor.23.2.339
• A. I. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13, 189–202, 1995. https://doi.org/10.1007/BF02574037
• M. L. Overton and R. S. Womersley, Optimality conditions and duality theory for minimizing sums of the largest eigenvalues of symmetric matrices, Mathematical Programming 62, 321–357, 1993. https://doi.org/10.1007/BF01585173
• F. Alizadeh, Interior point methods in semidefinite programming with applications to combinatorial optimization, SIAM Journal on Optimization 5(1), 13–51, 1995. https://doi.org/10.1137/0805002
• A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 149–190, 1996. https://doi.org/10.1017/S0962492900002646
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.