Optimization

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$, where $\delta$ is the largest absolute value of a subdeterminant of $A$. For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$, which grows with the number of variables $n$.

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$, and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$, a right-hand side $b\in\mathbb Z^m$, an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$. A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$. The integer program (10) is

$$\max\{c^Tx : Ax=b,\ 0\le x\le u,\ x\in\mathbb Z^n\},$$

and its LP relaxation is the same problem over $x\in\mathbb R^n$. Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$. An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$-norm $\|z-x\|_1=\sum_i|z_i-x_i|$.

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$, $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$: an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$-dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$. It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$, and the paper uses Sevast'anov's constant $c(m)=m$.

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

$$\|z^*-x^*\|_1\ \le\ m\cdot(2m\Delta+1)^m .$$

The constant is the paper's. The goal holds for all $m$, $n$, $b$, $c$ and $u$; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 5:8): for an LP optimum $x^*$, an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$, the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$.
2. Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
3. Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$-dimensional real normed space.
4. Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$, $\|w_j\|_\infty\le\Delta$.
5. Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$-norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$.
6. Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$.

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$-ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$. The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$, because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$-norm at most $m\Delta$. The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence ("$x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$, and it has to be derived from the extreme-point property of $P$.

Formalization scope

• All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
• "Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
• The $\ell_1$-distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
• The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
• Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$, with no hidden existential constant.
• The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$. The goal needs only the $\ell_\infty$ case on $\mathbb R^m$.
• Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$.

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

• F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
• E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
• S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
• V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

Motivation

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.

Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.

Setting

A network $N$ has a finite set $V$ of nodes, a source $s$ and a sink $t \neq s$, and a set of arcs, ordered pairs $(u,v)$ with $u \neq v$, at most one from each node to another. One arc is the return arc $(t,s)$; the other arcs form the set $A$, and each $(u,v) \in A$ has a capacity $c(u,v) > 0$. A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and flow conservation at every node, $s$ and $t$ included. Its value is $f(t,s)$, the flow returned along the return arc; a maximum flow has the largest value among all flows, and $f^*(t,s)$ denotes that value.

The residual network $N^f$ has an arc $(u,v)$ whenever $(u,v) \in A$ and $c(u,v) - f(u,v) > 0$, or $(v,u) \in A$ and $f(v,u) > 0$. An augmenting path is a directed path $s = u_1, \dots, u_p = t$ of distinct nodes in $N^f$. Each of its arcs $(u,v)$ has a residual amount $e(u,v)$, equal to $c(u,v) - f(u,v)$, $f(v,u)$, or $c(u,v) - f(u,v) + f(v,u)$ according to which of $(u,v)$, $(v,u)$ lie in $A$, and the path's augmentation is $\varepsilon = \min e(u_i, u_{i+1})$. Augmenting increases $f(t,s)$ by $\varepsilon$ and changes the flow on the arcs of the path accordingly, with the paper's own rule when both $(u,v)$ and $(v,u)$ are arcs. The labeling method produces flows $f^0, f^1, \dots$ by augmenting along a path relative to $f^k$ as long as one exists.

The rule studied here chooses, at every step, an augmenting path whose $\varepsilon$ is at least that of every other augmenting path relative to the current flow. The bound involves an integer $M > 1$ such that every partition of the nodes into $X \ni s$ and $\bar X \ni t$ has at most $M$ arcs of $N$ with one end on each side.

Formalization targets

Goal: Theorem 2 (p. 253)

For a network with integer capacities, $M$ as above, and a run $f^0, \dots, f^K$ of the labeling method with maximum augmentations started from an integer-valued flow,

$$K \;\le\; 1 + \log_{M/(M-1)} f^*(t,s),$$

and if no augmenting path relative to $f^K$ exists, then $f^K$ is a maximum flow.

Milestones

The milestone list follows the paper's argument:

1. augmentation produces a flow of value $f(t,s) + \varepsilon$ (§1.1, p. 249);
2. a flow is maximum if and only if it has no augmenting path (§1.1, pp. 249–250);
3. with integer capacities, $\varepsilon$ is a positive integer and the flows of the method stay integer-valued (§1.1, p. 250);
4. the cut inequality $c(X,\bar X) \ge f(X,\bar X) - f(\bar X,X) = f(t,s)$ (p. 254);
5. $f^*(t,s) - f^k(t,s) \le \varepsilon^k M$, where $\varepsilon^k = f^{k+1}(t,s) - f^k(t,s)$ (p. 254);
6. $f^*(t,s) - f^{k+1}(t,s) \le [f^*(t,s) - f^k(t,s)](1 - M^{-1})$ (p. 254);
7. $f^*(t,s) - f^k(t,s) \le f^*(t,s)(1 - M^{-1})^k$ (p. 254).

Significance

Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since $M \le n^2/2$ and $f^*(t,s)$ is at most $n^2$ times the average capacity, the bound is $O(n^2 \log(n^2 \bar c))$ in terms of the number of nodes $n$ and the average capacity $\bar c$ (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).

The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.

Difficulty

The obvious argument, that each augmentation raises the value by at least 1, gives only the bound $f^*(t,s)$, and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap $f^*(t,s) - f^k(t,s)$. The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.

Formalization scope

• Nodes form a finite type V with decidable equality. A : Finset (V × V) contains no loops and not $(t,s)$. Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of $N$, the return arc included).
• Flows are functions V → V → ℝ constrained only on the arcs of $N$. A maximum flow is the predicate IsMaxFlow, comparing $f(t,s)$ with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets $f^*(t,s) = g(t,s)$; every network has one.
• Augmenting paths are duplicate-free node lists whose consecutive pairs are arcs of $N^f$. The page prints Case (b) of the definition of $\varepsilon_i$ with the same hypothesis as Case (c); the corrected Case (b), $(u,v) \notin A$ and $(v,u) \in A$, is used, as the definition of $N^f$ (p. 251) and the list for $e(u,v)$ (p. 253) confirm.
• A run is IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum $\varepsilon$ among all augmenting paths.
• The crossing bound CrossArcsBounded N M counts the arcs of $N$, return arc included, with one end on each side of every $s$–$t$ partition. This is the literal reading of p. 253.
• Explicit constants. The bound is exactly $1 + \log_{M/(M-1)} f^*(t,s)$, written (K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with $M > 1$ a natural number. When $f^*(t,s) = 0$, Real.logb gives $0$ and the bound reads $K \le 1$. The contraction factor is 1 - (M : ℝ)⁻¹.
• A statement that bounds only runs of an unsatisfiable step predicate, drops the integrality of $f^0$ or of the capacities (the bound is false without them), or compares $\varepsilon$ only among paths of some restricted class does not formalize Theorem 2. A sorry-free check exhibits a four-node network with integer capacities and a valid maximum-augmentation step.
• Reusable beyond this mission: the return-arc network model, the augmentation step with the paper's opposite-arc rule, the integrality lemma, and the cut inequality. Proofs of any milestone are welcome, as are proofs of the converse in milestone 2 that could later be shared with mission 1.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• L. R. Ford, D. R. Fulkerson, Flows in Networks, RAND report R-375-PR, 1962; Princeton University Press, 1962. https://www.rand.org/pubs/reports/R375.html

Motivation

Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.

Bertsekas (1977) recast these models in one abstract framework: a monotone mapping $H$ that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, $J^*$ is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to $J^*$. The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).

