Operations Research

Motivation

A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.

Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.

Setting

A manufacturer produces at unit cost $c$. A retailer sells at the fixed retail price $p$. Leftover units are salvaged at $c_3$ per unit. Each unit of unmet demand costs the retailer a goodwill penalty $g \ge 0$ and the manufacturer an additional penalty $g_1 \ge 0$; write $g_2 = g + g_1$. The data satisfy $c_3 < c < p$.

The manufacturer chooses a policy $(c_1, c_2, R)$: the retailer pays $c_1$ per unit ordered and may return up to the fraction $R \in [0,1]$ of its order $Q$ for a credit $c_2$ per unit. The paper assumes

$$c_3 < c < c_1 < p, \qquad c_3 < c_2 \le c_1 < p. \qquad (1),\ (2)$$

Demand $X \ge 0$ is random with distribution function $F$. Three expected profits are defined as functions of the order $Q$: $EP_T(Q)$, equation (3), the profit of a company store in which the manufacturer sells directly; $EP_R(Q)$, equation (6), the independent retailer's profit under the policy; and $EP_M(Q)$, equation (8), the manufacturer's profit when the retailer orders $Q$. An optimal order for a profit function is a $Q \ge 0$ maximizing it over $[0,\infty)$. The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.

The Lean development uses the same letters: Costs carries $c, c_3, p, g, g_1$; Costs.Admissible K c1 c2 R is (1)–(2) with $0 \le R \le 1$; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; $F$ is cdf D for a demand law D.

Formalization targets

Goal: Theorem 3

A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of $c_1$ and $c_2$. Precisely, for every price $c_1$ with $c < c_1 < p$ there is a credit $c_2$ with

$$c_3 < c_2 < c_1, \qquad c_1 = (p+g) - \frac{(p+g_2-c)(p+g-c_2)}{p+g_2-c_3} \quad (11),$$

such that the policy $(c_1, c_2, R = 1)$ coordinates the channel for every continuous demand distribution on $[0,\infty)$ with finite mean. The credit is chosen before, and independently of, the demand law.

Milestones

1. (4)–(5): the company store has an optimal order, and $Q$ is optimal iff $F(Q) = (p+g_2-c)/(p+g_2-c_3)$.
2. (7): under an admissible policy, $Q$ is optimal for the retailer iff $0 = -c_1 + p + g - F(Q)[p+g-c_2] - F((1-R)Q)[(1-R)(c_2-c_3)]$.
3. (9)–(10): an admissible policy coordinates the channel iff (10) holds at every system-optimal order.
4. (11): with $R = 1$ and $c_2 < c_1$, coordination holds iff (11) holds, whatever the demand law.
5. Appendix, proof of Theorem 3: for $c < c_1 < p$, (11) has a solution $c_2$ with $c_3 < c_2 < c_1$.

Significance

The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs $(c_1, c_2)$ then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.

Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for $c_3 < c_2$ establishes only $c_2 > c_3 - g_1$, which suffices only when $g_1 = 0$, although the claim holds for all $g_1 \ge 0$. And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost $c_r > v \ge 0$, which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.

Difficulty

The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on $[0,\infty)$, including the boundary $Q = 0$. Coordination is a statement about sets of maximizers, not about one first-order condition: when $F$ is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where $F$ increases. The naive reading "both first-order conditions hold at $Q^*_T$" proves one inclusion only.

Formalization scope

Demand is a probability measure D on $\mathbb R$ with D (Iio 0) = 0 and finite mean (IsDemand), and $F$ is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy $g, g_1 \ge 0$, implicit in the paper. $R$ is a fraction in $[0,1]$. Optimal orders are maximizers over $Q \ge 0$ that are themselves $\ge 0$. Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator $p + g_2 - c_3$ is positive under these assumptions, so no division is degenerate.

The goal is not the algebraic statement "there is $c_2 \in (c_3, c_1)$ solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of $c_2$.

