Optimization

Completed

Combinatorics Information Theory Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming VIII: The Delsarte Linear Programming Bound for Binary CodesTextbook

Motivation

A binary error-correcting code is a set of $n$ -bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
1973: Delsarte proves the linear programming bound using association schemes.
1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$ .
2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$ , and a code is any set $C \subseteq \{0,1\}^n$ . The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$ . The weight $|\mathbf w|$ is the number of ones in $\mathbf w$ . The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$ , the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$ .

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$ .

For $0 \le i,t \le n$ the Krawtchouk numbers are

K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.

The distance distribution of a code $C$ is

\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.

The Delsarte linear program has variables $x_0,\dots,x_n$ . It maximizes $x_0+\dots+x_n$ subject to:

$x_0 = 1$ ;
$x_i = 0$ for $1 \le i \le d-1$ ;
$\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$ ;
$x \ge 0$ .

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$ .

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

Lemma 8.4.5. For every $I$ and $C$ , the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$ .
Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$ .
Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$ .
§8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$ . For a nonempty code with distance $d$ , the vector $\tilde x(C)$ is feasible for the program.
Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$ .
Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$ , while the sphere-packing bound gives $7281$ . Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$ , no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$ .

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$ , and $\tilde x_i = 0$ for $i < d$ . The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$ , and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$ , has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
The maximum $A(n,d)$ . $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$ . This family contains the empty code, so the maximum is attained.
Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$ .
LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$ , so they are vacuous for $d \le 1$ .
The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$ . Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$ .
Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$ .

No trivialization. The goal is not stated as " $A(n,d) \le \sup$ " with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$ ;
counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$ .

These are reusable for other LP and SDP bounds in coding theory.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

10 thms2 active usersReviewed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Understanding and Using Linear Programming VII: LP Rounding Schedules Unrelated Machines Within Twice the Optimal MakespanTextbook

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$ . The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$ . This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$ ; $d_{ij} > 0$ is the running time of job $j$ on machine $i$ . A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$ , the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$ , the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}

Its optimal value is $t^*(T)$ , with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$ ; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$ , $1$ in the row of job $j$ , and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$ .

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .

Milestones

Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$ .
Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$ .
Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ .
Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$ .

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ , and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$ : the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$ . The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$ . The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$ , which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$ . The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$ , as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$ . This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$ " is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$ ). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

Understanding and Using Linear Programming VI: The Minimax Theorem for Zero-Sum GamesTextbook

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$ . A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$ th and Bob his $j$ th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$ , $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$ . When the players randomize independently, Alice's expected payoff is

\mathbf x^T M \mathbf y = \sum_{i,j} m_{ij} x_i y_j .

The worst-case payoffs are

\beta(\mathbf x) = \min_{\mathbf y} \mathbf x^T M \mathbf y, \qquad \alpha(\mathbf y) = \max_{\mathbf x} \mathbf x^T M \mathbf y,

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$ ; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$ ; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$ ; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$ , $\sum_j y_j = 1$ , $\mathbf y \ge \mathbf 0$ .

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$ : worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$ , the value of the game, with

\beta(\tilde{\mathbf x}) = \tilde{\mathbf x}^T M \tilde{\mathbf y} = \alpha(\tilde{\mathbf y}) = v

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

$\beta$ and $\alpha$ are attained minima and maxima (p. 135).
Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$ , hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$ .
Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$ .
Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .
Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
The minimax equality (p. 137):

\max_{\mathbf x}\min_{\mathbf y}\mathbf x^T M \mathbf y = \min_{\mathbf y}\max_{\mathbf x}\mathbf x^T M \mathbf y .

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$ . The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$ . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

12 thms2 active usersReviewed

Convex Optimization Linear Optimization Operations Research·Captain: mikedeng1

Understanding and Using Linear Programming V: The Primal–Dual Central Path and the Self-Dual EmbeddingTextbook

Motivation

Interior point methods solve linear programs in a number of iterations polynomial in the input size, and in practice they compete with the simplex method on large instances. Their modern form goes back to Karmarkar's projective algorithm (Karmarkar 1984); the primal–dual path-following variant analysed in textbooks follows a curve, the central path, defined by a perturbed system of optimality conditions. Two facts make the method well defined. First, the central path exists and is unique whenever the primal and dual programs have strictly feasible points. Second, an arbitrary linear program, possibly infeasible or unbounded, can be embedded in an auxiliary program that has an explicit starting point on its own central path and whose suitable optimal solutions either solve the original program or certify that it has no optimum.

Chapter 7, §7.2 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer 2007), presents both facts in elementary form, following Terlaky (2001). This mission formalizes its three numbered lemmas.

Timeline. The homogeneous system bearing their names is due to Goldman and Tucker (1956), in the study of the structure of optimal solution sets; the self-dual embedding for interior point methods was introduced by Ye, Todd and Mizuno (1994), and the book's presentation follows the skew-symmetric form in Roos, Terlaky and Vial (2005).

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ . The linear program in equational form (7.2) is

\text{maximize } c^{T}x \text{ subject to } Ax=b,\ x\ge 0,

where $A$ has rank $m$ ; its dual (7.5) is: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\in\mathbb{R}^m$ . The notation $x>0$ means that all coordinates of $x$ are strictly positive. For $\mu>0$ the barrier function is $f_\mu(x)=c^{T}x+\mu\sum_{j=1}^n\ln x_j$ , defined for $x>0$ . The central-path system (7.4), in unknowns $x,s\in\mathbb{R}^n$ and $y\in\mathbb{R}^m$ , is

Ax=b,\qquad A^{T}y-s=c,\qquad (s_1x_1,\dots,s_nx_n)=\mu\mathbf 1,\qquad x,s\ge 0 .

For the embedding, the book switches to the inequality form (7.7): maximize $c^{T}x$ subject to $Ax\le b$ , $x\ge 0$ , with dual: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\ge 0$ . The Goldman–Tucker system (GTS) is

Ax-\tau b\le 0,\qquad -A^{T}y+\tau c\le 0,\qquad b^{T}y-c^{T}x\le 0,\qquad x,y\ge 0,\ \tau\ge 0,

and $\rho=\rho(x,y)=c^{T}x-b^{T}y$ is the slack of its last inequality. With $u=(y,x,\tau)\in\mathbb{R}^k$ , $k=n+m+1$ , (GTS) reads $M_0u\le 0$ , $u\ge 0$ for the skew-symmetric matrix

M_0=\begin{pmatrix}0&A&-b\\-A^{T}&0&c\\b^{T}&-c^{T}&0\end{pmatrix}.

Put $r=\mathbf 1+M_0\mathbf 1$ , $M=\begin{pmatrix}M_0&-r\\r^{T}&0\end{pmatrix}$ and $q=(0,\dots,0,k+1)\in\mathbb{R}^{k+1}$ . The self-dual program (SD) in $v=(u,\vartheta)$ is: maximize $-q^{T}v$ subject to $Mv\le q$ , $v\ge 0$ . Its slacks are $z=q-Mv$ , and a feasible $v$ is strictly complementary if $v_j>0$ or $z_j>0$ for every $j=1,\dots,k+1$ .

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

If (7.2) has a feasible $\tilde x>0$ and (7.5) has a feasible $\tilde y$ with $\tilde s=A^{T}\tilde y-c>0$ , then for every $\mu>0$

\exists!\,(x^*,y^*,s^*)\ \text{solving (7.4)},\qquad x^*=\arg\max\{f_\mu(x): Ax=b,\ x>0\}\ \text{(uniquely)}.

Milestones

Claim in the proof of Lemma 7.2.1 (p. 121): under the lemma's assumptions and for fixed $\mu>0$ , the set $Q=\{x: Ax=b,\ x>0,\ f_\mu(x)\ge f_\mu(\tilde x)\}$ is bounded.
Lemma 7.2.2 (p. 126): no solution of (GTS) has $\tau\ne 0$ and $\rho\ne 0$ ; exactly one of "a solution with $\tau>0$ " and "a solution with $\rho>0$ " exists; in the first case $\frac1\tau x$ and $\frac1\tau y$ are optimal for (7.7) and its dual; in the second, (7.7) is infeasible or unbounded.
Lemma 7.2.3 (p. 128): (SD) is feasible and bounded, every optimal solution has $\vartheta=0$ and its $u$ -part solves (GTS), and every strictly complementary optimal solution gives a solution of (GTS) with $\tau>0$ or $\rho>0$ .

Significance

Lemma 7.2.1 is what makes "the central path" a well-defined object: without existence, a path-following method has nothing to follow, and without uniqueness the point $x^*(\mu)$ that the algorithm approximates is not determined. It also identifies the barrier maximizer with the solution of the Lagrange system (7.4), which is the system the Newton steps of the algorithm linearize. Lemmas 7.2.2 and 7.2.3 remove the need for an interior starting point and for knowing in advance that the program has an optimum: every linear program reduces to computing a strictly complementary optimal solution of a program with a known interior point on its central path.

The three lemmas are classical and proved in the book (7.2.2 as a sketch). Formalizing them adds a machine-checked account of the central path in equational form, and of the Goldman–Tucker and self-dual constructions with explicit block matrices, reusable by any later formalization of interior point complexity bounds. As far as a search of the platform shows, no formal statement of the Goldman–Tucker system or of the self-dual embedding exists there; the nearest item, Lemma 9.5 of Introduction to Linear Optimization XII (Bertsimas–Tsitsiklis), characterizes the central path by KKT conditions and is not linked to a formal statement.

Difficulty

For Lemma 7.2.1, uniqueness of a maximizer follows from strict concavity, but existence does not: the feasible region $\{Ax=b,\ x>0\}$ is open relative to its affine hull and typically unbounded, and $f_\mu$ need not attain its supremum on such a set. The interior dual point is what rules out escape to infinity; the primal interior point is what rules out escape to the boundary. Identifying the maximizer with the unique solution of (7.4) further needs the Lagrange multiplier rule on an open set and the full row rank of $A$ to determine $y$ from $s$ .

For Lemma 7.2.2 the exclusivity and the optimality statements are weak-duality arguments, but existence of a solution with $\rho>0$ when (7.7) is infeasible or unbounded requires a Farkas-type alternative for both the primal and the dual, and the case split in the book's sketch ("the dual case is analogous") must be carried out. Lemma 7.2.3 requires bookkeeping with the block structure of $M$ and the skew-symmetry of $M_0$ .

