The OR Formalization Drive

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below $3/2$ unless P = NP. The natural question is therefore asymptotic: how small can the additive error $A(I) - OPT(I)$ be made, as a function of the optimum $OPT(I)$?

• 1974: D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey and R. L. Graham analysed First Fit and First Fit Decreasing, with asymptotic ratios $17/10$ and $11/9$ (SIAM J. Comput. 3(4)).
• 1981: W. Fernandez de la Vega and G. S. Lueker gave an asymptotic approximation scheme: for every $\varepsilon > 0$, $(1+\varepsilon)\,OPT(I) + 1$ bins in linear time (Combinatorica 1).
• 1982: N. Karmarkar and R. M. Karp replaced the multiplicative error by an additive one: $OPT(I) + O(\log^2 OPT(I))$ bins in polynomial time (Proc. 23rd FOCS). This mission formalizes that bound.
• 2017: R. Hoberg and T. Rothvoss improved the additive error to $O(\log OPT)$ (SODA 2017). Whether $OPT(I) + O(1)$ is achievable remains open.

Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.

Setting

An instance $I$ is a finite multiset of piece sizes in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, $SIZE(I)$ for the total size and $a(I)$ for the smallest size. A packing is a multiset of bins whose union is $I$ and in each of which the sizes sum to at most $1$; its cost is the number of bins, and $OPT(I)$ is the least cost.

A configuration is a nonempty multiset of sizes occurring in $I$ that fits in one bin. The fractional bin-packing problem is the linear program

$$(I)\qquad \min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x \ge 0,\quad Ax \ge b,$$

with one variable $x_j$ per configuration, where $A_{tj}$ counts the pieces of size $t$ in configuration $j$ and $b_t$ the pieces of size $t$ in $I$. Its value is $LIN(I)$. A basic feasible solution is an extreme point of the feasible region.

Geometric grouping with parameter $k$ sorts the pieces in non-increasing order and cuts them into consecutive groups $G_1, G_2, \dots, G_q$, each the shortest run of pieces of total size at least $k$. Within each group $G_i$ ($i \ge 2$) only as many of the largest pieces as $G_{i-1}$ has are kept; they are rounded up to the largest size in $G_i$, giving $G_i'$. The rounded pieces form $J$, and $G_1$ together with the unrounded leftovers $\Delta G_i$ form $J'$.

ALGORITHM 2 with a positive integer $k$ and a positive real $g$:

1. Eliminate all pieces of size $\le g$.
2. While $SIZE > 1 + \frac{1}{1-1/k}\ln\frac1g$: group the current instance into $J, J'$; pack $J'$ in at most $2k[2 + \ln\frac1g]$ bins; obtain a basic feasible solution $x$ of the LP of $J$ with cost at most $LIN(J)+1$; open $\lfloor x_j\rfloor$ bins of each configuration $j$, fill them with pieces, and delete the pieces so packed.
3. Pack the remaining pieces in at most $2 + \frac{2}{1-1/k}\ln\frac1g$ bins.
4. Reinsert the eliminated pieces, using a new bin only when necessary.

Its cost on $I$ is written $A(I)$.

Formalization targets

Goal: Theorem 4 with explicit constants

For every instance $I$ with $SIZE(I) \ge 2$, every packing that ALGORITHM 2 with $k=2$ and $g = 1/SIZE(I)$ can output is a packing of $I$ with

$$A(I) \le OPT(I) + \bigl(1 + \log_2 OPT(I)\bigr)\bigl(9 + 4\ln OPT(I)\bigr) + 2 + 4\ln OPT(I).$$

This is the paper's $A(I) \le OPT(I) + O(\log^2 OPT(I))$, with the constants that its proof yields.

The general bound for ALGORITHM 2

For integers $k \ge 2$, $0 < g \le \tfrac12$ and $SIZE(I) \ge 1$:

$$A(I) \le \max\Bigl\{(1+2g)\,OPT(I) + 1,\ OPT(I) + \Bigl[1 + \frac{\ln SIZE(I)}{\ln k}\Bigr]\Bigl[1 + 4k + 2k\ln\frac1g\Bigr] + 2 + \frac{2}{1-\frac1k}\ln\frac1g\Bigr\}.$$

Milestones

In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on $J'$, item 4 corrected); the per-iteration shrinking of $SIZE$; the bound on the number $t$ of iterations; the telescoping of $LIN$; the bin count after Step 3; the general bound.

Significance

The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme ($O(\log^2 OPT) = o(OPT)$). Varying $k$ and $g$ trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the $O(\log OPT)$ bound of Hoberg and Rothvoss.

The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.

Difficulty

Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most $m$ fractional variables, and after rounding down, the leftover pieces form an instance of size at most $m(J)$. With linear grouping that leftover is of order $1/\varepsilon^2$ and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance $J$ with $m(J) \le SIZE/k + O(\ln(1/g))$ distinct sizes while discarding only $O(k\ln(1/g))$ in $J'$. The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in $SIZE$, $LIN$ and $OPT$, with an additive loss per iteration; the harmonic-sum estimate behind $SIZE(J')$ and the telescoping of $LIN$ across iterations carry most of the weight.

Formalization scope

• Model. An instance is a Multiset ℝ with sizes in the open interval $(0,1)$; real sizes generalize the paper's rationals, and the interval is open because a group of size at least $k$ must contain more than $k$ pieces. Packings are Multiset (Multiset ℝ). $OPT$ and $LIN$ are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.
• Subroutine contract. The Fractional Bin-Packing procedure is modelled only by its stated output: any basic feasible solution of cost at most $LIN(J)+1$. The ellipsoid method of §6 is not modelled.
• Runs. ALGORITHM 2 is a relation Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.
• Explicit constants. $O(\log^2 OPT(I))$ in Theorem 4 is replaced by $(1+\log_2 OPT)(9 + 4\ln OPT) + 2 + 4\ln OPT$. The asymptotic threshold is made explicit as $SIZE(I) \ge 2$. $\ln$ is Real.log and $\log_2$ is Real.logb 2.
• Corrected statements. The last group of geometric grouping may fall short of $k$, which the paper ignores. For it, $\Delta G_q$ consists of the $\max(0, l_q - l_{q-1})$ smallest pieces. Theorem 2, item 4 is stated as $m(J) \le SIZE(J)/k + \ln(1/a(I)) + 1$; the printed version without $+1$ fails for $I = \{0.95, 0.95, 0.95, 0.9\}$, $k = 2$. Theorem 2 is stated for integers $k \ge 2$, which its proof needs. The iteration bound is stated for $t \ge 1$ and for the instance after Step 1.
• Out of scope. Running times, polynomiality, the function $T(m,n)$, the number of subroutine calls, §6, ALGORITHM 3 and Theorem 5.
• Ruling out trivial versions. "There exists a packing with at most $OPT(I) + \dots$ bins" is trivially true and is not the goal. The goal bounds every output of the algorithm, and the existence item shows that outputs exist.

Contributions welcome: milestone proofs; a harmonic-sum bound $\sum_{j=a}^{b} 1/j \le \ln\frac{b}{a-1}$; extreme-point facts for $\{x \ge 0 : Ax \ge b\}$ (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of $LIN$ and $OPT$ under the piecewise order.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), IEEE, pp. 312–320, 1982. https://doi.org/10.1109/SFCS.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1 + ε in linear time, Combinatorica 1(4), 349–355, 1981. https://doi.org/10.1007/BF02579456
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-case performance bounds for simple one-dimensional packing algorithms, SIAM J. Comput. 3(4), 299–325, 1974. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoss, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. 28th ACM-SIAM SODA, 2616–2625, 2017. https://doi.org/10.1137/1.9781611974782.172

