Optimization

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

• 2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
• 2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
• 2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$-approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$, symmetric if $f([n]\setminus S) = f(S)$ for all $S$, and $\mathrm{OPT}(f) = \max_{S} f(S)$.

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$, so that $\epsilon n$ is an integer. For integers $k, \ell$ put

$$f(k,\ell) = \begin{cases} (k+\ell)(n-k-\ell) & |k-\ell| \le m,\\ k(n-2\ell) + (n-2k)\ell + m^2 - 2m|k-\ell| & |k-\ell| > m. \end{cases}$$

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$, the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$. The cut function of the complete graph is $g(S) = |S|(n-|S|)$, with maximum $\tfrac14 n^2$. A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$; on balanced sets $f_C = g$.

A deterministic adaptive $q$-query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$. A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$.

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$:

1. every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

$$\mathrm{OPT}(f_C) = \tfrac12 n^2 (1 - 2\epsilon + 2\epsilon^2);$$

2. for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$-query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

$$\mathbb{E}_{A\sim\mu}\bigl[f_C(A(f_C))\bigr] \le \tfrac14 n^2 + \bigl(2e^{-\epsilon^2 n/8} + 2e^{-\epsilon^2 n/4}\bigr)\,\mathrm{OPT}(f_C).$$

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$.

Milestones

• Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$.
• Submodularity of $f_C$.
• The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$, attained at $S = C$.
• A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$.
• If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$.
• The deterministic case of the bound, averaged over $C$.

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$-approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

• The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$, following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
• The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$, written multiplied out.
• A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees $f$ only through query answers; it never receives $C$.
• Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$", is not what the proof gives for one and the same $\epsilon$. On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$, and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$. The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$, is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$.
• Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$.
• Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$, which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
• Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
• J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

Many polytopes that arise in combinatorial optimization, such as the matching, cut, stable set and travelling salesman polytopes, have exponentially many facets, yet some of them can be written as the linear projection of a polyhedron with far fewer facets. The smallest number of facets of such a lift decides whether the polytope admits a compact linear-programming formulation. Yannakakis (Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43 (1991)) showed that this number equals the nonnegative rank of the polytope's slack matrix, turning a question about formulations into a question about matrix factorizations. Gouveia, Parrilo and Thomas (arXiv:1111.3164v2) extended this correspondence from polytopes and nonnegative orthants to arbitrary convex bodies and closed convex cones.

Exact nonnegative rank is NP-hard to compute (Vavasis, SIAM J. Optim. 20 (2009)), so lower bounds matter. The oldest ones are combinatorial: they see only which entries of the slack matrix are zero. Goemans (Smallest compact formulation for the permutahedron, Math. Program. 153 (2015)) observed that a polytope with $n_C$ faces needs a lift with at least $\log_2 n_C$ facets. Section 4.2 of Gouveia–Parrilo–Thomas recasts these support-based bounds through the face lattice and derives, alongside Goemans' bound, a sharper antichain bound. This mission formalizes that chain of results.

Setting

Write $\mathbb{R}^n$ for Euclidean space with inner product $\langle\cdot,\cdot\rangle$. A polytope $C \subseteq \mathbb{R}^n$ is the convex hull of finitely many points; as throughout the paper, the origin is assumed to lie in its interior. The polar of $C$ is