Formalization scope

Vectors are functions Fin n → ℝ and Fin m → ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Matrices are Matrix (Fin m) (Fin n) ℝ, inequalities between vectors are componentwise, $x>0$ is ∀ j, 0 < x j. The rank condition of (7.2) is the hypothesis A.rank = m. Optimal solutions and unboundedness are expressed against every feasible point, never through a real supremum. The vector $u=(y,x,\tau)$ is indexed by Fin m ⊕ Fin n ⊕ Unit and $v=(u,\vartheta)$ by (Fin m ⊕ Fin n ⊕ Unit) ⊕ Unit; $M_0$ , $r$ , $M$ and $q$ are defined entrywise on these index types, with the last entry of $q$ equal to $k+1=n+m+2$ . "Exactly one" in Lemma 7.2.2 is Xor.

Lean's Real.log returns $0$ for nonpositive arguments, so a statement comparing $f_\mu$ over $\{Ax=b\}$ or $\{Ax=b,\ x\ge 0\}$ would be a different, and generally false or trivial, claim; every comparison of barrier values is restricted to points with all coordinates strictly positive. The unique solution of (7.4) is stated as existence plus equality of every solution with it, not as existence of some solution.

Useful infrastructure: strict concavity of sums of logarithms, the Lagrange multiplier rule for affine constraints (Mathlib's IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt or a direct orthogonality argument), compactness of closed bounded sets in Fin n → ℝ, and Farkas' lemma in the forms of Proposition 6.4.1 of the book. Proofs of the milestones, alternative arguments, and general lemmas about skew-symmetric linear programs are all welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4
T. Terlaky, An easy way to teach interior-point methods, European Journal of Operational Research 130(1), 2001, 1–19.
C. Roos, T. Terlaky, J.-P. Vial, Interior Point Methods for Linear Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/b100325
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt{n}L)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 1994, 53–67. https://doi.org/10.1287/moor.19.1.53
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
F. A. Potra, S. J. Wright, Interior-point methods, Journal of Computational and Applied Mathematics 124, 2000, 281–302.

6 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$ . An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$ . The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$ .

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$ , $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$ . A basis is an $m$ -element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$ .

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$ : $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$ ,

\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},

\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$ .
Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$ .
The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$ , $c^{T}\tilde x\ge c^{T}x_0$ .
Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$ , solve $A_Bx_B=b$ , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$ , extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$ -element basis, which requires the rank- $m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
$Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
a subset $B$ of indices is a Finset (Fin n); " $A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$ , together with B.card = m;
the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
"optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
"vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
Theorem 4.4.1 carries the extra hypothesis $n\ge 1$ : for $n=0$ there is no nonzero vector in $\mathbb{R}^0$ , the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$ , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

6 thms2 active usersReviewed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming I: Integral Bipartite Matchings, Total Unimodularity and König's TheoremTextbook

Motivation

Many combinatorial optimization problems are integer programs: linear objectives and linear constraints, with the extra requirement that the variables be integers. Dropping that requirement gives the LP relaxation, which is solvable efficiently but in general only bounds the integer optimum. For a small but important class of problems the relaxation loses nothing: its optimum is attained at an integral point, so linear programming solves the combinatorial problem exactly. Bipartite matching is the standard example, and the job-assignment problem that opens Chapter 3 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) is a maximum-weight perfect matching problem in a bipartite graph.

The same phenomenon, combined with linear programming duality, produces combinatorial min–max theorems. The oldest of them is König's theorem (1931) on matchings and vertex covers in bipartite graphs; Hall's marriage theorem (1935) follows from it. This mission formalizes the book's treatment of both strands: the integrality of the bipartite matching LP (Section 3.2), total unimodularity and König's theorem (Section 8.2), and, on the same objects for general graphs, the LP-rounding 2-approximation for vertex cover (Section 3.3).

Setting

Let $G = (V, E)$ be a finite simple graph. A bipartition of $G$ is a pair of disjoint sets $X, Y$ with $X \cup Y = V$ such that every edge joins a vertex of $X$ to a vertex of $Y$ ; $G$ is bipartite if it has one. A matching is a set $M \subseteq E$ in which each vertex is incident to at most one edge; a vertex cover is a set $C \subseteq V$ containing at least one end-vertex of every edge. A matching is maximum if no matching has more edges; a vertex cover is minimum if no vertex cover has fewer vertices.

The incidence matrix of $G$ has a row for each vertex and a column for each edge, with entry $1$ when the vertex lies on the edge and $0$ otherwise. A real matrix is totally unimodular if every square submatrix, obtained by deleting some rows and some columns, has determinant $0$ , $1$ or $-1$ .

Given real edge weights $w_e$ , the integer program (3.1) maximizes $\sum_{e} w_e x_e$ subject to $\sum_{e \ni v} x_e = 1$ for every vertex $v$ and $x_e \in \{0,1\}$ ; its 0/1 solutions are the perfect matchings. Its LP relaxation replaces $x_e \in \{0,1\}$ by $0 \le x_e \le 1$ . The vertex-cover relaxation (3.3) minimizes $\sum_v x_v$ subject to $x_u + x_v \ge 1$ for every edge $\{u,v\}$ and $0 \le x_v \le 1$ .

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

For every finite bipartite graph $G$ ,

\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{|C| : C \text{ a vertex cover of } G\}.

Total unimodularity (Lemmas 8.2.3–8.2.5)

A \text{ TU} \;\Rightarrow\; (A \mid e_i) \text{ TU}; \qquad A \text{ TU},\ b \in \mathbb{Z}^m,\ \max\{c^Tx : Ax \le b,\ x \ge 0\} \text{ attained} \;\Rightarrow\; \text{attained at some } x^* \in \mathbb{Z}^n;

and the incidence matrix of a bipartite graph is totally unimodular.

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

If the LP relaxation of (3.1) for a bipartite graph with real weights is feasible, it has an optimal solution with all $x_e \in \{0,1\}$ , which is also optimal for (3.1).

Consequences on the same objects

Hall's theorem (Theorem 8.2.1): if $|N(T)| \ge |T|$ for every $T \subseteq X$ , where $N(T) \subseteq Y$ is the set of neighbours of $T$ , then some matching covers every vertex of $X$ . And for an arbitrary graph, with $x^*$ optimal for (3.3), $S_{LP} = \{v : x^*_v \ge \tfrac12\}$ and $S_{OPT}$ a minimum vertex cover (§3.3, p. 38):

S_{LP} \text{ is a vertex cover and } |S_{LP}| \le 2\,|S_{OPT}| .

Significance

König's theorem says that for bipartite graphs the two natural certificates, a matching (a lower bound on any vertex cover) and a vertex cover (an upper bound on any matching), always meet. It makes maximum matchings and minimum vertex covers computable by linear programming, whereas minimum vertex cover in general graphs is NP-hard; Section 3.3's rounding bound quantifies what the LP still gives in that general case. Lemma 8.2.4 is the general tool behind this and behind the max-flow min-cut theorem that the book mentions on p. 148: any integer program with a totally unimodular constraint matrix and integral right-hand side can be solved as a linear program.

All results here are classical and proved. The formalization work is to connect them: Mathlib already has the definition of total unimodularity (Matrix.IsTotallyUnimodular), closure under appending unit-like rows, and Hall's theorem in the form of Finset.all_card_le_biUnion_card_iff_exists_injective. To the best of the drafting survey, neither König's theorem nor the total unimodularity of bipartite incidence matrices nor the integrality lemma 8.2.4 is in Mathlib, and no König statement was found among the platform's missions. The mission produces these in a form that later chapters on network flows and combinatorial duality can import.

Difficulty

The inequality "maximum matching $\le$ minimum vertex cover" is immediate, since each edge of a matching needs its own cover vertex. The difficulty is the reverse inequality, and it is exactly where bipartiteness is needed: the triangle has maximum matching $1$ and minimum vertex cover $2$ . Along the book's route, the obstacle is that LP duality equates the optima of the two relaxations, which are real numbers; one must show that both relaxations already have integral optimal solutions, which is the content of total unimodularity and Lemma 8.2.4. Theorem 3.2.1 is a separate integrality statement with equality constraints and weights of arbitrary sign; it is not a consequence of the Birkhoff–von Neumann theorem unless the graph is complete bipartite with equal sides.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality; edges are elements of Sym2 V, and a matching is a Finset (Sym2 V) of edges. Bipartiteness is the existence of finite sets $X, Y$ forming a bipartition; the empty graph and the empty vertex type are allowed and the statements remain the book's there. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Matrices are real; LP vectors are Fin n → ℝ (0-based indices) or indexed by the edge set or the vertices. An "optimal solution" is always a feasible point that is at least as good as every feasible point: no supremum or infimum over a possibly empty or unbounded set is used, and König's theorem asserts that both a maximum matching and a minimum vertex cover exist and have equal size. Lemma 8.2.4 takes $b \in \mathbb{Z}^m$ and allows real $c$ ; its conclusion is an integral optimal solution, not merely an integral feasible one. Theorem 3.2.1 is the perfect-matching version with equality constraints, not the " $\le 1$ " matching version discussed in the book's remarks.

A formalization in which König's theorem compares a supremum and an infimum of possibly empty sets, or in which "optimal" is not tied to feasibility, would be trivializing and is ruled out by these conventions.

Useful infrastructure, reusable beyond this mission: Laplace expansion arguments for totally unimodular matrices, the equivalence of the inequality form with the equational form, existence of optimal basic feasible solutions, and LP duality in inequality form (the platform's LinearOptimization.lp_strong_duality states duality for a general-form LP). Combinatorial proofs of König and Hall are equally welcome; only the statements are fixed.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §3.2–3.3 and §8.2. https://doi.org/10.1007/978-3-540-30717-4
D. Kőnig, "Gráfok és mátrixok", Matematikai és Fizikai Lapok 38 (1931), 116–119.
P. Hall, "On representatives of subsets", Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
A. J. Hoffman, J. B. Kruskal, "Integral boundary points of convex polyhedra", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956, 223–246. https://doi.org/10.1515/9781400881987-014
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, Chapter 19.

12 thms2 active usersReviewed

Algorithmic Game Theory Dynamic Programming Operations Research·Captain: mikedeng1

Bellman's Dynamic Programming VIII: Multi-Stage Games, Games of Survival and the Extended Min-Max TheoremTextbook

Why multi-stage games

Chapter X of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) carries the functional-equation method of the earlier chapters from one-player decision processes to two-player zero-sum games that are played over many stages. At each stage the two players make simultaneous choices, and those choices change the state in which the next stage is played. Games of survival are the standard example. They generalize the gambler's ruin: two players with finite resources play until one of them is ruined. The same framework is the discrete-time form of what Shapley (1953) called stochastic games. It underlies pursuit games, attrition models and the later theory of dynamic games in operations research and economics.