Motivation

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

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

Setting

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

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

The augmented Lagrangian is

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (p. 11)

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4

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

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

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

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

Milestones

In the order of the paper's proof:

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.

Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to $1 - 1/e$ when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online $b$-matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the $1 - 1/e$ bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.

Setting

There is a finite nonempty set $I$ of buyers. Buyer $i$ has a known budget $B(i) > 0$. Products $j = 1, \dots, m$ arrive one by one; when product $j$ arrives, every buyer's bid $b(i,j) \ge 0$ on it is revealed. The bid-to-budget ratio is

$$R_{\max} = \max_{i \in I,\, j} \frac{b(i,j)}{B(i)} .$$

A fractional allocation $y(i,j) \ge 0$ assigns fractions of products to buyers; the revenue from buyer $i$ is the minimum of $\sum_j b(i,j)\,y(i,j)$ and $B(i)$.

The offline fractional problem is the packing LP, which the paper calls the dual:

$$\max \sum_{j}\sum_{i} b(i,j)\,y(i,j) \quad\text{s.t.}\quad \sum_i y(i,j) \le 1 \ \ \forall j,\qquad \sum_j b(i,j)\,y(i,j) \le B(i)\ \ \forall i,\qquad y \ge 0 .$$

Its LP dual, the paper's primal, is the covering LP:

$$\min \sum_i B(i)\,x(i) + \sum_j z(j) \quad\text{s.t.}\quad b(i,j)\,x(i) + z(j) \ge b(i,j)\ \ \forall i,j,\qquad x, z \ge 0 .$$

The Allocation Algorithm has a parameter $c > 1$ and starts from $x \equiv 0$. When product $j$ arrives it takes a buyer $i$ maximizing $b(i,j)(1 - x(i))$. If $x(i) \ge 1$, the product is not sold. Otherwise it charges $i$ the minimum of $b(i,j)$ and $i$'s remaining budget, sets $y(i,j) \leftarrow 1$ and $z(j) \leftarrow b(i,j)(1 - x(i))$, and updates

$$x(i) \leftarrow x(i)\Big(1 + \frac{b(i,j)}{B(i)}\Big) + \frac{b(i,j)}{(c-1)\,B(i)} .$$

Its revenue is the total amount charged.

Formalization targets

Goal: Theorem 1

For every instance and every bound $R > 0$ with $b(i,j) \le R\,B(i)$ for all $i, j$, the Allocation Algorithm run with $c = (1+R)^{1/R}$, under any tie-breaking of the maximum, satisfies for every feasible $y'$ of the packing LP

$$\mathrm{Revenue} \;\ge\; \Big(1 - \frac1c\Big)(1 - R)\sum_{j}\sum_{i} b(i,j)\,y'(i,j).$$

With $R = R_{\max}$ this is the paper's statement that the algorithm is $(1 - 1/c)(1 - R_{\max})$-competitive; the fractional optimum bounds every integral offline allocation.

Milestones

The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:

1. the inequality $\ln(1+x)/x \ge \ln(1+y)/y$ for $0 < x \le y \le 1$;
2. Claim (1): the final $(x, z)$ is feasible for the covering LP;
3. Claim (2): the covering cost of the run equals $(1 + 1/(c-1))$ times the packing value of the run's own $y$;
4. Inequality (1): $x(i) \ge \frac{1}{c-1}\big(c^{\sum_j b(i,j) y(i,j)/B(i)} - 1\big)$ at every stage of the run;
5. Claim (3): $\sum_j b(i,j)\,y(i,j) \le B(i) + \max_j b(i,j)$, and the amount charged to $i$ is at least $(1 - R)\sum_j b(i,j)\,y(i,j)$;
6. weak duality for the LP pair above;

and, separately, the second sentence of Theorem 1,

$$\lim_{R\to 0^+}\Big(1 - \frac{1}{(1+R)^{1/R}}\Big)(1-R) = 1 - \frac1e .$$

