Operations Research

Motivation

Decisions under uncertainty are often modelled by a finite set of scenarios: possible futures $s\in S$ with weights $p_s$, each with its own optimization problem. Solving every scenario separately is easy but useless in practice, because the decision taken today cannot depend on which scenario will be revealed tomorrow. Progressive hedging, introduced by Rockafellar and Wets in Scenarios and policy aggregation in optimization under uncertainty (IIASA Working Paper WP-87-119, 1987; Mathematics of Operations Research 16(1), 1991), restores this nonanticipativity by iterating between scenario-wise solves and an averaging step, guided by price systems that act as multipliers. It is the standard decomposition method for multistage stochastic programs and is implemented in widely used software such as PySP/mpi-sppy. This mission formalizes the paper's convergence theorem in the convex case, Theorem 5.1, together with the duality theory of §4 and the proof steps of §5 it rests on.

Setting

Let $S$ be a finite set of scenarios with weights $p_s>0$, $\sum_s p_s=1$. For each $s$ the scenario subproblem $(P_s)$ is to minimize $f_s(x)$ over $x\in C_s\subset\mathbb R^n$, where $C_s$ is nonempty and closed and $f_s$ is locally Lipschitz with bounded level sets $\{x\in C_s\mid f_s(x)\le\alpha\}$. The convex case is when every $f_s$ and $C_s$ is convex.

A decision vector is split by time, $x=(x_1,\dots,x_T)$. A policy is a map $X:S\to\mathbb R^n$; the policy space $\mathcal E$ carries the inner product $\langle X,Y\rangle=\sum_s p_s X(s)\cdot Y(s)$ and norm $\|X\|=\langle X,X\rangle^{1/2}$. At each time $t$ the scenarios are partitioned into bundles $A\in\mathcal A_t$ of scenarios that cannot yet be told apart. The aggregation $\hat X=JX$ replaces $X_t(s)$ by its $p$-weighted average over the bundle of $s$ at time $t$, and $K=I-J$. The implementable policies are $\mathcal N=\{X\mid X_t$ constant on each $A\in\mathcal A_t\}$, the price systems are $\mathcal M=\{W\mid JW=0\}=\mathcal N^\perp$, and the admissible policies are $\mathcal C=\{X\mid X(s)\in C_s\ \forall s\}$. With $F(X)=\sum_s p_s f_s(X(s))$ the problem is

$$(P)\qquad \text{minimize } F(X) \text{ subject to } X\in\mathcal C\cap\mathcal N .$$

Its Lagrangian is $L(X,W)=F(X)+\langle X,W\rangle$ on $\mathcal C\times\mathcal M$, the dual is $(D)$: maximize $G(W)=\inf_{X\in\mathcal C}L(X,W)$ over $W\in\mathcal M$ with $G(W)>-\infty$.

The progressive hedging algorithm fixes $r>0$, starts from any $X^0$ and any $W^0\in\mathcal M$, and in iteration $\nu$ sets $\hat X^\nu=JX^\nu$, lets $X^{\nu+1}(s)$ minimize

$$f_s(x)+x\cdot W^\nu(s)+\tfrac12 r\,|x-\hat X^\nu(s)|^2\quad\text{over } x\in C_s$$

for every scenario, and updates $W^{\nu+1}=W^\nu+rKX^{\nu+1}$.

Formalization targets

Goal: Theorem 5.1

In the convex case with exact minimization, the sequences $\{\hat X^\nu\}$ and $\{W^\nu\}$ are bounded if and only if (P) and (D) have optimal solutions. In that case there are optimal $X^*$ for (P) and $W^*$ for (D) with

$$\hat X^\nu\to X^*,\qquad W^\nu\to W^*,$$

and, with $\|(X,W)\|_r=(\|X\|^2+r^{-2}\|W\|^2)^{1/2}$,

$$\|(\hat X^{\nu+1},W^{\nu+1})-(X^*,W^*)\|_r\le\|(\hat X^{\nu},W^{\nu})-(X^*,W^*)\|_r$$

for all $\nu\ge0$, strictly unless $(\hat X^\nu,W^\nu)=(X^*,W^*)$, and the step lengths $\|(\hat X^{\nu+1},W^{\nu+1})-(\hat X^\nu,W^\nu)\|_r$ are nonincreasing from $\nu=1$ on.

Milestones

