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

Quasi-Newton methods on nonsmooth functions

Quasi-Newton methods, BFGS above all, are the standard tool for smooth unconstrained minimization. They are also used directly on nonsmooth functions, where in practice they often converge to stationary points with linearly converging function values; the paper documents applications such as the design of low-order controllers (Lewis–Overton 2013, abstract and §1). Theory lags behind: as Lukšan and Vlček wrote, quoted on p. 136, "no global convergence has been proved for standard variable metric methods applied to nonsmooth problems". Methods with proved convergence modify quasi-Newton steps with bundle ideas; the unmodified method remains unexplained.

Lewis and Overton isolate the simplest nonsmooth case in which a complete analysis is possible: the Euclidean norm in the plane, minimized by any quasi-Newton method with an exact line search. The norm is differentiable everywhere except at its minimizer, so the method is well defined until it reaches the solution, yet the function is genuinely nonsmooth at the point the iterates approach. This mission formalizes that analysis (§3.1 of the paper).

Setting

Write $\|x\| = \sqrt{x^Tx}$ for the Euclidean norm of $x \in \mathbb R^2$ and $f(x) = \|x\|$. For $x \neq 0$, $f$ is differentiable with gradient $\nabla f(x) = \|x\|^{-1}x$; at $x = 0$ it is not differentiable.

A quasi-Newton method (Algorithm 2.1 of the paper) starts from $x_0 \neq 0$ and a symmetric positive definite matrix $H_0$. At iteration $k = 0, 1, \dots$ it

1. sets the search direction $p_k = -H_k\nabla f(x_k)$;
2. sets $x_{k+1} = x_k + t_kp_k$, where $t_k > 0$ is chosen by a line search;
3. stops if $f$ is not differentiable at $x_{k+1}$ or $\nabla f(x_{k+1}) = 0$;
4. otherwise sets $y_k = \nabla f(x_{k+1}) - \nabla f(x_k)$ and chooses any symmetric positive definite $H_{k+1}$ satisfying the secant condition $H_{k+1}y_k = t_kp_k$.

The line search is exact: $t_k$ minimizes $t \mapsto \|x_k + tp_k\|$. For the norm, the method stops exactly when some iterate equals $0$; "the algorithm does not terminate" means $x_k \neq 0$ for every $k$. The BFGS update (2.2) is one particular choice of $H_{k+1}$.

Two plane notions describe the motion of the iterates: the unsigned angle $\angle(u,v) = \arccos\big(u^Tv/(\|u\|\|v\|)\big) \in [0,\pi]$, and the orientation sign of $\operatorname{cross}(u,v) = u_1v_2 - u_2v_1$, positive when $v$ is a counterclockwise turn of $u$. A real sequence $\tau_k$ converges to $\mu$ Q-linearly with rate $r$ when $\tau_k \to \mu$ and $|\tau_{k+1}-\mu|/|\tau_k-\mu| \to r$ (p. 141). Finally, $\theta_k$ denotes the angle between $p_k$ and $-x_k$.

Formalization targets

Goal: Theorem 3.2 (p. 142)

For every non-terminating run of the method above, with any positive definite secant updates,

$$\frac{\|x_{k+1}\|}{\|x_k\|} \to \frac12,\qquad \|x_k\|\to 0,\qquad \angle(x_k,x_{k+1}) \to \frac{\pi}{3},$$

and there is $\sigma \in \{1,-1\}$ with $\sigma\operatorname{cross}(x_k,x_{k+1}) > 0$ for all large $k$: the iterates eventually rotate in one consistent direction.

Milestones

1. Proposition 3.1 (p. 141): for a general $f$ in $\mathbb R^n$, if $t_k$ is a local minimizer along the line and $f$ is differentiable at $x_{k+1}$, then $p_{k+1}^Ty_k = 0$.
2. One exact step (p. 142, the display for $x_{k+1}$): with $x^+ = x + tp$ the exact step, $0<\theta<\pi/2$, $\|x^+\| = \|x\|\sin\theta$, $\angle(x,x^+) = \pi/2-\theta$, and $x^+$ lies on the side of $p$.
3. The angle recursion (p. 142): $\sin\theta_{k+1} = \sqrt{(1-\sin\theta_k)/2}$.
4. The contraction (p. 142): $s\mapsto\sqrt{(1-s)/2}$ maps $[0,1]$ onto $[0,1/\sqrt2]$, is a contraction there, and its iterates tend to $1/2$.
5. Proposition 3.3 (p. 143): BFGS from $x_0 = [1;0]$, $H_0 = \begin{bmatrix}3&-\sqrt3\\-\sqrt3&3\end{bmatrix}$ never stops and gives exactly $x_k = 2^{-k}[\cos(k\pi/3);\sin(k\pi/3)]$.

Significance