Significance

Theorem 1 gives an explicit ratio for every value of $R_{\max}$, not only in the limit. It tends to the optimal deterministic ratio $1 - 1/e$ as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).

The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.

Difficulty

Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that $x$ only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of $c$ matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.

A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.

Formalization scope

Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with $B(i) > 0$ and $b(i,j) \ge 0$. The state of the algorithm records $x$, the amounts charged, $y$ and $z$; one iteration is step, the run after $k$ products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current $x$ and the product, required to return a maximizer of $b(i,j)(1-x(i))$; the theorem holds for every such rule. The constant $c = (1+R)^{1/R}$ is a real power and requires $R > 0$. The theorem is stated for any bound $R$ on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every $c > 1$, which covers the paper's choice. The paper's inequality for $\ln(1+x)/x$ allows $x = 0$, read as a limit; the Lean statement requires $x > 0$.

A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.

The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact-$R_{\max}$ form or the bound against integral allocations.

Selected references

• N. Buchbinder, K. Jain, J. Naor, Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue, Algorithms – ESA 2007, LNCS 4698, 2007. https://doi.org/10.1007/978-3-540-75520-3_24
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
• B. Kalyanasundaram, K. R. Pruhs, An Optimal Deterministic Algorithm for Online b-Matching, Theoretical Computer Science 233(1–2), 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

Why certify nonconvex scenario solutions

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

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

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

Setting

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

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

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

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

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

Formalization targets

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

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

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

Lean representation and committed conventions:

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

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

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

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

Selected references

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

Motivation

In a two-stage stochastic linear program a decision $x$ is taken before random data $\xi$ are observed, and a corrective recourse decision $y$ is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, $\int Q(x,\xi(\omega))\,P(d\omega)$, and for continuous or high-dimensional $\xi$ that integral cannot be evaluated exactly. Practical methods therefore replace $\xi$ by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.

Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.

Setting

The two-stage problem (2.11) is: minimize $\psi(x)=c^Tx+\int_\Omega Q(x,\xi(\omega))\,P(d\omega)$ subject to $Ax=b$, $x\ge 0$. The recourse cost $Q(x,\xi)$ is the optimal value of the second-stage problem (2.12),

$$Q(x,\xi)=\min\{q^Ty : Wy=h-Tx,\ y\ge 0\},\qquad \xi=(q,h,T),$$

with a deterministic $m_2\times n_2$ matrix $W$ (fixed recourse), and $Q=+\infty$ when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, $\{Wy:y\ge0\}=\mathbb R^{m_2}$, and dual feasibility: for every realization of $q$ some $u$ satisfies $W^Tu\le q$. Under these assumptions $Q$ is finite. The expected recourse function is $\mathcal Q(x)=\int Q(x,\xi(\omega))\,P(d\omega)$.

The Edmundson–Madansky law of an interval $[a,b]$, $a<b$, with mean $\xi^0$ puts mass $p_1=(b-\xi^0)/(b-a)$ at $a$ and $p_2=(\xi^0-a)/(b-a)$ at $b$ (2.32). For a box $\Xi=\times_{j=1}^m[a_j,b_j]$ and means $\xi^0_j$, the vector $\hat\xi$ with independent components of these two-point laws sits at the vertex $v$ with probability $\prod_j p_j(v_j)$.

Simple recourse is the case $W=[I,-I]$, $q=[q^+,q^-]$ with $q^+_j+q^-_j\ge0$, deterministic $T$ and random $h$ only. With $\chi=Tx$ the recourse cost splits into one-row costs $Q_j(\chi_j,h_j)=q^+_j(h_j-\chi_j)$ if $h_j\ge\chi_j$, and $q^-_j(\chi_j-h_j)$ otherwise.

Formalization targets

Goal: the Edmundson–Madansky bound for independent components (p. 46)