1. Propositions 3.1–3.3: existence for the scenario subproblems, the lower bound $\hat\alpha=\min_{\mathcal C}F=E\{\min(P_s)\}\le\min(P)$, well-posedness of every modified subproblem (unique solution in the convex case), and compact level sets of $F$ on $\mathcal C$.
2. Theorem 4.2 and Proposition 4.4 (in the convex case): the scenario-wise subgradient conditions $-W^*(s)\in\partial f_s(X^*(s))+N_{C_s}(X^*(s))$ are equivalent to a saddle point of $L$, and the analogous conditions are necessary and sufficient for the iterates.
3. Proposition 4.5 and Theorem 4.6: the perturbation function $\Phi(U)=\min\{F(X)\mid X\in\mathcal C,\ KX=U\}$ and the duality $-\infty<\min(P)=\sup(D)$, $\operatorname{argmax}(D)=-\partial\Phi(0)$.
4. Proposition 5.3: each iteration is the unique saddle point of a proximal saddle function.
5. From the proof of Theorem 5.1: firm nonexpansiveness (5.26) of the iteration map in $\|\cdot\|_r$, and the identification of its fixed points with primal–dual optimal pairs.

Significance

Theorem 5.1 is the guarantee behind progressive hedging in the convex case: solving only small scenario problems and averaging, the method finds a nonanticipative optimal policy and an optimal price system whenever these exist, with a distance to the solution that never increases. The dual sequence $W^\nu$ converges to a solution of (D), which gives the prices of information that the paper interprets economically. Boundedness of the iterates is an exact test for solvability.

The result is classical and fully proved on paper; its proof reduces the algorithm to Rockafellar's proximal point algorithm for a maximal monotone operator. No machine-checked version is known to exist. The mission produces a formal statement and, eventually, a proof of the full chain from scenario data to convergence, including the duality theorem of §4, which is of independent use for scenario-based stochastic programming. A related platform mission in this series treats the nonconvex case (limits of the algorithm satisfy first-order conditions).

Difficulty

The algorithm is not a proximal point method in the variable $X$: it acts on the pair $(\hat X,W)$, and the averaged policy $\hat X^\nu$ is in general not admissible while $X^\nu$ is in general not implementable. The step that fails in a direct attempt is showing that the map $(\hat X^\nu,W^\nu)\mapsto(\hat X^{\nu+1},W^{\nu+1})$ is firmly nonexpansive, which requires recognizing it as the resolvent of the monotone operator of a saddle function restricted to $\mathcal N\times\mathcal M$, in the rescaled norm $\|\cdot\|_r$ rather than in the original product norm. A second difficulty is duality: identifying the fixed points of the iteration with optimal pairs of (P) and (D) needs the convex duality theory of §4 for an extended-real-valued perturbation function without any constraint qualification.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); policies are functions S → EuclideanSpace ℝ (Fin n) with S a Fintype. Time periods are a monotone map assigning each coordinate to its period, and each $\mathcal A_t$ is a Setoid S; no refinement between periods is assumed. The standing assumptions of §3 are fields of the model structure, and the convex case is a separate hypothesis.

The inner product (2.2), norm (2.3) and $\|\cdot\|_r$ (5.2) are explicit weighted sums. Mathlib's norm on a function type is the sup norm; it is used only for topology (boundedness, convergence, local Lipschitz continuity, compactness), which coincides with that of (2.3) in finite dimension. Stating (5.3) or (5.26) with Mathlib's sup norm would change the inequalities and is ruled out. Optimal values $\min(P)$, $\sup(D)$, $G$, $\Phi$, $\hat\alpha$ and $\ell$ are EReal infima and suprema, so that infeasibility gives $+\infty$ and an unbounded dual objective gives $-\infty$; real-valued sInf would silently return $0$ there. A solution of (D) must have $G(W^*)>-\infty$. The algorithm is a predicate on sequences, with $X^0$ arbitrary and $W^0\in\mathcal M$; Proposition 3.2 shows the predicate is satisfiable.

Subgradients and normal cones are those of convex analysis; the normal cone is the published definition FirstOrderOpt.ConvexTheory.normalCone. Not formalized: the nonconvex (Clarke) parts of §4, the linear-quadratic case and its rate result, and inexact minimization.

A complete development needs: separable minimization over product sets, finite-dimensional compactness arguments, convex duality for a perturbation function on a subspace, and the convergence of the proximal point algorithm for maximal monotone operators (Rockafellar 1976, Theorem 1 and Proposition 1). The last two are reusable well beyond this mission; contributions of either as standalone results are welcome.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, IIASA Working Paper WP-87-119, 1987; Mathematics of Operations Research 16(1):119–147, 1991. https://pure.iiasa.ac.at/id/eprint/2933/ — https://doi.org/10.1287/moor.16.1.119
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5):877–898, 1976. https://doi.org/10.1137/0314056
• G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Mathematical Journal 29(3):341–346, 1962. https://doi.org/10.1215/S0012-7094-62-02933-2
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A two-stage stochastic program with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a second-stage (recourse) decision is chosen after the outcome is known, both subject to constraints and both incurring costs. The model is the standard framework for planning under uncertainty in operations research: capacity planning, production and inventory, energy dispatch, finance.