Setting

States, controls, policies. $S$ (nonempty) and $C$ are sets. Each $x\in S$ has a nonempty constraint set $U(x)\subseteq C$. $M$ is the set of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$, and a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors. The policy is stationary if $\mu_k=\mu$ for all $k$.

Functions and the mapping $H$. $F$ is the set of functions $J:S\to[-\infty,\infty]$, ordered pointwise, and $e$ is the constant function $1$. A mapping $H:S\times C\times F\to[-\infty,\infty]$ is given, and it is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for every $x$ and $u\in U(x)$. It defines

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

$T^k$ is the $k$-fold composition, with $T^0$ the identity, and $(T_{\mu_0}\cdots T_{\mu_{N-1}})$ applies $T_{\mu_{N-1}}$ first.

Costs. A terminal function $\bar J\in F$ with $\bar J(x)>-\infty$ is given. The cost of a policy, the optimal cost, the $N$-stage optimal cost and the limit of the DP algorithm are

$$J_\pi=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J^*=\inf_{\pi}J_\pi,\quad J_N=\inf_{\pi}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J_\infty=\lim_{N\to\infty}T^N(\bar J),$$

all pointwise. $J_\mu$ denotes the cost of the stationary policy $\{\mu,\mu,\dots\}$.

Assumptions. D: $H(x,u,\bar J)\le\bar J(x)$ for all $x$, $u\in U(x)$. Under D every sequence above is nonincreasing, so the limits exist in $[-\infty,\infty]$. D.1: for every sequence with $J_{k+1}\le J_k\le\bar J$, $\lim_k H(x,u,J_k)=H(x,u,\lim_k J_k)$. D.2: there is $\alpha>0$ such that $H(x,u,J)-\alpha r\le H(x,u,J-re)\le H(x,u,J)$ for all $r>0$ and $J\le\bar J$.