Theorem 3.2 is a complete convergence-rate analysis of unmodified quasi-Newton methods on a function that is nonsmooth at its minimizer. It shows that the observed linear convergence is not an artefact of a particular update: the rate $1/2$ and the turn $\pi/3$ are forced by the exact line search and the secant condition alone, for every positive definite secant update. Proposition 3.3 shows that both constants are attained exactly by BFGS, so the theorem cannot be improved. The paper's experiments for $n > 2$ (§3.2, p. 143) suggest similar behaviour, with observed rates growing with $n$, and the authors state that they do not know how to extend the analysis; a formal two-dimensional analysis is the natural base for any attempt in higher dimension.

As far as we know none of these results has a machine-checked proof. A formalization would contribute the first verified statements about quasi-Newton iterations on a nonsmooth function, a reusable form of the exact-line-search orthogonality (Proposition 3.1, valid for any $f$ in any dimension), and an explicit, checked BFGS run in closed form.

Difficulty

The analysis rests on rotating and scaling so that $x_k = [1;0]$, after which every quantity is an explicit trigonometric expression. In a formal setting this "without loss of generality" is not free: one must show that the exact step, the angles, the secant condition and the next direction all transform correctly under rotations and scalings, or carry out the computation in invariant form. The direction $p_{k+1}$ is only known up to sign from Proposition 3.1; fixing the sign requires positive definiteness of $H_{k+1}$. The orientation claim is the most delicate part: the paper argues it from approximate values for large $k$, which has to become an exact sign argument that holds eventually. Proposition 3.3 needs an induction through the BFGS formula with exact arithmetic in $\sqrt3$, including that each updated matrix stays positive definite.

Formalization scope

Vectors are Fin 2 → ℝ (or Fin n → ℝ in Proposition 3.1) and matrices Matrix (Fin 2) (Fin 2) ℝ. The Euclidean norm is written out as $\sqrt{x^Tx}$, since Lean's default norm on Fin 2 → ℝ is the sup norm; with the sup norm every statement would change meaning. The gradient of the norm is the explicit formula $\|x\|^{-1}x$. Positive definiteness is Matrix.PosDef, which includes symmetry (Proposition 3.1 needs it). A run is the predicate IsExactNormRun: $x_0\neq0$, positive definite $H_k$, $t_k>0$, exact steps minimizing over all real $t$ (equivalent to $t>0$ here, because $p_k$ is a descent direction), and the secant condition whenever the method has not stopped. Non-termination is the separate hypothesis $x_k\neq0$ for all $k$. Q-linear convergence of the vectors is read through the real sequence $\|x_k\|$, following the proof's last line. Angles are unsigned and orientation is the sign of cross; "consistent orientation" is an eventual sign, not a limit of signed angles.

Corrections relative to the printed text, each disclosed in the item's Formalization Note:

• Proposition 3.3 says the iterates rotate clockwise; they rotate counterclockwise ($x_1 = [1/4;\sqrt3/4]$), and the Lean states the counterclockwise formula.
• The proof of Theorem 3.2 says "the angle $\theta_k$ approaches $\pi/3$"; in fact $\theta_k\to\pi/6$ and the turn $\pi/2-\theta_k$ tends to $\pi/3$. No item states a limit for $\theta_k$.
• The remark before Theorem 3.2 that termination "can happen only if $H_{k-1}$ is a multiple of the identity" is false ($H_0 = \operatorname{diag}(1,2)$, $x_0=[1;0]$ gives $x_1 = 0$) and is not formalized.
• The display for $x_{k+1}$ is a normalized form; its milestone states the invariant content for arbitrary $x\neq0$.

A trivializing formalization is ruled out: the run predicate keeps positive definiteness and exactness (without them $p_k$ may be an ascent direction and Theorem 3.2 is false), its secant field is guarded so that it never involves the junk gradient at $0$, and Proposition 3.3's existence clause certifies that the predicate is satisfiable.