$$C^\circ = \{\, y \in \mathbb{R}^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.$$

Let $\operatorname{ext}(C)$ be the set of extreme points of $C$ (its vertices). The slack operator $S_C$ is the function $S_C(x, y) = 1 - \langle x, y\rangle$ on $\operatorname{ext}(C) \times \operatorname{ext}(C^\circ)$. The extreme points of $C^\circ$ correspond to the facets of $C$, the facet of $y$ being $\{x \in C : \langle x, y\rangle = 1\}$, so $S_C$ is the canonical vertex–facet slack matrix of $C$ and is nonnegative.

An $\mathbb{R}^k_+$-factorization of $S_C$ consists of maps $A : \operatorname{ext}(C) \to \mathbb{R}^k_+$ and $B : \operatorname{ext}(C^\circ) \to \mathbb{R}^k_+$ with $S_C(x, y) = \langle A(x), B(y)\rangle$. The nonnegative rank $\operatorname{rank}_+(C)$ is the least such $k$, and $+\infty$ if there is none.

The support $\operatorname{supp}(S_C)$ is the $0/1$ matrix with a one where $S_C(x,y) \ne 0$. A Boolean factorization of it of intermediate dimension $k$ assigns subsets $A(x), B(y) \subseteq [k] = \{1,\dots,k\}$ with $S_C(x,y) \ne 0 \iff A(x) \cap B(y) \ne \emptyset$; the least such $k$ is the Boolean rank.

A face of $C$ is the empty set or a set of maximizers in $C$ of a linear functional; $C$ itself is a face. The face lattice $L(C)$ is the set of faces ordered by inclusion, and the Boolean lattice $2^{[k]}$ is the set of subsets of $[k]$ ordered by inclusion. An embedding $\varphi : L(C) \to 2^{[k]}$ satisfies $H \subseteq F \iff \varphi(H) \subseteq \varphi(F)$.

Formalization targets

Goal: Corollary 4.13 (p. 16)

For a polytope $C$:

$$\text{(1)}\quad \operatorname{rank}_+(C) \ \ge\ \min\Big\{ k : p \le \tbinom{k}{\lfloor k/2 \rfloor} \Big\}$$

for every antichain of $p$ faces of $C$ (no face contained in another), and

$$\text{(2)}\quad \operatorname{rank}_+(C) \ \ge\ \log_2 n_C ,$$

where $n_C$ is the number of faces of $C$, including $\emptyset$ and $C$.

Milestones

1. §4.2, p. 15. For a nonnegative matrix $M$, $\operatorname{rank}_B(M) \le \operatorname{rank}_+(M)$: a nonnegative factorization of intermediate dimension $k$ yields a Boolean factorization of $\operatorname{supp}(M)$ of the same dimension.
2. Theorem 4.11, p. 15. $\operatorname{supp}(S_C)$ has a Boolean factorization of intermediate dimension $k$ if and only if $L(C)$ embeds into $2^{[k]}$.
3. Corollary 4.12, p. 15. $\operatorname{rank}_+(C) \ge \min\{k : L(C) \text{ embeds into } 2^{[k]}\}$.

Significance

Both bounds depend only on the combinatorial type of the polytope. For a square they give $\operatorname{rank}_+ \ge \log_2 10 \approx 3.32$ and $\operatorname{rank}_+ \ge 4$; for a three-dimensional cube $\log_2 28 \approx 4.81$ and $6$ (p. 16). For the regular $n$-gon, whose slack matrices all have rank $3$, the face-count bound gives $\operatorname{rank}_+ \ge \log_2 n$, which is of the optimal order (Example 4.14). Theorem 4.11 is the statement that the Boolean rank of a slack matrix, also known as its rectangle covering number, is an invariant of the face lattice; the rectangle-covering version is phrased as Theorem 2.9 of Fiorini, Kaibel, Pashkovich and Theis (Combinatorial bounds on nonnegative rank and extended formulations, arXiv:1111.0444), as cited by the paper.

The results are proved in the paper. The formalization provides machine-checked definitions of the polar, the slack operator of a polytope, its nonnegative and Boolean ranks and its face lattice, reusable for later work on extension complexity (for instance, rectangle-covering lower bounds for specific polytopes). No formal proof of these statements is known to exist in Lean or on this platform.

Difficulty

Milestone 1 and the passage from Corollary 4.12 to Corollary 4.13 are short: Sperner's theorem is available in Mathlib as IsAntichain.sperner, and an embedding of $L(C)$ into $2^{[k]}$ is injective. The weight lies in Theorem 4.11, which needs facts about polytopes that Mathlib does not state in this form: every vertex is an exposed point, each extreme point of the polar cuts out a face, every face of a polytope is the convex hull of the vertices it contains, and every proper face is the intersection of the facets containing it, with those facets indexed by $\operatorname{ext}(C^\circ)$. The last fact is where the origin-in-the-interior assumption and the polar enter, and it fails for faces described by an arbitrary list of inequalities that is not the facet description. A second, smaller difficulty is finiteness: the face-count bound needs the set of faces of a polytope to be finite.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with the Euclidean inner product. The polar is the one-sided polar above, not Mathlib's absolute polar. A polytope is the convex hull of a Finset with the origin in its interior; $n = 0$ is allowed ($C = \{0\}$), and all targets hold there. Faces are Mathlib's exposed faces (IsExposed ℝ C F), which include $\emptyset$ and $C$, as the paper's counts do; for a polytope these are all faces. The factorization maps are total functions on $\mathbb{R}^n$ constrained only on extreme points. The nonnegative rank is valued in ℕ∞, the infimum of the empty family being $+\infty$; part (2) of the goal is stated for every finite value of the rank. Part (1) is stated for every antichain of faces, equivalent to the paper's "largest antichain". "Smallest $k$" is sInf of a set of naturals that is nonempty in each case (the set of $k$ with $p \le \binom{k}{\lfloor k/2\rfloor}$, and the set of $k$ admitting an embedding of the finite lattice $L(C)$).

The paper says "lattice embedding". Its proof of Theorem 4.11 constructs, and uses, only a map that preserves and reflects inclusion, and $\varphi(F) = \bigcup_{v \in F} A(v)$ need not preserve joins or meets; the formalization reads "lattice embedding" as an order embedding (Face C ↪o Finset (Fin k)) throughout.

Trivializing formalizations are ruled out: the rank is not a natural-number infimum (which would be $0$ when no factorization exists); faces are not arbitrary subsets of $C$; and an embedding is order-reflecting, not merely monotone (every poset maps monotonically into $2^{[0]}$).

Welcome contributions: a proof of milestone 1; a library of polytope facts (vertices are exposed points, faces are convex hulls of their vertices, finiteness of the face lattice, facets from the polar), which is reusable well beyond this mission; then Theorem 4.11 and the corollaries.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Math. Oper. Res. 38(2):248–264, 2013; arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• M. X. Goemans, Smallest compact formulation for the permutahedron, Math. Program. 153:5–11, 2015. https://doi.org/10.1007/s10107-014-0757-1
• S. Fiorini, V. Kaibel, K. Pashkovich, D. O. Theis, Combinatorial bounds on nonnegative rank and extended formulations, Discrete Math. 313(1):67–83, 2013; arXiv:1111.0444. https://arxiv.org/abs/1111.0444
• S. A. Vavasis, On the complexity of nonnegative matrix factorization, SIAM J. Optim. 20(3):1364–1377, 2009. https://doi.org/10.1137/070709967

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves $1 - 1/e$, a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$, and a randomized smooth local search achieves $2/5 - o(1)$. The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.

Timeline. Feige, Mirrokni and Vondrák: $1/4$, $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$, which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements and $f : 2^X \to \mathbb{R}$ a function with $f(S) \ge 0$ for all $S$ and

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \quad (S, T \subseteq X).$$

Write $OPT = \max_{S \subseteq X} f(S)$. The multilinear extension of $f$ is

$$F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{j \notin S} (1 - x_j),$$

the expected value of $f$ on a random set containing each $i$ independently with probability $x_i$.

For $A \subseteq X$ and $\delta \in [-1,1]$, the random set $\mathcal{R}(A,\delta)$ is sampled with bias $\delta$ based on $A$: each element of $A$ is included independently with probability $p = (1+\delta)/2$, each element of $B = X \setminus A$ with probability $q = (1-\delta)/2$. The potential is $\Phi(A) = \mathbf{E}[f(\mathcal{R}(A,\delta))]$ and the smoothed marginal value of $x$ is

$$\omega_{A,\delta}(x) = \mathbf{E}[f(\mathcal{R}(A,\delta) \cup \{x\})] - \mathbf{E}[f(\mathcal{R}(A,\delta) \setminus \{x\})].$$

Algorithm SLS starts from $A = \emptyset$. At each iteration it obtains estimates $\tilde\omega_{A,\delta}(x)$ within $\pm\frac{1}{n^2}OPT$ of $\omega_{A,\delta}(x)$. If some $x \notin A$ has $\tilde\omega_{A,\delta}(x) > \frac{2}{n^2}OPT$ it adds $x$; otherwise, if some $x \in A$ has $\tilde\omega_{A,\delta}(x) < -\frac{2}{n^2}OPT$ it removes $x$; otherwise it stops and returns a random set $\mathcal{R}(A, \delta')$.

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

With $\delta = 1/3$, and $\delta' = 1/3$ with probability $0.9$ or $\delta' = -1$ with probability $0.1$: for every run from $\emptyset$ whose estimates are all accurate and which has terminated at $A$,

$$\tfrac{9}{10}\,\mathbf{E}[f(\mathcal{R}(A,\tfrac13))] + \tfrac{1}{10}\,f(X \setminus A) \ge \Big(\frac{2}{5} - \frac{9}{5n}\Big) OPT,$$

and, for every $\delta \in (0,1]$, every run of $k$ iterations with accurate estimates has $k < n^2/\delta$ (fewer than $3n^2$ for $\delta = 1/3$).

Milestones, in attack order

• Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)g(\emptyset) + p\,g(A)$.
• Display (∗): for three independently sampled sets, $\mathbf{E}[f(A_1(p_1) \cup A_2(p_2) \cup A_3(p_3))] \ge \sum_{I \subseteq \{1,2,3\}} \prod_{i\in I} p_i \prod_{i \notin I}(1-p_i) f(\bigcup_{i \in I} A_i)$.
• The increment identity $\Phi(A \cup \{x\}) - \Phi(A) = \delta\,\omega_{A,\delta}(x)$ for $x \notin A$, and its removal counterpart.
• $0 \le \Phi(A) \le OPT$.
• The terminal upper estimates $\mathbf{E}[f(R \cup (B\cap C))],\ \mathbf{E}[f(R \cap (B \cup C))] \le \mathbf{E}[f(R)] + \frac{2}{n}OPT$.
• The two lower bounds in $27$ths on the same two expectations.
• The final chain $\mathbf{E}[f(R)] + \frac19 f(B) + \frac2n OPT \ge \frac49 OPT$.

Significance

The $2/5$ bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.

The result is proved in the paper; it has been superseded in ratio by later algorithms reaching $1/2$. To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the $o(1)$ as $\frac{9}{5n}$, "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$, which are averages over the random set, not for $f$ at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with $\delta = 1/3$ the $27$ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$. A different split or a different $\delta$ gives a different constant.

Formalization scope

The ground set is a Fintype X with decidable equality; sets are Finset X; $f$ is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: $f \ge 0$ (§3), value-oracle access (modelled by $f$ itself), $n = |X|$, and $n \ge 1$ (Nonempty X), so that $\frac{1}{n^2}$ and $\frac{9}{5n}$ are not Lean's junk value of division by zero. $OPT$ is Finset.sup' over all subsets, which has no junk value. Every expectation over independently sampled sets is an exact finite sum: the multilinear extension for $\mathcal{R}(A,\delta)$, and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry $0 \le p \le 1$.

The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from $\emptyset$, every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$"); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$, which equals $f(X \setminus A)$.

A statement "every $A$ satisfying the terminal conditions gives $2/5 - 9/(5n)$" would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at $\emptyset$, the thresholds, the step order, the accuracy of every estimate, termination and the $0.9/0.1$ mixture.

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$, and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• S. O. Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205
• G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6):1740–1766, 2011. https://doi.org/10.1137/080733991