For linear recourse problems, duality was developed in the 1960s and early 1970s by Wets and others, partly under integrability restrictions on the random data. R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality (Pacific J. Math. 62 (1976), doi:10.2140/pjm.1976.62.173), treat the convex case, where every cost and constraint function is convex, by embedding the problem in a family of perturbed problems and applying the perturbational theory of convex duality (Rockafellar, Conjugate Duality and Optimization, SIAM 1974) together with the theory of convex integral functionals. The paper's dual variables are integrable price systems, interpreted as equilibrium prices for perturbations of the constraints; it is the starting point of a series of papers by the same authors on stochastic convex programming (relatively complete recourse, Kuhn–Tucker conditions, singular multipliers).

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. A vector $x_1\in\mathbb R^{n_1}$ is chosen subject to $x_1\in C_1$ and $f_{1i}(x_1)\le 0$ ($i=1,\dots,m_1$), at cost $f_{10}(x_1)$. Then $s\in S$ is observed and $x_2(s)\in\mathbb R^{n_2}$ is chosen subject to $x_2(s)\in C_2$ and $f_{2i}(s,x_1,x_2(s))\le 0$ ($i=1,\dots,m_2$), at cost $f_{20}(s,x_1,x_2(s))$. The aim is to minimize the expected cost

$$f_{10}(x_1)+\int_S f_{20}(s,x_1,x_2(s))\,\sigma(ds).$$

The standing assumptions are: $C_1$, $C_2$ convex, closed and nonempty; $f_{1i}$ and $f_{2i}(s,\cdot,\cdot)$ convex and finite everywhere; $s\mapsto f_{2i}(s,x_1,x_2)$ measurable, summable for $i=0$ and bounded for $i\ge 1$.

Decisions live in $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$ and perturbations in $U=\mathbb R^{m_1}\times\mathcal L^\infty_{m_2}$. The perturbation functional $F(x,u)$ is the expected cost if $x$ satisfies the constraints with right-hand sides $u_1$ and, almost surely, $u_2(s)$, and $+\infty$ otherwise. The problem $\mathbf P$ minimizes $F(x,0)$.

The space $Y=\mathbb R^{m_1}\times\mathcal L^1_{m_2}$ is paired with $U$ by $\langle u,y\rangle=u_1\cdot y_1+\int_S u_2(s)\cdot y_2(s)\,\sigma(ds)$, and $V=\mathbb R^{n_1}\times\mathcal L^1_{n_2}$ with $X$ in the same way. The Lagrangian is $L(x,y)=\inf_{u\in U}\{\langle u,y\rangle+F(x,u)\}$, the dual $\mathbf D$ maximizes $g(y)=\inf_{x\in X}L(x,y)$ over $y\in Y$, and the perturbation function is $\varphi(u)=\inf_{x\in X}F(x,u)$. Conjugates $\varphi^*$, $\varphi^{**}$ are taken with respect to the pairing of $U$ with $Y$.

Formalization targets

Goal: Theorem 3

If $C_1$ and $C_2$ are bounded, then

$$\min\mathbf P=\sup\mathbf D>-\infty,$$

and in fact $\varphi$ is a proper convex function on $U$, lower semicontinuous for the weak topology $\sigma(U,Y)$, the infimum defining $\varphi(u)$ is attained for every $u\in U$, and $\varphi^{**}=\varphi$. The goal is the theorem exactly as printed, all conclusions included.

Milestones

1. p. 174: for bounded measurable $x_1(\cdot)$, $x_2(\cdot)$, the functions $s\mapsto f_{2i}(s,x_1(s),x_2(s))$ are measurable, summable for $i=0$ and essentially bounded for $i\ge1$.
2. Proposition 3: $F$ is convex, not identically $+\infty$, and lower semicontinuous on $X\times U$ for the norm topology and for the weak topology induced by $V\times Y$.
3. (4.9): with $C_1,C_2$ bounded, $X_0=\{x: x_1\in C_1,\ x_2(s)\in C_2\text{ a.s.}\}$ is weakly compact in $X$, and $X_0'=\{x_2\in\mathcal L^\infty_{n_2}: x_2(s)\in C_2\text{ a.s.}\}$ is compact in $\sigma(\mathcal L^\infty_{n_2},\mathcal L^1_{n_2})$.
4. (4.1): $g(y)=\inf_{u}\{\langle u,y\rangle+\varphi(u)\}=-\varphi^*(-y)$.
5. (4.2): $\varphi^{**}(0)=\sup\mathbf D$.

The mission also poses the explicit form (1.8) of the Lagrangian and Corollary 1 (dual solutions are the negatives of subgradients of $\varphi$ at $0$; saddle-point characterization of primal solutions when $\partial\varphi(0)\ne\emptyset$).