If $\xi$ has independent components $\xi_j\in[a_j,b_j]$ with means $\xi^0_j$, and $\varphi$ is convex on $\Xi=\times_j[a_j,b_j]$, then

$$E\varphi(\xi)\le\sum_{v\in\mathrm{vert}\,\Xi}\Big(\prod_{j=1}^m p_j(v_j)\Big)\varphi(v).$$

The book applies it to $\varphi=Q(x,\cdot)$; the goal is stated for every convex $\varphi$, with the explicit weights of (2.32).

Milestones

1. Properties (b), (d), (e) of p. 40: $Q(x,\cdot)$ is piecewise linear and convex in $(h,T)$; $Q(\cdot,\xi)$ is convex piecewise linear in $x$; the expected recourse function is finite and convex under finite second moments.
2. The Jensen lower bound (2.26)–(2.27) on a partition (a published, proved theorem, reused).
3. The dual-multiplier lower bound (2.30)–(2.31).
4. The one-dimensional Edmundson–Madansky inequality (2.32)–(2.34).
5. For simple recourse: separability (2.46)–(2.49), the closed form (2.51) of $EQ_j$, and the bounds (2.55)–(2.56) from the one-block problem.

Significance

The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.

The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.

Difficulty

The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs $\varphi$ with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on $[0,1]^2$ with means $(\tfrac12,\tfrac12)$ and $\varphi(x,y)=(x-y)^2$, the product law gives $\tfrac12$ while mass $\tfrac12$ at $(1,0)$ and at $(0,1)$ gives $1$. The book's remark that the product law is extremal among all laws on $\Xi$ with the given mean fails for this reason when $m\ge2$, and is not part of this mission.

For the recourse properties the difficulty is bookkeeping: $Q$ is an extended-real optimal value, and finiteness, measurability in $\omega$ and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.

Formalization scope

Vectors are functions from finite index types to $\mathbb R$ (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives $+\infty$ and unboundedness $-\infty$ exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with $a_j<b_j$, and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.

Conventions fixed where the page is silent or ambiguous:

• Properties (b), (d), (e) are stated on all of $\mathbb R^{n_1}$: under the standing complete-recourse assumption $K_2=\mathbb R^{n_1}$. "Convex piecewise linear" is rendered as a maximum of finitely many affine functions.
• The book's hypothesis of finite second moments in (e) is kept as stated, componentwise.
• The book writes $Q$ for both $Q(x,\xi)$ and $\mathcal Q(x)$, and reuses $\tilde Q$, $\tilde\psi$ for different functions in (2.27) and (2.30)–(2.31); the Lean names are recourseCost, expectedRecourse and dualLowerBound.
• In (2.51) a conditional mean on a null event is $0$ in Lean; it always appears multiplied by that event's probability, so the formula is unchanged.
• In (2.56) the minimum is a real infimum over the nonempty first-stage feasible set; attainment is not claimed.
• No constant of the chapter is hidden behind $O(\cdot)$; all bounds are explicit.

A goal stated for affine $\varphi$ (where it is an equality), or with $\hat\xi$ allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.

A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.

Selected references

• P. Kall, A. Ruszczyński, K. Frauendorfer, "Approximation Techniques in Stochastic Programming", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 2, pp. 33–64. https://doi.org/10.1007/978-3-642-61370-8
• A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Annals of Mathematical Statistics 30 (1959), 743–746. https://doi.org/10.1214/aoms/1177706203
• P. Kall, Stochastic Linear Programming, Springer 1976. https://doi.org/10.1007/978-3-642-66252-2
• R. J-B Wets, "Stochastic programs with fixed recourse: the equivalent deterministic program", SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
• K. Frauendorfer, "Solving SLP recourse problems with arbitrary multivariate distributions — the dependent case", Mathematics of Operations Research 13 (1988), 377–394. https://doi.org/10.1287/moor.13.3.377
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer 1997, Ch. 8. https://doi.org/10.1007/b97617