Formalization targets

Goal: convergence of the DP algorithm (Proposition 9)

If D holds, and either D.1 holds or $J_N=T^N(\bar J)$ for every $N\ge1$, then

$$J_\infty=J^*.$$

Milestones

1. Lemma 1. Under D, $J^*(x)=\lim_{N\to\infty}J_N(x)$ for every $x$.
2. Proposition 3. Under D, and either D.1 or (D.2 and $T^N(\bar J)>-\infty$ everywhere), $J_N=T^N(\bar J)$ for a given $N\ge1$.
3. Proposition 6. Under D and D.1, $J^*=T(J^*)$, and every $J'\le\bar J$ with $J'\le T(J')$ satisfies $J'\le J^*$.
4. Corollary 6.2. Under D and D.1, $J_\mu=T_\mu(J_\mu)$ for every stationary policy, and every $J'\le\bar J$ with $J'\le T_\mu(J')$ satisfies $J'\le J_\mu$.
5. Proposition 8. Under D and D.1, a stationary policy $\{\mu^*,\mu^*,\dots\}$ is optimal if and only if $T_{\mu^*}(J_{\mu^*})=T(J_{\mu^*})$.

The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is $\lim_N T^N(\bar J)=J^*$?

Significance

The result. Proposition 9 justifies value iteration from $\bar J$ for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise $J^*$ as the largest solution of Bellman's equation below $\bar J$ and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show $J_N\ne T^N(\bar J)$ when D.1 is dropped together with D.2 or with the finiteness condition $T^N(\bar J)>-\infty$. Under the mirror assumption I, $J_\infty=J^*$ can fail, so the asymmetry between the two sign conditions is part of the content.

Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.

Difficulty

The obvious argument for Proposition 9, "$J_N=T^N(\bar J)$ and $J_N\to J^*$", hides two separate interchanges of limits and infima. Lemma 1 interchanges $\inf_\pi$ with $\lim_N$, which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the $N$-stage infimum over policies must be matched by the iterated infimum $T^N$, which requires building near-optimal selectors stage by stage and passing a limit through $H$ $N$ times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach $-\infty$, which is why that branch needs $T^N(\bar J)>-\infty$. All arithmetic is in $[-\infty,\infty]$, where expressions such as $\infty-\infty$ are not defined, and $J^*$, $J_N$, $T^N(\bar J)$ may equal $-\infty$ even though $\bar J$ does not.

Formalization scope

The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; $F$ is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. $T$ is an infimum over U x only, and $J^*$, $J_N$ are infima over admissible policies. $J_\pi$ and $J_\infty$ are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.

$J_N$ is defined for every $N$, and Propositions 3 and 9 quantify over $N\ge1$ as the paper does. In Proposition 3 the condition $T^N(\bar J)>-\infty$ belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and $\bar J>-\infty$ are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, $J^*$ and $J_N$ would be $+\infty$, and several statements would hold trivially; the model rules this out.

Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and $T^{N+1}(\bar J)\le T^N(\bar J)$ under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.

Selected references

• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699147
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. https://www.mit.edu/~dimitrib/abstractdp_MIT.html

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than $(k+1)^{-(1+\epsilon)}$ for every $\epsilon > 0$.

When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like $1/k$; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an $O(1/(k+1)^2)$ rate for the squared distance. This mission formalizes that result.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$, $v \in Ay$, and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is $\mu$-strongly monotone if $\langle x - y, u - v\rangle \ge \mu\|x-y\|^2$ for all such pairs. A single-valued $C : H \to H$ is $\beta$-cocoercive if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$, and $L_C$-Lipschitz if $\|Cx - Cy\| \le L_C\|x - y\|$.

The problem is to find $x^* \in \operatorname{zer}(A + B + C)$, that is, $0 \in Ax^* + Bx^* + Cx^*$, where $A$, $B$ are maximal monotone and $C$ is monotone and single-valued. For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$.

Algorithm 3 fixes stepsizes $(\gamma_k)_{k\ge 0} \subseteq (0,\infty)$ and an initial point $x_A^0 \in H$, sets $x_B^0 = J_{\gamma_0 B}(x_A^0)$, $u_B^0 = \gamma_0^{-1}(x_A^0 - x_B^0)$, and iterates for $k \ge 0$

$$x_B^{k+1} = J_{\gamma_k B}(x_A^k + \gamma_k u_B^k),\quad u_B^{k+1} = \tfrac{1}{\gamma_k}(x_A^k + \gamma_k u_B^k - x_B^{k+1}),\quad x_A^{k+1} = J_{\gamma_{k+1}A}(x_B^{k+1} - \gamma_{k+1}u_B^{k+1} - \gamma_{k+1}Cx_B^{k+1}).$$

The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from $\gamma_0$:

$$\text{(3.6)}\quad \gamma_{k+1} = \frac{-2\gamma_k^2\mu_C\eta + \sqrt{(2\gamma_k^2\mu_C\eta)^2 + 4(1+2\gamma_k\mu_B)\gamma_k^2}}{2(1+2\gamma_k\mu_B)}, \qquad \text{(3.7)}\quad \gamma_{k+1} = \frac{\gamma_k}{\sqrt{1 + 2\gamma_k(\mu_B - \gamma_kL_C^2/2)}}.$$

Formalization targets

Goal: Theorem 3.3, both parts

Let $B$ be $\mu_B$-strongly monotone with $\mu_B \ge 0$.

1. If $C$ is $\beta$-cocoercive and $\mu_C$-strongly monotone ($\mu_C > 0$), $\eta \in (0,1)$, $\gamma_0 \in (0, 2\beta(1-\eta))$ and the stepsizes follow (3.6), then for every $x^* \in \operatorname{zer}(A+B+C)$

$$\exists K\ \forall k \ge 0:\quad \|x_B^k - x^*\|^2 \le \frac{K}{(k+1)^2}.$$

2. If $C$ is $L_C$-Lipschitz, $\mu_B > 0$, $\gamma_0 \in (0, 2\mu_B/L_C^2)$ and the stepsizes follow (3.7), the same conclusion holds.

The goal asserts the shape of the rate only; the constant $K$ is not fixed.

Milestones

• Proposition 3.1, Parts 1 and 2: the one-step inequalities (3.9) and (3.10) for Algorithm 3 with arbitrary admissible stepsizes.
• Stepsize facts from the proof of Theorem 3.3: the identities that make (3.9) and (3.10) telescope, the monotonicity of the stepsizes (3.6), and the limits $(k+1)\gamma_k \to 1/(\mu_C\eta + \mu_B)$ for (3.6) and $(k+1)\gamma_k \to 1/\mu_B$ for (3.7).

Significance

The theorem shows that strong monotonicity of $B$ or $C$ can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for $x_B^k$, it applies directly to splitting schemes for strongly convex composite problems $\min f + g + h$ with $h$ smooth, where $x_B^k$ is the proximal point of $g$.

The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.

Difficulty

The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form $\|x_B^{k}-x^*\|^2 \lesssim \gamma_k^2$, and one must then show $\gamma_k$ decays exactly like $1/k$. The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form $c/k$ instead is a different algorithm and not covered by the theorem.

Formalization scope

• $H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.
• Resolvents are not constructed. They are families JA JB : ℝ → H → H required to satisfy the resolvent inclusion $\gamma^{-1}(x - J(\gamma)x) \in A(J(\gamma)x)$ for every $\gamma > 0$; for maximal monotone operators such maps exist and are unique, so nothing is lost.
• Algorithm 3 is a single recursive definition of the triple $(x_A^k, x_B^k, u_B^k)$ from $x_A^0$, the stepsizes, the resolvent families and $C$; the paper's loop index $k = 1, 2, \dots$ matches recursion (3.8) shifted by one.
• The stepsize rules (3.6) and (3.7) are recursive real sequences, used verbatim; each theorem assumes the paper's parameter ranges.
• $O(1/(k+1)^2)$ is rendered as $\exists K\,\forall k,\ \|x_B^k - x^*\|^2 \le K/(k+1)^2$, with $K$ chosen after all data (initial point, operators, constants, $\gamma_0$, $x^*$) and before $k$. No explicit constant is stated.
• Strong monotonicity of $C$ means $\mu_C > 0$; only $\mu_B = 0$ is allowed, as on the page. With $\mu_B = \mu_C = 0$ rule (3.6) keeps $\gamma_k$ constant and the rate fails, so a formalization allowing $\mu_C = 0$ would be false. In Part 2, $L_C > 0$ is assumed so that the stepsize interval is meaningful, and $C$ is assumed monotone, as in problem (1.1) and as used in the paper's proof of (3.10).
• The paper states (3.9) and (3.10) for all $k \ge 0$; at $k = 0$ the initial point $x_A^0$ is not a resolvent output, and both inequalities fail in general. The milestones state them for $k \ge 1$. Theorem 3.3 is unaffected, since finitely many initial terms do not change an $O(\cdot)$ bound.
• The display $\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}(2\gamma_k\mu_B + 2\gamma_{k+1}\mu_C\eta)$ on p. 845 has $\gamma_k$ and $\gamma_{k+1}$ swapped inside the bracket; the milestone states the corrected identity $\gamma_k\gamma_{k+1}(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta)$.
• A trivializing formalization, such as one in which the resolvent hypothesis is unsatisfiable, the stepsize interval is empty, or the rate constant may depend on $k$, is ruled out: the hypotheses are met by $A = 0$, $B = \mu_B I$ (with resolvents $J_{\gamma A} = I$, $J_{\gamma B} = (1+\gamma\mu_B)^{-1}I$) and $C = cI$ with $c > 0$, and $K$ is quantified before $k$.

Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.

Selected references

• D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017), 829–858. https://doi.org/10.1007/s11228-017-0421-z (preprint: https://arxiv.org/abs/1504.01032)
• R. I. Boţ, E. R. Csetnek, A. Heinrich and C. Hendrich, On the convergence rate improvement of a primal-dual splitting algorithm for solving monotone inclusion problems, Mathematical Programming 150 (2015), 251–279. https://doi.org/10.1007/s10107-014-0766-0
• A. Chambolle and T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, Journal of Mathematical Imaging and Vision 40 (2011), 120–145. https://doi.org/10.1007/s10851-010-0251-1
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