Significance

Theorem 3 gives, for bounded constraint sets, the absence of a duality gap between a convex recourse problem with essentially bounded decisions and its Lagrangian dual over integrable multipliers, together with existence of an optimal decision. Through Corollary 1 it reduces the necessity of the Kuhn–Tucker (saddle-point) optimality conditions to the single question whether $\partial\varphi(0)$ is nonempty, and through the paper's later results it describes the directional derivatives of the optimal value with respect to perturbations of the constraints.

The result has been proved since 1976; it has not been machine-checked. A formal development produces the problem model on $\mathcal L^\infty$ and $\mathcal L^1$ spaces, the weak topologies of the pairings, and conjugate duality for extended-real-valued functions on such paired spaces, none of which is currently available as a ready-made Lean statement on this platform.

Difficulty

The obvious argument fails at two points. First, $\inf\mathbf P=\sup\mathbf D$ is $\varphi(0)=\varphi^{**}(0)$, and the biconjugate equals $\varphi$ only for a lower semicontinuous proper convex function in a topology compatible with the pairing. Lower semicontinuity of $\varphi$ in the norm topology of $U$ is not enough: the pairing is with $\mathcal L^1$, not with the norm dual of $\mathcal L^\infty$, so the relevant topology is the weak topology $\sigma(U,Y)$, and an infimum of lower semicontinuous functions is in general not lower semicontinuous. Second, the lower semicontinuity of $F$ itself, in the weak topology, is a statement about convex integral functionals on $\mathcal L^\infty$ that rests on measurability of the integrands in $s$ jointly with continuity in the decision variables. Boundedness of $C_1$, $C_2$ is what supplies the compactness that is otherwise missing.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ and the products $u_1\cdot y_1$, $u_2(s)\cdot y_2(s)$ are dot products. Constraint indices $i=1,\dots,m$ are Fin m.
• $\mathcal L^\infty_n$ and $\mathcal L^1_n$ are Mathlib's Lp (Fin n → ℝ) ⊤ σ and Lp (Fin n → ℝ) 1 σ, spaces of almost-everywhere classes; all second-stage conditions are stated almost surely. $\sigma$ is a probability measure (IsProbabilityMeasure).
• Values in $\mathbb R\cup\{\pm\infty\}$ are EReal; infima and suprema are lattice operations in EReal, so there are no junk values for empty or unbounded sets. Every sum has a real first summand, so no $\infty-\infty$ convention enters.
• The expected cost is a real Bochner integral; its integrand is summable for $x_2\in\mathcal L^\infty$ (milestone 1), so it is the true expected cost. No extended-real-valued function is ever integrated.
• A weak topology "induced by the pairing" is the coarsest topology making every functional of the pairing continuous; the product weak topology on $X\times U$ is the product of the two. These are passed explicitly. Replacing them by the norm topologies would make the lower semicontinuity statements strictly weaker and the compactness statement false; such a formalization does not count.
• An extended-real function is convex when its epigraph is convex, and proper when it never takes $-\infty$ and is somewhere finite.
• Boundedness of $C_1$, $C_2$ is assumed exactly where the paper assumes it: Theorem 3, (4.9) and Corollary 1.

A complete development needs the identification of $\mathcal L^\infty$ with the dual of $\mathcal L^1$ on a probability space (for weak-* compactness), lower semicontinuity of convex integral functionals, and conjugate duality on paired locally convex spaces. These are reusable well beyond this mission. Proofs of milestones, and of auxiliary lemmas of this kind as separate theorems, are welcome. The mission Stochastic Convex Programming: Basic Duality 2 formalizes the paper's other main result, on the first-stage problem and attainment of the recourse.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• R. T. Rockafellar, Integrals which are convex functionals, II, Pacific Journal of Mathematics 39(2) (1971) 439–469. https://doi.org/10.2140/pjm.1971.39.439
• R. J.-B. Wets, Stochastic programs with fixed recourse: the equivalent deterministic program, SIAM Review 16(3) (1974) 309–339. https://doi.org/10.1137/1016053

Motivation

A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.

The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.

Setting

Let $r,s$ be positive integers and give $\mathbb R^{r+s}$ its Euclidean norm. Write $w=(w_1,w_2)$, with $w_1\in\mathbb R^r$ and $w_2\in\mathbb R^s$. Let $K\subseteq\mathbb R^s$ be nonempty, closed, and convex, and put $D=\mathbb R^r\times K$. For $w\in D$, the normal cone is

$$N_D(w)=\{v\in\mathbb R^{r+s}:\langle v,c-w\rangle\leq0\text{ for every }c\in D\}.$$

For $w\notin D$, $N_D(w)$ is empty. Thus the inclusion $y\in Aw+N_D(w)$ itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.