The chapter builds on von Neumann's min-max theorem (1928), which Bellman assumes without proof (§ 3, Eq. (3.4)). It proves three kinds of result: existence and uniqueness for the general multi-stage game equation (§§ 11–16), existence and uniqueness for games of survival with integer payoffs (§ 19), and an extended min-max theorem for ratios of bilinear forms (§ 23). Bellman proposes the ratio as a criterion for non-zero-sum games.

Setting

A matrix game is given by a real $M\times N$ matrix $A=(a_{ij})$ . Player $A$ chooses row $i$ with probability $p_i$ and player $B$ chooses column $j$ with probability $q_j$ ; $p$ and $q$ are distribution vectors (points of the standard simplex). The expected return to $A$ is

E_A(p,q)=\sum_{i,j}a_{ij}\,p_i\,q_j .

The game has value $v$ when $\max_p\min_q E_A=v=\min_q\max_p E_A$ , all extrema attained. In the Lean development this is IsMaxMinMinMaxValue, and the bilinear form is bilin.

In the general multi-stage game (§ 12) the state is a pair of vectors $P\in D\subseteq\mathbb R^n$ , $P'\in D'\subseteq\mathbb R^{n'}$ with norms $\|P\|=\sum_i|P_i|$ . In state $(P,P')$ , $A$ chooses $u$ in a choice domain $S(P,P')$ and $B$ chooses $v$ in $S'(P,P')$ . $A$ receives $R(u,v)$ , and play continues from the state $T(P,P';u,v)$ , $T'(P,P';u,v)$ with weight $h(P,P';u,v)$ . Mixed strategies $G$ , $G'$ are probability measures on the choice domains. The multi-stage game equation is

f(P,P')=\max_G\min_{G'}\iint\big[R(u,v)+h(P,P';u,v)\,f(T,T')\big]\,dG(u)\,dG'(v)=\min_{G'}\max_G[\ \cdots\ ].

A game of survival with integer payoffs (§ 19) has one integer state $x$ , the resources of $A$ out of a fixed total $d$ . $A$ is ruined at $x\le0$ and wins at $x\ge d$ . At each stage the players play the $2\times2$ game with matrix $\begin{pmatrix}-1&a\\c&-b\end{pmatrix}$ , whose entries are the transfers to $A$ .

Formalization targets

Goal: the extended min-max theorem (Chapter X, Theorem 7)

For real matrices $A=(a_{ij})$ , $B=(b_{ij})$ with $\sum_{i,j}b_{ij}p_iq_j\ge d>0$ for all distribution vectors $p,q$ ,

\max_p\min_q\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}=\min_q\max_p\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}.

It is the chapter's final result, and its statement involves only finite matrices.

Milestones

Eq. (3.4), von Neumann's theorem $V_A=V_B$ . It is already on the platform as AGT.zero_sum_minimax (existence of a saddle point) and enters as a reference.
Lemma 1: the value of a one-stage game moves by at most the largest change of its kernel, $|L(f)-L_1(F)|\le\max_{u,v}\,[\,|R-R_1|+|h|\,|f(T,T')-F(T,T')|\,]$ .
Theorem 1: under hypotheses (4a)–(4e), the multi-stage game equation has a unique solution among functions continuous on $D\times D'$ that vanish at the origin, and it is the uniform limit on bounded regions of the successive approximations.
Theorem 3: the successive approximations converge from any admissible initial function.
Theorem 4: stability, $|f(P,P')-F(P,P')|\le\sum_{n\ge0}\Delta(k^nc)$ .
Theorem 5: the game of survival equation with boundary values $0$ and $1$ has a unique solution with values in $[0,1]$ .

Significance

Theorem 7 gives a value for ratio games, the games in which a player maximizes a return per unit of a resource consumed. Bellman uses it to give a rationale for the play of non-zero-sum games (§ 24) and to derive the approximate equation (22.4) for non-zero-sum games of survival. Chapter XI, Theorem 5 generalizes it to Markovian decision processes. Theorem 1 is the existence and uniqueness result that justifies replacing an infinite game by its functional equation, and Theorems 3 and 4 make that equation usable for computation and perturbation. Theorem 5 is an early uniqueness theorem for a discrete stochastic game with absorbing boundaries.

None of these statements is formalized on the platform. Von Neumann's theorem is (AGT.zero_sum_minimax, and Sion's theorem as FamousTheorems.sion_minimax_theorem). Theorem 7 is a classical result: with a positive denominator the ratio is quasiconcave in $p$ and quasiconvex in $q$ . This mission asks for a machine-checked proof of the book's statement, by Bellman's route or by any other. Theorems 1, 3 and 4 need a formal theory of games whose mixed strategies are probability measures on moving compact choice domains. No such theory is on the platform yet.

Difficulty

The ratio in Theorem 7 is not bilinear, and in general it is neither concave in $p$ nor convex in $q$ , so neither von Neumann's theorem nor a concave-convex min-max theorem applies to it directly. For Theorem 1, the contraction argument needs each one-stage game to have a value and the value to depend continuously on the state. That requires a min-max theorem for continuous games on compact sets, together with continuity of the value when the choice domains move. In Theorem 5, existence follows from monotone iteration. The uniqueness step is the hard part: the operator is not a contraction in the sup norm, and a second solution must be ruled out even at states where the optimal mixed strategies are degenerate.

Formalization scope

Distribution vectors are points of stdSimplex ℝ ι for nonempty finite types. "Max-min equals min-max" always asserts attainment (IsGreatest/IsLeast) and never uses sSup/sInf, which return $0$ on empty or unbounded sets. Theorem 7 must not assume a saddle point; its only hypothesis is the bound on the denominator.
States are Fin n → ℝ with the $\ell^1$ norm of Eq. (12.1). Choice domains are nonempty compact sets (NonemptyCompacts), and mixed strategies are probability measures of full mass on them. "Vary continuously" in (4b), which the book does not define, is read as continuity in Mathlib's topology on nonempty compact sets (for a metric space, the topology of the Hausdorff distance).
The maxima $w(c)$ of (4d) and $\Delta(c)$ of Theorem 4 are expressed through majorants, which is equivalent to the book's condition. $k\ge0$ is stated explicitly. In Lemma 1 the kernels are assumed measurable and bounded on $S\times S'$ so that the integrals exist, and each game having a value is a hypothesis, as in Bellman's footnote 4.
Theorem 3's "converges" is stated as uniform convergence on bounded regions, the mode of Theorem 1, whose proof Theorem 3 repeats. Theorem 4's unspecified $c$ is any $c\ge\|P\|+\|P'\|$ . The book's p. 301 prints the first min-max of Theorem 4 with the subscripts $G$ , $G'$ interchanged; the equation used is that of Theorem 1.
Theorem 5 adds the implicit $d\ge1$ : for $d\le0$ the boundary conditions contradict each other. The state is an integer and $f:\mathbb Z\to\mathbb R$ .
Taking the choice domains constant would trivialize Theorem 1: condition (4d) would then force $R\equiv0$ on them. The choice domains therefore depend on the state.
Not included: Theorem 2 (optimal strategies of the infinite game, which needs a model of the game's plays), Theorem 6 (non-zero-sum survival; the boundary conditions (21.3) do not cover all states, see the moderation notes).

Contributions of reusable infrastructure are welcome: the min-max theorem for continuous games on compact sets (Eq. (4.2)), continuity of the value in the choice domains, and value iteration for contracting game operators.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics, 2010. DOI 10.2307/j.ctv1nxcw0f
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 1928. DOI 10.1007/BF01448847
L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39, 1953. DOI 10.1073/pnas.39.10.1095
M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8, 1958. DOI 10.2140/pjm.1958.8.171
I. L. Glicksberg, A further generalization of the Kakutani fixed point theorem, with application to Nash equilibrium points, Proceedings of the AMS 3, 1952. DOI 10.1090/S0002-9939-1952-0046638-5

9 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$ . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$ , or is destroyed without mining anything with probability $1 - p_1$ . Bonanza has the corresponding data $p_2$ and $r_2$ . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$ -stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$ . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$ , yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$ , $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$ ), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$ , $\sum_k p_{ik} < 1$ , $0 \le c_{ik} \le 1$ , $c_{ik} + c'_{ik} = 1$ , equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$ , (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
Theorem 2: for $0 \le p_i < 1$ , $0 \le r_i \le 1$ , the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$ , the B-branch when the reverse inequality holds, and both on equality.
Theorem 3: the same rule for two mines with $K$ outcomes per use.
Theorem 5: for each $N$ , the $N$ -stage process has exactly two decision regions: a sector along the $x$ -axis where A is optimal and a sector along the $y$ -axis where B is optimal, separated by a ray through the origin.
Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$ .
Theorem 7: if $g$ solves (5.1) with an added term $h$ , then $|f - g| \le \max_R|h|/q$ on every rectangle $R$ , where $q = \min(1-p_1, 1-p_2)$ .

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$ -stage process is a word in $n$ letters whose number of candidates grows like $n^N$ . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$ , and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$ -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$ , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$ ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$ -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$ .

Choices made explicit:

Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$ , $0 \le r_i \le 1$ .
The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$ .

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Convex Optimization Information Theory Linear algebra+1·Captain: naimengye

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$ , and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$ ? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$ , which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$ , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$ . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$ , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$ , sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$ , and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$ , write $F_T c = \sum_{j \in T} c_j v_j$ . A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$ ; with this convention $F_T c$ is just the product $Fc$ . Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$ .

Definition 1.1. For an integer $S$ , the $S$ -restricted isometry constant $\delta_S$ is the smallest quantity such that