Conic quadratic problems (also called second-order cone programs) arise directly in applications such as contact problems with Coulomb friction, and a wide range of nonlinear convex problems can be rewritten in this form (Lobo, Vandenberghe, Boyd and Lebret 1998). Interior-point methods solve them in polynomial time, but around 2000 the available software for conic quadratic problems handled far fewer variables than linear programming software. Ben-Tal and Nemirovski (2001) therefore asked whether a conic quadratic problem can be replaced by a linear program of comparable size. Their construction replaces each second-order cone by a polyhedral cone that is exact up to a factor $1+\varepsilon$. The feasible set of the resulting linear program, projected back to the original variables, lies between the feasible set of the original problem and that of its $\varepsilon$-relaxation.

This sandwich is only useful if the relaxed problem is close to the original one, and in general it is not: the paper notes that (CQP) can be infeasible while every relaxation with $\varepsilon>0$ is feasible. Proposition 4.1 of the paper, the target of this mission, gives a sufficient condition under which the two feasible sets are $O(\varepsilon)$-close.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y^Ty}$ be the Euclidean norm. A conic quadratic problem in the variable $x\in\mathbb R^n$ is

$$\text{(CQP)}\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell,\ \ell=1,\dots,m\bigr\},$$

where $A$ is a $k_0\times n$ matrix and $b\in\mathbb R^{k_0}$ (the inequality $Ax\ge b$ is componentwise), and for each $\ell$ the matrix $A_\ell$ is $k_\ell\times n$, $b_\ell\in\mathbb R^{k_\ell}$, $c_\ell\in\mathbb R^n$ and $d_\ell\in\mathbb R$. For $\varepsilon>0$ the $\varepsilon$-relaxation is

