Optimization

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

• 1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$, $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
• 1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$. It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$, $s^2_i + B_i \le s^3_i$. The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$.

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$. Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$, Johnson defines

$$K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,$$

the sums running over the items in the first $u$ (resp. $v$) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

$$\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}$$

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$, then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

$$\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .$$

Milestones

1. Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
2. Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$, so that

$$\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),$$

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$, so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$. 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$, and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$.

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$, and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$, so the empty instance has makespan $0$. An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$, $H_{v+1}$. Statements with maxima over positions assume $n \ge 1$.

Hypotheses made explicit or corrected:

• $\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$, as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
• Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
• Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
• Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
• The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$, would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is $\ell_1$-penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).

Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into $K$ cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).

Setting

A sample is a point $z = (z^{(y)}, z^{(x)})$ with a response $z^{(y)} \in \mathbb R$ and a feature vector $z^{(x)} \in \mathbb R^m$, so the samples live in $\mathbb R^{m+1}$. The sample space $\mathcal Z \subseteq \mathbb R^{m+1}$ is a compact set, and $\mathbb R^{m+1}$ carries the norm $\|z\|_\infty = \max(|z^{(y)}|, \max_j |z^{(x)}_j|)$. A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$.

A learning algorithm maps each training set $\mathbf s$ to a hypothesis $\mathcal A_{\mathbf s}$; with a loss $l(h, z)$, it is $(K, \epsilon(\cdot))$-robust (Definition 2, p. 396) if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$, fixed independently of the data, such that for every $\mathbf s \in \mathcal Z^n$, every training point $s \in \mathbf s$, every $z \in \mathcal Z$ and every $i$,

$$s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).$$

For a metric $\rho$ on $\mathcal Z$ and $\epsilon > 0$, a set $\hat T \subseteq \mathcal Z$ is an $\epsilon$-cover of $\mathcal Z$ if every point of $\mathcal Z$ is within distance $\le \epsilon$ of a point of $\hat T$; the covering number $\mathcal N(\epsilon, \mathcal Z, \rho)$ is the least cardinality of such a cover (Definition 1, p. 394).

For a coefficient vector $w \in \mathbb R^m$ let $\|w\|_1 = \sum_j |w_j|$. Given $c > 0$, the Lasso is

$$\min_{w} \ \frac1n \sum_{i=1}^n \big(s_i^{(y)} - w^\top s_i^{(x)}\big)^2 + c\|w\|_1, \tag{5}$$

a Lasso algorithm returns a minimizer $\mathcal A_{\mathbf s} = w$ of (5) for each $\mathbf s$, and the loss is the absolute prediction error $l(w, z) = |z^{(y)} - w^\top z^{(x)}|$. Finally $Y(\mathbf s) = \frac1n \sum_{i=1}^n [s_i^{(y)}]^2$.

Formalization targets

Goal: Example 6 (p. 404)

For every compact $\mathcal Z \subseteq \mathbb R^{m+1}$, every $c > 0$, every Lasso algorithm $\mathcal A$ and every $\gamma > 0$,

$$\mathcal A \text{ is } \Big(\mathcal N(\gamma/2, \mathcal Z, \|\cdot\|_\infty),\ \big(Y(\mathbf s)/c + 1\big)\gamma\Big)\text{-robust}.$$

The statement holds for every selection of a minimizer, since (5) need not have a unique solution.

Milestones

1. Optimality bound (proof of Lemma 3, p. 419): every Lasso solution satisfies $\|w^*\|_1 \le \frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2$.
2. Lemma 3 (p. 419): for all $z_a, z_b \in \mathbb R^{m+1}$,

$$|l(w^*(\mathbf s), z_a) - l(w^*(\mathbf s), z_b)| \le \Big[\frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2 + 1\Big] \|z_a - z_b\|_\infty.$$

3. Theorem 6 (p. 402): for a metric $\rho$ on $\mathcal Z$ and $\gamma > 0$, if $|l(\mathcal A_{\mathbf s}, z_1) - l(\mathcal A_{\mathbf s}, z_2)| \le \epsilon(\mathbf s)$ whenever $z_1 \in \mathbf s$ and $\rho(z_1, z_2) \le \gamma$, and $\mathcal N(\gamma/2, \mathcal Z, \rho) < \infty$, then $\mathcal A$ is $(\mathcal N(\gamma/2, \mathcal Z, \rho), \epsilon(\cdot))$-robust.

Significance

Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form $\epsilon(\mathbf s) + M\sqrt{(2K\ln 2 + 2\ln(1/\delta))/n}$ with $K$ a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.

The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the $\ell_1$/$\ell_\infty$ pairing on $\mathbb R \times \mathbb R^m$, and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.

Difficulty