(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$ . The $S, S'$ -restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$ . The paper writes $\theta_S$ for $\theta_{S,S}$ . These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$ , and $F$ a real $p \times m$ matrix with $FA = 0$ . Let $S \ge 1$ satisfy

\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}

If $y = Af + e$ where $e$ is supported on a set of size at most $S$ , then $f$ is the unique minimizer of $(P_1')$ .

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$ , and let $c$ be supported on a set $T$ with $|T| \le S$ . Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$ .

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$ ), and the two dual sparse reconstruction properties, Lemma 2.1 ( $\ell^2$ version) and Lemma 2.2 ( $\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$ , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$ , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$ . Given such a $w$ , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$ ; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ( $T_0 \cup T_n$ ) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$ , are what Lemma 2.1 gives for a set of size $S$ ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$ ; the mission states the lemma with $\theta_{S,S'}$ , which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$ , and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$ ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$ . The definitions are total in $S, S'$ , and each theorem carries the paper's domain conditions ( $S \ge 1$ , and $2S \le m$ , $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$ , so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$ ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$ " is a positive function of the real number $\delta_S$ , quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$ , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$ ) belong to a separate mission.

Selected references

E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

9 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VIII: Bounds on Optimal Stock AllocationsTextbook

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$ , and $J$ is the finite set of bases. For each base $j$ :

$T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$ ;
$T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$ , integers with $1 \le T^e_{ij} < T^r_{ij}$ ;
$\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$ . The latter is constant for $t \ge T^r_{ij}$ , since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
$X_{ijt}$ is the cumulative demand at base $j$ through period $t$ , a nonnegative integer random variable, nondecreasing in $t$ , with finite mean;
$h_{ij} > 0$ , $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$ , the expected cost of that period is

G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,

and stock left at the end of the horizon costs

Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$ , $t = 0, \dots, T_{i0}$ , with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$ , and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$ . The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$ , which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$ . Its largest optimal solution is written $\hat S_{ijt}$ .

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$ , for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$ ,

\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$ : its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$ .
Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$ .
The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$ .
Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$ .
Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$ , $\tilde S_{ijt} \le S^*_{ijt}$ . Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$ , also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$ , provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ .

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$ . Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$ , an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$ . This must be shown feasible, to change only $S_{ijk}$ , and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$ , and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$ , [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
$G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$ , and a tsum for $Q$ . The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$ .
"The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
"An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$ ; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$ 's series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$ ", the book's $\lceil F^{-1}\rceil$ / $\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso " $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ ". Separability is stated both for optimal plans and for optimal values.
Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$ . Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

10 thms2 active usersReviewed

Completed

Dynamic Programming Dynamical Systems·Captain: Lucas

Lindgren 2022: Dynamic-Programming Price Adjustment and Lyapunov StabilityResearch Paper

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$ , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$ , and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$ . Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$ ; the aggregate expenditure is

E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,

whose value function is $J(t,p)$ . The Hamiltonian (eq. (8)) is

H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$ , and the HJB equation (eq. (10)) reads

\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$ . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$ .

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$ , then on any interval $[t,T]$ on which

E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$ , it is strictly positive on $[t,T)$ .

Milestones

Eq. (4): under the normalization $\langle p,p\rangle=1$ , $\langle p,\dot p\rangle=0$ .
Eq. (9): for $m>0$ , $v$ minimizes $H$ if and only if $mv=-\nabla J$ .
Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .

Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$ .
Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$ .

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$ , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$ , $J=ap^2+cs$ , $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

8 thms2 active usersReviewed

Dynamic Programming Operations Research·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains I: Optimality of Order-Up-To Policies by Dynamic ProgrammingTextbook

Motivation

A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.

Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).

Setting

One item is stocked at one location. At the start of each period the inventory position $y$ is observed and a quantity $u \ge 0$ is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density $g$ on $(0,\infty)$ that is positive and continuous. Unmet demand is backordered. Costs are linear: $c$ per unit ordered, $h$ per unit on hand at the end of a period, $b$ per unit backordered at the end of a period, and future costs are discounted by $\alpha \in (0,1)$ . The one-period cost is

L(y) = \begin{cases} h\displaystyle\int_0^y (y-x)g(x)\,dx + b\int_y^\infty (x-y)g(x)\,dx, & y > 0,\\[1mm] b\displaystyle\int_0^\infty (x-y)g(x)\,dx, & y \le 0. \end{cases}

The book assumes throughout that $b > \frac{1-\alpha}{\alpha}\,c$ : the backorder cost outweighs the saving from deferring a purchase.

The $n$ -period value functions are $f_1 = L$ and, for $n \ge 2$ ,

f_n(y) = \min_{u \ge 0}\Big\{ c\,u + L(y) + \alpha\int_0^\infty f_{n-1}(y+u-x)\,g(x)\,dx \Big\}.

An order $u$ is optimal at $y$ if it attains this minimum over all $u \ge 0$ . The order-up-to rule with level $s$ orders $u(y) = \max\{0, s-y\}$ . The marginal function of eq. (2.8) is $F_n(w) = c + \alpha\int_0^\infty f_n'(w-x)\,g(x)\,dx$ . In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.

Formalization targets

Goal: Theorem 2 (p. 18) in its $n$ -period form

For every horizon $n \ge 2$ , either there is a real level $s_n^*$ with

u_n^*(y) = \max\{0,\ s_n^* - y\} \ \text{optimal for every } y,

or ordering nothing is optimal for every $y$ (level $-\infty$ ); and there is $N \ge 2$ such that the level is real for all $n \ge N$ . No value of $s_n^*$ is fixed: the goal asserts the shape of the optimal policy only.

Milestones, in attack order

$L$ is convex (p. 21).
Every $f_n$ , $n \ge 1$ , is convex (p. 19, property (c)).
Every $f_n$ is differentiable with $-(c+b) \le f_n' \le h/(1-\alpha)$ (p. 20).
Property (b): given an optimal real level $s$ for horizon $n \ge 2$ , $f_n' = -c + L'$ below $s$ and $f_n' = L' + \alpha\int_0^\infty f_{n-1}'(\cdot - x)g(x)\,dx$ from $s$ on (p. 19).
Given such a level, $F_n(w) \to (1-\alpha)c - b\alpha < 0$ as $w \to -\infty$ (p. 19).
Property (a): optimal real levels are nondecreasing in the horizon, $s_n^* \le s_{n+1}^*$ (p. 18).

Significance

The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for $(s-1,s)$ policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.

The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.

Difficulty

The argument is an induction on $n$ whose hypothesis carries convexity, the derivative formula (b), and bounds on $f_n'$ . The delicate step is the existence of a finite root of $F_n$ : its limit at $-\infty$ depends on whether the previous level was finite. For $n = 1$ nothing is ordered and the limit is $c - b\alpha$ , which the assumption $b > \frac{1-\alpha}{\alpha}c$ does not make negative. The book's base case ("left to the reader") therefore fails when $c > \alpha b$ : with $\alpha = \tfrac12$ , $c = 1$ , $b = \tfrac32$ the two-period problem never orders. The goal is corrected accordingly.

Two properties the book's induction also carries are not usable as printed. Property (d), $f_n' \le f_{n-1}'$ , is false: for large $y$ , $f_n'(y)$ approaches $h(1 + \alpha + \dots + \alpha^{n-1})$ , which increases with $n$ . The second-derivative clause of property (c) fails at $y = 0$ whenever $g(0^+) > 0$ . A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.

Formalization scope

Horizon. The book states Theorem 2 for "the optimal policy" without a horizon. Its proof is an induction on a finite horizon, and the passage $n \to \infty$ is left as a conjecture (p. 21). The goal is the finite-horizon theorem; no infinite-horizon value function is constructed.
Lead time. The proof sets $\tau = 1$ "to simplify notation"; so does the formalization. Theorem 1 (dependence on the inventory position only) and Theorem 3 (general $\tau$ , whose level equation is the conjectured infinite-horizon one) are not stated.
Level $-\infty$ . The goal allows "never order" as the order-up-to rule with level $-\infty$ and adds eventual finiteness; see Difficulty.
Added hypotheses. $c \ge 0$ , $h > 0$ (the book uses $\lim_{w\to\infty} f_n'(w - x) > 0$ ), $0 < \alpha$ (the book divides by $\alpha$ ), and a finite mean $\int_0^\infty x\,g(x)\,dx < \infty$ (without it $L$ is infinite). All are fields of Model, together with positivity and continuity of $g$ on $(0,\infty)$ , $\int_0^\infty g = 1$ , and $b > \frac{1-\alpha}{\alpha}c$ .
Minimum and derivatives. $f_n$ is defined with the infimum over $u \ge 0$ of a nonnegative quantity; optimality is always against every $u' \ge 0$ . Statements about $f_n'$ assert differentiability (Differentiable, HasDerivAt) and do not read deriv as evidence of it.
Levels. The book's $s_n^*$ is "the unique solution of (2.6)"; milestones take any real level at which the order-up-to rule is optimal.

A recursion in which ordering is restricted to order-up-to rules, or in which $f_n$ is defined through $s_n^*$ , would make the goal a tautology; here $f_n$ is defined by minimization over all $u \ge 0$ and optimality is checked against all orders.

Needed infrastructure: convexity and differentiation of parametric integrals against a density on $(0,\infty)$ , and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 2, Section 2.1. https://doi.org/10.1007/b138879
S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in K. J. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958 (no DOI).
K. J. Arrow, T. Harris and J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906814
R. Bellman, I. Glicksberg and O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

9 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Introduction to the Scenario Approach V: Support Sets Certify the Violation of Nonconvex Scenario SolutionsTextbook

Why certify nonconvex scenario solutions

The scenario approach replaces an optimization problem with uncertain constraints $\theta\in\Theta_\delta$ , $\delta\in\Delta$ , by the program that enforces only $N$ constraints $\Theta_{\delta_1},\dots,\Theta_{\delta_N}$ drawn at random from the distribution $\mathbb P$ of the uncertainty. Its solution $\theta^*$ is then judged by its violation, the probability that a new instance $\delta$ is not satisfied. For convex programs in $\mathbb R^d$ the violation is controlled by the dimension $d$ alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most $d$ support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.

Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:

2006–2008: the violation of convex scenario solutions is bounded, and then characterized exactly, in terms of $d$ .
2018: the wait-and-judge theory (Campi and Garatti, Math. Programming 2018) evaluates the violation from the number of support constraints counted after solving the program; it extends to nonconvex programs but requires a nondegeneracy assumption.
2018: Campi, Garatti and Ramponi (IEEE TAC 2018) prove a bound in terms of the size of any support set, with no convexity and no nondegeneracy assumption. This is the result formalized here, stated in the book as Eq. (8.15).

Setting

Let $\Theta$ be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let $f:\Theta\to\mathbb R$ be a cost and $\Theta_\delta\subseteq\Theta$ constraint sets indexed by $\delta\in\Delta$ , where $\Delta$ carries a probability $\mathbb P$ . Neither $f$ nor the $\Theta_\delta$ is required to be convex. With a sample $\delta_1,\dots,\delta_N$ drawn independently from $\mathbb P$ , the scenario program is

\min_{\theta\in\Theta} f(\theta)\quad\text{subject to}\quad \theta\in\bigcap_{i=1,\dots,N}\Theta_{\delta_i},\tag{8.12}

and $\theta^*$ denotes its solution, assumed to exist and be unique for every sample.

The violation of a decision is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$ (Definition 3.1).

A support set (Definition 8.8) is a subset $\{\Theta_{\delta_{i_1}},\dots,\Theta_{\delta_{i_k}}\}$ of the constraints such that the program with only these constraints in place has the same solution $\theta^*$ as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let $\sigma^*$ be the cardinality of the support set returned, for every sample, by some fixed algorithm.

Formalization targets

Goal: the support-set bound, Eq. (8.15)

For every function $\epsilon:\{0,1,\dots,N\}\to[0,1]$ with $\epsilon(N)=1$ ,

\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\sum_{k=0}^{N-1}\binom Nk\,(1-\epsilon(k))^{N-k}.

The level function $\epsilon$ is free: the statement is one inequality per admissible $\epsilon$ , and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.

Milestone: the level function for a confidence $\beta$ , Eq. (8.16)

For $\beta\in[0,1]$ let

\epsilon(k)=\begin{cases}1 & k=N,\\ 1-\sqrt[N-k]{\dfrac{\beta}{N\binom Nk}} & \text{otherwise.}\end{cases}

The arithmetic half states that $\epsilon$ maps $\{0,\dots,N\}$ into $[0,1]$ , $\epsilon(N)=1$ , and the right-hand side of (8.15) equals $\beta$ (for $N\ge1$ ). The probabilistic half states $\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\beta$ .

Significance

The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size $\sigma^*$ can assert $V(\theta^*)\le\epsilon(\sigma^*)$ with confidence $1-\beta$ . The book's Figure 8.12 shows that $\epsilon(k)$ for $\beta=10^{-6}$ remains well below $1$ for $k$ up to a sizeable fraction of $N$ . Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.

The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size $\sigma^*$ or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.

Difficulty

The natural first step is: condition on the support set being a particular index set $I$ with $|I|=k$ , and argue that the solution is then a function of the $k$ sampled constraints in $I$ alone, while the other $N-k$ samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns $I$ " depends on all $N$ samples, and the solution of the reduced program on $I$ is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that $\sigma^*$ is random and data-dependent: a bound for each fixed $k$ does not directly give a bound at the random level $\epsilon(\sigma^*)$ , and the role of the condition $\epsilon(N)=1$ must be accounted for at $k=N$ .

Formalization scope

Lean representation and committed conventions:

$\Theta$ and $\Delta$ are arbitrary types with measurable structures; $\mathbb P$ is a probability measure on $\Delta$ ; a sample is ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over $0,\dots,N-1$ .
A subset of constraints is a Finset (Fin N); the reduced program with index set $I$ has feasible set $\bigcap_{i\in I}\Theta_{\delta_i}$ (all of $\Theta$ for $I=\emptyset$ ).
The solution map $\theta^*$ is a parameter with the hypothesis that $\theta^*(\omega)$ is the unique solution of the full program for every sample.
"Has the same solution" in Definition 8.8 means: the reduced program has a unique solution and it equals the unique solution of the full program. Existence of solutions is not assumed for reduced programs in general, only for those that are support sets.
The algorithm is an arbitrary map alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; $\sigma^*$ is the cardinality of its output. The goal is universal over such maps.
$\epsilon$ is a real function on $\mathbb N$ with $\epsilon(k)\in[0,1]$ for $k\le N$ and $\epsilon(N)=1$ .
The violation is real-valued in $[0,1]$ ; the probability of the event is compared in $[0,\infty]$ with ENNReal.ofReal of the real right-hand side.

Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is measurable in $\Theta\times\Delta$ ; the solution map is measurable; each event $\{\omega:\text{the algorithm returns }J\}$ is measurable; $\theta^*$ exists and is unique for every sample; $N\ge1$ in the arithmetic half of (8.16).

A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when $f$ has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.

Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018, §8.6, pp. 101–105. https://doi.org/10.1137/1.9781611975444
M. C. Campi, S. Garatti, F. A. Ramponi, A general scenario theory for nonconvex optimization and decision making, IEEE Transactions on Automatic Control, 2018. https://doi.org/10.1109/TAC.2018.2808446
M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. https://doi.org/10.1007/s10107-016-1056-9
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control, 2006. https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization, 2008. https://doi.org/10.1137/07069821X
S. Floyd, M. Warmuth, Sample compression, learnability, and the Vapnik–Chervonenkis dimension, Machine Learning, 1995. https://doi.org/10.1007/BF00993593

7 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Information Sharing in a Supply Chain with a Common Retailer 2: Under Production Economy the Retailer Earns Weakly More from Sequential Information Contracting and the Manufacturers from ConcurrentResearch Paper

Motivation

Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.

Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).

Setting

Two manufacturers $i \in \{0,1\}$ sell substitutable products through a common retailer. 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 intensity and $\theta$ is a demand shock with mean $0$ and variance $\sigma^2 > 0$ . The retailer observes a demand signal $Y$ with $E[Y \mid \theta] = \theta$ and a linear-expectation structure $E[\theta \mid Y] = \beta Y$ , where $\beta = \beta(t,\sigma)$ is the signal weight. Producing $q$ units costs $bq - c_e q^2$ with $c_e > 0$ ; the paper writes $c = -c_e$ and assumes $c_e < 2/(1+\phi)$ (the Assumption, p. 251). Retailing is costless.

The game has three stages.

Information contracting. Under concurrent contracting the retailer offers both manufacturers the same payment $T \ge 0$ for the signal; they decide simultaneously and play a Pareto-optimal pure equilibrium. Under sequential contracting she offers a payment $T_f$ to a first manufacturer $k$ and, after his decision, a payment $T_s$ to the other; the outcome is a subgame-perfect equilibrium (SPE). The retailer commits not to share for free after a rejection (§6.2).
Pricing. Given the information statuses $X_i \in \{I, U\}$ , each manufacturer sets a wholesale price $w_i$ (a function of $Y$ if informed, a constant otherwise), then the retailer sets retail prices; the solution concept is Bayesian Nash equilibrium.
Demand realizes and profits are collected.

The ex ante profits of the pricing equilibrium are denoted $\pi_M(0)$ , $\pi_M^U(1)$ , $\pi_M^I(1)$ , $\pi_M(2)$ for a manufacturer and $\pi_R(n)$ for the retailer, $n$ the number of informed manufacturers. $n_e^N$ , $n_e^C$ , $n_e^S$ denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.

Formalization targets

Goal: Proposition 8(d)

For every $\phi > 0$ and $0 < c_e < 2/(1+\phi)$ , pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)

\Pi_R^C \le \Pi_R^S, \qquad \Pi_M^S \le \Pi_M^C ,

where $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The second inequality is asserted for all $c_e$ except at most two values depending only on $\phi$ . The comparisons about every pricing equilibrium family exclude the single value $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$ (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.

Milestones

Lemma 1: the pricing equilibrium exists and, for $c_e \ne c_e^*$ , is unique and linear in $Y$ with explicit coefficients.
§4.2: the ex ante profits $\pi_M(\cdot)$ and $\pi_R(\cdot)$ in closed form.
Lemma 5(a)–(c) and Lemma 5(d): sign comparisons of these profits in $c_e$ , with thresholds $1/(1+\phi)$ , $(4+5\phi)/[(2+3\phi)(1+\phi)]$ , $c_e^a$ and $c_e^N$ .
Proposition 7: thresholds $c_e^C$ , $c_e^S$ such that

n_e^Z = 0 \text{ for } c_e < \tfrac{1}{1+\phi}, \quad n_e^Z = 2 \text{ for } \tfrac{1}{1+\phi} \le c_e < c_e^Z, \quad n_e^Z = 1 \text{ for } c_e^Z \le c_e < \tfrac{2}{1+\phi}.

Proposition 6(b): the same structure for $n_e^N$ with a threshold $c_e^N$ .
Proposition 8(a): $c_e^N < c_e^S \le c_e^C$ .

Significance

Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.

The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.

Difficulty

The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of $(c_e, \phi)$ whose thresholds $c_e^a$ , $c_e^N$ are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.

Formalization scope

Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.

Admissible strategies are measurable with square-integrable $w_i(Y)$ , and constant for an uninformed manufacturer; ex ante optimality over them is the Bayesian equilibrium condition.
The retailer's rule is a best response for every wholesale price pair and signal value, off path included.
The production cost is the uncapped quadratic $bq - c_e q^2$ . The paper caps the quantity at $\bar q = b/(2c_e)$ but assumes the cap is reached with negligible probability (footnote 11, p. 251) and computes every result of §4.2 and §6 without it. The condition $b < a$ of that footnote is not imposed.
Contracting uses pure strategies, nonnegative payments, and no free-sharing move after a rejection.
A concurrent outcome is a payment and a pure equilibrium whose retailer payoff equals the supremum of her payoffs over Pareto-optimal equilibria. The supremum is not always attained: for large $c_e$ the paper's optimal payment $\pi_M^I(1) - \pi_M(0)$ makes $(U,U)$ an equilibrium that Pareto-dominates the one-informed outcome it selects.
Threshold statements take the two-clause form: the stated value of $n$ is attained on each region with its printed endpoints, and is the only value on the region's interior. Thresholds depend only on $\phi$ and are quantified before all other parameters.
The manufacturers' comparison in the goal excludes at most two values of $c_e$ . At the thresholds $c_e^C$ , $c_e^S$ outcomes with different manufacturer totals coexist, and the universal comparison fails.
A correction of the paper. At $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$ , which lies in $(1/(1+\phi), 2/(1+\phi))$ , the slope of the best-response wholesale price (2) is exactly $-1$ . The equations $w_i = \hat w_i(w_j)$ are then singular, and every status profile has a continuum of pricing equilibria (for $n = 0$ , $w_{1,2} = \bar w \pm t$ for every $t$ ) whose ex ante profits differ. Lemma 1's uniqueness claim fails there, so do the §4.2 identities for every equilibrium family, and so does every statement built on them. Each statement that quantifies over all pricing equilibria therefore assumes $c_e \ne c_e^*$ ; existence is still asserted at $c_e^*$ .

The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.

Selected references

Shang W., Ha A. Y., Tong S., 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
Ericson W. A., A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969 (cited for the formula of $\beta(t,\sigma)$ , which this mission does not use).
Vives X., Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999, §2.7.2.
Li L., 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

17 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization IV: Descent and Stationary Cluster Points of the Proximal Gradient MethodResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an $\ell_0$ or $\ell_{1/2}$ penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.

For a smooth part $h$ whose gradient is $L$ -Lipschitz, the classical analysis allows any constant step size $\beta \in (0, 1/L)$ , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when $h + P$ has the Kurdyka–Łojasiewicz property. When $h$ is nonconvex, however, $L$ is governed by the most negative curvature of $h$ as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of $h$ alone would require.

Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of $h$ imposes no restriction on the step size: it suffices to bound the curvature of $h$ after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . The problem is

\min_{x \in \mathbb{R}^n}\; h(x) + P(x),

under the paper's standing assumptions: $h : \mathbb{R}^n \to \mathbb{R}$ is twice continuously differentiable with a bounded Hessian $\nabla^2 h$ ; $P : \mathbb{R}^n \to (-\infty, +\infty]$ is proper (never $-\infty$ , finite somewhere) and closed (lower semicontinuous); and for every $\tau > 0$ and $u$ the proximal problem $\min_y \tau P(y) + \frac12\|y - u\|^2$ has a minimizer. Neither $h$ nor $P$ is assumed convex.

A vector $v$ is a regular subgradient of $P$ at $x$ (with $P(x) < \infty$ ) if $P(z) \ge P(x) + \langle v, z - x\rangle - \varepsilon\|z - x\|$ for all $z$ near $x$ , for every $\varepsilon > 0$ . The limiting subdifferential $\partial P(x)$ collects the limits $v = \lim v^t$ of regular subgradients $v^t$ at points $x^t \to x$ with $P(x^t) \to P(x)$ . A point $x$ is stationary if

0 \in \nabla h(x) + \partial P(x).

Given a step size $\beta > 0$ and an arbitrary starting point $x^0$ , the proximal gradient method generates $(x^t)_{t \ge 0}$ by

x^{t+1} \in \operatorname*{Arg\,min}_x \Bigl\{ \langle \nabla h(x^t), x - x^t\rangle + \frac{1}{2\beta}\|x - x^t\|^2 + P(x) \Bigr\}. \tag{43}

Any minimizer may be selected. A cluster point of $(x^t)$ is the limit of a subsequence $x^{t_i}$ .

The step-size condition involves a convex function $q$ and a constant $\ell > 0$ with

-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I \quad \text{for all } x, \tag{44}

where $\preceq$ is the Loewner order on symmetric linear maps.

Formalization targets

Goal: Theorem 4

Suppose $q$ is twice continuously differentiable and convex, $\ell > 0$ , (44) holds, and $(x^t)$ is generated by (43) with $\beta \in (0, 1/\ell)$ . Then

h(x^{t+1}) + P(x^{t+1}) \le h(x^t) + P(x^t) \quad \text{for all } t,

and every cluster point $x^*$ of $(x^t)$ , if one exists, satisfies $0 \in \nabla h(x^*) + \partial P(x^*)$ .

The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.

Milestones

In the order of the paper's proof:

Eq. (3): robustness of $\partial$ under $x^t \to x$ , $f(x^t) \to f(x)$ , $v^t \to v$ .
Eq. (45): under (44), $(h+q)(v) \le (h+q)(u) + \langle \nabla h(u) + \nabla q(u), v - u\rangle + \frac{\ell}{2}\|v - u\|^2$ .
Eq. (46): $h(x^{t+1}) + P(x^{t+1}) \le h(x^t) + P(x^t) + \bigl(\frac{\ell}{2} - \frac{1}{2\beta}\bigr)\|x^{t+1} - x^t\|^2$ .
The summed bound after (46): $\bigl(\frac{1}{2\beta} - \frac{\ell}{2}\bigr)\sum_{t=0}^{N-1}\|x^{t+1} - x^t\|^2 + h(x^N) + P(x^N) \le h(x^0) + P(x^0)$ .
Vanishing steps: if a cluster point exists, $\|x^{t+1} - x^t\| \to 0$ .
Function-value convergence: if $x^{t_i} \to x^*$ , then $P(x^{t_i+1}) \to P(x^*)$ .
Eq. (47): $0 \in \nabla h(x^t) + \frac{1}{\beta}(x^{t+1} - x^t) + \partial P(x^{t+1})$ for every $t$ .

Significance

The result. For $h = h_1 - h_2$ a difference of convex $C^2$ functions with $\nabla h_1$ being $L_1$ -Lipschitz, (44) holds with $q = h_2$ and $\ell = L_1$ , so the step size may be taken in $(0, 1/L_1)$ whatever the curvature of $h_2$ . For an indefinite quadratic $h(x) = \frac12\langle x, Qx\rangle$ the admissible range becomes $(0, 1/\lambda_{\max}(Q))$ instead of $(0, 1/\max_i|\lambda_i(Q)|)$ , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of $h + P$ , so the sequence is bounded whenever $h + P$ is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.

Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.

Difficulty

The descent part rests on (45), a descent inequality for $h + q$ whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for $h$ alone and does not apply, since $\nabla h$ may have a much larger Lipschitz constant than $\ell$ .

The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only $x^{t_i+1} \to x^*$ but also $P(x^{t_i+1}) \to P(x^*)$ , because the limiting subdifferential is closed only under $P$ -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against $x^*$ . The objective may be $+\infty$ at $x^0$ , so summability of the steps has to be extracted without assuming a finite starting value.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). $h$ and $q$ are real-valued; $P$ takes values in EReal, and every objective value $h(x) + P(x)$ is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its $\varepsilon$ -neighbourhood form, and the limiting subdifferential requires all three convergences $x^t \to x$ , $P(x^t) \to P(x)$ , $v^t \to v$ . Stationarity is $\exists w \in \partial P(x),\ \nabla h(x) + w = 0$ . The update (43) is a relation on sequences: $x^{t+1}$ minimizes the bracket over all of $\mathbb{R}^n$ , with no uniqueness and a free starting point. A cluster point is the limit of $x^{\varphi(i)}$ for a strictly increasing $\varphi$ .

Trivializing formalizations are ruled out: (44) is not replaced by " $\nabla h$ is $\ell$ -Lipschitz", which is the classical special case $q = 0$ ; $P(x^0) < \infty$ , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without $P(x^t) \to P(x)$ is not used, since that would make stationarity a weaker statement.

Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.

Selected references

G. Li and T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. Preprint arXiv:1407.0753v6. https://arxiv.org/abs/1407.0753 · https://doi.org/10.1137/140998135
H. Attouch, J. Bolte and B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems: proximal algorithms, forward–backward splitting, and regularized Gauss–Seidel methods, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
K. Bredies and D. A. Lorenz, Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009 (reference [9] of Li–Pong; no stable link recorded there).
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

13 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization III: For Semi-Algebraic Problems the ADMM Sequence Converges and Has Finite LengthResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) is a standard method for problems of the form $\min_x h(x)+P(\mathcal Mx)$ , in which a smooth loss $h$ is composed with a structured, possibly nonsmooth regularizer $P$ through a linear map $\mathcal M$ . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the $\ell_0$ constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective $\mathcal M$ . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the $x$ -block.