$$\text{(CQP}_\varepsilon)\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le (1+\varepsilon)\bigl[c_\ell^Tx-d_\ell\bigr],\ \ell=1,\dots,m\bigr\}.$$

$\mathrm{Feas}(P)$ denotes the feasible set of a problem $(P)$; in Lean these are feas P and feasRelaxed P ε, subsets of Fin n → ℝ, for a problem datum P : CQP n k₀ m.

Two conditions on (CQP) are used.

1. Strict feasibility: there are $\bar x$ and $r>0$ with $A\bar x\ge b$ and $\|A_\ell\bar x-b_\ell\|_2\le[c_\ell^T\bar x-d_\ell]-r$ for every $\ell$ (IsStrictlyFeasible P x̄ r).
2. Semiboundedness: there is $R$ such that every feasible $x$ of (CQP) satisfies $c_\ell^Tx-d_\ell\le R$ for every $\ell$ (IsSemibounded P R).

Put $\gamma(\varepsilon)=R\varepsilon/r$.

Formalization targets

Goal: Proposition 4.1

If (CQP) has $m\ge1$ conic constraints and is strictly feasible and semibounded, then for every $\varepsilon>0$ with $\gamma(\varepsilon)<1$,

$$\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))\,\mathrm{Feas}(\mathrm{CQP}_\varepsilon)\ \subseteq\ \mathrm{Feas}(\mathrm{CQP})\ \subseteq\ \mathrm{Feas}(\mathrm{CQP}_\varepsilon). \tag{14}$$