The development needs elementary plane geometry with arccos, the BFGS update (reused from the published definition ShannoCG.SCONB.bfgsUpdate), and the contraction principle (Mathlib's ContractingWith). Rotation-invariance lemmas for the method would be reusable for any analysis of quasi-Newton methods on norms. Proofs of any milestone, and in particular an invariant treatment of the normalization step, 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
• D. F. Shanno, Conjugate gradient methods with inexact searches, Math. Oper. Res. 3 (1978) 244–256 (the additive form of the BFGS update). https://doi.org/10.1287/moor.3.3.244
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006 (quasi-Newton methods and the secant condition). https://doi.org/10.1007/978-0-387-40065-5

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 its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.

Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.

Setting

A manufacturer (EM) produces at unit cost $m$ and sells to a retailer at unit transfer price $c$; the retailer sells at price $p$, unsold units are salvaged at $u$ at either site, and each unit of unmet demand costs a goodwill loss $s$. The standing assumptions are $p > m > 0$, $u < m$ and $s \ge 0$.

Before production, the retailer states a forecast $q \ge 0$. A QF contract $\{c,(\alpha,\omega)\}$ with $\omega\in[0,1]$ and $\alpha\ge-\omega$ obliges the EM to make up to $q(1+\alpha)$ available and the retailer to buy at least $q(1-\omega)$. The EM then builds $Q$. A demand signal $\mu$ with distribution function $\Theta$ is observed, the retailer buys $r$, and market demand is filled from the retailer's stock. In this mission the signal is perfect ($\sigma_\varepsilon = 0$): market demand equals $\mu$, so its distribution $F$ equals $\Theta$.

Given $\mu$, the retailer's profit from buying $r$ is

$$G(r\mid\mu) = p\min[\mu,r] - c\,r - s[\mu-r]^+ + u[r-\mu]^+,$$

and it buys $r^*_{QF} = \mu\perp[q(1-\omega),Q]$, the point of the interval closest to $\mu$. The EM's expected profit (2) is $\pi_{EM,QF}(Q;q) = (c-u)E_\mu\{r^*_{QF}\} - (m-u)Q$. The retailer's forecast problem maximizes $\pi_{R,QF}(q) = E_\mu\{G(r^*_{QF}\mid\mu)\}$ with the EM building $q(1+\alpha)$. A central planner earns $\Pi_{CC}(Q) = E_\mu\{p\min[\mu,Q]-s[\mu-Q]^+ + u[Q-\mu]^+\} - mQ$, maximized at

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

The total flexibility of the contract is $\psi = (1+\alpha)/(1-\omega)$.

Formalization targets

Goal: Proposition 6(a)

With $\sigma_\varepsilon = 0$, the QF contract with flexibility $\psi$ and transfer price

$$\bar c(\psi) = u + \frac{m-u}{\dfrac1\psi F\!\left(\dfrac1\psi F^{-1}\!\left(\dfrac{p+s-m}{p+s-u}\right)\right) + \dfrac{m-u}{p+s-u}} \tag{4}$$

is system-efficient: the retailer's unique optimal forecast is $\hat q = Q^*_{CC}/(1+\alpha)$, the EM's unique optimal production given $\hat q$ is $\hat q(1+\alpha) = Q^*_{CC}$, and the resulting expected system profit equals $\max_Q \Pi_{CC}(Q)$.

Milestones

1. §4: $Q^*_{CC}$ exists and is the unique maximizer of $\Pi_{CC}$.
2. §6.1: given $\mu$, the retailer's unique optimal purchase in $[a,b]$ is $\mu\perp[a,b]$.
3. Proposition 3(a): for $\omega<1$, the optimal forecast $q^*_{QF}$ is strictly positive, finite, and the unique solution of the first-order condition (3).
4. §7: for any forecast $q\ge0$, expected system profit equals $\Pi_{CC}(q(1+\alpha))$; hence it is maximal when the production level $q(1+\alpha)$ matches $Q^*_{CC}$.

Significance

The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).

The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing $\Theta$, a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, $\alpha = 0$, retailer side only) do not cover them.

Difficulty

Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at $\hat q$ pins down $c$, so nothing is left to adjust for the EM, whose incentive to build more than the contracted $q(1+\alpha)$ has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of $\mu$ on two moving thresholds $q(1+\alpha)$ and $q(1-\omega)$, and strict concavity must come from the strict increase of $\Theta$ rather than from a density.

Formalization scope

All objects live in the namespace TsayQF.EffQF. The law of $\mu$ is a probability measure $\nu$ on $\mathbb R$ with $\mu\in L^2(\nu)$, whose distribution function cdf ν is differentiable and strictly increasing on $\mathbb R$ (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: $Q^*_{CC}$ enters as a real number with the hypothesis $F(Q^*_{CC}) = \kappa_S$, which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in $[0,\infty)$, the EM's production in $[q(1+\alpha),\infty)$, purchases in $[q(1-\omega),Q]$, central production in $\mathbb R$.

Hypotheses made explicit: $Q^*_{CC} > 0$ in the goal and a positive marginal value of the forecast at $q=0$ in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; $\omega<1$ (Proposition 3's case). The transfer price is only required to satisfy $u<c<p+s$ rather than $m<c<p$, because $\bar c(\psi)$ can exceed $p$ when $s>0$. The milestones are the $\sigma_\varepsilon = 0$ instances of the paper's general statements.

Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be $q(1+\alpha)$, as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at $\bar c(\psi)$ is exactly $q(1+\alpha)$. The efficient price is the explicit formula (4), not "a price that makes $Q^*_{CC}$ optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against $\Pi_{CC}$ at every production level, not by definition.

Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, 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
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in OR & MS vol. 11, 2003, §6.2.5. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed. 2019, Ch. 14. https://doi.org/10.1002/9781119584445