Setting

Fix $\mathcal M:\mathbb R^n\to\mathbb R^m$ linear, $h:\mathbb R^n\to\mathbb R$ twice continuously differentiable with bounded Hessian, and $P:\mathbb R^m\to(-\infty,+\infty]$ proper (finite somewhere) and closed (lower semicontinuous). For $\beta>0$ the augmented Lagrangian is

L_\beta(x,y,z)=h(x)+P(y)-\langle z,\mathcal Mx-y\rangle+\tfrac\beta2\|\mathcal Mx-y\|^2 .

The ADMM produces $(x^t,y^t,z^t)_{t\ge0}$ from arbitrary $(x^0,z^0)$ by

y^{t+1}\in\operatorname*{Arg\,min}_y L_\beta(x^t,y,z^t),\quad x^{t+1}\in\operatorname*{Arg\,min}_x L_\beta(x,y^{t+1},z^t),\quad z^{t+1}=z^t-\beta(\mathcal Mx^{t+1}-y^{t+1}).

Assumption 1 with $\mathcal T_1=0$ asks for $\sigma,\delta>0$ , $\gamma\in(0,1)$ and symmetric maps $\mathcal Q_1,\mathcal Q_2,\mathcal Q_3$ with $\mathcal M\mathcal M^*\succeq\sigma\mathcal I$ , $\mathcal Q_1\succeq\nabla^2h(x)\succeq\mathcal Q_2$ and $\mathcal Q_3\succeq[\nabla^2h(x)]^2$ for all $x$ , $\mathcal Q_2+\beta\mathcal M^*\mathcal M\succeq\delta\mathcal I$ , and $\delta\mathcal I\succ\frac{2}{\sigma\beta\gamma}\mathcal Q_3$ .