The left-hand side is the image of $\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ under $y\mapsto\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))y$, not a Minkowski sum.

Milestones

The milestones follow the paper's proof in order.

1. The right inclusion $\mathrm{Feas}(\mathrm{CQP})\subseteq\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ for $\varepsilon>0$.
2. For $y\in\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ and $t_\ell=c_\ell^Ty-d_\ell$, every $\delta\in[0,1]$ with $\delta\ge\varepsilon t_\ell/(r+\varepsilon t_\ell)$ for all $\ell$ makes $x_\delta=(1-\delta)y+\delta\bar x$ feasible for (CQP).
3. Under semiboundedness, the same $\delta$ satisfies $(1-\delta)t_\ell\le R$ for all $\ell$.
4. If $\delta=\varepsilon t/(r+\varepsilon t)$ with $t\ge0$, $(1-\delta)t\le R$ and $\gamma(\varepsilon)<1$, then $t\le R/(1-\gamma(\varepsilon))$ and $\delta\le\gamma(\varepsilon)$.

Significance

The result. Proposition 4.1 turns the qualitative sandwich "exact ⊆ polyhedral ⊆ relaxed" into a quantitative statement. When a problem is strictly feasible with margin $r$ and its conic right-hand sides are bounded by $R$ on the feasible set, the relaxed feasible set, shrunk towards $\bar x$ by $1-\gamma(\varepsilon)$, lies inside the exact one. The error of the relaxation is thus controlled by $\gamma(\varepsilon)=R\varepsilon/r$, which is linear in $\varepsilon$. Together with the paper's main theorem, that a polyhedral $\varepsilon$-approximation of the Lorentz cone with $O(k\ln(1/\varepsilon))$ variables and inequalities exists, this measures how well a linear program of moderate size approximates the conic problem. The paper uses it this way for the examples in its introduction.