Motivation

A Markov Decision Model (MDM) formalizes sequential decision-making under uncertainty: a controller observes the current state of a system, chooses an action, receives a reward, and the system moves to a new (random) state whose law depends on the current state and action. This framework underlies dynamic programming across operations research, economics, and engineering — inventory control, sequential portfolio choice, queueing control, and reinforcement learning are all instances of it. The finite-horizon theory developed here is the foundation on which every later chapter of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds, including the infinite-horizon, partially observed, and optimal-stopping variants treated later in the book.

The classical treatment of dynamic programming for finite state and action spaces goes back to Bellman (1957) and is standard textbook material (see e.g. Puterman, Markov Decision Processes, 1994). The generalization to Borel state and action spaces — needed as soon as a state variable is continuous, as in almost every financial application — requires genuine measure-theoretic care: suprema over an infinite (even uncountable) action set need not be attained, and the resulting value function need not be measurable. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete Time Case (1978) is the classical reference for this general theory; Bäuerle and Rieder's treatment isolates the exact abstract hypothesis — the Structure Assumption (SAN) below — under which the finite-horizon theory goes through cleanly, separating the recursive (Bellman) machinery from the case-by-case verification of when it applies.

Setting

A Markov Decision Model with planning horizon $N \in \mathbb{N}$ consists of a state space $E$ and action space $A$ (measurable spaces), and, for each stage $n = 0,\dots,N-1$: a measurable set $D_n \subseteq E \times A$ of admissible state-action pairs (containing the graph of some measurable selection $E \to A$); a stochastic transition kernel $Q_n(\cdot \mid x,a)$ giving the law of the next state; a measurable one-stage reward $r_n : D_n \to \mathbb{R}$; and a terminal reward $g_N : E \to \mathbb{R}$.

A decision rule at time $n$ is a measurable $f_n : E \to A$ with $f_n(x) \in D_n(x) := \{a : (x,a) \in D_n\}$ for every $x$; an $N$-stage policy $\pi = (f_0,\dots,f_{N-1})$ is a sequence of such rules. Given $\pi$ and an initial state $x$ at time $n$, the process evolves as a (non-stationary) Markov chain, and the value of $\pi$ is the expected total reward

$$V_n^\pi(x) := \mathbb{E}^\pi_{n,x}\!\left[\sum_{k=n}^{N-1} r_k\bigl(X_k, f_k(X_k)\bigr) + g_N(X_N)\right],$$

with value function $V_n(x) := \sup_\pi V_n^\pi(x)$, the best attainable expected reward. A policy is optimal if $V_0^\pi = V_0$. Write $\mathrm{IM}(E)$ for the measurable functions $E \to [-\infty,\infty)$ (never $+\infty$), and define, for $v \in \mathrm{IM}(E)$, the one-step operators $L_n v(x,a) := r_n(x,a) + \int v(x')\, Q_n(dx' \mid x,a)$, $T_n^f v(x) := L_n v(x, f(x))$, and $T_n v(x) := \sup_{a \in D_n(x)} L_n v(x,a)$. A decision rule $f$ is a maximizer of $v$ at time $n$ if $T_n^f v = T_n v$.

Formalization targets

Goal: Theorem 2.3.8 (the Structure Theorem)