Partition the real square matrix $A$ into blocks $A_{11}$, $A_{12}$, $A_{21}$, and $A_{22}$, where $A_{11}$ is $r\times r$. When $A_{11}$ is nonsingular, its Schur complement in $A$ is

$$A/A_{11}=A_{22}-A_{21}A_{11}^{-1}A_{12}.$$

A real matrix $M$ is positive definite in the theorem's sense when $v^\top Mv>0$ for every nonzero $v$. Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write $\mathbb R^s_+$ for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.

Formalization targets

General closed convex set

For $T_K(w)=Aw+N_{\mathbb R^r\times K}(w)$, the first target is the sufficient condition

$$\det A_{11}\ne0\quad\text{and}\quad v^\top(A/A_{11})v>0\;(v\ne0) \quad\Longrightarrow\quad T_K^{-1}:\mathbb R^{r+s}\to\mathbb R^{r+s}\text{ is Lipschitz}.$$

Here “is Lipschitz” includes that exactly one inverse value exists at every $y$. The assertion holds for every nonempty closed convex $K$; it is not restricted to polyhedral sets.

Nonnegative orthant

When $K=\mathbb R^s_+$, the second target is an equivalence:

$$T_{\mathbb R^s_+}^{-1}\text{ is everywhere defined, single-valued and Lipschitz} \quad\Longleftrightarrow\quad \det A_{11}\ne0\text{ and }A/A_{11}\text{ is a P-matrix}.$$

The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.

Significance

The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.

A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.

Difficulty

Nonsingularity of the full matrix $A$ alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as $w_2$ reaches different faces of $K$. A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of $\mathbb R^{r+s}$. For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.

Formalization scope

Lean represents $\mathbb R^{r+s}$ as a Euclidean space indexed by the disjoint union of $\mathrm{Fin}(r)$ and $\mathrm{Fin}(s)$. This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular $A_{11}$ in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains $r,s>0$ as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.

The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex $K$, matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.

Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.

Selected references

• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 43–62, 1980. DOI 10.1287/moor.5.1.43.

Motivation

Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve $0 = \bar f^\nu(x)$, where $\bar f^\nu$ averages a random integrand over $\nu$ observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.

When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation

$$0 \in f(z, x) + N(x),$$

where $N$ is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of $N$: the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.

Setting

Let $Z$ be a separable Banach space with norm $\|\cdot\|$, and let $|\cdot|$ be the Euclidean norm on $\mathbb R^n$ and $\mathbb R^m$. A multifunction $G : Z \rightrightarrows \mathbb R^n$ assigns a set $G(z) \subseteq \mathbb R^n$ to each $z$. Its graph is $\operatorname{gph} G$ and its inverse is $G^{-1}(x) = \{z \mid x \in G(z)\}$.

For sets $A_t$ indexed by $t \downarrow 0$, the upper limit $\limsup A_t$ consists of the points $x$ with $x = \lim x_k$, $x_k \in A_{t_k}$ for some $t_k \downarrow 0$, and the lower limit of the points reachable along every such sequence. The contingent derivative of $G$ at $(z, x) \in \operatorname{gph} G$ is the multifunction $DG(z|x)$ with

$$\operatorname{gph} DG(z|x) = \limsup_{t \downarrow 0} t^{-1}\big[\operatorname{gph} G - (z,x)\big].$$