The formalization. The proposition is proved in the paper; no machine-checked version is known. This mission produces a Lean formalization of conic quadratic problems and their relaxations with the Euclidean norm, together with the strict feasibility and semiboundedness conditions and the proof. The Lorentz-cone approximation results of the same paper are the subject of the companion missions I and II of this series.

Difficulty

The right inclusion is immediate. The left inclusion does not follow from convexity alone. A relaxed-feasible point $y$ may violate every conic constraint of (CQP), and nothing about $y$ bounds how far it is from $\mathrm{Feas}(\mathrm{CQP})$. The needed information comes from semiboundedness, which constrains only feasible points of (CQP). That hypothesis therefore cannot be applied to $y$ itself, and the shrink factor $\gamma(\varepsilon)$ must be obtained without any bound on $c_\ell^Ty-d_\ell$ given in advance. The obvious attempt, bounding the violation at $y$ by $\varepsilon R$, fails for exactly this reason.

Formalization scope

• Vectors of $\mathbb R^n$ are Fin n → ℝ; the $m$ conic constraints are indexed by Fin m (0-based) with a dependent family of matrices (ℓ : Fin m) → Matrix (Fin (k ℓ)) (Fin n) ℝ, so the row sizes $k_\ell$ may differ. The norm is written out as eucNorm y = √(∑ i, y i ^ 2); Mathlib's norm on Fin k → ℝ is the sup norm and is not used.
• Only feasible sets are compared; the objective $e$ is carried as data but plays no role.
• Correction 1. In hypothesis (i) the page prints $[c_\ell^Tx-d_\ell]-r$ without the bar over $x$. The proof uses $c_\ell^T\bar x-d_\ell-r$, which is what IsStrictlyFeasible states.
• Correction 2. The goal assumes $m\ge1$, which the paper leaves implicit. With $m=0$, semiboundedness is vacuous and $R$ may be negative, so $\gamma(\varepsilon)<0$. Then the map $y\mapsto\gamma\bar x+(1-\gamma)y$ extrapolates beyond $y$ and can leave $\{Ax\ge b\}$. An example is $n=1$, $A=[1]$, $b=0$, $\bar x=1$, $y=0$, $R=-1$, $r=\varepsilon=1$. For $m\ge1$ the hypotheses force $R\ge r>0$.
• $\varepsilon$ ranges over all $\varepsilon>0$ with $\gamma(\varepsilon)<1$, as in the paper; it is not restricted to $(0,1]$.
• The second milestone is stated for every $\delta\in[0,1]$ that dominates all ratios $\varepsilon t_\ell/(r+\varepsilon t_\ell)$, rather than only for the paper's $\delta=\max_\ell$. This includes the paper's case.
• The goal cannot be satisfied trivially. The strict feasibility and semiboundedness hypotheses are jointly satisfiable (for example $n=m=1$, the constraint $|x|\le 1$ written as $\|x\|_2\le 1$, $\bar x=0$, $r=1$, $R=1$), and the conclusion is the full two-sided inclusion with the paper's $\gamma(\varepsilon)$, not the existence of some contraction factor.
• Needed infrastructure: Euclidean-norm convexity (the triangle inequality and homogeneity for eucNorm, or a transfer to EuclideanSpace ℝ (Fin k)) and linearity of Matrix.mulVec and dotProduct. A convexity lemma for feas P would be reusable beyond this mission, and contributions of it are welcome.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0
• Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.

Timeline:

• 1955. Beale (§5, Theorems 2 and 3) and Dantzig independently introduce two-stage linear programs with random data; Beale proves that the expected cost is convex in the first-stage decision, and that the cost is convex in the random data for fixed decision.
• 1967. Walkup and Wets, Stochastic Programs with Recourse, study the domain of the expected recourse function and its properties under fixed recourse.
• 1974. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, gives the systematic treatment of convexity, finiteness and polyhedrality of the expected recourse function, now textbook material (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 3).

Setting