Under the Structure Assumption (SAN) — the existence of sets $\mathrm{IM}_n \subseteq \mathrm{IM}(E)$, $\Delta_n \subseteq F_n$ with $g_N \in \mathrm{IM}_N$, $T_n$ mapping $\mathrm{IM}_{n+1}$ into $\mathrm{IM}_n$, and every $v \in \mathrm{IM}_{n+1}$ admitting a maximizer in $\Delta_n$ — the value function satisfies the Bellman equation $V_n = T_n V_{n+1}$ (with $V_n \in \mathrm{IM}_n$), and every sequence of maximizers of $V_1,\dots,V_N$ defines an optimal policy. This is the weakest level at which the theorem holds: it names an abstract structural hypothesis rather than a specific sufficient condition (e.g. compactness plus semicontinuity, treated in a later mission), so any future refinement of sufficient conditions for (SAN) leaves this statement untouched.

Significance

Reducing an $N$-stage optimization over an infinite-dimensional policy space to $N$ one-stage optimizations — literally the content of the Bellman equation — is what makes dynamic programming computationally and theoretically tractable at all. For finite state and action spaces this reduction is elementary (a supremum over a finite set is always attained); the content of the Structure Theorem is doing this correctly when $E$, $A$ are general Borel spaces, where existence of the supremum and of a measurable maximizing selection are not automatic and must be assumed abstractly.

Formalizing this theorem produces machine-checked statements of the finite-horizon Bellman equation and verification theorem in the generality actually used throughout the book's finance applications (wealth is real-valued, portfolios are vector-valued — never finite sets). The statement, proof, and every hypothesis are original to this textbook chapter; no formalized version of this general-Borel-space theory exists on the platform. The closest prior art, finite state-and-action-space Bellman equations and verification theorems (e.g. discounted infinite-horizon and stochastic-shortest-path theorems for finite MDPs), is a strictly weaker special case in which the Structure Assumption's existence-of-maximizer clause is automatic; this mission's goal is not restated as a reference to that prior art; the generalization is exactly the mission's content.

Difficulty

The obvious first attempt — prove $V_n = T_n V_{n+1}$ directly from the definitions of $V_n$ and $V_n^\pi$ — runs into two separate obstructions that (SAN) is built to bypass simultaneously. First, $\sup_\pi V_n^\pi(x)$ and $\sup_{a \in D_n(x)} L_n V_{n+1}(x,a)$ are a priori different suprema (over policies versus over actions), and showing they agree requires that the pointwise supremum over decision rules $f \in F_n$ of $L_n V_{n+1}(x, f(x))$ equals the supremum over bare actions $a \in D_n(x)$ — which needs a measurable selection achieving (or approaching) the action-wise optimum, not just its existence pointwise. Second, $V_{n+1}$ itself must be shown measurable — an a priori supremum of measurable functions over an uncountable index set (all policies) need not be measurable — before the integral $\int V_{n+1}\, dQ_n$ even makes sense. (SAN)'s three clauses are exactly what supplies both a well-behaved measurability class $\mathrm{IM}_n$ closed under $T_n$ and a measurable maximizing selection at every stage, letting a backward induction on $n$ establish both facts together.

Formalization scope

State and action spaces are arbitrary measurable spaces (MeasurableSpace E, MeasurableSpace A type classes), not restricted to Borel subsets of Polish spaces, since none of this mission's statements use topology. Time is indexed by ℕ rather than Fin N, with n < N as an explicit side condition throughout (documented in MODERATION_NOTES.md); this changes no content but avoids Fin-cast noise in the several backward recursions the chapter's operators require. Extended-real values (EReal) are used throughout for value functions, restricted by hypothesis to never equal $+\infty$, matching $\mathrm{IM}(E) := \{v : E \to [-\infty,\infty)\}$ exactly; a formalization using plain ℝ-valued value functions would be a strictly stronger — and unfaithful — claim, since it silently assumes no policy can drive the expected reward to $-\infty$.

The mission does not construct the canonical path measure on the full trajectory space via the Ionescu–Tulcea theorem; the value of a policy is instead built as an explicit backward accumulator recursion over the model's one-step kernels, which computes the same quantity by the tower property of conditional expectation. Definitions 2.1.1, 2.1.5, 2.2.2, 2.3.1, and 2.3.6 — the Markov Decision Model, (Markov and history-dependent) policies, and the operators — are restated from scratch in this mission's own namespace, since drafts in this series cannot import one another; later missions in the same series restate the same vocabulary independently. A trivializing formalization of the goal would state $V_n$ as an unspecified object merely postulated to satisfy the Bellman equation (Theorem 2.3.7's weaker claim) rather than as the supremum-over-policies value function fixed before the theorem — this mission states the latter.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
• K. Hinderer, Foundations of Non-stationary Dynamical Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994.

Motivation

Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds $C_0$ units of a perishable product (airline seats, hotel rooms, seasonal goods) and must choose prices over a finite selling horizon while demand is random and responds to price. The exactly optimal policy solves a stochastic dynamic program whose state is the remaining inventory, and it changes the price after every sale. In practice sellers often prefer a simpler rule, fixed in advance: solve the deterministic version of the problem, in which random demand is replaced by its mean, and charge the resulting prices whatever happens.

Gallego and van Ryzin (Management Science 1994) showed that in continuous time with Poisson demand this fixed-price heuristic is asymptotically optimal, and bounded its relative loss by the coefficient of variation of demand. Bitran and Caldentey's survey (MSOM 2003, §3.2.1) extends this bound to a discrete-time, periodic-review model with general demand distributions, as Proposition 8, proved in the paper's Appendix. The proof combines three ingredients: a Lagrangian duality argument showing that the deterministic problem is an upper bound on the optimal expected revenue, a sample-path comparison of lost sales, and a distribution-free moment bound of Gallego (1992) on $E[(X-C)^+]$.

Setting

A single product is sold over $N \ge 1$ periods $n = 1, \dots, N$ starting from inventory $C_0$. In period $n$ the seller charges a price $p \ge 0$, and the demand $D_n(p)$ is a nonnegative random variable with finite mean $E[D_n(p)]$, whose law may depend on $n$ and $p$ arbitrarily. With inventory $C$ the seller sells $\min\{D, C\}$ units; unmet demand is lost.

The optimal expected revenue $V_1(C_0)$ is defined by the Bellman recursion $V_{N+1} \equiv 0$,

$$V_n(C) = \sup_{p \ge 0} E\big[p\min\{D_n(p), C\} + V_{n+1}\big(C - \min\{D_n(p), C\}\big)\big].$$

The deterministic problem (32)–(33) is

$$V_1^{\det}(C_0) = \sup_{p \in [0,\infty)^N} \sum_{n=1}^N p_n E[D_n(p_n)] \quad \text{subject to} \quad \sum_{n=1}^N E[D_n(p_n)] \le C_0,$$

and $p^{\det}$ denotes an optimal solution. The deterministic-price heuristic charges $p^{\det}_n$ in period $n$ regardless of sales. Its period demands $D_n(p_n^{\det})$ are independent, $\mathscr{D}_n^{\det} = \sum_{i=1}^n D_i(p_i^{\det})$ is the cumulative demand, and its expected revenue is

$$V_1(p^{\det}, C_0) = \sum_{n=1}^N p_n^{\det} E\Big[D_n(p_n^{\det}) - \big(D_n(p_n^{\det}) - (C_0 - \mathscr{D}_{n-1}^{\det})^+\big)^+\Big].$$

With $\sigma_n^2 = \operatorname{Var}(\mathscr{D}_n^{\det})$, eq. (34) defines

$$\eta_n^{\det}(C_0) = \frac{\sqrt{\sigma_n^2 + (C_0 - E[\mathscr{D}_n^{\det}])^2} - (C_0 - E[\mathscr{D}_n^{\det}])}{2},$$

and $\nu(C_0) = \sigma_N / E[\mathscr{D}_N^{\det}]$ is the coefficient of variation of the total demand.

Formalization targets

Goal: Proposition 8, eq. (35)

Assume that $p \mapsto p\,E[D_n(p)]$ is concave and $p \mapsto E[D_n(p)]$ is convex on $[0,\infty)$ for each $n$, that some price $p^\infty \ge 0$ has $\sum_n E[D_n(p^\infty)] < C_0$, and that $p^{\det}$ is optimal for (32)–(33). Then

$$1 \ge \frac{V_1(p^{\det}, C_0)}{V_1(C_0)} \ge \frac{1}{V_1^{\det}(C_0)} \sum_{n=1}^N p_n^{\det} E[D_n(p_n^{\det})]\left(1 - \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}\right) \ge 1 - \max_n \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}.$$