A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity $EP_R = k \cdot EP_T + \text{const}$ under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.

Selected references

• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003, 227–339. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

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

Why a threshold rule matters

In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984

The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215

Observations and threshold rules

Let $n\ge1$, and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables. Write $X_n^*=\max(X_1,\ldots,X_n)$. For a threshold $c\ge0$, the weak threshold rule $t(c)$ takes the first $X_i$ with $i<n$ and $X_i\ge c$; the strict threshold rule $s(c)$ uses $X_i>c$. If no earlier observation qualifies, either rule takes $X_n$, even when $X_n$ is below the threshold. Hence every rule returns exactly one observed reward.

The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,

$$E^+X_{t(c)}=E[X_{t(c)}\mathbf1_{\{X_{t(c)}\ge c\}}], \qquad E^+X_{s(c)}=E[X_{s(c)}\mathbf1_{\{X_{s(c)}>c\}}].$$

The last forced observation may contribute to $E X_{t(c)}$ or $E X_{s(c)}$ while contributing zero to $E^+X_{t(c)}$ or $E^+X_{s(c)}$. This difference is essential to the theorem's middle bounds. A median $m$ of $X_n^*$ means both $P(X_n^*<m)\le\tfrac12$ and $P(X_n^*>m)\le\tfrac12$. Define the excess sum $\beta=\sum_{i=1}^n E(X_i-m)^+$, where $x^+=\max(x,0)$. The two median inequalities allow an atom at $m$, and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)

Formalization targets

Theorem 1: a median threshold

For every median $m$, the goal retains both of the paper's conditional conclusions:

$$\begin{aligned} \beta\ge m&\Longrightarrow E X_n^*\le2E^+X_{s(m)}\le2E X_{s(m)},\\ \beta\le m&\Longrightarrow E X_n^*\le2E^+X_{t(m)}\le2E X_{t(m)}. \end{aligned}$$

At equality $\beta=m$, both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if $a^*=E(X_n^*-a^*)^+$ and $b^*=\sum_iE(X_i-b^*)^+$, then every $a^*\le c\le b^*$ satisfies the same chain with $t(c)$. Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215

What the result gives

Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison $E X_n^*\le2E X_\tau$. For a reward distribution with atoms, the theorem says exactly when to use $>$ and when to use $\ge$. Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214

The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.

Where the formal proof is delicate

The event that a rule reaches index $i$ depends on the observations before $i$. Establishing its independence from the excess of $X_i$ requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at $n$ also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)

Formalization scope

Lean indexes the $n$ observations by Fin $n$ with $n>0$. Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop $n$. The rules are the least qualifying index or that final index. The paper's $s(m)>i-1$ and $t(m)>i-1$ therefore become $i\le s(m)$ and $i\le t(m)$. Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.

Expectations use the extended nonnegative integral of the positive part, taking values in $[0,\infty]$. This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state $m\ge0$ directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds $a^*$ and $b^*$ are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.

The goal cannot be satisfied by replacing $E^+X_\tau$ with $E X_\tau$, by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.

Selected references

• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), 1213–1216, 1984. DOI: 10.1214/aop/1176993150

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

Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point $x$ has to satisfy $0 \in f(x) + \partial\psi_C(x)$. In applications the data $f$ depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation $f(p, x) = 0$ the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.

S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.

This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.

Setting

Let $X$ be a real normed linear space and $X'$ its topological dual, the continuous linear functionals on $X$. Let $C \subseteq X$ be closed and convex. The normal-cone operator of $C$ is