Constants $c\in\mathbb R^n$, $f\in\mathbb R^p$ and an $m\times p$ matrix $D=(d_{ik})$ are given. The data $A=(\alpha_{ij})$, an $m\times n$ matrix, and $\beta\in\mathbb R^m$ are random variables on a probability space $(\Omega,P)$: their distribution is known when the first-stage decision $x\in\mathbb R^n$, $x\ge0$, is chosen, and their values are known when the second-stage decision $y\in\mathbb R^p$, $y\ge0$, is chosen. The cost is

$$C=c'x+f'y,\qquad Ax+Dy=\beta. \qquad(5.3),(5.4)$$

For a right-hand side $b\in\mathbb R^m$ the second-stage value is

$$Q(b)=\min\{f'y : y\ge0,\ Dy=b\},$$

and for fixed data the cost of a first-stage decision is $C(x)=c'x+Q(\beta-Ax)$. The expected cost is

$$E(C)(x)=\int_\Omega \bigl(c'x+Q(\beta(\omega)-A(\omega)x)\bigr)\,dP(\omega).$$

The problem is to choose $x\ge0$ minimising $E(C)$. In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.

Formalization targets

Goal: Theorem 2 (p. 182)

Assume that for every $x\ge0$ the second-stage minimum is attained for almost every outcome and that $\omega\mapsto C(x,\omega)$ is integrable. Then

$$E(C)(\lambda_1x_1+\lambda_2x_2)\le\lambda_1E(C)(x_1)+\lambda_2E(C)(x_2)\qquad(x_1,x_2\ge0,\ \lambda_1,\lambda_2\ge0,\ \lambda_1+\lambda_2=1),$$

that is, $E(C)$ is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of $(A,\beta)$.

Milestones

1. Pointwise convexity (last display of the proof of Theorem 2, p. 182): for fixed data $(A,\beta)$, with the minimum attained at every $x\ge0$,

$$C(\lambda_1x_1+\lambda_2x_2)\le\lambda_1C(x_1)+\lambda_2C(x_2).$$

2. Theorem 3 (p. 182): for fixed $x$, the cost $(A,\beta)\mapsto c'x+Q(\beta-Ax)$ is jointly convex on every convex set of data on which the second-stage minimum is attained.
3. Eqs. (5.5)–(5.6) (p. 182): for a finitely supported distribution, $A=A_r$ and $\beta=\beta_r$ with probability $p_r$, the value $E(C)(x)$ is the minimum of $c'x+\sum_r p_r f'y_r$ over non-negative $y_r$ with $A_rx+Dy_r=\beta_r$ for all $r$; minimising $E(C)$ is then a linear program.

Significance

The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in $x$, whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate $E(C)$ from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.

Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of $c'x+E\,Q$ for an arbitrary distribution.

Difficulty

The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some $x$ and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain $x\ge0$ the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family $(y_r)_r$ has to be matched with the probability-weighted sum of per-scenario minima.

Formalization scope

• Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and $y\ge0$ is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.
• The second-stage value is the real infimum of $f'y$ over the feasible set. It equals $0$ on an infeasible or unbounded-below second stage, so each theorem assumes attainment of the minimum where it is evaluated (the paper's "value of $y$ that minimizes $C$"). The goal assumes attainment for almost every outcome at every $x\ge0$.
• $E(C)$ is the Bochner integral, which is $0$ for a non-integrable integrand, so the goal assumes integrability of $C(x,\cdot)$ at every $x\ge0$ (the paper's "mean value $E(C)$").
• Convexity is claimed on $\{x : x\ge0\}$, the paper's domain, not on all of $\mathbb R^n$. Theorem 3 is stated for fixed non-negative $x$ (the model's first-stage domain) and on every convex set of data on which the minimum is attained, since the paper names no domain.
• A formalization in which the value is an unconstrained infimum without attainment, or the expectation is taken without integrability, is trivially convex on the region where the default values apply and does not state Beale's theorem; such variants are ruled out.
• Reusable beyond this mission: basic facts on the optimal value of a parametric linear program in its right-hand side and cost data, and convexity of integrals of pointwise-convex integrands. Proofs of the milestones and of the goal, and alternative formulations in extended reals, are welcome.

Selected references

• E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2):173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
• G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
• F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
• D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM Journal on Applied Mathematics 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4