The constants are the paper's, and the goal is the full chain.

Milestones

1. Gallego's bound (Appendix, (*)): for square-integrable $X$, $E[(X - C)^+] \le \frac12\big(\sqrt{\operatorname{Var}X + (C - EX)^2} - (C - EX)\big)$, which is at most $\frac12\sqrt{\operatorname{Var} X}$ when $EX \le C$.
2. Eq. (24): in one period, $E[p\min\{D(p), C\}] \le p\min\{E[D(p)], C\}$, so $V(C) \le V^{\det}(C)$.
3. Proposition 6, eq. (26): in one period, $V(C, p^{\det})/V(C) \ge 1 - \nu^{\det}/2$.
4. $V_1^{\det}$ is concave in the capacity (first sentence of the Appendix proof).
5. Proposition 8, first assertion: $V_1(C_0) \le V_1^{\det}(C_0)$.
6. The Appendix display bounding $V_1(p^{\det}, C_0)$ below by $\sum_n p_n^{\det}E[D_n](1 - E[(\mathscr{D}_n^{\det} - C_0)^+]/E[D_n])$.
7. Eq. (36), after the goal: if $E[D_n(p)] = T_n\lambda(p)$, one constant price solves (32)–(33) and $1 \ge V_1(p^{\det},C_0)/V_1(C_0) \ge 1 - \nu(C_0)/2$.

Significance

The result gives a guarantee for a pricing policy that needs no inventory tracking: its relative loss is controlled by the first two moments of cumulative demand, with no distributional assumption beyond finite variance. When demand grows while its coefficient of variation shrinks, as for sums of independent period demands, the guarantee tends to one, which is the discrete-time form of asymptotic optimality of fixed prices. The upper bound $V_1 \le V_1^{\det}$ is used throughout revenue management as the benchmark for heuristics (fluid or deterministic LP bounds).

The paper's proof is complete in the Appendix, and the mathematics is not in question beyond minor typos. None of it is machine-checked. A formal development adds a checked Bellman model of periodic-review pricing with general demand laws, a checked fluid upper bound for it, and a checked form of Gallego's moment bound, all reusable for other revenue-management statements. A related platform theorem, RevenueManagement.deterministic_upper_bound (mission The Theory and Practice of Revenue Management III), states the deterministic bound for a Bernoulli-arrival model with at most one sale per period; the model here is different (arbitrary demand laws, continuous inventory), and neither statement implies the other.

Difficulty

The upper bound $V_1(C_0) \le V_1^{\det}(C_0)$ is the hard part. The natural induction replaces $V_2$ by $V_2^{\det}$ and applies Jensen's inequality, but $V_2^{\det}(C)$ is $-\infty$ at capacities where the remaining deterministic problem is infeasible, while $V_2(C)$ stays nonnegative. The induction therefore fails as stated when mean demand never vanishes. The paper's argument also passes through the Lagrangian dual of (32)–(33), and strong duality for that program on $[0,\infty)^N$ under the Slater point $p^\infty$ is not available in Mathlib in this form.

The lower bound is less deep but technical: it needs the product law of the period demands, linearity of expectation for truncated sums, and variances of partial sums. Gallego's inequality is elementary once the right quadratic bound on $(x - C)^+$ is found, but it is not in Mathlib.

Formalization scope

• Periods are Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by $[0,\infty)$ with finite mean, required at every price (laws at negative prices never enter a statement).
• The Bellman value is computed in $[0,\infty]$ with the lower Lebesgue integral and ⨆ over $p \ge 0$, so no supremum takes a junk value; the paper's $V_n$ is valueToGo M (N - n + 1). Ratios use its real value.
• $V_1^{\det}$ is an EReal supremum over the feasible set ($-\infty$ if infeasible). In the goal $p^{\det}$ is an optimal solution, so $V_1^{\det}(C_0)$ is its objective value.
• The heuristic's demands are independent: the joint law is the product measure.
• Implicit hypotheses made explicit: "concave objective and convex feasible region" is read as concavity of $p\,E[D_n(p)]$ and convexity of $E[D_n(p)]$ on $[0,\infty)$, the latter making (33) convex for every capacity; existence of the optimal deterministic solution; finite variance and positive mean of each $D_n(p_n^{\det})$; and $V_1^{\det}(C_0) > 0$, without which the ratios are $0/0$.
• The typo $\mathscr{D}_n^{\det} := \sum_{i=1}^n D_n(p^{\det})$ on p. 221 is read as $\sum_{i=1}^n D_i(p_i^{\det})$.