$$\partial\psi_C(x) = \begin{cases} \{y \in X' : y(c - x) \le 0 \text{ for all } c \in C\}, & x \in C, \\ \emptyset, & x \notin C. \end{cases}$$

A generalized equation is the inclusion $0 \in f(x) + \partial\psi_C(x)$, for a function $f$ from an open set $\Omega \subseteq X$ to $X'$. For $C = X$ it is the equation $f(x) = 0$. For $C$ the nonnegative orthant of $\mathbb R^n$ it is the nonlinear complementarity problem. For a general closed convex $C$ it is the variational inequality over $C$.

Let $x_0 \in \Omega$ solve the generalized equation, and let $f$ be Fréchet differentiable at $x_0$. Linearising $f$ gives the multifunction

$$T x = f(x_0) + f'(x_0)(x - x_0) + \partial\psi_C(x).$$

The generalized equation is strongly regular at $x_0$ with associated Lipschitz constant $\lambda$ if there are neighbourhoods $U$ of $0$ in $X'$ and $V$ of $x_0$ with the following property: for every $y \in U$ the inclusion $y \in Tx$ has exactly one solution $s(y)$ in $V$, and $\|s(y_1) - s(y_2)\| \le \lambda \|y_1 - y_2\|$ on $U$. The condition depends only on $f(x_0)$, $f'(x_0)$ and $C$.

In the parametric problem the function is $f(p, x)$, with $p$ in a topological space $P$ and base point $p_0$. Its partial derivative in $x$ is $f'(p, x)$.

Formalization targets

Goal: Theorem 2.1 (p. 45)

Assume that $f'$ exists on $P \times \Omega$, that $f$ and $f'$ are continuous at $(p_0, x_0)$, and that $x_0$ solves $0 \in f(p_0, x) + \partial\psi_C(x)$, strongly regularly with constant $\lambda$. Then for every $\varepsilon > 0$ there are neighbourhoods $N_\varepsilon$ of $p_0$ and $W_\varepsilon$ of $x_0$, and a function $x : N_\varepsilon \to W_\varepsilon$, with two properties. First, $x(p)$ is the unique solution in $W_\varepsilon$ of $0 \in f(p, x) + \partial\psi_C(x)$. Second,

$$\|x(p) - x(q)\| \le (\lambda + \varepsilon)\,\|f(p, x(q)) - f(q, x(q))\| \qquad (p, q \in N_\varepsilon).$$

Milestones: the steps of the proof (p. 46)

Write $L$ for the linearisation at $(p_0, x_0)$, $r(p, x) = f(p_0, x_0) + f'(p_0, x_0)(x - x_0) - f(p, x)$ for the residual, and $\Phi_p(x) = V \cap L^{-1}[r(p, x)]$. The milestones are four claims of the proof:

1. On the closed ball $V_\varepsilon$, the fixed points of $\Phi_p$ are exactly the solutions of the perturbed inclusion.
2. $\|\Phi_p(x_1) - \Phi_p(x_2)\| \le \lambda\delta \|x_1 - x_2\|$ on $V_\varepsilon$.
3. $\Phi_p$ maps $V_\varepsilon$ into itself.
4. The contraction principle on $V_\varepsilon$, with the bound $\|x(p) - x\| \le (1 - \lambda\delta)^{-1} \|\Phi_p(x) - x\|$ (2.5).

Companion results

• Corollary 2.2 (pp. 46–47). If $P$ lies in a normed space and $\|f(p, x) - f(q, x)\| \le \nu \|p - q\|$, then $x(\cdot)$ is Lipschitzian with modulus $\nu(\lambda + \varepsilon)$.
• Theorem 2.3 (p. 47). Let $\Phi_p(x_0)$ be the unique local solution of the linear generalized equation $0 \in f(p, x_0) + f'(p_0, x_0)(x - x_0) + \partial\psi_C(x)$. Then $\|x(p) - \Phi_p(x_0)\| \le \alpha_\varepsilon(p)\|p - p_0\|$, with $\alpha_\varepsilon(p) \to 0$.
• Theorem 2.4 (p. 48). This is a perturbation lemma for linear generalized equations $0 \in Ax + a + \partial\psi_C(x)$. Near $(A_0, a_0)$ the localised inverse stays single-valued, and it is Lipschitzian with modulus $\lambda(1 - \lambda\|A - A_0\|)^{-1}$.
• The case $C = X$ (remark on p. 45). There strong regularity is equivalent to $f'(x_0)$ having a continuous linear inverse.
• Strong regularity is the weakest possible condition (remark on p. 47). For the canonical perturbation $f(p,x) = f(x_0) + f'(x_0)(x - x_0) - p$, $p \in X'$, locally unique solvability with a Lipschitzian solution map $x(\cdot)$ near $p_0 = 0$ is exactly strong regularity at $x_0$.

Significance

Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at $x_0$, the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.

The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for $C^1$ maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of $X$.

Difficulty

The obvious approach is to apply the classical implicit-function theorem. It fails because $x \mapsto f(x) + \partial\psi_C(x)$ is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood $V$ and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: $\delta$ from $\varepsilon$, then $U$ and $V$, then the ball radius $\rho$, then the parameter neighbourhood. The estimate (2.4) has to come out with the constant $\lambda + \varepsilon$ and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of $X$, for example through the completeness of $X'$.

Formalization scope

• $X'$ is StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off $C$, and an inclusion $0 \in f(x) + \partial\psi_C(x)$ is written $-f(x) \in \partial\psi_C(x)$.
• Strong regularity is a predicate on $(C, f(x_0), f'(x_0), x_0, \lambda)$ with real $\lambda$. It requires existence, uniqueness in $V$ and the Lipschitz bound.
• $f$ is a total function $P \times X \to X'$ whose values off $P \times \Omega$ carry no hypothesis. The conclusion therefore asserts $W_\varepsilon \subseteq \Omega$.
• Differentiability is HasFDerivAt at every point of $\Omega$, for every $p$. Continuity of $f'$ at $(p_0, x_0)$ is joint and in operator norm.
• Uniqueness is uniqueness within $W_\varepsilon$, never global. Global uniqueness is false in general. Dropping uniqueness, or quantifying $\varepsilon$ after the neighbourhoods, would trivialize the goal, and the statements are written to exclude both.
• Theorem 2.1, Corollary 2.2 and Theorem 2.3 do not assume completeness, as printed. Theorem 2.4 assumes a Banach space, as printed.
• The contraction-principle milestone assumes completeness, under which the principle as invoked holds.
• Corollary 2.2 asks for its Lipschitz hypothesis on $N_\varepsilon \times V_\varepsilon$, sets that Theorem 2.1 produces. It is therefore stated on fixed neighbourhoods given in advance.
• Theorem 2.4 also asserts $\lambda\|A - A_0\| < 1$, which its proof secures.

A complete development needs the following:

• the mean-value inequality for Fréchet-differentiable maps on convex sets;
• the contraction principle on a closed ball;
• a fixed-point argument that obtains the fixed point through the complete space $X'$.

The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1):43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3

Motivation

Routing several commodities through one capacitated network at the same time is a basic problem of network optimization, with applications to communication networks, VLSI layout and divide-and-conquer graph algorithms. Its optimum is the value of a linear program, but the natural certificates of an upper bound are combinatorial: every cut of the network limits how much can be routed across it. For a single commodity the max-flow min-cut theorem says that the best cut certificate is exact. With many commodities it is not, and the size of the gap between the best flow and the best cut is the question of this mission.

• 1988–1999, Leighton and Rao proved that for uniform demands (one unit between every pair of vertices) the gap is $O(\log n)$ on an $n$-vertex network, and that the bound is attained on expanders (Leighton–Rao, JACM 1999; FOCS 1988).
• 1990–1995, Klein, Rao, Agrawal and Ravi extended a polylogarithmic bound to arbitrary demands, $O(\log C \log D)$ in the total capacity $C$ and total demand $D$ (Combinatorica 15, 1995); Plotkin and Tardos improved it to $O(\log^2 k)$ in the number of commodities $k$ (Combinatorica 15, 1995).
• 1995, Linial, London and Rabinovich (Combinatorica 15, 1995), and independently Aumann and Rabani (SIAM J. Comput. 1998), showed that the gap is bounded by the least distortion of embedding a metric derived from the network into $\ell_1$, and obtained the bound $O(\log k)$ from Bourgain's embedding theorem. This mission formalizes that theorem, Theorem 4.1 of the Linial–London–Rabinovich paper.

Setting

A multicommodity flow network has a finite vertex set $V$, capacities $C_{i,j} = C_{j,i} \ge 0$ (zero for non-edges and on the diagonal), and $k$ commodities: commodity $\mu$ has a source $s_\mu$, a sink $t_\mu$ and a demand $D_\mu \ge 0$.

A feasible concurrent flow of value $\lambda$ sends, for every $\mu$, $\lambda D_\mu$ units of commodity $\mu$ from $s_\mu$ to $t_\mu$: arc flows $f_\mu(i,j) \ge 0$ satisfy conservation of matter, with net outflow $\lambda D_\mu$ at $s_\mu$, $-\lambda D_\mu$ at $t_\mu$ and $0$ elsewhere, and the total flow of all commodities through each undirected edge $\{i,j\}$, in both directions, is at most $C_{i,j}$. The maxflow of the network is the largest such $\lambda$.

For $S \subseteq V$, $\mathrm{Cap}(S) = \sum_{i \in S}\sum_{j \notin S} C_{i,j}$ is the capacity of the edges leaving $S$, and $\mathrm{Dem}(S)$ is the total demand of the pairs that $S$ separates, i.e. with $|S \cap \{s_\mu,t_\mu\}| = 1$. Every flow of value $\lambda$ has to push $\lambda\,\mathrm{Dem}(S)$ units across the cut, so

$$\mathrm{maxflow} \le \frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \quad\text{for every } S \text{ with } \mathrm{Dem}(S) > 0.$$

A semi-metric on $V$ is a function $d \ge 0$ with $d(i,i) = 0$, symmetry and the triangle inequality; distinct points may be at distance $0$, as in the paper.

Formalization targets

Goal: Theorem 4.1

There is an absolute constant $C_0 > 0$ such that every network in which some commodity has $D_\mu > 0$ and $s_\mu \ne t_\mu$ has a set $S \subseteq V$ with $\mathrm{Dem}(S) > 0$ and

$$\frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \le C_0 \log(\max(k,2)) \cdot \mathrm{maxflow}.$$

The constant is not fixed; only the shape $O(\log k)$ in the number of commodities is asserted.

Milestones, in the order the proof uses them

1. Weak duality (§4, p. 226): $\lambda\,\mathrm{Dem}(S) \le \mathrm{Cap}(S)$ for every feasible $\lambda \ge 0$ and every $S$.
2. LP duality display (p. 227): $\mathrm{maxflow} = \min_d \dfrac{\sum_{\{i,j\}} C_{i,j} d_{i,j}}{\sum_\mu D_\mu d_{s_\mu,t_\mu}}$ over semi-metrics $d$.
3. Corollary 3.4, Claim 2 (p. 223): every finite semi-metric space with $k$ marked pairs has a non-expanding map into some $\ell_1^m$ that shrinks each marked pair by at most $C_1 \log(\max(k,2))$.
4. Coordinate minimum (p. 227): for points of $\ell_1^m$, the cost-to-demand ratio is at least its value on the best single coordinate.
5. 0/1 rounding (pp. 227–228): for symmetric real weights $a$ and nonnegative symmetric weights $b$, the minimum of $\sum a_{ij}|z_i - z_j| / \sum b_{ij}|z_i - z_j|$ over real vectors $z$ is attained at a 0/1 vector.

Significance

The theorem bounds the flow–cut gap: the integrality gap of the linear relaxation of the sparsest cut problem is $O(\log k)$, so solving one linear program and rounding gives an $O(\log k)$-approximation to the sparsest cut. Sparsest-cut approximations are the engine of approximation algorithms for minimum bisection, graph partitioning, crossing number and VLSI layout. The dependence on $k$ rather than on the number of vertices matters when few pairs carry demand. The bound is tight up to the constant: on constant-degree expanders with all-pairs unit demands the gap is $\Omega(\log n)$ (Leighton–Rao).

The result has been proved since 1995 and is textbook material (Williamson–Shmoys, Ch. 15). It has no machine-checked proof. A formalization adds a verified bridge between concurrent flows, LP duality on networks and $\ell_1$ embeddings of finite metrics; each piece is reusable on its own. Corollary 3.4, Claim 2 in particular is a terminal version of Bourgain's theorem, of which no formal proof exists either.

Difficulty

Two steps carry the weight. The first is the duality between concurrent flows and metrics: Mathlib has no linear programming duality theorem in a form that applies directly, and the dual of the arc-flow program has to be identified with a minimum over semi-metrics, which needs a shortest-path argument on top of LP duality. The second is the embedding: Claim 2 of Corollary 3.4 must achieve distortion $O(\log k)$ on the $k$ marked pairs, independent of $|X|$. A direct application of Bourgain's theorem to the whole space gives $O(\log |X|)$, which is not enough when $k$ is much smaller than the number of vertices, and the paper's proof is a one-line reference to an earlier argument.

Formalization scope

• Vertex sets are finite types V with [Fintype V] [DecidableEq V]; capacities are a function C : V → V → ℝ with symmetry, nonnegativity and zero diagonal as fields of a Network structure. Commodities are indexed by Fin k; coincident or repeated pairs are allowed.
• Flows are arc flows; the capacity bounds the total over all commodities and both directions. maxflow is the supremum of feasible values; Lean's sSup returns $0$ on an unbounded set, which only happens without a commodity of positive demand and distinct endpoints, and the goal assumes one.
• Sums over edges are over unordered pairs: the page's $\sum_{i \ne j}$ in the LP-duality and coordinate displays counts each edge twice, while $\mathrm{Cap}$ counts it once; the statements use $\tfrac12\sum_i\sum_j$ in both places, which removes the factor-2 slip without changing the proof.
• Explicit constants. The paper's $O(\log k)$ in Theorem 4.1 is $C_0 \log(\max(k,2))$ with $C_0$ quantified before the network; the $\Omega(1/\log k)$ of Corollary 3.4 is $1/(C_1\log(\max(k,2)))$ with $C_1$ quantified before the metric space. The $\max(k,2)$ keeps $k = 1$ in scope, where $\log k = 0$.
• Out of scope. The deterministic polynomial-time algorithms of Theorem 4.1 and Corollary 3.4, and the target dimension $\ell_1^{O(n^2)}$ of the latter, are not stated; the statements assert the existence of the cut and of the embedding.
• The 0/1 rounding step adds $b \ge 0$, which the page omits but its argument needs.
• A trivializing formalization is ruled out: the constant $C_0$ is quantified before the network, so it cannot depend on the instance, and maxflow is defined from flows, not as the metric minimum.
• Contributions welcome: an LP duality theorem for finite-dimensional linear programs in the form needed here, a formal Bourgain-type embedding with terminal distortion, and the max-flow min-cut theorem for undirected capacities.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995) 215–245. https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27 (1998) 291–301. https://doi.org/10.1137/S0097539794285983
• T. Leighton, S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46 (1999) 787–832. https://doi.org/10.1145/331524.331526
• J. Bourgain, On Lipschitz embedding of finite metric spaces in Hilbert space, Israel J. Math. 52 (1985) 46–52. https://doi.org/10.1007/BF02776078
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, Chapter 15. https://doi.org/10.1017/CBO9780511921735