The constant in the robustness level depends on the training set through $Y(\mathbf s)$, while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on $\mathbf s$ proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by $\epsilon(\mathbf s)$ and the cells must depend only on $\mathcal Z$ and $\gamma$. A cover by balls is not a partition, and the radius of the cover ($\gamma/2$) and the closeness threshold in Theorem 6 ($\gamma$) differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between $\|w\|_1$ and $\|\cdot\|_\infty$ is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.

Formalization scope

• $\mathbb R^{m+1}$ is ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly $\|\cdot\|_\infty$. $\|w\|_1$ is written out as $\sum_j |w_j|$, since the default norm on Fin m → ℝ is the sup norm; $w^\top x$ is dotProduct w x.
• The sample space is a set Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.
• The covering number is Mathlib's Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is $\mathcal Z$ itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return $0$ and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.
• A Lasso algorithm is any function A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies $c > 0$, which the paper leaves implicit. The factor $1/n$ is a real division; for $n = 0$ it is $0$ in Lean, the objective reduces to $c\|w\|_1$, and all statements remain true.
• The robustness level is $(Y(\mathbf s)/c + 1)\gamma$ in Example 6 and $\frac{1}{nc}\sum_i [s_i^{(y)}]^2 + 1$ in Lemma 3, each in its printed form.

Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. doi:10.1007/s10994-011-5268-1
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society, Series B 58(1) (1996) 267–288. doi:10.1111/j.2517-6161.1996.tb02080.x
• H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, IEEE Transactions on Information Theory 56(7) (2010) 3561–3574. doi:10.1109/TIT.2010.2048503
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. jmlr.org/papers/v2/bousquet02a

Motivation