The limiting subdifferential $\partial f(x)$ of $f$ consists of limits $v$ of regular subgradients $v^t$ at points $x^t\to x$ with $f(x^t)\to f(x)$ . A point $x$ is stationary if $0\in\nabla h(x)+\mathcal M^*\partial P(\mathcal Mx)$ .

A set in $\mathbb R^N$ is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations $p_i=0$ and strict inequalities $g_j<0$ ; a function is semi-algebraic if its graph is. A proper $f$ has the KL property at $\hat x\in\operatorname{dom}\partial f$ if there are $\eta>0$ , a neighbourhood $V$ of $\hat x$ and a continuous concave $\varphi:[0,\eta)\to\mathbb R_+$ with $\varphi(0)=0$ , $\varphi\in C^1(0,\eta)$ , $\varphi'>0$ , such that $\varphi'(f(x)-f(\hat x))\,\operatorname{dist}(0,\partial f(x))\ge1$ whenever $x\in V$ and $f(\hat x)<f(x)<f(\hat x)+\eta$ . A KL function is proper, closed, and KL at every point of $\operatorname{dom}\partial f$ .

In the Lean development $L_\beta$ is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space $\mathbb R^n\times\mathbb R^m\times\mathbb R^m$ with the Euclidean inner product.

Formalization targets