$G$ is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when $t^{-1}[G(z + t w') - x] \to DG(z|x)(w)$ as $t \downarrow 0$ and $w' \to w$. A single-valued $g$ is B-differentiable at $z$ when $t^{-1}[g(z + tw') - g(z)] \to Dg(z)(w)$ in the same sense.

The deterministic problem is $0 \in f(z, x) + N(x)$ with $f : Z \times \mathbb R^n \to \mathbb R^m$, data $z$ and solution map $J(z)$. At a reference pair $(z^*, x^*)$ set $F = f(z^*, \cdot) + N$. The analytical assumptions M.1–M.4 are as follows. $f$ is jointly continuous and B-differentiable in each variable, with the $z$-derivative $D_z f(z^*, x^*)$ strong (uniform in $x$ near $x^*$). $N$ is closed and proto-differentiable. $F$ is subinvertible: $0 \in F(x^*)$, and a closed-graph, convex-valued selection of $F^{-1}$ near $0$ passes through $x^*$. The contingent derivative $DF^{-1}(0|x^*)$ is at most single-valued.

The statistical problem has i.i.d. random elements $s_1, s_2, \dots$ of a measurable space $S$ and an integrand $f : U \times S \to \mathbb R^m$ on a compact neighborhood $U$ of $x^*$. It satisfies the probabilistic assumptions P.1–P.4: continuity in $x$, measurability in $s$, a finite second moment at one point, and a Lipschitz bound $|f(x_1,s) - f(x_2,s)| \le a(s)|x_1 - x_2|$ with $E a(s_1)^2 < \infty$. The M-estimate $x^\nu$ is a measurable solution of

$$0 \in \bar f^\nu(x) + N(x), \qquad \bar f^\nu(x) = \frac1\nu\sum_{i=1}^\nu f(x, s_i),$$

and the true equation is $0 \in Ef(x) + N(x)$ with $F = Ef + N$.

Formalization targets

Goal: Theorem 2.7 (asymptotic distribution of M-estimates)

Under P.1–P.4 on a compact neighborhood $U$ of $x^*$, B-differentiability of $Ef$ at $x^*$, and M.2–M.4 for $F = Ef + N$, every sequence of measurable solutions $x^\nu$ of (2.5) with $x^\nu \to x^*$ almost surely satisfies

$$\sqrt\nu\,[x^\nu - x^*] \xrightarrow{\ \mathcal D\ } DF^{-1}(0|x^*)(-w^*), \qquad w^* \sim \mathcal N\big(0, \operatorname{cov} f(x^*, s_1)\big).$$

The goal fixes the limit law completely: the map is the contingent derivative of $F^{-1}$, and the Gaussian has the covariance of the integrand at $x^*$.

Milestones

• Theorem 2.4 gives bounds in probability, $P\{|x^\nu - x^*| > \delta\} \le P\{\alpha\lambda\|z^\nu - z^*\| > \delta\}$. Its proof uses the upper-Lipschitz property $U \cap F^{-1}(y) \subseteq x^* + \lambda|y|B$ (a display of the proof).
• Theorem 2.6 is the abstract limit theorem: if $\tau_\nu^{-1}[z^\nu - z^*] \to_{\mathcal D} w$, then $\tau_\nu^{-1}[x^\nu - x^*] \to_{\mathcal D} DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$. Its proof uses two displays: semi-differentiability of the localized solution map, with $DJ(z^*|x^*)(w) = DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$, and a Lipschitz bound $|x - x^*| \le \lambda\|z - z^*\|$ on $U \cap J(z)$.
• Proposition A1, Corollary A2 and Theorem A3 concern the space $C_m(U)$ under P.1–P.4. The integrand and the empirical means are random elements of $C_m(U)$, and $\sqrt\nu(\bar f^\nu - Ef)$ converges in distribution to a Gaussian element of $C_m(U)$.

The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.

Significance

Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When $N$ is the normal cone of a polyhedron, $DF^{-1}(0|x^*)$ is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.

The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.

Difficulty

The classical argument linearizes $F$ at $x^*$, inverts the Jacobian and applies the delta method. Here $F$ is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from $x^*$. The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.

The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function $\bar f^\nu$, so convergence of $\bar f^\nu$ at finitely many points is not enough. The central limit theorem must hold in the sup norm on $C_m(U)$, which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), and $Z$ is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ($t \downarrow 0$ is 𝓝[>] 0, and $(t,w') \to (0^+,w)$ is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. $s_1$ is s 0, empirical means sum over Finset.range ν, and (2.5) is required for $\nu \ge 1$. $F = Ef + N$ is empty off $U$. Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of $w^*$ is fixed through linear functionals: $\langle\ell, w^*\rangle \sim \mathcal N(0, \operatorname{Var}\langle\ell, f(x^*,s_1)\rangle)$. In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.

Explicit choices relative to the printed text:

1. The paper states that an almost surely convergent sequence of solutions "converges to the point $x^*$" (Theorems 2.6 and 2.7). This is false when the true equation has a second solution: $f(z,x) = x^2 - x - z$, $N \equiv \{0\}$, $z^* = x^* = 0$ satisfies M.1–M.4 with $J(0) = \{0, 1\}$. The formalization assumes $x^\nu \to x^*$ almost surely instead.
2. $0 \in F(x^*)$ (presupposed by $DF^{-1}(0|x^*)$) is explicit in Theorem 2.4 and the upper-Lipschitz display.
3. The threshold for "all sufficiently small $\delta$" in Theorem 2.4 is chosen with $U$ and $\lambda$, before the random elements.
4. Proposition A1 and Corollary A2 carry P.1–P.4, as stated or inherited on the Appendix page, though their measurability conclusions use only P.1.
5. In the limit theorems, the single-valued map $DF^{-1}(0|x^*)$ is a function $L$ whose values lie in the contingent derivative at every point.

The conclusion of the goal names its limit: the image of the stated Gaussian under a map $L$ whose values lie in the contingent derivative of $F^{-1}$. A statement asserting only that $\sqrt\nu(x^\nu - x^*)$ converges in distribution to some limit, or replacing $DF^{-1}(0|x^*)$ by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with $f(x,s) = x$, $N \equiv \{0\}$).

A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in $C(K)$ for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.

Selected references

• A. J. King and R. T. Rockafellar, Asymptotic theory for solutions in statistical estimation and stochastic programming, Mathematics of Operations Research 18(1) (1993). https://doi.org/10.1287/moor.18.1.148
• A. J. King and R. T. Rockafellar, Sensitivity analysis for nonsmooth generalized equations, Mathematical Programming 55 (1992) 193–212. https://doi.org/10.1007/BF01581199
• A. J. King, Generalized delta theorems for multivalued mappings and measurable selections, Mathematics of Operations Research 14(4) (1989) 720–736. https://doi.org/10.1287/moor.14.4.720
• J. Dupačová and R. J.-B. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4) (1988) 1517–1549. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Asymptotic properties of statistical estimators in stochastic programming, Annals of Statistics 17(2) (1989) 841–858. https://doi.org/10.1214/aos/1176347146
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 221–233. https://projecteuclid.org/euclid.bsmsp/1200512988
• A. Araujo and E. Giné, The Central Limit Theorem for Real and Banach Valued Random Variables, Wiley, 1980.

Motivation

A flexible manufacturing system is a set of machines through which parts of several types travel along fixed routes; each machine serves several buffers and must pay a set-up time whenever it switches from one buffer to another. Real-time scheduling decides, as the system evolves, which buffer each machine works on. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989) introduced simple distributed policies for this problem, of which the most natural is the clearing policy: a machine keeps working on a buffer until it is empty, and only then switches. They proved that every clear-a-fraction policy, a subclass of clearing policies, keeps every buffer bounded on acyclic systems whenever each machine has spare capacity, and left open whether clear-a-fraction policies stabilize all systems in which material flows around cycles.

Kumar and Seidman (IEEE Trans. Automat. Control 35(3), 1990, doi:10.1109/9.50339) answered no. Their Example 1 is a single part type that visits two machines in the order 1, 2, 2, 1. Every machine has spare capacity, yet under the clearing policy the buffer levels grow without bound, and they do so even when all set-up times are zero, so the instability comes from machines starving each other rather than from time lost to set-ups. Until then, instability had been suspected to require positive set-up times. Shortly afterwards Lu and Kumar exhibited instability of a static buffer-priority rule in a re-entrant network (IEEE Trans. Automat. Control 36, 1991); together these examples started the study of stability of multiclass queueing networks.

Setting

A manufacturing system has part types $p$ arriving at rates $d_p > 0$. Parts of type $p$ follow a route of length $n_p$: their $i$-th operation is at machine $\mu_{p,i}$, and they wait for it in buffer $b_{p,i}$, where each part needs processing time $\tau_{p,i} > 0$. Machine $m$ serves the buffers $B_m = \{b : \mu_b = m\}$, and switching from $b$ to $b'$ costs set-up time $\delta_{b,b'} \ge 0$.

Flows are continuous (fluid). The level of buffer $b$ at time $t \ge 0$ is $x_b(t) = x_b(0) + u_b(t) - y_b(t) \ge 0$, where $y_b(t)$ is its cumulative output and $u_b(t)$ its cumulative input: $d_p t$ for the first buffer of a route, and the output of the preceding buffer otherwise. Each machine works in runs: run $k$ is a set-up phase of length $\delta_{\beta_{k-1},\beta_k}$ followed by a processing phase on buffer $\beta_k$, during which the buffer is drained at rate $1/\tau_b$ while it is nonempty and passed through at its inflow rate when it is empty. The system is stable if $\sup_{0 \le t < \infty} x_b(t) < \infty$ for every buffer.

A clearing policy (Definition 1) is one in which a machine processing $b$ continues until the first time that $b$ is empty and some other buffer of the same machine is nonempty, and then commences a set-up for one of the nonempty buffers.

Example 1. One part type arrives at rate $d = 1$ and visits machine 1, machine 2, machine 2 and machine 1; its buffers are $1, 2, 3, 4$, so $B_1 = \{1, 4\}$ and $B_2 = \{2, 3\}$. Processing times are $\tau_1, \dots, \tau_4 > 0$, and $\delta_k$ is the time to set up to buffer $k$. The parameters satisfy the critical condition and the capacity condition

$$\tau_2 + \tau_4 > 1, \qquad \tau_1 + \tau_4 < 1, \qquad \tau_2 + \tau_3 < 1. \tag{3–5}$$

The initial state is $x(0) = (\xi, 0, 0, 0)$, with machine 1 set up for buffer 4 and machine 2 set up for buffer 3. Write

$$\lambda = \frac{\tau_4}{1-\tau_2} > 1, \quad \alpha = \frac{(\tau_4+1)(\delta_1+\delta_2)}{1-\tau_2} + \delta_3(\tau_4+1) + \delta_4, \quad \beta = \frac{\tau_4(\delta_1+\delta_2)}{1-\tau_2} + \tau_4\delta_3 + \delta_4.$$

Formalization targets

Goal: Example 1, both cases

Assume (3)–(5).

1. If $\delta_1, \dots, \delta_4 > 0$, there is $\xi_0$ such that for every $\xi \ge \xi_0$ ($\xi > 0$) a clearing trajectory from $(\xi, 0, 0, 0)$ exists, and every such trajectory has

$$\sup_{0 \le t < \infty} x_1(t) = +\infty.$$

2. If $\delta_1 = \dots = \delta_4 = 0$, the same holds for every $\xi > 0$.

Milestone: the Case 1 cycle map

For $\xi$ large enough, every clearing trajectory from $(\xi, 0, 0, 0)$ reaches, at $T_1 = (\lambda + \tau_2/(1-\tau_2))\xi + \alpha$,

$$x(T_1) = (\lambda\xi + \beta, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Milestone: the Case 2 magnification

With zero set-up times and any $\xi > 0$, every clearing trajectory reaches, at $t_5 = (\tau_2+\tau_4)\xi/(1-\tau_2)$,

$$x(t_5) = (\lambda\xi, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Significance

The example shows that the condition $\rho_m < 1$ on every machine, which is necessary for stability and sufficient for the existence of some stabilizing policy, does not make natural distributed policies stable once material flows around a cycle. The throughput of the line falls to $1/(\tau_2+\tau_4) < 1$ part per unit time although each machine could handle the demand. This motivates the paper's two positive results: sufficient conditions under which clear-a-fraction policies are stable (Theorem 1), and a supervisory mechanism that stabilizes any policy (Theorem 2), which are the subjects of the other missions of this series. The example is also an early instance of the phenomenon later studied as instability of multiclass fluid networks under work-conserving policies.

The paper's argument is a stage-by-stage computation of piecewise linear trajectories. No machine-checked version of it exists. A formal proof has to make precise what the paper leaves to the reader: that the clearing rule determines the trajectory, that the stage formulas are what that trajectory does, and that the cycle can be restarted. The formal model of runs, set-ups and the clearing rule built here is the same as in the other missions of the series.

Difficulty

The arithmetic of each cycle is routine once the trajectory is known. The difficulty is in the universal quantifier: the claim covers every clearing trajectory, and the clearing rule is defined implicitly, through "the first time thereafter" at which a buffer is empty and another one is nonempty. At several switching instants the buffer a machine switches to is empty and only starts to fill at that instant, and with zero set-up times a machine may begin a run at an instant where the switching condition already holds. Showing that each switch happens exactly when the paper says, and that the fluid levels then follow the printed formulas (including the reduced rate of a machine working on an empty buffer), is a uniqueness argument for a hybrid system, not a simulation. The existence half asks for the converse: an explicit trajectory, defined for all time, with infinitely many runs whose start times tend to infinity.

Formalization scope

• Time is real ($t \ge 0$); flows are fluid; there are no transport delays or assembly.
• The system is a general structure (part types Fin P, machines Fin M, buffers ⟨p, i⟩ with i : Fin (n p), paper index $i$ = Lean index $i+1$), instantiated as Example 1 with $d = 1$, route $(1,2,2,1)$, and $\delta_{b,b'} = \delta_{b'}$ for $b \ne b'$; staying on a buffer costs nothing.
• A trajectory is a schedule of runs per machine (possibly finitely many, the last lasting forever), with only finitely many run starts in any bounded interval. Processing obeys a rate cap ($y_b$ grows at most at rate $1/\tau_b$, and only while machine $\mu_b$ is in a processing phase of $b$) and runs at full rate while the buffer is nonempty.
• In Definition 1, a target buffer counts as "nonempty" when it is demanding: positive level, or inflow starting at that instant. The no-early-exit condition is imposed on the open processing interval. Under the literal reading (positive level) or a closed interval, the paper's own trajectories are not clearing, and the goal would hold vacuously; the existence clause in the goal rules out that trivialization.
• "Set up for buffer $b$ at time $T$" means the run in force on $(s_k, s_{k+1}]$.
• Unboundedness is stated for buffer 1: for every $C$ there is $t \ge 0$ with $x_1(t) > C$; "$\xi$ large enough" is $\exists \xi_0, \forall \xi \ge \xi_0$.

Useful contributions include lemmas about fluid trajectories that do not depend on the example (continuity of levels, the pass-through rate on an empty buffer, restarting a trajectory at a run boundary), which also serve the other missions of the series.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34, 139–148, 1989 (reference [18] of the paper).
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Trans. Automat. Control 36, 1991.