Trivializing formalizations ruled out: $V_1$ is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; $\eta_n^{\det}$ is the expression (34), not a hypothesis-supplied bound on expected overflow; the goal does not assume strong duality or a Lagrange multiplier, since that is the proof's key step; independence is built into the joint law, not assumed as an inequality; variances are taken only under square integrability, since Mathlib's variance is $0$ for infinite variance.

Needed infrastructure: measurability of the Bellman integrand (monotonicity of $V_n$ in inventory), Jensen's inequality for $\min\{\cdot, C\}$ (ConcaveOn.le_map_integral), Lagrangian strong duality for a separable concave program with one convex constraint, marginals and variances of sums under Measure.pi, and Gallego's bound. The duality and moment results are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the upper bound, are welcome.

Selected references

• G. R. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–230, 2003. https://doi.org/10.1287/msom.5.3.203.16061
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11(1):55–60, 1992 (as cited in Bitran and Caldentey 2003).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993.

Motivation

Multistage stochastic linear programs model decisions taken in periods $t = 1, \dots, T$ while a random vector $\xi_t$ is revealed period by period: production and capacity planning, energy scheduling, asset–liability management. With finitely many scenarios the problem is one very large linear program with a tree structure, and decomposition methods solve it by passing information up and down the scenario tree instead of solving it whole. John R. Birge's Nested Decomposition for Stochastic Programming Algorithm (NDSPA), published in Operations Research in 1985 (DOI), is the multistage extension of the L-shaped method of Van Slyke and Wets (SIAM J. Appl. Math. 1969) and the ancestor of the nested Benders and stochastic dual dynamic programming codes in use today.

The paper reports a practical defect of the method: degeneracy leads to many repeated solutions of the same scenario problem (Remark 4, p. 996–997), an effect Abrahamson (1980) had observed for deterministic nested decomposition. Propositions 3 and 4 (p. 997) identify where the degeneracy comes from: cuts that bind at the ancestor force the descendant problems that produced them into degenerate bases. This mission formalizes those two propositions.

Setting

Fix a node of a finite scenario tree: scenario $j$ at period $t$, with decision $x \in \mathbb{R}^{n}$. Its ancestor's decision $x^{a}$ enters only through the right-hand side of its equality rows. After $r$ feasibility cuts and $s$ optimality cuts have been added, the node solves the scenario problem (7):

$$\min\ c^\top x + \theta \quad\text{s.t.}\quad A x = \xi + B x^{a},\quad D_l^\top x \ge d_l\ (l \le r),\quad E_l^\top x + \theta \ge e_l\ (l \le s),\quad x \ge 0,$$

over $x$ and a free scalar $\theta$, which stands in for the expected future cost. During NDSPA's forward pass the node also carries the restriction $\theta = 0$; a last-period node has no future cost and keeps that restriction.

A descendant problem (period $t+1$, scenario $j' \in J'$) has the same shape, with right-hand side $\xi_{j'} + B_{j'} x$ depending on the node's decision $x$. Two kinds of cut flow from descendants to the node:

• a feasibility cut arises when a descendant is infeasible at some $x^0$: a Farkas certificate $\lambda$ of that infeasibility, with parts $\pi, \rho, \sigma$ on the descendant's rows (7.2), (7.3), (7.4), yields the cut $D^\top x \ge d$ with $D = -\pi^\top B_{j'}$ and $d = \pi^\top \xi_{j'} + \rho^\top d_{j'} + \sigma^\top e_{j'}$;
• an optimality cut is built in NDSPA Step 3a from optimal dual vectors $\lambda_{j'}$ of all descendants at the current $\bar x$ and weights $p_{j'}$: $E = -\sum_{j'} p_{j'} \pi_{j'}^\top B_{j'}$ and $e = \sum_{j'} p_{j'} (\pi_{j'}^\top \xi_{j'} + \rho_{j'}^\top d_{j'} + \sigma_{j'}^\top e_{j'})$. It is added only if it cuts off the current point, the test (9): $\bar\theta < e - E^\top \bar x$.

A cut $E^\top x + \theta \ge e$ is valid when $e - E^\top x$ never exceeds the weighted sum of the descendants' objective values at feasible points, for any $x$. A basic solution of (7) is a point at which all equality rows hold and $n + 1$ linearly independent constraints are active; it is degenerate when more than $n + 1$ constraints are active.

Formalization targets

Goal: Proposition 4

Let two distinct valid optimality cuts $l_1, l_2$ bind at $(\bar x, \bar\theta)$. Let each descendant $j'$ have an optimal basic feasible solution $z_{j'}$ and an optimal dual vector $\lambda_{j'}$ at $\bar x$, and suppose the Step 3a cut built from these duals fails (9), so that $\bar\theta \ge e - E^\top \bar x$. Then

$$\exists\, j' \in J' : \ z_{j'} \text{ is a degenerate basic solution of the problem (7) of } j' \text{ at } \bar x .$$

Milestone: Proposition 3

If descendant $j'$ generates feasibility cut $l'$ of the node and that cut binds at $\bar x$, then

$$\text{every basic feasible solution of the problem (7) of } j' \text{ with } \bar x \text{ in (7.2) is degenerate.}$$

Significance

The result. The two propositions explain a failure mode that every nested-decomposition implementation meets. The backward pass of NDSPA stalls, adding no cut, at exactly the points where Proposition 4 applies, and the degenerate descendant bases it predicts are what make the same ancestor basis recur over many iterations. The analysis motivated the partitioning method of Section 3 of the paper and the intermediate problem of Birge (1980), and it is the reason later codes pay attention to the choice among multiple optimal duals.

Formalizing it. The paper states both propositions without proof and refers the proofs to Birge (1980), an unpublished technical report. A machine-checked proof makes the statements self-contained. It also pins down what they assume: which cuts are meant, which invariants of the algorithm they rely on, and which notion of degeneracy applies to a problem with a free variable and inequality cuts. The definition layer (scenario problems with their cut families, LP duals, Farkas certificates, the Step 3a cut) is reusable for any statement about nested Benders or L-shaped methods. The finite convergence of the nested method is the subject of a separate private formalization (Birge and Louveaux, Ch. 6, Thm. 1, StochasticProg.Multistage.thm1_finite_convergence), so this mission does not restate NDSPA's convergence.

Difficulty

The statements connect the geometry of the ancestor's value function to the combinatorics of descendant bases. For Proposition 4 the difficulty is that nothing in the hypotheses mentions the descendants' bases directly: they speak of two cuts at the ancestor and one failed test. The conclusion is a statement about the descendants' simplex bases, so the ancestor-level information has to be transported down to the descendant problems, where the relevant objects (optimal bases, optimal duals, optimal-value functions of the right-hand side) are not unique in exactly the degenerate case the proposition is about. Two hypotheses that look dispensable are not. Without distinctness a duplicated cut gives a counterexample. Without validity a cut that is not a lower bound can bind anywhere. For Proposition 3 the certificate must be the one that generated the cut; an arbitrary cut row that happens to bind says nothing about the descendant.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the variable of (7) is $z = (x, \theta) \in$ Fin (n+1) → ℝ with $\theta$ its last coordinate. The paper suppresses transposes; here they are explicit, and a row vector times a matrix ($\pi B$) is vecMul. Basic, basic feasible and degenerate solutions are the general-form notions of Bertsimas and Tsitsiklis (Defs. 2.9–2.10), reused from the public definition BasicSolution, applied to the whole constraint family of (7), the free $\theta$ included. A last-period node is represented with the restriction $\theta = 0$, which pairs one extra variable with one extra active equality and so preserves basicness and degeneracy.

Readings of informal words, each stated in the items:

• "generate a feasibility constraint": the Van Slyke–Wets construction from a Farkas certificate at an earlier input $x^0$, stated against the descendant's current constraint family;
• "binding for some solution": the row holds with equality at the point; feasibility or optimality of the point for the ancestor is not assumed, which strengthens both statements;
• "two constraints of type (7.4)": two distinct cuts, both valid, the invariants NDSPA maintains;
• "every set of optimal solutions … that produces $E$ and $e$": one optimal basic feasible solution and one optimal dual vector per descendant, the cut computed from those duals;
• "degenerate": general-form degeneracy, not the standard-form count of zero components.

Correction to the page. Step 3a prints $E = -\sum \pi B_t$ and $e = \sum \pi \xi$. The formalization completes $e$ with the terms $\rho^\top d + \sigma^\top e$ from the descendants' own cuts, without which the cut is not a valid lower bound when the descendants carry cuts. It also adds weights $p_{j'} > 0$; conditional probabilities are a special case, and $p \equiv 1$ is the printed sum. The data $A$, $B$ may differ between descendants, which is more general than the paper.

Proposition 3 is vacuous when the descendant is infeasible at $\bar x$; that is the paper's statement. No trivializing reading is available for the goal: the cuts are computed from certificates and duals inside the statement, never taken as arbitrary vectors, and a sorry-free local check confirms that all hypotheses of Proposition 4 hold together on a small instance. Propositions 1 and 2, NDSPA's convergence, the partitioning method of Section 3 and the computational study are out of scope. Contributions welcome: proofs of Propositions 3 and 4, and supporting lemmas on LP duality and basis stability over general-form constraint families.

Selected references

• J. R. Birge, Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs, Operations Research 33(5):989–1005, 1985. https://doi.org/10.1287/opre.33.5.989
• R. M. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
• J. R. Birge, Solution Methods for Stochastic Dynamic Linear Programs, Technical Report SOL 80-29, Stanford University, 1980.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Defs. 2.9–2.10).
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011 (nested L-shaped method for multistage problems). https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Many problems in signal processing, statistics and operations research ask to minimize a sum $\Theta = \Phi + \Psi$ of a nonsmooth convex term $\Phi$ (a constraint indicator, an $\ell^1$ penalty) and a smooth term $\Psi$. The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its classical convergence theory requires $\Psi$ to be convex and the step size to stay below $2/L_\Psi$, where $L_\Psi$ is the Lipschitz constant of $\nabla\Psi$.