Goal: Theorem 3 (p. 13)

Under the standing assumptions and Assumption 1 with $\mathcal T_1=0$ , if $h$ and $P$ are semi-algebraic and the ADMM sequence has a cluster point $(x^*,y^*,z^*)$ , then

(x^t,y^t,z^t)\to(x^*,y^*,z^*),\qquad 0\in\nabla h(x^*)+\mathcal M^*\partial P(\mathcal Mx^*),\qquad \sum_{t}\|x^{t+1}-x^t\|<\infty .

No constants are fixed: every parameter is quantified exactly as in the paper.

Milestones

(35): some $w\in\partial L_\beta(x^{t+1},y^{t+1},z^{t+1})$ has $\|w\|\le C\|x^{t+1}-x^t\|$ for $t\ge1$ .
(36): $L_\beta(x^t,y^t,z^t)-L_\beta(x^{t+1},y^{t+1},z^{t+1})\ge D\|x^{t+1}-x^t\|^2$ for $t\ge1$ .
(39): $L_\beta(x^t,y^t,z^t)\to L_\beta(x^*,y^*,z^*)$ .
Finite termination when $L_\beta$ reaches its limit value.
(41): the one-step KL estimate.
Remark 4(1): the goal with " $L_\beta$ is a KL function" in place of semi-algebraicity.
$L_\beta$ is semi-algebraic when $h$ and $P$ are.
Proper closed semi-algebraic functions are KL functions, with $\varphi(s)=cs^{1-\theta}$ .

Milestones 6, 7 and 8 together imply the goal.

Significance

The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the $x$ -trajectory, for a nonconvex ADMM without any convexity of $h$ or $P$ . Semi-algebraicity covers the paper's applications: polynomial losses, the $\ell_0$ constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of $L_\beta$ , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).

Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.

Difficulty

The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires $L_\beta$ to drop by a multiple of $\|x^{t+1}-x^t\|^2+\|y^{t+1}-y^t\|^2+\|z^{t+1}-z^t\|^2$ , while the ADMM only guarantees a drop proportional to $\|x^{t+1}-x^t\|^2$ (Remark 4(2)). The relative-error bound (35) is likewise in terms of the $x$ -step alone, and relating the $y$ - and $z$ -blocks back to the $x$ -block uses the surjectivity of $\mathcal M$ and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in $x$ .

The semi-algebraic part has a separate difficulty: showing that $L_\beta$ is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ its adjoint. $P$ and $L_\beta$ take values in EReal, never passed through toReal except where the value is provably finite. $\succeq$ is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with $\phi=0$ ; argmin steps are "value at most the value anywhere", with no uniqueness; $y^0$ is unconstrained. The triple space is the nested $L^2$ product, so its inner product is the sum of the block inner products.

The KL inequality is stated for every $v\in\partial f(x)$ , which encodes $\operatorname{dist}(0,\emptyset)=+\infty$ . Writing it with Metric.infDist 0 (∂f x) would give $\operatorname{dist}(0,\emptyset)=0$ and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of $\operatorname{dom}\partial f$ , only on a neighbourhood and only for values in $(f(\hat x),f(\hat x)+\eta)$ ; $\varphi$ is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. $\eta$ is a positive real, which is equivalent to the paper's $\eta\in(0,\infty]$ .

The hypotheses $\phi=0$ and $\mathcal T_1=0$ are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.

Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.

Selected references

G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://arxiv.org/abs/1407.0753 (v6 is the cited version)
H. Attouch, J. Bolte, P. Redont, A. Soubeyran, Proximal alternating minimization and projection methods for nonconvex problems: an approach based on the Kurdyka–Łojasiewicz inequality, Math. Oper. Res. 35(2), 2010. https://doi.org/10.1287/moor.1100.0449
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4), 2007. https://doi.org/10.1137/050644641
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

17 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization II: The Proximal ADMM Sequence Is Bounded Under CoercivityResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) splits a problem of the form $\min_x h(x) + P(\mathcal M x)$ into a sequence of simpler subproblems, one in which the nonsmooth term $P$ enters only through its proximal map and one in which only the smooth term $h$ appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as $\ell_0$ - or $\ell_{1/2}$ -regularized least squares, where $P$ is nonconvex and possibly discontinuous and convex theory does not apply.

Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on $h$ , $P$ and $\mathcal M$ under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.

Setting

Let $n, m \ge 0$ . The data are:

$h : \mathbb{R}^n \to \mathbb{R}$ , twice continuously differentiable with bounded Hessian $\nabla^2 h$ ;
$P : \mathbb{R}^m \to (-\infty, +\infty]$ , proper (never $-\infty$ , finite somewhere) and closed (lower semicontinuous);
$\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ linear, with adjoint $\mathcal M^*$ ;
a penalty $\beta > 0$ and a convex, twice continuously differentiable $\phi : \mathbb{R}^n \to \mathbb{R}$ .

The augmented Lagrangian is

L_\beta(x, y, z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac{\beta}{2}\|\mathcal M x - y\|^2 ,

and the Bregman distance of $\phi$ is $D_\phi(x_1, x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$ . A sequence $(x^t, y^t, z^t)_{t\ge 0}$ is generated by the proximal ADMM if, from arbitrary $x^0, z^0$ ,

y^{t+1} \in \operatorname*{Arg\,min}_y L_\beta(x^t, y, z^t), \quad x^{t+1} \in \operatorname*{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\}, \quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).

For a linear self-map $\mathcal T$ , write $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ , and write $\succeq$ , $\succ$ for the semidefinite and definite order of symmetric maps. Assumption 1 asks for $\sigma > 0$ with $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ (so $\mathcal M$ is surjective), bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$ , maps $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$ with $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$ , $\delta > 0$ with $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$ , a bound $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2\phi]^2$ , and $\gamma \in (0,1)$ with

\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\Bigl(\frac1\gamma\mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\Bigr).

Formalization targets

Goal: Theorem 2 (p. 11)

Suppose Assumption 1 holds and, with the same $\sigma$ and $\gamma$ , there is $0 < \zeta < 2\beta\gamma$ with

h_0 := \inf_x\Bigl\{h(x) - \frac{1}{\sigma\zeta}\|\nabla h(x)\|^2\Bigr\} > -\infty. \tag{29}

Suppose that either (i) $\mathcal M$ is invertible and $\liminf_{\|y\|\to\infty} P(y) = \infty$ , or (ii) $\liminf_{\|x\|\to\infty} h(x) = \infty$ and $\inf_y P(y) > -\infty$ . Then

\sup_{t \ge 0}\ \bigl(\|x^t\| + \|y^t\| + \|z^t\|\bigr) < \infty .

Milestones

The milestones are the numbered displays of the paper's proof:

Eq. (13): $\mathcal M^* z^{t+1} = \nabla h(x^{t+1}) + \nabla\phi(x^{t+1}) - \nabla\phi(x^t)$ .
Eq. (20): the one-step estimate $L_\beta(w^{t+1}) \le L_\beta(w^t) + \tfrac12\|x^{t+1}-x^t\|^2_{\frac{2}{\sigma\beta\gamma}\mathcal Q_3 - \delta\mathcal I - \mathcal T_2} + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ for $t \ge 1$ .
Eq. (30): the merit quantity $L_\beta(w^t) + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ stays below its value at $t = 1$ .
Eq. (31): $\sigma\|z^t\|^2 \le \frac1\gamma\|\nabla h(x^t)\|^2 + \frac1{1-\gamma}\|x^t - x^{t-1}\|^2_{\mathcal T_1^2}$ for $t \ge 1$ .
Eq. (32): a lower estimate of that value at $t = 1$ by $\mu h(x^t) + (1-\mu)h_0 + \frac{c}{\sigma}\|\nabla h(x^t)\|^2 + P(y^t) + \frac\beta2\|\mathcal M x^t - y^t - z^t/\beta\|^2 + \ldots$ , where $c = \frac{1-\mu}{\zeta} - \frac{1}{2\beta\gamma} > 0$ .

Significance

The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with $\mathcal M = \mathcal I$ , and a strongly convex quadratic $h$ with a regularizer that is bounded below and a general surjective $\mathcal M$ falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.

Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.

Difficulty

The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves $L_\beta$ , which contains $-\langle z, \mathcal M x - y\rangle$ and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through $\nabla h(x^t)$ and the last primal step, and the part involving $\|\nabla h(x^t)\|^2$ is then paid for out of $h$ itself. Condition (29) exists to make exactly this trade possible, which is why it couples $\zeta$ to the $\gamma$ of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from $y^t$ through $z^t$ to $x^t$ using invertibility of $\mathcal M$ , and (ii) goes from $x^t$ through $z^t$ to $y^t$ . In case (i) the lower bound on $P$ that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.

Formalization scope

Spaces and values. Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and $\mathcal M$ is a continuous linear map with Mathlib's adjoint. $P$ , $L_\beta$ and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.
Assumption 1 is one definition with its witnesses $\sigma, \delta, \gamma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \mathcal Q_3$ as explicit parameters, and $\succeq$ is Mathlib's Loewner order on self-maps. $\|x\|^2_{\mathcal T}$ is $\langle x, \mathcal T x\rangle$ for every $\mathcal T$ , including indefinite ones.
Condition (29) takes $\zeta$ and a real lower bound $h_0$ as parameters, with the same $\sigma$ and $\gamma$ as Assumption 1.
The algorithm is a relation on sequences. An argmin is a global minimizer, not necessarily unique. $x^0$ and $z^0$ are free, and $y^0$ is unconstrained. No existence of minimizers is asserted.
Coercivity is stated in its $\forall r\,\exists R$ form, and "invertible" is bijectivity of $\mathcal M$ .
Boundedness means one radius for all three blocks and all $t \ge 0$ .