A two-stage stochastic linear program with fixed recourse chooses a first-stage decision $x$ before a random vector $\xi$ is observed, and then pays for a cheapest corrective action $y$ once $\xi$ is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.

Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of $x$ (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.

Setting

The data are a random element $\xi=(c,q,p,T)$ with $c\in\mathbb R^n$, $q\in\mathbb R^{\bar n}$, $p\in\mathbb R^{\bar m}$ and $T$ an $\bar m\times n$ matrix, distributed according to a probability measure $\mu$. The recourse matrix $W$ ($\bar m\times\bar n$), the first-stage matrix $A$ ($m\times n$) and $b\in\mathbb R^m$ are fixed. The recourse function is

$$Q(x,\xi)=\min\{q(\xi)y \mid Wy=p(\xi)-T(\xi)x,\ y\ge0\},$$

equal to $+\infty$ if the second-stage program is infeasible and $-\infty$ if it is unbounded.

The weak covariance condition (Definition 2.2) requires $c_j$, $q_jp_i$ and $q_jt_{ik}$ to be integrable for all indices; it does not require $q$, $p$ or $T$ themselves to be integrable. The paper also assumes throughout that $W$ has full row rank (p. 312).

Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and $(+\infty)+(-\infty)=+\infty$. The expected recourse is $\mathcal Q(x)=E_\xi\{Q(x,\xi)\}$ and the objective is

$$Z(x)=\bar c\,x+\mathcal Q(x),\qquad \bar c=E_\xi\{c(\xi)\}.$$

The induced constraints are $K_2=\bigcap_{\zeta\in\tilde\Xi_{p,T}}\{x : p-Tx\in\operatorname{pos}W\}$, where $\operatorname{pos}W=\{Wy:y\ge0\}$ and $\tilde\Xi_{p,T}$ is the support of the distribution of $(p,T)$. The fixed constraints are $K_1=\{x: Ax=b,\ x\ge0\}$, and $K=K_1\cap K_2$. The deterministic equivalent program (8.2) is to minimize $Z$ over $K$.

A convex program of the form $\min\{f(x) : Ax=b,\ x\ge0,\ x\in D\}$ with finite value $v$ is stable (Definition 8.1(iv)) if there is $\pi\in\mathbb R^m$ with $v\le f(x)+\pi(b-Ax)$ for all $x\in D$, $x\ge0$. Equivalently, the dual obtained by perturbing $b$ is solvable and has no duality gap.

Formalization targets

Goal: Theorem 8.11 (p. 337)

If the weak covariance condition holds, $W$ has full row rank, $K_2$ is a polyhedron and the program is finite, $v=\inf_K Z\in\mathbb R$, then

$$\exists\,\pi\in\mathbb R^m:\quad v\le Z(x)+\pi\,(b-Ax)\quad\text{for all }x\in K_2,\ x\ge0 .$$

Milestones

1. Corollary 7.3 (p. 328). The value $t\mapsto\min\{cx\mid Ax=t,\ x\ge0\}$ is a finite maximum of affine functions on $\operatorname{pos}A$, or $-\infty$ on all of $\operatorname{pos}A$.
2. Proposition 7.5 (p. 329). $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ for each $\xi$ in the support, concave polyhedral in $q$, and convex polyhedral in $(p,T)$.
3. Theorem 7.6 (p. 329). $Z$ is convex on $K$, and it is either finite on $K$ or identically $-\infty$ on $K$.
4. Theorem 7.7 (pp. 329–330). If $Z>-\infty$ on $K$, then $|Z(x)-Z(x^0)|\le\bar B\|x-x^0\|$ on $K$ (Euclidean norm).
5. Lemma 8.9 (p. 337). A finite program $\min\{f(x): Ax=b,\ x\ge0\}$ whose objective is convex and Lipschitz on a polyhedral domain is stable.

Significance

Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function $\phi(u)=\inf\{Z(x) : Ax=b-u,\ x\in K_2\cap\mathbb R^n_+\}$ at $u=0$, and hence a bounded rate of change of the optimal value under perturbations of $b$. The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically $-\infty$ on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.

The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on $K_2$ for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.

Difficulty

The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of $Q(\cdot,\xi)$. It fails unless that constant is integrable, and the weak covariance condition, not integrability of $\xi$, is what has to deliver this, uniformly over the finitely many second-stage bases.

For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of $Z$ has curved boundary, the perturbation function can have infinite slope at $0$; the polyhedral hypothesis on $K_2$ is what excludes this.

Formalization scope

• Types. Vectors are Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper ($c$, $q$, $\pi$) enter through dotProduct. The law $\mu$ is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). $Q$ is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.
• The integral. $\mathcal Q$ is written as lintegral of the positive part minus lintegral of the negative part, with $+\infty$ whenever the positive part is $+\infty$. This is the paper's $(+\infty)+(-\infty)=+\infty$; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be $0$ for non-integrable integrands and make every expected-cost statement trivial, and it is not used. $\bar c$ is a Bochner integral, legitimate because Definition 2.2 makes each $c_j$ integrable.
• Readings of informal words.
  • "Has first moments" is Integrable.
  • "Convex polyhedron" means finitely many weak linear inequalities; $\emptyset$ and $\mathbb R^n$ are included.
  • "Finite convex (concave) polyhedral function on $S$" means equal on $S$ to the maximum (minimum) of finitely many affine functions. The $x$ and $(p,T)$ parts of Proposition 7.5 are stated as a dichotomy with the identically $-\infty$ case; the $q$ part is stated, as Corollary 7.4 gives it, as finite concave polyhedral on $\operatorname{pos}(W^T,-W^T,I)$ when the recourse problem is feasible.
  • "Convex" for the extended-real $Z$ (Theorem 7.6) is ConvexOn of toReal on the finite branch.
  • "Bounded on $K$" (Theorem 7.7) is read as $Z>-\infty$ on $K$, the proof's own reading. Finiteness on $K$ is part of the conclusion.
  • "Convex and Lipschitz on a polyhedron" (Lemma 8.9) means the objective's domain is the polyhedron.
  • "The program is finite" means the infimum over $K$ is a real number.
  • "Stable" is the Kuhn–Tucker form above: a multiplier compared against the primal value, not merely a solvable dual. The latter would allow a duality gap.