Attouch, Peypouquet and Redont (authors' manuscript of SIAM J. Optim. 24 (2014)) derive an inertial forward-backward algorithm (IFB) as a time discretization of a second-order dissipative dynamical system with Hessian-driven damping. The added inertial terms cost essentially nothing to compute, yet they allow step sizes beyond $2/L_\Psi$ and a smooth part $\Psi$ that is not convex, provided the sum $\Theta$ is.

Timeline of the relevant results:

• Heavy-ball-with-friction methods, the inertial discretizations of $\ddot u + \alpha\dot u + \nabla\Phi(u) = 0$, were introduced by Polyak (1964) and developed by Alvarez and Attouch (2001) for proximal schemes.
• Hessian-driven damping for one potential: Alvarez, Attouch, Bolte and Redont (2002); for a nonsmooth potential plus a smooth one, the continuous dynamics underlying (IFB): Attouch, Maingé and Redont (2012).
• The discrete algorithm (IFB) and its weak convergence in Hilbert spaces: Attouch, Peypouquet and Redont (2014), the paper of this mission.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. Let $\Phi : H \to \mathbb R\cup\{+\infty\}$ and $\Psi : H \to \mathbb R$, and write $\Theta = \Phi + \Psi$ and $\mathcal S = \operatorname{Argmin}\Theta$. A vector $g$ is a subgradient of $\Phi$ at $u$, written $g \in \partial\Phi(u)$, if $\Phi(u) < +\infty$ and $\Phi(u) + \langle g, v - u\rangle \le \Phi(v)$ for all $v$.

Hypothesis H fixes positive constants $L_\Psi$, $a$, $b$ and a step size $\lambda$ with:

• $H_\Phi$: $\Phi$ is proper, lower semicontinuous and convex;
• $H_\Psi$: $\Psi$ is differentiable and $\nabla\Psi$ is $L_\Psi$-Lipschitz;
• $H_\lambda$: $0 < \lambda < \Lambda = \min\{1/a,\ 2(a+b)/(bL_\Psi)\}$;
• $H_\Theta$: $\Theta$ is convex and bounded from below.

Algorithm (IFB). From any $(u_0, y_0) \in H \times H$, compute for $k \ge 0$

$$0 \in \frac{u_{k+1}-u_k}{\lambda} + \partial\Phi(u_{k+1}) + a u_k - b y_k, \qquad 0 = \frac{y_{k+1}-y_k}{\lambda} + \nabla\Psi(u_{k+1}) - a u_{k+1} + b y_{k+1}.$$

A sequence $u_k$ converges weakly to $p$, written $u_k \rightharpoonup p$, if $\langle u_k, v\rangle \to \langle p, v\rangle$ for every $v \in H$. The analysis uses the velocity $\xi_k = u_k - u_{k-1}$, the energy $E_k = \Theta(u_k) + \gamma\|\xi_k\|^2$ with $\gamma = (1-a\lambda)/(2b\lambda^2)$, and two auxiliary real sequences $G_k(q)$ and $F_k(q)$, defined from $u$, $y$ and a reference point $q$ by (17) and (18) of the paper.

Formalization targets

Goal: Theorem 1

Under Hypothesis H, for every sequence generated by (IFB),

$$\lim_{k\to\infty}\Theta(u_k) = \inf\Theta;$$

if $\mathcal S \ne \emptyset$ and one of (i) $\mathcal S$ is a singleton, (ii) $\Phi$ is differentiable with weak-to-weak sequentially continuous gradient, (iii) $\nabla\Psi$ is weak-to-weak sequentially continuous, (iv) $\Psi$ is convex, holds, then

$$u_k \rightharpoonup p \quad\text{for some } p \in \mathcal S;$$

and if $\mathcal S = \emptyset$, then $\|u_k\| \to +\infty$.

Milestones

In the order of the paper's argument: Proposition 2 (energy decrease, $\sum\|\xi_k\|^2 < \infty$); Proposition 3 (the identity and inequality (19) for $F_k(q)$); Proposition 4 ($G_k(q)$ is bounded above for $q\in\operatorname{dom}\Phi$); the lower bound (28) on $F_k(q)$; Lemma 5 (a real-sequence lemma); Proposition 6 ($\Theta(u_k)\to\inf\Theta$, weak cluster points lie in $\mathcal S$); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of $(u_k)$ and convergence of $F_k(q)$ when $\mathcal S \ne\emptyset$).

Significance

The result gives convergence of a forward-backward type method under a step-size bound $\Lambda$ that can be made arbitrarily large by choosing $a$ small, and for a smooth term $\Psi$ that need not be convex. The special case $\Phi = \delta_C$ (indicator of a closed convex set) yields an inertial gradient-projection method, and the paper applies the theorem to feasibility problems, the CQ algorithm, Pareto fronts and $\ell^1$ signal recovery.

The theorem is proved in the paper; to our knowledge it is not formalized anywhere. A complete formalization would provide a machine-checked Liapunov analysis of an inertial proximal method in an infinite-dimensional Hilbert space, including the passage from a minimizing sequence to weak convergence. The milestones Proposition 2, 3 and 8 are energy estimates that also underlie other inertial and proximal schemes.

Difficulty

The energy $E_k$ controls the values $\Theta(u_k)$ and the velocities $\xi_k$, but not the iterates themselves. The first idea, proving that $\|u_k - q\|$ is nonincreasing for every $q \in \mathcal S$ (Fejér monotonicity, the standard route for the classical forward-backward method), does not come out of the energy estimates for (IFB): the inertial variable $y_k$ couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence $F_k(q)$, carries the auxiliary sum $G_k(q)$, whose upper bound already requires the full Hypothesis H. Because $H$ is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of $\Theta$, and the final step, uniqueness of the weak cluster point, needs a separate argument in each of the cases (i)–(iv) together with Opial's lemma, which is not in Mathlib.

Formalization scope

• $H$ is a general real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.
• $\Phi$ and $\Theta$ take values in EReal. Properness excludes $-\infty$. Convexity of an extended-valued function is convexity of its epigraph in $H\times\mathbb R$, because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires $\Phi(u) < +\infty$, so $\partial\Phi(u) = \emptyset$ off $\operatorname{dom}\Phi$.
• (IFB) is encoded as the subgradient inclusion, not through the proximity operator. Weak convergence is convergence of all inner products $\langle u_k, v\rangle$; weak cluster points are weak limits along strictly increasing subsequences.
• $L_\Psi > 0$ is assumed (harmless: a Lipschitz gradient is Lipschitz with every larger constant). The step size $\lambda$ is written lam.
• $\xi_k$, $z_k$, $E_k$, $G_k$, $F_k$ are defined on all natural indices, and each statement quantifies $k \ge 1$ (or $k \ge 2$ for $G_k$) as the paper does. Energies and values are never truncated to real numbers, so no statement becomes true through the convention EReal.toReal ⊤ = 0.
• Deviation from the printed text: Proposition 4 is printed under $H_\Phi$ and $H_\Psi$ only, but its proof invokes Proposition 2, which needs all of Hypothesis H, and the printed statement is false for step sizes above $\Lambda$ (e.g. $H=\mathbb R$, $\Phi = x^2/2$, $\Psi = 3x^2/2$, $a=2$, $b=0.02$, $\lambda = 10$). The milestone is stated under the full Hypothesis H.
• A formalization in which $\partial\Phi(u)$ is nonempty at points of infinite value, in which the energy is converted to a real number, or in which Hypothesis H cannot be satisfied, would make these statements trivial or vacuous, and is ruled out by the definitions above.

A complete development needs Opial's lemma, weak sequential compactness of bounded sets in Hilbert space, weak lower semicontinuity of lower semicontinuous convex functions, the descent lemma for functions with Lipschitz gradient, and monotonicity of the subdifferential. These are reusable well beyond this mission; contributions of any of them, and of the milestones in any order, are welcome.

Selected references

• H. Attouch, J. Peypouquet, P. Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, SIAM J. Optim. 24(1), 2014 (statements cited from the authors' manuscript of Aug 2013). https://doi.org/10.1137/130910294
• H. Attouch, P.-E. Maingé, P. Redont, A second-order differential system with Hessian-driven damping; application to non-elastic shock laws, Differential Equations and Applications 4(1), 2012. https://doi.org/10.7153/dea-04-02
• F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Analysis 9, 2001. https://doi.org/10.1023/A:1011253113155
• F. Alvarez, H. Attouch, J. Bolte, P. Redont, A second-order gradient-like dissipative dynamical system with Hessian-driven damping, J. Math. Pures Appl. 81(8), 2002. https://doi.org/10.1016/S0021-7824(01)01253-3
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0