Ruling out trivial versions. A formalization that bounds only $x^t$ , fixes $\gamma$ or $\zeta$ to an example's values, lets (29) use a fresh $\gamma$ , adds a lower bound on $P$ in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.

Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound $\|\nabla\phi(a) - \nabla\phi(b)\|^2 \le \|a-b\|^2_{\mathcal T_1^2}$ from the Hessian sandwich, and strong convexity of the $x$ -subproblem. Proofs of individual milestones are welcome independently.

Selected references

G. Li and T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015; preprint arXiv:1407.0753v6. https://arxiv.org/abs/1407.0753 (DOI 10.1137/140998135)
S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Found. Trends Mach. Learn. 3(1), 2011. https://doi.org/10.1561/2200000016
H. Attouch, J. Bolte and B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 2: Johnson's Rule for Three MachinesResearch Paper

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

Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
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

13 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Robustness and Generalization IV: Robustness of the Lasso on a Compact Sample SpaceResearch Paper

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

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$ .
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.

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

7 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?

Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.

Setting

A Bayesian routing game $\Gamma(\lambda)$ has a single origin–destination pair, a finite set of edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ (each route a set of edges), and a finite set of network states $\mathcal S$ . Travelers of total demand $D>0$ are split into populations $i\in\mathcal I$ , one per TIS; population $i$ has size $\lambda^iD$ , where the size vector $\lambda$ lies in the simplex $\Delta=\{\lambda:\lambda^i\ge0,\ \sum_i\lambda^i=1\}$ . Each population receives a signal (its type) $t^i$ from a finite set $\mathcal T^i$ ; states and type profiles $t=(t^i)_i$ are drawn from a common prior $\pi\in\Delta(\mathcal S\times\mathcal T)$ . Edge $e$ in state $s$ has cost $c^s_e(w)$ at load $w$ , positive, strictly increasing and differentiable.

A strategy profile $q$ assigns to each population and type a split $q^i_r(t^i)\ge0$ of its demand over routes, with $\sum_rq^i_r(t^i)=\lambda^iD$ ; these form the polytope $\mathcal Q(\lambda)$ . It induces route flows $f_r(t)=\sum_iq^i_r(t^i)$ and edge loads $w_e(t)=\sum_{r\ni e}f_r(t)$ . A traveler of population $i$ with signal $t^i$ forms the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ and evaluates the expected route cost $\mathbb E[c_r(q)\mid t^i]=\sum_{s,t^{-i}}\sum_{e\in r}\beta^i(s,t^{-i}\mid t^i)\,c^s_e(w_e(t))$ . A Bayesian Wardrop equilibrium (BWE) is a $q\in\mathcal Q(\lambda)$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is

C^{i*}(\lambda)=\sum_{t^i\in\mathcal T^i}\Pr(t^i)\min_{r\in\mathcal R}\mathbb E[c_r(q^*)\mid t^i].

The weighted potential is $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$ , and $\Psi(\lambda)=\min_{q\in\mathcal Q(\lambda)}\Phi(q)$ is its equilibrium value. In route-flow form, $\widehat\Phi(f)$ is the same expression in terms of $f$ ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand $D$ , nonnegativity) and one information impact constraint per population, $\widehat J^i(f)\le\lambda^iD$ , where $\widehat J^i(f)=D-\sum_r\min_{t^i}f_r(t^i,\widehat t^{-i})$ measures how much of the demand reacts to population $i$ 's signal. Let $\mathcal F^\dagger$ be the set of minimizers of $\widehat\Phi$ subject to (14a)–(14c) only, and

\Lambda^\dagger=\{\lambda\in\Delta:\ \exists f^\dagger\in\mathcal F^\dagger,\ \widehat J^i(f^\dagger)\le\lambda^iD\ \ \forall i\}.

In the two-stage game, travelers first choose a TIS, inducing $\lambda$ , and then play $\Gamma(\lambda)$ . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:

\lambda^i>0\ \Longrightarrow\ C^{i*}(\lambda)=\min_{j\in\mathcal I}C^{j*}(\lambda)\qquad\forall i\in\mathcal I.\tag{31}

Formalization targets

Goal: Theorem 4

For every $\lambda\in\Delta$ and every BWE of $\Gamma(\lambda)$ ,

(31)\ \text{holds}\iff\lambda\in\Lambda^\dagger .

With the existence of a BWE for every $\lambda\in\Delta$ , this is the paper's statement that the set of equilibrium adoption rates is $\Lambda^\dagger$ .

Milestones

Theorem 1. $q$ is a BWE of $\Gamma(\lambda)$ iff $q$ minimizes $\Phi$ over $\mathcal Q(\lambda)$ ; the equilibrium edge load $w^*(\lambda)$ is unique.
Proposition 2. A route flow in the flow polytope $\mathcal F(\lambda)$ ((14a)–(14c) plus all information impact constraints) is an equilibrium flow iff it minimizes $\widehat\Phi$ over $\mathcal F(\lambda)$ .
Lemma 5. $\Psi$ is convex on $\Delta$ , and with $z^{ij}=e_i-e_j$ and $V^{ij*}=C^{j*}-C^{i*}$ ,

\lim_{\epsilon\to0^+}\frac{\Psi(\lambda+\epsilon z^{ij})-\Psi(\lambda)}{\epsilon}=-D\,V^{ij*}(\lambda).

Proposition 5. $\Lambda^\dagger$ is convex, $\Lambda^\dagger=\operatorname{argmin}_{\lambda\in\Delta}\Psi(\lambda)$ , and the equilibrium edge load equals the size-independent load $w^\dagger$ of $\mathcal F^\dagger$ iff $\lambda\in\Lambda^\dagger$ .

A separate item states the existence of a BWE for every $\lambda\in\Delta$ .

Significance

The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On $\Lambda^\dagger$ the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.

Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).

Difficulty

The direction " $\lambda\in\Lambda^\dagger$ implies (31)" is not a pointwise statement about costs: it follows from $\Lambda^\dagger$ being the argmin of $\Psi$ together with the formula linking directional derivatives of $\Psi$ to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with $\lambda$ ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors ( $\lambda^i=0$ ) that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity $\Lambda^\dagger=\operatorname{argmin}\Psi$ needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.

Formalization scope

The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, $D>0$ , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of $\mathbb R$ , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).

Conventions: size vectors range over the probability simplex; $\Psi$ is the infimum of $\Phi$ over $\mathcal Q(\lambda)$ and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); $C^{i*}$ is the last form of the paper's (7), well defined when $\lambda^i=0$ ; $\widehat J^i$ is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; $\mathcal F^\dagger$ and similar sets are argmin sets. Lemma 5 is stated for the directions $z^{ij}$ with $\lambda^j>0$ (otherwise $\lambda+\epsilon z^{ij}$ leaves the simplex); $\lambda^i=0$ is allowed.

A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and $\Lambda^\dagger$ is defined by (30) from the flow problem (28), not as the argmin of $\Psi$ , so the goal is not a restatement of Proposition 5.

Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope $\mathcal F(\lambda)$ ), are welcome.

Selected references

M. Wu, S. Amin, A. E. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999 (preprint: https://arxiv.org/abs/1808.10590)
W. H. Sandholm, Potential games with continuous player sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
A. V. Fiacco, J. Kyparisis, Convexity and concavity properties of the optimal value function in parametric nonlinear programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986. https://doi.org/10.1007/BF00938592

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program II: Stability of the Deterministic Equivalent Convex ProgramResearch Paper

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

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$ .
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)$ .
Theorem 7.6 (p. 329). $Z$ is convex on $K$ , and it is either finite on $K$ or identically $-\infty$ on $K$ .
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).
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

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program I: The Induced Feasibility Region Is a Closed Convex Polyhedron When T Is FixedResearch Paper

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

Theorem 4.1. Under weak covariance, $K_2^\mu = K_2^p = K_2^s$ .
Corollary 4.5. Under weak covariance, $K_2 = K_2^p = K_2^\mu = K_2^s$ .
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)$ .
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

8 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research·Captain: mikedeng1

A New Projection Method for Variational Inequality Problems: The Hyperplane Projection Method Converges to a Solution Under Continuity and Generalized MonotonicityResearch Paper

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

16 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Operations Research·Captain: mikedeng1

Conjugate Gradient Methods with Inexact Searches: The Self-Scaled Direction Is a Multiple of Beale's Restart DirectionResearch Paper

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

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Information Sharing in a Supply Chain with a Common Retailer 1: Under Production Diseconomy the Retailer Earns More from Sequential Information Contracting and the Manufacturers from ConcurrentResearch Paper

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.

The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$ . The retailer then sets retail prices.
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

§4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$ .
§4.2: the closed forms of the seven ex ante profits.
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)$ .
Proposition 1(b): without contracting, no information is shared.
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.
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.

17 thms2 active usersReviewed

Missions

Understanding and Using Linear Programming VIII: The Delsarte Linear Programming Bound for Binary CodesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming VII: LP Rounding Schedules Unrelated Machines Within Twice the Optimal MakespanTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.3.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming VI: The Minimax Theorem for Zero-Sum GamesTextbook

Why zero-sum games belong in a linear programming course

Setting

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming V: The Primal–Dual Central Path and the Self-Dual EmbeddingTextbook

Motivation

Setting

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming I: Integral Bipartite Matchings, Total Unimodularity and König's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

Total unimodularity (Lemmas 8.2.3–8.2.5)

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

Consequences on the same objects

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming VIII: Multi-Stage Games, Games of Survival and the Extended Min-Max TheoremTextbook

Why multi-stage games

Setting

Formalization targets

Goal: the extended min-max theorem (Chapter X, Theorem 7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Setting

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for nnn mines)

Milestones

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Goal: Theorem 2 (p. 18) in its $n$ -period form

Milestone: the level function for a confidence $\beta$ , Eq. (8.16)