• Standing assumptions. Full row rank of $W$ appears in Theorems 7.7 and 8.11, where the proof uses square nonsingular submatrices of $W$. It is omitted from Theorem 7.6 and Corollary 7.3 (Theorem 7.2's rank assumption), where it is not needed; this makes those statements stronger.
• Corrections to the page. Theorem 8.11 is printed with "$K$ is polyhedral", $K=K_1\cap K_2$, and read literally it is false. Take $T(\xi)$ uniform on the unit circle, $p\equiv1$, $W=(1)$, $q\equiv0$, $c\equiv(-1,0)$ and $K_1=\{x_2=1,\ x\ge0\}$. Then $K_2$ is the unit disk and $K=\{(0,1)\}$ is polyhedral with finite value $0$, but no multiplier exists. The goal therefore assumes "$K_2$ is polyhedral", as the sentence before Lemma 8.9 and the proof require. In the dual (8.3) the page writes $c$ for $\bar c$.
• Ruled out. A statement of stability as "the dual supremum is attained" without equality to the primal value is not the goal, and neither is a hypothesis making $K$ empty or $Z$ identically $-\infty$: the finiteness hypothesis excludes both.
• Infrastructure. The needed pieces are Minkowski–Weyl for polyhedra (PointedCone.FG/DualFG in Mathlib), LP duality with $\pm\infty$ values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.

Selected references

• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• R. M. Van Slyke and R. J.-B. Wets, A duality theory for abstract mathematical programs with applications to optimal control theory, J. Math. Anal. Appl. 22(3):679–706, 1968 (cited by Wets for Definition 8.1 and the dual (8.3)).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 3. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A two-stage stochastic program with recourse is a linear program in which a decision $x$ is taken before a random vector $\xi$ is observed, and a corrective (recourse) decision $y$ is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in $x$ alone, and the first question is which $x$ are admissible at all: the random second-stage constraints induce constraints on $x$ that are not written down anywhere in the data.

Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix $W$ is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix $T$ is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.

Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every $x$ feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random $W$. The 1974 survey collects these results in the form formalized here.

Setting

The data are a fixed real $\bar m \times \bar n$ matrix $W$ and a random vector $\xi = (c, q, p, T)$ with $c \in \mathbb{R}^n$, $q \in \mathbb{R}^{\bar n}$, $p \in \mathbb{R}^{\bar m}$ and $T$ an $\bar m \times n$ matrix. The law of $\xi$ is a probability measure $\mu$ on the product space, and its support $\tilde\Xi$ is the smallest closed set of measure one. The recourse function is

$$Q(x,\xi) = \min\{\, q(\xi)y \mid Wy = p(\xi) - T(\xi)x,\ y \ge 0 \,\},$$

equal to $+\infty$ when the program is infeasible and $-\infty$ when it is unbounded below. The expected recourse $\mathcal Q(x) = E_\xi\{Q(x,\xi)\}$ uses the paper's integral: the sum of the positive part $\int Q^+ d\mu \in [0,+\infty]$ and the negative part $-\int Q^- d\mu \in [-\infty,0]$, with $(+\infty) + (-\infty) = +\infty$.

The weak covariance condition (Definition 2.2) asks that $c_j$, $q_j p_i$ and $q_j t_{ik}$ be integrable for all $i, j, k$. Write $\operatorname{pos} W = \{Wy \mid y \ge 0\}$. The candidate feasibility sets for the induced constraints are

• $K_2^\mu$: the $x$ for which, with probability one, some $y \ge 0$ solves $Wy = p(\xi) - T(\xi)x$;
• $K_2^p$: the $x$ for which such a $y$ exists for every $\xi \in \tilde\Xi$;
• $K_2^s = \{x \mid \mathcal Q(x) < +\infty\}$;
• $K_2 = \bigcap_{\zeta \in \tilde\Xi_{p,T}} K_2(\zeta)$, where $\tilde\Xi_{p,T}$ is the support of the law of $(p,T)$ and $K_2(\zeta) = \{x \mid p - Tx \in \operatorname{pos} W\}$ for $\zeta = (p,T)$.

A convex polyhedron is a set $\{x \mid Gx \ge \alpha\}$ given by finitely many linear inequalities; $\emptyset$ and $\mathbb{R}^n$ are polyhedra.

Formalization targets

Goal: Theorem 4.10

If $T$ is fixed and $\xi$ satisfies the weak covariance condition, then

$$K_2 = \{x \in \mathbb{R}^n \mid Gx \ge \alpha\} \quad \text{for some finite system } G, \alpha,$$

so $K_2$ is a closed convex polyhedron. The number of inequalities is not fixed in advance, and $K_2$ may be empty.

Milestones

1. Theorem 4.1. Under weak covariance, $K_2^\mu = K_2^p = K_2^s$.
2. Corollary 4.5. Under weak covariance, $K_2 = K_2^p = K_2^\mu = K_2^s$.
3. Theorem 4.6. For every set $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$, $K_2 = \bigcap_{\zeta \in \Sigma} K_2(\zeta)$.
4. Theorem 4.7. $K_2$ is closed and convex; if the closed positive hull $\operatorname{pos}(\tilde\Xi_{p,T})$ is a convex polyhedral cone, $K_2$ is a convex polyhedron.

Significance

Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of $(p, T)$. This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when $p(\xi)$ has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.

The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).

Difficulty

Two steps resist the obvious approach. First, $K_2^p \subseteq K_2^s$ needs an integrable upper bound for the positive part of $Q(x,\cdot)$ on the whole support. $Q$ is only piecewise linear in $\xi$, can equal $-\infty$, and $q$, $p$, $T$ are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra $K_2(\zeta)$, and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of $p$ is the content of the goal, and the resulting system may be inconsistent, in which case $K_2 = \emptyset$.

Formalization scope

Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is $\mathbb{R}^n \times \mathbb{R}^{\bar n} \times \mathbb{R}^{\bar m} \times \mathbb{R}^{\bar m \times n}$ with its Borel structure, and $\mu$ is a probability measure on the whole space (the paper's sample space $\Xi$ only carries $\mu$). Readings fixed by the formalization:

• "has first moments" (Def. 2.2) is Integrable with respect to $\mu$.
• The integral is the paper's: two lower Lebesgue integrals, returning $+\infty$ whenever the positive part diverges. Mathlib's EReal subtraction ($\top - \top = \bot$) and the Bochner integral of toReal (zero for non-integrable functions) would both make $K_2^s$ wrong and are not used.
• "support" is Mathlib's Measure.support; $\tilde\Xi_{p,T}$ is the support of the pushforward under the (continuous, hence measurable) projection onto $(p,T)$.
• "$T$ is fixed" means $T(\xi) = T_0$ with probability one, a weaker hypothesis than pointwise constancy.
• "convex polyhedron" is the solution set of finitely many weak linear inequalities, the number of them existentially quantified; "convex polyhedral cone" is the conic hull of finitely many vectors; "closed positive hull" is the closure of the conic hull.
• Full row rank of $W$ is the paper's standing assumption (p. 312) and is carried as a hypothesis of Theorem 4.1, Corollary 4.5 and Theorem 4.10; it is inessential for them.
• Theorem 4.6 is stated as "for every $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$". The literal statement fails: a closed half-plane has no extreme points, so the "inverse of convex closure" would give $\Sigma = \emptyset$ and an intersection equal to $\mathbb{R}^n$.
• The set on p. 314 (iii) is printed $K_2^p$.

A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral $\mathcal Q$ would make $K_2^s = \mathbb{R}^n$. Neither is used.

A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of $\operatorname{pos} W$ (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.

Selected references

• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• R. M. Van Slyke and R. J.-B. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
• D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Ch. 3. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).

When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.

Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.

Timeline:

• 1976: Korpelevich, extragradient method, Lipschitz monotone maps.
• 1987–1994: Khobotov (1987), Iusem (1994) and others: extragradient variants with Armijo-type stepsize rules, which need one projection per trial step.
• 1997: Iusem and Svaiter, a separating-hyperplane variant of extragradient for monotone maps (reference [9] of the paper).
• 1999: Solodov and Svaiter, Algorithm 2.1: two projections per iteration, convergence under condition (1.2) below.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C \subseteq \mathbb{R}^n$ be closed and convex and $F : \mathbb{R}^n \to \mathbb{R}^n$ continuous. The problem $\mathrm{VI}(F, C)$ is to find $x^*$ with

$$x^* \in C, \qquad \langle F(x^*), x - x^*\rangle \ge 0 \quad \text{for all } x \in C. \tag{1.1}$$

Its solution set is $S$. The projection onto a nonempty closed convex set $K$ is $P_K[x] := \arg\min_{y \in K}\|y - x\|$. The projected residual is $r(x) := x - P_C[x - F(x)]$; its zeros are exactly the points of $S$.

Condition (1.2) requires, for every $x^* \in S$,

$$\langle F(x), x - x^*\rangle \ge 0 \qquad \text{for all } x \in C. \tag{1.2}$$

It holds when $F$ is monotone or pseudomonotone, and in cases where $F$ is neither.

Algorithm 2.1. Fix $\gamma, \sigma \in (0,1)$ and $x^0 \in C$. Given $x^i$: if $r(x^i) = 0$, stop. Otherwise let $k_i$ be the smallest nonnegative integer $k$ with

$$\langle F(x^i - \gamma^k r(x^i)), r(x^i)\rangle \ge \sigma\|r(x^i)\|^2, \tag{2.1}$$

set $\eta_i = \gamma^{k_i}$, $z^i = x^i - \eta_i r(x^i)$, $H_i = \{x \mid \langle F(z^i), x - z^i\rangle \le 0\}$, and

$$x^{i+1} = P_{C \cap H_i}[x^i].$$

The hyperplane $\partial H_i$ separates $x^i$ from $S$.

Formalization targets

Goal: Theorem 2.1

If $C$ is closed and convex, $F$ is continuous, $S \ne \emptyset$ and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of $S$:

$$\exists\, \hat x \in S:\quad x^i \to \hat x \quad (i \to \infty).$$

The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.

Milestones (in attack order)

• Lemma 2.1 (p. 768): for nonempty closed convex $B$, $\langle x - P_B[x], z - P_B[x]\rangle \le 0$ for $z \in B$, and $\|P_B[x]-P_B[y]\|^2 \le \|x-y\|^2 - \|P_B[x]-x+y-P_B[y]\|^2$.
• Residual characterization (p. 767): $x \in S \iff r(x) = 0$.
• (2.5) (p. 769): $\langle F(x), r(x)\rangle \ge \|r(x)\|^2$ for $x \in C$.
• Linesearch well-definedness (p. 769): for $x \in C$ with $r(x) \ne 0$, some $k$ satisfies (2.1).
• Lemma 2.2 (p. 768): $x^{i+1} = P_{C\cap H_i}[\bar x^i]$ with $\bar x^i = P_{H_i}[x^i]$.
• (2.6) (pp. 769–770): $\|x^{i+1}-x^*\|^2 \le \|x^i-x^*\|^2 - \|x^{i+1}-\bar x^i\|^2 - \big(\eta_i\sigma/\|F(z^i)\|\big)^2\|r(x^i)\|^4$ for every $x^* \in S$.
• (2.8) (p. 770): $\eta_i\|r(x^i)\| \to 0$.

Significance

Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.

The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.

Difficulty

The Fejér-type inequality (2.6) quickly gives bounded iterates and $\eta_i\|r(x^i)\| \to 0$. The obvious next step, concluding $r(x^i) \to 0$, fails: nothing prevents the stepsizes $\eta_i$ from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of $k_i$ and the continuity of $F$ enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in $S$ at the end of the argument, which is why the condition must hold for every $x^* \in S$. Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to $S$, is strictly weaker.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.
• Projection encoding. projOnto K x is a nearest point of $K$ to $x$ when one exists, chosen by Classical.choose, and the junk value $x$ otherwise. On nonempty closed convex sets it is exactly $P_K[x]$; the paper only projects onto such sets ($C$, $H_i$, $C \cap H_i$), so the junk value is never reached under the hypotheses.
• Stopping-rule encoding. A run is a sequence x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If $r(x^i) = 0$ the method has stopped and the run stalls, $x^{i+1} = x^i$; otherwise $k_i$ is the least index satisfying (2.1) and $x^{i+1} = P_{C \cap H_i}[x^i]$. A stalled point is a solution, so finitely terminating runs are included in the goal.
• Parameters $\gamma, \sigma$ are real with $0 < \gamma < 1$, $0 < \sigma < 1$, universally quantified; $n$, $C$, $F$ and $x^0 \in C$ are arbitrary.
• (2.6) is stated for one generic step ($x \in C$, $r(x)\ne 0$, $k$ satisfying (2.1)) rather than along a run; it is the same inequality with $x^i, k_i$ abstracted.
• Trivializing formalizations are ruled out: condition (1.2) is quantified over every solution and every $x \in C$ (not replaced by monotonicity or an existential), $k_i$ is the least index satisfying (2.1), the update projects $x^i$ onto $C \cap H_i$ (not onto $C$ alone), the stopped case is pinned down by the stall encoding, and the conclusion is convergence of the whole sequence to one solution, not $r(x^i) \to 0$ or $\operatorname{dist}(x^i, S) \to 0$.
• Needed infrastructure: existence, uniqueness and variational characterization of the projection (Mathlib has exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in $\mathbb{R}^n$. The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.

Selected references

• M. V. Solodov and B. F. Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37(3), 765–776, 1999. https://doi.org/10.1137/S0363012997317475
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Matecon 12, 747–756, 1976.
• A. N. Iusem and B. F. Svaiter, A variant of Korpelevich's method for variational inequalities with a new search strategy, Optimization 42, 309–321, 1997. https://doi.org/10.1080/02331939708844365
• P. T. Harker and J.-S. Pang, Finite-dimensional variational inequality and nonlinear complementarity problems: a survey of theory, algorithms and applications, Math. Programming 48, 161–220, 1990. https://doi.org/10.1007/BF01582255
• F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

Motivation

Conjugate gradient methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using only gradients and a handful of stored vectors. This makes them the standard choice when $n$ is too large for Newton or quasi-Newton methods, which store an $n\times n$ matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most $n$ steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.

D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as $-\hat H g$, where $\hat H$ is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor $\gamma_t$. Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.

• 1952: Hestenes and Stiefel, linear conjugate gradients.
• 1964: Fletcher and Reeves, nonlinear conjugate gradients.
• 1969: Polak and Ribière, a second nonlinear variant.
• 1972: Beale, a restart procedure that keeps the computed direction $d_t$.
• 1977: Powell's restart criterion (Powell 1977).
• 1978: Shanno's reformulation as memoryless and two-update quasi-Newton methods (this paper).

Setting

Vectors are columns in $\mathbb R^n$. A prime denotes transpose: $u'v$ is the inner product and $uv'$ the outer product. An iterative method produces points $x_k$, steps $p_k = x_{k+1}-x_k = \alpha_k d_k$ along search directions $d_k$, gradients $g_k = \nabla f(x_k)$, and gradient changes $y_k = g_{k+1}-g_k$. A line search is exact when $p_k'g_{k+1} = 0$.

The BFGS update of a matrix $H$ with the pair $(p,y)$ is

$$H^+ = H - \frac{p\,y'H + H y\,p'}{p'y} + \left(1+\frac{y'Hy}{p'y}\right)\frac{pp'}{p'y}.$$

A restart cycle begins at iteration $t$. At a later iteration $k>t$, Shanno's self-scaled restart matrix is

$$\hat H_k = \gamma_t\left(I - \frac{p_ty_t'+y_tp_t'}{p_t'y_t} + \frac{y_t'y_t}{p_t'y_t}\frac{p_tp_t'}{p_t'y_t}\right) + \frac{p_tp_t'}{p_t'y_t}, \qquad \gamma_t = \frac{p_t'y_t}{y_t'y_t}.$$

The matrix $\hat H_{k+1}$ is its BFGS update with $(p_k,y_k)$, and the self-scaled two-update direction is $d_{k+1} = -\hat H_{k+1}g_{k+1}$. The unscaled variant uses the BFGS update of $I$ in place of the first matrix.

Beale's direction is

$$d_{k+1} = -g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t.$$

The quadratic case has gradient $g(x) = Ax + c$ with $A$ symmetric positive definite.

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Let $A$ be symmetric positive definite, $g_i = Ax_i + c$ and $t<k$. Assume that for $t\le i\le k$ we have $x_{i+1} = x_i + p_i$, $p_i = \alpha_i d_i$ and $p_i'g_{i+1}=0$, that $p_t'Ap_i = 0$ for $t<i\le k$, and that $p_t, p_k \ne 0$. Then

$$-\hat H_{k+1}g_{k+1} = \gamma_t\left(-g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t\right).$$

This is the paper's claim that "for $f(x)$ quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly $\gamma_t$.

Companion statements

• The unscaled two-update direction equals Beale's direction exactly.
• Both two-update directions are descent directions, $g_{k+1}'d_{k+1} < 0$, whenever $p_t'y_t > 0$ and $p_k'y_k > 0$. No exact search is needed.

Milestones on the path

• (34): the expansion of $-\hat H_{k+1}g_{k+1}$.
• (40): its form under an exact search.
• (41): gradients along a run on a quadratic.
• $p_t'g_{k+1} = 0$.
• (38), corrected by a factor 2: the action of the self-scaled restart matrix.
• (42): its form when $p_t'g_{k+1} = 0$.
• (43): the direction after substitution.

Significance

The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with $p'y>0$. The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale $\gamma_t$ changes only the length of the step, not its direction.

Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:

• a checked statement of the claim with every hypothesis explicit, including the conjugacy the proof takes as known;
• a corrected version of display (38), which is misprinted;
• reusable definitions of the additive BFGS update and of Beale's direction.

Difficulty

The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, $p_t'g_{k+1}=0$. It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of $p_t$ with all later steps. The second is $y_k'p_t = 0$, which again comes from conjugacy. Beale's formula also has to be matched in its $d$-form: the coefficient $\frac{y'g}{d'y}d$ equals $\frac{y'g}{p'y}p$ only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with $p'y>0$ must be shown to remain positive definite, and this has to be done twice.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product $u'v$ is u ⬝ᵥ v, the outer product $uv'$ is vecMulVec u v, and $Hv$ is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case $c = -A\hat x$. Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: $p_t \ne 0$ and $p_k\ne0$ in the quadratic statements, and $p_t'y_t\ne 0$ or $p'y>0$ in the generic ones.

The conjugacy $p_t'Ap_i=0$ for $t<i\le k$ is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range $k\le t+n-1$ of Beale's formula is not assumed.

Several formalizations would make the claim easier than the paper's, and none of them is used:

• defining the direction by the expanded formula (34), or the restart matrix by (38);
• adding orthogonality or conjugacy hypotheses beyond those listed;
• concluding only that the two directions are parallel;
• dropping the restart term of Beale's direction;
• allowing a zero denominator.

The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.

Selected references

• D. F. Shanno, Conjugate Gradient Methods with Inexact Searches, Mathematics of Operations Research 3(3) (1978) 244–256. https://doi.org/10.1287/moor.3.3.244
• E. M. L. Beale, A derivation of conjugate gradients, in F. A. Lootsma (ed.), Numerical Methods for Nonlinear Optimization, Academic Press, 1972, 39–43.
• M. J. D. Powell, Restart procedures for the conjugate gradient method, Mathematical Programming 12 (1977) 241–254. https://doi.org/10.1007/BF01593790
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• S. S. Oren and E. Spedicato, Optimal conditioning of self-scaling variable metric algorithms, Mathematical Programming 10 (1976) 70–90. https://doi.org/10.1007/BF01580654

Motivation

Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).

The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.

Setting

Two manufacturers $i \in \{1, 2\}$ sell substitutable products through one retailer. The demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition, and $\theta$ is a random shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ that is unbiased, $E[Y \mid \theta] = \theta$, and has linear expectation: $E[\theta \mid Y] = \beta Y$ for a weight $\beta$ (in the paper $\beta = t\sigma^2/(1+t\sigma^2)$, with $t$ the signal accuracy). The retailing cost is zero, and manufacturer $i$ produces $q$ units at cost $bq + c_d q^2$ with $b, c_d > 0$: a production diseconomy.

The game has four stages.

1. The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
2. The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
3. The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$. The retailer then sets retail prices.
4. Demand realizes and payoffs are received.

The pricing stage is a Bayesian game. Its equilibrium ex ante profits are $\pi_M(n)$, $\pi_M^I(1)$, $\pi_M^U(1)$ for the manufacturers and $\pi_R(n)$ for the retailer, where $n$ is the number of informed manufacturers. They define a payoff table for the contracting stage.

Two contracting protocols are compared.

• Concurrent contracting: the retailer offers both manufacturers the same payment $T$, and they accept or reject simultaneously; a Pareto-optimal pure equilibrium is the outcome, and the retailer chooses $T$.
• Sequential contracting: the retailer offers one manufacturer $T_f$, he accepts or rejects, then the retailer offers the other $T_s$, and he decides having observed the first decision. The retailer cannot commit to $T_s = T_f$, and the solution is subgame perfect equilibrium.

Formalization targets

Goal: Proposition 4(d)

For every $\phi > 0$, $c_d > 0$ and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),

$$\Pi_R^{C} \le \Pi_R^{S}, \qquad \Pi_M^{S} \le \Pi_M^{C},$$

with both inequalities strict when $c_d > (\sqrt2 - 1)/(1+\phi)$. Here $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The paper's word "higher" is read as $\ge$ because for small $c_d$ neither protocol sells information and all profits coincide.

Milestones

1. §4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
2. Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$.
3. §4.2: the closed forms of the seven ex ante profits.
4. Lemma 3: $\pi_M(2) > \pi_M^I(1) > \pi_M(0) > \pi_M^U(1)$, $\pi_R(0) > \pi_R(1) > \pi_R(2)$, $\pi_R(1) - \pi_R(2) > \pi_R(0) - \pi_R(1)$.
5. Proposition 1(b): without contracting, no information is shared.
6. Propositions 2 and 3: thresholds $c_d^C$ and $c_d^{S1}, c_d^{S2}$, depending only on $\phi$, at which the number of informed manufacturers changes under each protocol.
7. Proposition 4(a): $c_d^{S1} < c_d^C < c_d^{S2}$.

Significance

The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in $(c_d, \phi)$ (Figure 1 of the paper).

Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is $c_d^{S2}$. No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.

Difficulty

Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities $E[\theta Y] = \sigma^2$ and $E[Y^2] = \sigma^2/\beta$. The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold $c_d^{S2}$ has no closed form; it is the root of a convex rational function of $c_d$.

Formalization scope

The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:

• The probability space carries $\theta$ and $Y$ in $L^2$, with the two conditional-expectation identities holding almost everywhere. $\beta$ is a parameter fixed by $E[\theta \mid Y] = \beta Y$; Ericson's formula for $\beta$ is not formalized.
• Wholesale strategies are measurable, square-integrable functions of the signal value, and constants for an uninformed manufacturer. A pricing equilibrium is ex ante optimality over such strategies, which is equivalent to the paper's conditional optimization. The retailer's rule must be a best response at every wholesale-price pair.
• The payoff table is produced by an arbitrary pricing-equilibrium family, not by the §4.2 closed forms. A formalization that takes the closed forms as the definition of the profits would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out.
• Payments are nonnegative, only pure strategies are used in the contracting games, and the concurrent outcome selects, among Pareto-optimal equilibria, the one best for the retailer.
• Threshold statements use two clauses: the printed value is attained on the closed region, and it is the only value on the region's interior. The thresholds depend only on $\phi$.
• Demands may be negative (θ is unbounded), as in the paper's formulas.

A complete development needs:

• the conditional-expectation algebra behind Lemma 1 and §4.2;
• rational-function inequalities for Lemma 3;
• a case analysis of the two contracting games.

The model layer is shared with the companion mission on production economy.

Selected references

• G. Shang, A. Y. Ha, S. Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• W. A. Ericson, A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969.
• L. Li, Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, H. Zhang, Confidentiality and information sharing in supply chain coordination, Management Science 54(8):1467–1481, 2008. https://doi.org/10.1287/mnsc.1070.0851
• A. Y. Ha, S. Tong, H. Zhang, Sharing imperfect demand information in competing supply chains with production diseconomies, Management Science 57(3):566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295
• X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999.