Operations Research

Machine Learning Optimization Statistics·Captain: mikedeng1

Generalization Bounds in the Predict-then-Optimize Framework II: Margin-Based Generalization Bound for the SPO Loss under the Strength PropertyResearch Paper

Motivation

In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.

El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.

Setting

Decisions live in $\mathbb R^d$ with a norm $\|\cdot\|$ ; cost vectors are linear functionals with the dual norm $\|c\|_*=\max_{\|w\|\le1}c^\top w$ . The feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle $w^*$ maps each cost vector $c$ to some minimizer $w^*(c)\in\arg\min_{w\in S}c^\top w$ . The SPO loss of a prediction $\hat c$ against the realized cost $c$ is

\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c),

and the linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$ , with $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$ and $\rho_2(\mathcal C)=\sup_{c\in\mathcal C}\|c\|_2$ for the set $\mathcal C$ of possible true costs.

A cost vector is degenerate if $\min_{w\in S}\hat c^\top w$ has more than one optimal solution; $\mathcal C^\circ$ is the set of degenerate costs. The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$ . The region $S$ has the strength property with parameter $\mu>0$ if

\hat c^\top\big(w-w^*(\hat c)\big)\ge\frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all }w\in S\text{ and all }\hat c .

For $\gamma>0$ the $\gamma$ -margin SPO loss $\ell^\gamma_{\rm SPO}(\hat c,c)$ equals $\ell_{\rm SPO}(\hat c,c)$ when $\nu_S(\hat c)>\gamma$ and $\frac{\nu_S(\hat c)}{\gamma}\ell_{\rm SPO}(\hat c,c)+\big(1-\frac{\nu_S(\hat c)}{\gamma}\big)\omega_S(c)$ otherwise. It dominates the SPO loss.

Data $(x,c)$ are drawn from a distribution $\mathcal D$ on features $\mathcal X$ and costs in $\mathcal C$ , and $\mathcal H$ is a class of prediction functions $f:\mathcal X\to\mathbb R^d$ . The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$ and the empirical margin risk is $\hat R^\gamma_{\rm SPO}(f)=\frac1n\sum_i\ell^\gamma_{\rm SPO}(f(x_i),c_i)$ . The multivariate empirical Rademacher complexity is $\hat{\mathfrak R}^n(\mathcal H)=\mathbb E_{\boldsymbol\sigma}\big[\sup_{f\in\mathcal H}\frac1n\sum_i\boldsymbol\sigma_i^\top f(x_i)\big]$ with i.i.d. Rademacher vectors $\boldsymbol\sigma_i\in\{\pm1\}^d$ , and $\mathfrak R^n(\mathcal H)$ is its expectation over the sample.

Formalization targets

Goal: Theorem 4, second display (pp. 19–20)

In the $\ell_2$ set-up, under the strength property with $\mu>0$ and for fixed $\gamma>0$ , for every $\delta>0$ , with probability at least $1-\delta$ over an i.i.d. sample of size $n$ , for all $f\in\mathcal H$ :

R_{\rm SPO}(f)\le\hat R^\gamma_{\rm SPO}(f)+\Big(\frac{2\sqrt2\rho_2(\mathcal C)+2\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\mathfrak R^n(\mathcal H)+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .

Milestones

Theorem 3(a): $\|w^*(\hat c_1)-w^*(\hat c_2)\|\le\frac{\|\hat c_1-\hat c_2\|_*}{\mu\min\{\nu_S(\hat c_1),\nu_S(\hat c_2)\}}$ .
Theorem 3(b): the same Lipschitz-like bound for $\ell_{\rm SPO}(\cdot,c)$ , with an extra factor $\|c\|_*$ .
Theorem 3(c): $\ell^\gamma_{\rm SPO}(\cdot,c)$ is $\frac{\|c\|_*+\mu\,\omega_S(c)}{\gamma\mu}$ -Lipschitz for the dual norm.
Eq. (7) with $C=\sqrt2$ (Maurer's vector contraction inequality): for $L$ -Lipschitz $\Phi_i$ on Euclidean $\mathbb R^d$ ,

\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_i\sigma_i\Phi_i(f(x_i))\Big]\le\sqrt2L\,\hat{\mathfrak R}^n(\mathcal H).

Theorem 4, first display: for any fixed sample with costs in $\mathcal C$ ,

\hat{\mathfrak R}^n_{\gamma\rm SPO}(\mathcal H)\le\Big(\frac{\sqrt2\rho_2(\mathcal C)+\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\hat{\mathfrak R}^n(\mathcal H).

Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over $\gamma\in(0,\bar\gamma]$ , is not part of this mission.

Significance

The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of $\mathcal H$ itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions $p$ and $d$ (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where $\nu_S$ can also be computed. When most predictions stay far from degeneracy, $\hat R^\gamma_{\rm SPO}\approx\hat R_{\rm SPO}$ and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).

The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.

Difficulty

The SPO loss is discontinuous in $\hat c$ at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and $\mathcal H$ is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from $\mathcal C^\circ$ . Convexity and compactness of $S$ alone do not give that: for an $\ell_p$ ball with $2<p<\infty$ the strength property fails for every $\mu>0$ (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant $\sqrt2$ must not depend on the dimension $d$ . The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.

Formalization scope

The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the $\ell_2$ statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: $S$ nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and $\mu>0$ , $\gamma>0$ . The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads $1/0$ as $+\infty$ . Expectations over signs are finite averages over sign patterns. $\omega_S(\mathcal C)$ and $\rho_2(\mathcal C)$ are suprema over a nonempty bounded $\mathcal C$ containing the cost almost surely. "With probability at least $1-\delta$ " is the statement that the outer $\mathcal D^n$ -measure of the failure event is at most $\delta$ .

Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and $\hat{\mathfrak R}^n(\mathcal H)$ is integrable, since otherwise Lean's junk value $0$ would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses $f$ and $\ell_{\rm SPO}(f(x),c)$ measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton $S$ would make $\mathcal C^\circ$ empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.

A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.

Selected references

O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, Mathematics of Operations Research, 2023; preprint arXiv:1905.11488v3, 2022. https://arxiv.org/abs/1905.11488
A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, Algorithmic Learning Theory (ALT), 2016. https://arxiv.org/abs/1605.00251
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
V. Koltchinskii, D. Panchenko, Empirical Margin Distributions and Bounding the Generalization Error of Combined Classifiers, Annals of Statistics 30(1), 2002. https://doi.org/10.1214/aos/1015362183

9 thms3 active usersReviewed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Local Search Heuristics for k-Median and Facility Location Problems IV: Local Search with Multi-Copy Moves for Capacitated Facility Location Has Locality Gap 4Research Paper

Motivation

Facility location asks where to open service points (warehouses, plants, servers) and how to connect customers to them so that the total opening cost plus the total connection cost is minimum. In the capacitated version each facility can serve only a limited number of customers, which is the situation in most applications: a warehouse has a floor area, a server a bandwidth. The problem is NP-hard, and the algorithms used in practice for it are often simple local search heuristics: start from a solution and repeatedly apply a small change that lowers the cost, until no such change exists.

The quality of such a heuristic is measured by its locality gap: the largest possible ratio between the cost of a solution that no allowed change can improve and the cost of an optimum solution. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave locality-gap analyses for k-median, uncapacitated facility location, and the capacitated problem in which several copies of a facility may be opened. This mission formalizes their §5, the capacitated case.

Timeline (as surveyed on pp. 545–546 of the paper). For the variant 1-CFL, where at most one facility may be opened at each location, Korupolu, Plaxton and Rajaraman (1998) showed that local search with add, drop and swap moves has locality gap at most 8 when capacities are uniform; Chudak and Williamson (IPCO 1999) refined this to 6, and Pál, Tardos and Wexler gave a local search with gap 9 for nonuniform capacities. For ∞-CFL, the variant with copies studied here, the known algorithms were LP-based: a 3-approximation of Chudak and Shmoys (1999) for uniform capacities, a 4-approximation of Jain and Vazirani for nonuniform capacities, and a 2-approximation of Mahdian, Ye and Zhang. Arya et al. (2004) analysed local search for ∞-CFL with nonuniform capacities: with a new move that drops any set of open copies and opens several copies of one facility, the locality gap is at most 4 (Theorem 5.5), and scaling the facility costs gives $2 + \sqrt3 + \epsilon$ (p. 561). The tight example for uncapacitated facility location (§4.3) also shows a locally optimum solution of cost 3 times the optimum, so the locality gap of the procedure lies between 3 and 4; its exact value was left open (§6).

Setting

An instance consists of a finite set $C$ of clients, a set $F$ of facilities and a distance $c$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji}$ is the cost of serving client $j$ from facility $i$ . Every facility $i$ has an opening cost $f_i \ge 0$ and an integer capacity $u_i > 0$ . Any number of copies of a facility may be opened; each copy of $i$ costs $f_i$ and serves at most $u_i$ clients.

A solution $X$ opens a finite list of copies, copy $s$ being a copy of facility $\mathrm{loc}(s)$ , and assigns every client $j$ to a copy $\sigma(j)$ so that each copy $s$ serves at most $u_{\mathrm{loc}(s)}$ clients. Write $N_X(s)$ for the set of clients served by copy $s$ and $N_X(T)$ for the clients served by a set $T$ of copies. Its costs are

\mathrm{cost}_f(X) = \sum_s f_{\mathrm{loc}(s)}, \qquad \mathrm{cost}_s(X) = \sum_{j\in C} c_{j\,\mathrm{loc}(\sigma(j))}, \qquad \mathrm{cost}(X) = \mathrm{cost}_f(X) + \mathrm{cost}_s(X).

The neighbourhood (9) of a solution whose multiset of open facilities is $S$ consists of

$S + s'$ : one more copy of any facility $s'$ ;
$S - T + l\cdot\{s'\}$ : close any set $T$ of open copies and open $l \ge 1$ copies of a facility $s'$ , provided $l\,u_{s'} \ge |N_S(T)|$ .

$X$ is locally optimum if no neighbour, with any feasible assignment of the clients, has smaller cost.

Formalization targets

Goal: Theorem 5.5

For every instance with at least one client, every locally optimum solution $X$ and every solution $O$ ,

\mathrm{cost}(X) \le 4\,\mathrm{cost}(O).

Milestones

In the order the paper's proof uses them:

Lemma 5.1 (service cost): $\mathrm{cost}_s(X) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$ .
Lemma 5.2: for every set $U$ of copies of $X$ and every facility $s'$ ,

\left\lceil \frac{|N_X(U)|}{u_{s'}}\right\rceil f_{s'} + \sum_{s\in U} |N_X(s)|\, c_{ss'} \ge \sum_{s\in U} f_s .

Lemma 5.4: in the graph with arcs $v_s \to w_o$ of length $c_{so}$ and $w_o \to \mathrm{sink}$ of length $f_o/u_o$ , $|N_X(s)|$ units can be routed from every $v_s$ at cost at most $\mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$ .
Inequality (10): the shortest-path flow, with $T_o$ the copies routed through $w_o$ , satisfies $\sum_o\sum_{s\in T_o}|N_X(s)|(c_{so} + f_o/u_o) \le \mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$ .
Inequality (11): $\sum_o f_o + \sum_o \sum_{s\in T_o} |N_X(s)|(c_{so} + f_o/u_o) \ge \mathrm{cost}_f(X)$ .
Lemma 5.3 (facility cost): $\mathrm{cost}_f(X) \le 3\,\mathrm{cost}_f(O) + 2\,\mathrm{cost}_s(O)$ .

A companion item states the scaled bound of p. 561: a local optimum for facility costs $(\sqrt3 - 1) f$ has cost at most $(2 + \sqrt3)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 5.5 gives a constant locality gap for a local search procedure for capacitated facility location with copies and nonuniform capacities, a variant previously approached through LP-based algorithms; the drop-add move it analyses is the paper's new operation for this problem. The scaled bound $2 + \sqrt3 \approx 3.732$ gives an approximation algorithm once local search is run to approximate local optimality. The paper also shows (Figure 13, the procedure T-hunt) that the exponentially large neighbourhood can be searched with a knapsack oracle, so the analysis applies to an implementable algorithm.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a checked model of capacitated facility location with copies (solutions, costs, the multiset neighbourhood) and of the locality-gap argument. The per-copy model and the flow comparison of Lemma 5.4 are reusable for other capacitated location problems and for local search analyses that compare a local optimum with an optimum through a flow or a matching.

Difficulty

The obvious attempt imitates the uncapacitated analysis: close one copy of $X$ and send its clients to a nearby copy of $O$ . With capacities this fails, since that copy of $O$ may be too small to absorb them, and single-copy moves do not certify a constant bound. With the drop-add move a single copy of $O$ must be charged for a whole group of copies of $X$ , and the groups must be chosen so that the charges add up to a constant times $\mathrm{cost}(O)$ ; the rounding $\lceil |N_X(T)|/u_{s'}\rceil$ of the number of new copies costs an additional $\mathrm{cost}_f(O)$ that has to be absorbed as well.

Formalization scope

Solutions. A solution is a structure CFLSol Cl Fa u: a number n of open copies, a map loc : Fin n → Fa giving the facility of each copy, and an assignment σ : Cl → Fin n with the capacity constraint for every copy. Copies are separate indices because $N_S(s)$ is per copy. Its multiset of facilities is the image multiset of loc.
Costs. A solution's cost is computed under its own assignment. The paper's cost of a multiset is the minimum over feasible assignments. Because every neighbour is compared with every feasible assignment, and $O$ ranges over every assignment, the statements are equivalent to the paper's. The move with $T = \{s\}$ , $s' = \mathrm{loc}(s)$ , $l = 1$ makes every reassignment of $X$ 's clients a neighbour, so a locally optimum $X$ carries a minimum-cost assignment.
Neighbourhood. Local optimality ranges over the whole of (9): every $s'$ , every set $T$ of copies (including $\emptyset$ and all copies) and every $l \ge 1$ with $l u_{s'} \ge |N_X(T)|$ . It is not restricted to what the search procedure T-hunt examines.
Standing assumptions. Distances are nonnegative, symmetric and satisfy the triangle inequality on $C \cup F$ ; $d(x,x) = 0$ is not assumed. Capacities are natural numbers with $u_i > 0$ ; costs are real with $f_i \ge 0$ ; every client has unit demand. Ratios $f_o/u_o$ and the ceiling of Lemma 5.2 are computed in $\mathbb R$ .
Added hypothesis. The goal, Lemmas 5.2 and 5.3 and the companion assume at least one client. Without clients a single idle copy of a facility with $f = 1$ , $u = 1$ is locally optimum at cost 1 while the empty solution costs 0, so these statements fail. The paper's instances implicitly have clients.
No trivialization. $O$ is any solution, not a fixed optimum, and the bounds are multiplied out ( $\mathrm{cost}(X) \le 4\,\mathrm{cost}(O)$ , never a ratio). The empty solution is excluded only by the presence of a client, not by a default cost.
Out of scope. The procedure T-hunt and the knapsack oracle, running time, the $\epsilon$ of approximate local optimality, and arbitrary demands.

Contributions are welcome at every level: proofs of the milestones, alternative proofs of Lemma 5.4 or (10) (for instance through a matching argument instead of flows), and general infrastructure for multiset neighbourhoods and assignment problems.

Selected references

V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100

10 thms3 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Local Search Heuristics for k-Median and Facility Location Problems I: Single-Swap Local Search for k-Median Has Locality Gap 5Research Paper

Motivation

The k-median problem asks where to open $k$ facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.

Local search is among the most widely used heuristics for it: start from any $k$ facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with $k$ facilities. This mission formalizes that result.

Timeline of the relevant bounds:

Korupolu, Plaxton and Rajaraman (SODA 1998) analysed a local search for k-median that opens $k(1+\epsilon)$ facilities and costs at most $3 + 5/\epsilon$ times the optimum with $k$ facilities.
Charikar, Guha, Tardos and Shmoys (STOC 1999) gave the first constant-factor approximation for metric k-median, by LP rounding ( $6\tfrac23$ ).
Jain and Vazirani (J. ACM 2001) and Charikar and Guha (FOCS 1999) improved the constant with primal–dual methods to 6 and 4.
Arya et al. (STOC 2001; SIAM J. Comput. 2004) proved the locality gap 5 for single swaps and $3 + 2/p$ for swaps of $p$ facilities at a time, with matching examples.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. Write $c_{ji} = d(j,i)$ for the cost of serving client $j$ by facility $i$ .

For a nonempty set $S \subseteq F$ of open facilities every client is served by its nearest open facility, and the cost of $S$ is

\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.

The k-median problem asks for a set $S$ of at most $k$ facilities of minimum cost.

A swap $\langle s, s'\rangle$ closes a facility $s \in S$ and opens a facility $s' \notin S$ , giving $S - s + s' = (S \setminus \{s\}) \cup \{s'\}$ . The neighbourhood of $S$ is

\mathcal B(S) = \{ S - \{s\} + \{s'\} \mid s \in S,\ s' \notin S \},

and $S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$ . The local search starts from an arbitrary set of $k$ facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly $k$ facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.

The analysis uses the following notation. For a solution $A$ , let $\sigma_A$ assign each client to a nearest facility of $A$ , let $A_j = c_{j\sigma_A(j)}$ be the service cost of client $j$ , and let $N_A(a)$ be the set of clients served by $a \in A$ . For two solutions $S$ and $O$ put $N^o_s = N_O(o) \cap N_S(s)$ . A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$ ; $s$ is bad if it captures some $o \in O$ and good otherwise.

Formalization targets

Goal: Theorem 3.2

For every metric instance, every $k$ , every locally optimum set $S$ of exactly $k$ facilities and every nonempty set $O$ of at most $k$ facilities,

\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O).

The comparison solution $O$ is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.

Milestones, in the order the proof uses them

A facility $o$ is captured by at most one facility of $S$ (remark after Definition 3.1).
Property 3.1: for each $o$ there is a bijection $\pi$ of $N_O(o)$ with $\pi(N^o_s) \cap N^o_s = \emptyset$ whenever $s$ does not capture $o$ .
When $|S| = |O|$ there are $|O|$ swaps $\langle s, o\rangle$ , one for each $o \in O$ , such that no facility capturing two or more facilities of $O$ is used, every good facility is used at most twice, and a used $s$ captures no $o' \ne o$ .
Inequality (2): for a locally optimum $S$ and such a swap $\langle s, o\rangle$ ,

\sum_{j \in N_O(o)} (O_j - S_j) + \sum_{\substack{j \in N_S(s)\\ j \notin N_O(o)}} \bigl(O_j + O_{\pi(j)} + S_{\pi(j)} - S_j\bigr) \ge 0.

Significance

Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of $p \ge 1$ facilities, where the bound $3 + 2/p$ is 5 for $p = 1$ . Combined with the standard device of accepting only swaps that improve the cost by a factor $1 - \epsilon/Q$ , it yields a polynomial-time $5/(1-\epsilon)$ -approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping $\pi$ ) are the reusable part.

The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.

Difficulty

The obvious argument adds up the inequalities $\mathrm{cost}(S - s + o) \ge \mathrm{cost}(S)$ over a pairing of $S$ with $O$ , rerouting the clients of the closed facility $s$ to the nearest remaining facility. This fails when a single facility of $S$ serves most clients of several facilities of $O$ : closing it leaves those clients with no nearby open facility, and no bound in terms of $\mathrm{cost}(O)$ follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when $S$ and $O$ share facilities.

Formalization scope

Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and $d(x,x) = 0$ is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes $S$ nonempty with S.card = k, which is the paper's $k \ge 1$ . Local optimality quantifies over every swap $\langle s, s'\rangle$ with $s \in S$ and $s' \notin S$ , exactly the neighbourhood $\mathcal B(S)$ of Theorem 3.2, and not only over the swaps with $s' \in O$ that the proof uses. The inequality is stated multiplied out, $\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O)$ , so it is meaningful when $\mathrm{cost}(O) = 0$ .

The milestones quantify over nearest-facility assignments $\sigma_S$ , $\sigma_O$ with arbitrary ties. Capture is stated in integers as $|N_O(o)| < 2|N^o_s|$ . The bijection $\pi$ of $N_O(o)$ is a permutation of all clients fixing every client outside $N_O(o)$ ; in inequality (2) it is a single permutation preserving every $N_O(o)$ . Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.

A formalization in which local optimality ranges over the swaps $\langle s, o\rangle$ , $o \in O$ , only, or in which $|O| = |S|$ or $O$ optimal is assumed, or in which the cost of the empty set is $0$ , is a different statement and is ruled out.

A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping $\pi$ are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently of the goal.

Selected references

V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
K. Jain, V. V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

8 thms3 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Jointly Constrained Biconvex Programming II: The Convex-Envelope Branch-and-Bound Algorithm Converges to a Global SolutionResearch Paper

Motivation

Bilinear programs, which minimize an objective containing a term $x^\top y$ over constraints on $x$ and $y$ , model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term $x^\top y$ is not convex, so such problems can have local minima that are not global. For example, $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$ . When $x$ and $y$ are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple $x$ and $y$ , this property is lost.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.

Timeline:

1969, Falk and Soland: a branch-and-bound scheme for separable nonconvex programs using convex envelopes, the pattern this algorithm follows.
1976, McCormick: convex underestimators of factorable functions, including the envelope of $xy$ on a rectangle.
1983, Al-Khayyal and Falk: the envelope of $xy$ over a rectangle (Theorem 2), the branch-and-bound algorithm for jointly constrained biconvex programs, and a proof of its convergence.

Setting

Fix $n \ge 1$ and a box $\Omega = \{(x,y) \in \mathbb{R}^n \times \mathbb{R}^n : l \le x \le L,\ m \le y \le M\}$ with coordinate rectangles $\Omega_i = [l_i, L_i] \times [m_i, M_i]$ . Problem $\mathcal P$ is

\min\ \varphi(x,y) = f(x) + x^\top y + g(y) \quad \text{subject to } (x,y) \in S \cap \Omega,

with $f$ , $g$ convex (and continuous) on their boxes, $S$ closed and convex, and $S \cap \Omega \neq \emptyset$ . Its optimal value is $v^*$ .

The convex envelope $\mathrm{Vex}_B\, h$ of a function $h$ over a set $B$ is the pointwise supremum of all convex functions that underestimate $h$ on $B$ . For a box $B$ , the node function $\psi^B(x,y) = f(x) + \mathrm{Vex}_B\, x^\top y + g(y)$ is convex and lies below $\varphi$ on $B$ . The subproblem at node $B$ , minimizing $\psi^B$ over $S \cap B$ , is a convex program.

A run of the algorithm is a sequence of stages. Stage $0$ has the single open node $\Omega$ . At stage $k$ the Best Bound Rule selects an open node $B_k$ whose subproblem value is least, and the stage point $(x^k, y^k)$ is its subproblem solution. The best lower bound is $v_b^k = \psi^{B_k}(x^k, y^k)$ and the best upper bound is $V_b^k = \min_{l \le k} \varphi(x^l, y^l)$ . The selected node is then split. The algorithm picks the coordinate $I$ with the largest gap $x^k_i y^k_i - \mathrm{Vex}_{(B_k)_i}\, x_i y_i$ and replaces the rectangle $(B_k)_I$ by the four subrectangles cut out by the point $(x^k_I, y^k_I)$ (Figure 1 of the paper). All other rectangles are kept. The stage function $\psi^k$ assigns to each point of $\Omega$ the least node value $\psi^B$ among the open boxes containing it.

Formalization targets

Goal: convergence to a global solution

For every run,

\text{every accumulation point } (\bar x, \bar y) \text{ of } (x^k, y^k) \text{ solves } \mathcal P, \qquad \lim_k v_b^k = v^* = \lim_k V_b^k .

Milestones

In attack order:

Theorem 2: $\mathrm{Vex}_\Omega\, xy = \max\{mx + ly - lm,\ Mx + Ly - LM\}$ on a rectangle.
Theorem 3: the envelope is exact on the rectangle's boundary.
The Corollary, in two parts:
- separability, $\mathrm{Vex}_\Omega\, x^\top y = \sum_i \mathrm{Vex}_{\Omega_i}\, x_i y_i$ ;
- exactness at points whose every coordinate pair lies on $\partial\Omega_i$ .
Along runs: $\psi^k \le \psi^{k+1} \le \varphi$ on $\Omega$ .
The bound chain $v_b^1 \le v_b^2 \le \cdots \le v^* \le \cdots \le V_b^2 \le V_b^1$ .
Termination when $v_b^k = V_b^k$ .
The gradient bound $\gamma_i$ .
The equicontinuity estimate $\|z - w\| < \varepsilon/(n\gamma) \Rightarrow |\mathrm{Vex}_B\, x^\top y(z) - \mathrm{Vex}_B\, x^\top y(w)| < \varepsilon$ within every sub-box $B$ .
The limit identity: along a convergent subsequence of stage points, $v_b^{k_t} \to \varphi(\bar x, \bar y)$ .

Theorem 4 of the paper, on the envelope of $\sum f_i(x_i) + x^\top y + \sum g_i(y_i)$ with concave $f_i, g_i$ , is included as a further target.

Significance

The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.

As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.

Difficulty

The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.

Formalization scope

Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from $0$ and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on $\mathbb{R}^{2n}$ is written out explicitly.

Hypotheses and corrections relative to the page:

Continuity of $f$ and $g$ on their boxes is added; the paper uses it without stating it. $n > 0$ is assumed. The box form of convexity (p. 276) is used.
Corollary, second clause (p. 276): "for all $(x,y) \in \partial\Omega$ " is false for $n \ge 2$ (take $\Omega_1 = \Omega_2 = [0,2]^2$ , $x = y = (0,1)$ ). It is stated for points with every $(x_i, y_i) \in \partial\Omega_i$ .
Well-definedness of the stage function (p. 277) is false from stage 3 on. Two open boxes can share a point at which their node functions differ, and the stage function then jumps. It is not a target. The stage function takes the minimum over the open boxes containing a point, and the continuity asserted on p. 279 is not formalized. The piecewise convexity asserted there is formalized as convexity of each open node function on its box.
Equicontinuity (p. 282): the display $|H_i^{kj}(x_i,y_i) - H_i^{kj}(u_i,v_i)| \le |x_i y_i - u_i v_i|$ is false, and so is equicontinuity of the stage functions on all of $\Omega$ . The estimate is stated within each sub-box, with the paper's $\delta = \varepsilon/(n\gamma)$ .

Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.

Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.

Selected references

F. A. Al-Khayyal and J. E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
J. E. Falk and R. M. Soland, An Algorithm for Separable Nonconvex Programming Problems, Management Science 15(9):550–569, 1969. https://doi.org/10.1287/mnsc.15.9.550
G. P. McCormick, Computability of Global Solutions to Factorable Nonconvex Programs: Part I — Convex Underestimating Problems, Mathematical Programming 10:147–175, 1976. https://doi.org/10.1007/BF01580665
H. Konno, Bilinear Programming: Part II. Applications of Bilinear Programming, Technical Report 71-10, Operations Research House, Stanford University, 1971 (reference [10] of Al-Khayyal and Falk; no online copy known). https://doi.org/10.1287/moor.8.2.273

16 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Jointly Constrained Biconvex Programming I: A Biconcave Function Attains Its Minimum on the BoundaryResearch Paper

Motivation

The bilinear program

\min_{(x,y)} \; c^T x + x^T A y + d^T y \quad \text{subject to} \quad x \in X,\ y \in Y,

with $X \subseteq \mathbb{R}^p$ and $Y \subseteq \mathbb{R}^q$ polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on $x$ and on $y$ are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of $X \times Y$ (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set $S$ of pairs $(x, y)$ , so that constraints may couple $x$ and $y$ . They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.

Setting

Write points of $\mathbb{R}^p \times \mathbb{R}^q$ as $(x, y)$ , and let $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ be a nonempty compact set. No convexity of $S$ is assumed. Let $\varphi : \mathbb{R}^p \times \mathbb{R}^q \to \mathbb{R}$ be continuous on $S$ .

The function $\varphi$ is biconcave over $S$ (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside $S$ : for every fixed $y$ , the map $x \mapsto \varphi(x, y)$ is concave on every convex set $C$ with $C \times \{y\} \subseteq S$ ; and for every fixed $x$ , the map $y \mapsto \varphi(x, y)$ is concave on every convex set $D$ with $\{x\} \times D \subseteq S$ . Equivalently, $\varphi$ is concave along every segment of $S$ that is parallel to the $x$ -block or to the $y$ -block. A bilinear objective $f(x) + x^T y + g(y)$ with $f$ and $g$ concave is biconcave; joint concavity of $\varphi$ is not required.

The boundary $\partial S$ is the topological frontier of $S$ in $\mathbb{R}^p \times \mathbb{R}^q$ : the closure of $S$ minus its interior. A solution of $\min\{\varphi(x,y) : (x,y) \in S\}$ is a point $z \in S$ with $\varphi(z) \le \varphi(w)$ for all $w \in S$ (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is $d\big((x,y),(x',y')\big) = \sqrt{\|x-x'\|^2 + \|y-y'\|^2}$ .

Formalization targets

Goal: Theorem 1 (p. 274)

If $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ ( $p + q \ge 1$ ) is nonempty and compact, and $\varphi$ is continuous on $S$ and biconcave over $S$ , then

\exists\, z^* \in \partial S \quad \text{with} \quad \varphi(z^*) = \min\{\varphi(x, y) : (x, y) \in S\}.

The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on $\partial S$ (a constant $\varphi$ is a counterexample to that).

Milestones

Proof of Theorem 1, p. 274. If $(\bar x, \bar y) \in \operatorname{int} S$ and $(x^*, y^*) \in \partial S$ is a nearest boundary point in Euclidean distance $d^*$ , then the closed Euclidean ball of radius $d^*$ about $(\bar x, \bar y)$ lies in $S$ , and with $(s,t) = 2(\bar x, \bar y) - (x^*, y^*)$ the points $(s,t)$ , $(x^*, t)$ and $(s, y^*)$ are feasible.
Proof of Theorem 1, p. 275, first display. For $\varphi$ biconcave over $S$ and segments $[x^*, s] \times \{\tfrac12 y^* + \tfrac12 t\}$ , $\{x^*\} \times [y^*, t]$ , $\{s\} \times [y^*, t]$ inside $S$ ,

\varphi\big(\tfrac12(x^*,y^*) + \tfrac12(s,t)\big) \ge \tfrac12\varphi(x^*, \tfrac12y^*+\tfrac12t) + \tfrac12\varphi(s, \tfrac12y^*+\tfrac12t) \ge \tfrac14\big[\varphi(x^*,y^*)+\varphi(x^*,t)+\varphi(s,y^*)+\varphi(s,t)\big].

Example, p. 274. The program $\min\{-x + xy - y : -6x + 8y \le 3,\ 3x - y \le 3,\ 0 \le x, y \le 5\}$ has the solution $(7/6, 1/2)$ , which is not an extreme point of the feasible region, and no extreme point is a solution.
Example, p. 274. $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$ , the first of which is not global.

Significance

Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to $\partial S$ , and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.

The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.

Difficulty

The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. $S$ need not be convex, so it has no useful extreme-point structure, and $\varphi$ is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.

What remains is local geometry around an interior minimizer: one must find points of $S$ around it at which biconcavity can be applied in both blocks, and control their membership in $S$ without convexity. The feasibility of the mixed points $(x^*, t)$ and $(s, y^*)$ , which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.

Formalization scope

Points are pairs in EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.
The theorem is the "more general context" of p. 274, independent of the paper's Problem 𝒫: the standing assumptions (a)–(c) of p. 274 (convex $f$ , $g$ ; closed convex $S$ ; a box $\Omega$ ) do not enter.
Hypotheses of the goal: IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on $S$ ), and BiconcaveOn S φ. One hypothesis is added: $0 < p + q$ . For $p = q = 0$ the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.
Biconcavity is read over $S$ : concavity on every convex subset of each section of $S$ . Assuming instead concavity of each partial function on the whole space would be a stronger hypothesis and a weaker theorem.
Trivializing formalizations ruled out: the statement assumes neither joint concavity of $\varphi$ nor convexity of $S$ (either would reduce it to the Bauer principle), and it covers sets with nonempty interior; the case of empty interior, where $\partial S = S$ , is included but is not the only case.
Corrected misprint (milestone 3): the paper prints the solution of example 3 as $(7/16, 1/2)$ . That point has objective value $-23/32$ , while the feasible vertex $(1,0)$ has value $-1$ . On the edge $3x - y = 3$ the objective equals $3x^2 - 7x + 3$ , minimized at $x = 7/6$ , value $-13/12$ , the global minimum. The Lean states the corrected point $(7/6, 1/2)$ ; the milestone text is kept verbatim.
In milestone 4, "local solution" is IsLocalMinOn relative to the box, and non-globality of $(-1, 3)$ records the paper's word "proper".
Infrastructure needed: nearest boundary points of compact sets (Mathlib has IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.

Selected references

Faiz A. Al-Khayyal and James E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
James E. Falk, A Linear Max-Min Problem, Mathematical Programming 5:169–188, 1973. https://doi.org/10.1007/BF01580119
Hiroshi Konno, A Cutting Plane Algorithm for Solving Bilinear Programs, Mathematical Programming 11:14–27, 1976. https://doi.org/10.1007/BF01580367
Olvi L. Mangasarian, Equilibrium Points of Bimatrix Games, Journal of the Society for Industrial and Applied Mathematics 12(4):778–780, 1964. https://doi.org/10.1137/0112064
Heinz Bauer, Minimalstellen von Funktionen und Extremalpunkte, Archiv der Mathematik 9:389–393, 1958. https://doi.org/10.1007/BF01900582

7 thms3 active usersReviewed

Completed

Bandit Algorithms Optimization Probability+1·Captain: naimengye

Multi-armed Bandit Allocation Indices VI: Bandit Sampling Processes, Favourable Priors and Invariance of the IndexTextbook

Motivation

The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target $T$ (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives $\nu(\bar x, n) = \bar x + \nu(0, n)$ , a scale parameter gives $\nu(\bar x, n) = \bar x\,\nu(1, n)$ , and for target processes the target can be absorbed into the state, $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$ . These identities are what make the tables of Chapter 8 one-dimensional.

Setting

A sampling model consists of a likelihood $f(\cdot \mid \theta)$ , a family of priors $\pi(\cdot \mid p)$ on the parameter indexed by the parameters $p$ of a conjugate family, and the Bayes update $p \mapsto p_x$ of those parameters after observing $x$ ; the family is conjugate if the posterior of $\pi(\cdot \mid p)$ given $X = x$ is $\pi(\cdot \mid p_x)$ . The predictive distribution is $f(\cdot \mid p) = \int f(\cdot \mid \theta)\pi(d\theta \mid p)$ . The reward process moves from $p$ to $p_x$ with $x \sim f(\cdot \mid p)$ and earns $r(p) = \int x f(x \mid p)dx$ . The target process with target $T$ moves to the completion state $C$ if $x \ge T$ and to $p_x$ otherwise, earning the current probability of success $r(p) = f([T, \infty) \mid p)$ , and $0$ in $C$ . A state $p$ is favourable if $r(p_{x_1 \cdots x_m}) \le r(p)$ for every finite sequence of observations $x_i < T$ . For the invariance theorems the parameters are $(\bar x, n)$ with the update $((n\bar x + x)/(n+1), n+1)$ ; $\mu$ is a location parameter of the likelihood if $f(\cdot \mid \mu + c)$ is $f(\cdot \mid \mu)$ shifted by $c$ , and $\bar x$ is a location parameter of the prior family if $\pi(\cdot \mid \bar x + c, n)$ is $\pi(\cdot \mid \bar x, n)$ shifted by $c$ ; scale parameters are defined with $x \mapsto bx$ , $b > 0$ . The Gittins index is that of the Bandit Algorithms model on these chains.

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

If $\mu$ is a location parameter of a reward process with a conjugate prior family in which $\bar x$ is a location parameter and the parameters update as the sample mean and count, then for every $n > 0$

r(\bar x + c, n) = r(\bar x, n) + c \quad\text{and}\quad \nu(\bar x, n) = \bar x + \nu(0, n),

under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.

Milestones

Proposition 7.4 (favourable state: $\nu = r$ ); Example 7.5 (Bernoulli target process, $\nu(\alpha, \beta) = \alpha/(\alpha + \beta)$ ); Example 7.6 (normal target process with known variance, $\nu(\bar x, n) = \Phi(\bar x (1 + n^{-1})^{-1/2})$ for $\bar x \ge 0$ ); Theorem 7.11 (scale parameter: $\nu(\bar x, n) = \bar x\,\nu(1, n)$ ); Theorem 7.17 (target process with a location parameter: $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$ ).

Significance

Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of $n$ alone and that of the exponential process as a function of $n$ and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.

None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.

Difficulty

The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by $c$ times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most $r(p)$ , which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of $\bar x_m (1 + 1/(n+m))^{-1/2}$ in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that $\alpha/(\alpha + \beta + m)$ decreases.

Formalization scope

The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters $(\bar x, n)$ it is required on $n > 0$ only (IsConjugateOn): a proper prior has $n > 0$ , and conjugacy at every $(\bar x, n) \in \mathbb{R}^2$ is impossible with a location parameter, since at $n = -1$ the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: $a \in (0, 1)$ ; integrable observations and L&S Assumption 35.6 for the reward processes; $n > 0$ for the invariance theorems and $\bar x > 0$ for the scale theorem; $\alpha, \beta > 0$ ; $\bar x \ge 0$ and $n > 0$ for the normal example.

Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.

Selected references

J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 7. doi:10.1002/9780470980033
J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 1974.
D. M. Jones, Search Procedures for Industrial Chemical Research, PhD thesis, University of Wales, 1975.
H. Raiffa, R. Schlaifer, Applied Statistical Decision Theory, Harvard University Press, 1961.
T. S. Ferguson, Mathematical Statistics: A Decision Theoretic Approach, Academic Press, 1967.
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 34–35. doi:10.1017/9781108571401

9 thms3 active usersReviewed

Completed

Bandit Algorithms Dynamic Programming Optimization+1·Captain: naimengye

Multi-armed Bandit Allocation Indices V: Restless Bandits, Indexability and Whittle Indices for Monotone ModelsTextbook

Motivation

Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and $m$ of $n$ must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$ , the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.

Setting

A restless bandit is a Markov decision process with two actions, active ( $u = 1$ ) and passive ( $u = 0$ ), each with its own transition kernel and reward. Under a deterministic stationary Markov policy $g$ with passive subsidy $W$ the reward in state $x$ is $r(x, g(x)) + W(1 - g(x))$ , and the average reward from $x$ is the Cesàro limit of the expected rewards. The optimal average reward $g(W)$ is the supremum over such policies and initial states; a policy is optimal if it attains $g(W)$ from every initial state; $E_0(W)$ is the set of states in which some optimal policy is passive; the bandit is indexable if $E_0(W)$ is nondecreasing in $W$ ; and $W(x) = \inf\{W : x \in E_0(W)\}$ .

The spinning plates asset lives on $\{1, \dots, k\}$ : active moves $x \to x + 1$ at rate $\lambda(x)$ , passive moves $x \to x - 1$ at rate $\mu(x)$ , $\lambda(k) = \mu(1) = 0$ , and $r(x)$ is earned under both actions, $r$ increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy $(y)$ is passive exactly on $\{x \ge y\}$ ; under it the asset alternates between $y - 1$ and $y$ , spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$ , so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$ , and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$ . The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$ , passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$ , and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$ .

Formalization targets

Goal: Theorem 6.4

For the spinning plates asset: (i) if $\phi$ is strictly decreasing over the thresholds $1 \le y \le k + 1$ , the asset is indexable; (ii) if additionally $W^*$ is strictly decreasing over the states, the Whittle index is

W(x) = W^*(x) = \frac{R(x+1) - R(x)}{\phi(x) - \phi(x+1)}, \qquad 1 \le x \le k.

Milestones

Eqs. (6.9)–(6.10): the monotone policy $(y)$ earns $W\phi(y) + R(y)$ from every initial state and $g(W) = \max_y [W\phi(y) + R(y)]$ , because a monotone policy always achieves $g(W)$ ; Theorem 6.5, the same two statements for the vigour bandit with $\psi$ increasing and $W^{**}$ increasing.

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.

None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.

Difficulty

The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$ , so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as $\{0,1\}$ -strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$ . Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.

Formalization scope

Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$ , $\nu(1) = \rho(k) = 0$ , rates in $[0, 1]$ , and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ and positive interior rates, which Theorem 6.4's hypothesis (i) implies.

Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary $\{0,1\}$ -policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 6. doi:10.1002/9780470980033
P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25(A), 1988. doi:10.2307/3214163
R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. doi:10.2307/3214547
K. D. Glazebrook, C. Kirkbride, D. Ruiz-Hernandez, Spinning plates and squad systems: policies for bi-directional restless bandits, Advances in Applied Probability 38(1), 2006. doi:10.1239/aap/1143936141
J. Niño-Mora, Restless bandits, partial conservation laws and indexability, Advances in Applied Probability 33(1), 2001. doi:10.1017/S0001867800010661
C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queueing network control, Mathematics of Operations Research 24(2), 1999. doi:10.1287/moor.24.2.293

7 thms3 active usersReviewed

Completed

Bandit Algorithms Linear Optimization Optimization+1·Captain: naimengye

Multi-armed Bandit Allocation Indices IV: The Achievable Region, Generalized Conservation Laws and the Adaptive Greedy AlgorithmTextbook

Motivation

Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.

Setting

There are $N$ job types $E = \{1, \dots, N\}$ . A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$ , a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$ , positive on $S$ and zero off it, such that for every policy

\sum_{i \in S} A_i^S x_i^\pi \ge b(S) \quad (S \subseteq E), \qquad \sum_{i \in E} A_i^E x_i^\pi = b(E),

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$ . GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$ , sets $\bar y_E$ to the maximum, removes $i_N$ , and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$ ; its outputs are the order $i_1, \dots, i_N$ , the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$ .

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$ , $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$ , and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$ , namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$ .

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$ : the achievable region is the polytope

P(A, b) = \Big\{x \in \mathbb{R}_+^N : \sum_{i \in S} A_i^S x_i \ge b(S),\ S \subset E,\ \sum_{i \in E} A_i^E x_i = b(E)\Big\};

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$ ); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.

Significance

Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.

None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from $S$ , and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$ ; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of $b(S)$ requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets $\{i_1, \dots, i_{k-2}\}$ , which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$ ; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$ , which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$ . Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.

Selected references

J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Bandit Algorithms Machine Learning+1·Captain: naimengye

Introduction to Multi-Armed Bandits XI: Bandits and Agents, Incentivized Exploration via Hidden ExplorationTextbook

Motivation

A recommendation system learns from the users it serves: the diner who tries a restaurant produces the review the next diner reads. Each user would rather exploit what is already known than explore for the benefit of those who come later, so a population of self-interested agents under-explores, and an alternative that looks bad on sparse early evidence may never be tried again even when it is the best. Chapter 11 of Slivkins, Introduction to Multi-Armed Bandits (arXiv:1904.07272), treats incentivized exploration: a principal who cannot force the agents but can recommend, and who, because it aggregates what earlier agents observed, knows more than any one of them. The question is whether recommendations alone can induce enough exploration to learn as fast as an ordinary bandit algorithm. The model is that of Kremer, Mansour and Perry (JPE 2014) and the results are those of Mansour, Slivkins and Syrgkanis (EC 2015, Operations Research 2020), specialized to two arms; the single-round problem is Bayesian persuasion in the sense of Kamenica and Gentzkow (AER 2011).

Setting

There are $K$ arms and $T$ rounds. A mean reward vector $\mu \in [0,1]^K$ is drawn from a known prior $P$ , and each pull of arm $a$ yields a reward drawn from a known family $D_{\mu_a}$ with mean $\mu_a$ . In round $t$ the principal recommends an arm $\mathrm{rec}_t$ ; agent $t$ , who knows the prior, the family, the algorithm and the round but not the past, sees only $\mathrm{rec}_t$ , chooses $a_t$ , collects $r_t \sim D_{\mu_{a_t}}$ and leaves; the principal observes $(a_t, r_t)$ . The chapter works with two arms, ordered so that the prior means satisfy $\mu^0_1 \ge \mu^0_2$ , with a prior of finite support and finitely many reward values.

An algorithm is Bayesian incentive-compatible (BIC, Definition 11.4) if following its recommendation is in every agent's interest given what the agent knows: for every round $t$ and arms $a \ne a'$ with $\Pr[\mathrm{rec}_t = a, E_{t-1}] > 0$ ,

\mathbb{E}[\mu_a - \mu_{a'} \mid \mathrm{rec}_t = a,\ E_{t-1}] \ge 0, \tag{11.1}

where $E_{t-1}$ is the event that all previous agents complied. A BIC algorithm is then an ordinary bandit algorithm whose recommendations are followed, and the run has the law of the Bayesian bandit of Chapter 3. Two contrasting policies frame the chapter. GREEDY reveals the history and lets agents exploit, $a_t \in \arg\max_a \mathbb{E}[\mu_a \mid H_t]$ (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal $\mathrm{sig}$ , with probability $\varepsilon$ it recommends a target arm $a_{\mathrm{trg}}(\mathrm{sig})$ , otherwise the arm maximizing $\mathbb{E}[\mu_a \mid \mathrm{sig}]$ , ties to arm 1. Its posterior gap is $G = \mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{sig}]$ . RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm $\mathrm{ALG}$ as the target: $N_0$ initial rounds recommend arm 1; afterwards, with probability $\varepsilon$ the round is an exploration round in which $\mathrm{ALG}$ chooses (and is fed the reward), and otherwise the exploitation branch recommends $\min\arg\max_a \mathbb{E}[\mu_a \mid S_t]$ , where $S_t$ is the data of all exploration rounds so far (11.10). The quantity that governs everything is $G_{1,n} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,n}]$ (11.11), the posterior gap after $n$ samples of arm 1, and Property (11.12), that $\Pr[G_{1,n} > 0] > 0$ for some $n$ : arm 2 can appear better after enough samples of arm 1.

Formalization targets

Goal: Theorem 11.15

RepeatedHE with exploration probability $\varepsilon > 0$ and $N_0$ initial samples of arm 1 is BIC as long as

\varepsilon < \tfrac13\,\mathbb{E}\big[G \cdot \mathbf 1\{G > 0\}\big], \qquad G = G_{N_0+1} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,N_0}],

for any bandit algorithm $\mathrm{ALG}$ and any horizon. The threshold depends on the prior alone.

Milestones

Theorem 11.7 (GREEDY never chooses arm 2 with probability at least $\mu^0_1 - \mu^0_2$ ) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$ ) with Claim 11.12 (the arm-2 side of the constraint suffices); Corollary 11.14 (RepeatedHE is BIC under the round-by-round condition); Theorem 11.19 (without Property (11.12) no BIC algorithm ever plays arm 2, ties to arm 1).

Significance

The results say when exploration can be incentivized at all and how. Theorem 11.7 shows that revealing everything is not a solution: the greedy dynamics gets stuck on arm 1 with a probability that does not shrink with $T$ , and Corollary 11.8 turns that into $\Omega(T)$ Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with $\mathrm{ALG}$ arbitrary, at a per-round rate $\varepsilon$ fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers $\mathrm{ALG}$ 's regret to RepeatedHE up to the prior-dependent factors $N_0$ and $1/\varepsilon$ , so $\tilde O(\sqrt T)$ regret is attainable subject to incentives. Theorem 11.19 closes the picture: Property (11.12) is necessary as well as sufficient. Together they characterize which priors admit incentivized exploration and give an algorithm that works for all of them.

Nothing of this is machine-checked. The mission adds to the Bayesian layer of mission III (prior, posterior by Bayes' rule, Bayesian regret) the BIC constraint on a joint law, GREEDY as a policy, the single-round HiddenExploration on an abstract finite signal, and the law of RepeatedHE; all of it is reusable for the $K$ -arm and the "explore all explorable arms" extensions of the literature review.

Difficulty

Theorem 11.7 is a martingale argument: the posterior gap along the history is a Doob martingale, the first round in which arm 2 is chosen is a bounded stopping time, and optional stopping gives $\mathbb{E}[Z_\tau] = \mu^0_1 - \mu^0_2$ ; all of this has to be set up on the joint law of $(\mu, H_T)$ of mission III, where the posterior is defined by Bayes' rule and the identification with a conditional expectation is itself a theorem (posterior_eq_condProb). Lemma 11.10 is the heart of the chapter and is not a computation about $\mathrm{rec}$ : it works with $F(E) = \mathbb{E}[G\mathbf 1_E]$ , splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when $G > 0$ , and closes with $F(G > 0) + F(G < 0) = \mathbb{E}[\mu_2 - \mu_1] \le 0$ ; the only place where the analysis uses that both branches are functions of the signal is the step $\mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{rec} = 2] = \mathbb{E}[G \mid \mathrm{rec} = 2]$ , and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal $S_t$ , where $\mathrm{ALG}$ 's choice is a randomized function of $S_t$ , and then the monotonicity of $\mathbb{E}[G_t\mathbf 1\{G_t > 0\}]$ in $t$ , a two-line consequence of $S_{t+1}$ determining $S_t$ that presupposes the posterior given $S_t$ is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on $\mu$ given that data. Corollary 11.8 needs the independence of the event " $\mu_1 < 1 - 2\alpha$ and arm 2 is never chosen" from $\mu_2$ . Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.

Formalization scope

Arms are Fin 2, the book's arm 1 being index 0; rounds are Fin T. The prior is a probability measure on mean vectors supported on a finite set $F \subseteq [0,1]^2$ , with $\mu^0_1 \ge \mu^0_2$ as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean $\nu$ for $\nu \in [0,1]$ ). BIC is defined on a joint law of $(\mu, \text{record})$ of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event $E_{t-1}$ of (11.1) is the sure event of that law, which is the standard reading of "the agents believe all previous agents complied". For a bandit policy the law is mission III's jointMeasure. Conditional expectations are written as finite sums over $F$ , so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk $0$ that never enters a theorem. GREEDY allows arbitrary tie-breaking; HiddenExploration's exploitation branch breaks ties toward arm 1 as Algorithm 11.1 does; the tie convention of Theorem 11.19 is the strict form of BIC for arm 2. The law of RepeatedHE is an explicit finitely supported measure, $\mu$ and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the $\varepsilon$ -coin, $\mathrm{ALG}$ 's kernel on its own history, or the exploitation arm, then $D_{\mu_{a_t}}$ ); it is written this way because $\mathrm{ALG}$ is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$ (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.

Trivializations are excluded: $\varepsilon > 0$ throughout; the BIC condition is asserted only where the recommendation has positive probability, and the sums in it are over the finite support, so an unsatisfiable hypothesis cannot hide in a measure-zero set. Welcome contributions: the optional-stopping argument on jointMeasure, the identification of explPostMean with the conditional expectation given the exploration data, the Bayes-rule algebra behind Lemma 11.10, and the counting lemmas on heRecords.

Selected references

A. Slivkins, Introduction to Multi-Armed Bandits, Foundations and Trends in Machine Learning 12(1-2), 2019, Chapter 11. arXiv:1904.07272, doi:10.1561/2200000068
I. Kremer, Y. Mansour, M. Perry, Implementing the "Wisdom of the Crowd", Journal of Political Economy 122(5), 2014. doi:10.1086/676597
Y. Mansour, A. Slivkins, V. Syrgkanis, Bayesian Incentive-Compatible Bandit Exploration, Operations Research 68(4), 2020 (EC 2015). doi:10.1287/opre.2019.1919
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. doi:10.1257/aer.101.6.2590
M. Sellke, A. Slivkins, The Price of Incentivizing Exploration: A Characterization via Thompson Sampling and Sample Complexity, Operations Research 71(5), 2023. doi:10.1287/opre.2022.2401

10 thms3 active usersReviewed

Completed

Mechanism Design·Captain: naimengye

The Theory and Practice of Revenue Management IV: AuctionsTextbook

Why a reserve price, and why it does not matter which auction

Airlines selling last seats, Priceline's name-your-own-price, procurement of supply contracts: Chapter 6 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) treats auctions as pricing mechanisms and asks what revenue they earn and how to design them. Its centre is Myerson's (1981) theory for independent private values: whatever the mechanism, so long as bidders with higher valuations are more likely to win and the lowest type gains nothing, the firm's expected revenue is the expected virtual value $\sum_i J(v_i) y_i(v)$ of the winners, with $J(v) = v - (1 - F(v))/f(v)$ (Theorem 6.1, the revenue equivalence theorem). Maximizing that expression pointwise gives the optimal auction: the standard first- or second-price auction with a reserve price $v^*$ at the zero of $J$ (Theorem 6.2). This mission formalizes the second-price form of Theorem 6.2 as its goal, with the dominant-strategy and first-price equilibria of the informal analysis, Theorem 6.1, the optimal allocation and Proposition 6.1 on list prices as supporting results.

Setting

$N$ customers have i.i.d. valuations on $[0, \bar v]$ with a continuously differentiable, strictly increasing distribution $F$ and positive density $f$ (PrivateValues, IsRegular); the joint law is the product measure (joint). A direct-revelation mechanism (Mechanism) maps reported valuations to allocations $y_i(v) \in \{0, 1\}$ , at most $C$ units in total, and payments $p_i(v)$ . For a report $w$ by customer $i$ , $P_i(w)$ is the win probability, $R_i(w)$ the expected payment and $S_i(w) = w P_i(w) - R_i(w)$ the surplus (winProb, expPayment, expSurplus); incentive compatibility, $S_i(w) \ge w P_i(w') - R_i(w')$ , is the equilibrium condition of the direct mechanism (IsIncentiveCompatible). The chapter's mechanisms are the $C$ -unit second-price auction with reserve price $r$ (secondPriceReserve: the $C$ highest valuations above $r$ win and pay the larger of $r$ and the highest losing valuation), the list-price mechanism for $N \le C$ (listPrice), and the single-unit first-price auction with its equilibrium bid $b^*(v) = v - \int_0^v P(s)\,ds / P(v)$ , $P = F^{N-1}$ (firstPriceBid).

Formalization targets

Goal: Theorem 6.2

With $J$ strictly increasing (Assumption 7.2) and $v^*$ its zero, the $C$ -unit second-price auction with reserve price $v^*$ is a feasible, incentive-compatible mechanism with monotone allocations and zero surplus at zero, and its expected revenue is at least that of every such mechanism: reserve_price_auction_optimal.

Supporting targets

Bidding one's valuation is dominant in the second-price auction (Sect. 6.2.2.1); the bid (6.4) solves the first-order condition (6.3), is a symmetric equilibrium of the first-price auction and shades below the valuation (Sect. 6.2.2.2); Theorem 6.1, revenue equals expected virtual surplus and each expected payment is $w P_i(w) - \int_0^w P_i$ ; the pointwise optimal allocation of Sect. 6.2.5; and Proposition 6.1, a list price at $v^*$ is optimal when $N \le C$ .

Proposition 6.2 (asymptotic optimality of list prices, a law-of-large-numbers statement about scaled auctions), the first-price form of Theorem 6.2 with its equilibrium (6.9) stated without proof, and the dynamic, replenishment and network auctions of Sects. 6.3-6.5 (Propositions 6.3-6.11, from Vulcano, van Ryzin and Maglaras and from Cooper and Menich) are not targets of this mission.

Significance

Theorem 6.1 is the tool that lets revenue be computed from allocations alone, which is why the first- and second-price auctions of Examples 6.1-6.3 earn the same $(N-1)/(N+1)$ and why any dynamic pricing scheme that ends with the same winners earns the same as the optimal auction (Sect. 6.2.6.3). Theorem 6.2 says a firm with private-value customers cannot do better than a standard auction with the right reserve price, and Proposition 6.1 that with enough capacity a list price already does it: auctions are a small-numbers phenomenon. These are the foundations on which the chapter's dynamic auctions and the list-price comparisons of Sects. 6.3-6.4 rest, and Myerson's optimal auction has no machine-checked proof in its multi-unit form.

Difficulty

Theorem 6.1 is an envelope argument in measure-theoretic clothing: incentive compatibility gives the two-sided inequalities of Appendix 6.A, monotonicity of $P_i$ makes $S_i$ convex with derivative $P_i$ almost everywhere, so $S_i(w) = \int_0^w P_i$ , and then an integration by parts against the density converts $\int (w P_i(w) - S_i(w)) f(w)\,dw$ into $\int J(w) P_i(w) f(w)\,dw$ ; the win probabilities are integrals over a product measure with one coordinate replaced, and Fubini is needed to return to $\mathbb E[J(v_i) y_i(v)]$ . The goal then needs the reserve-price auction shown incentive compatible (a dominant-strategy argument on the threshold payment), measurable, monotone and with zero surplus at zero, and the pointwise optimal allocation integrated. The first-price item is calculus on an interval integral with a vanishing denominator at $0$ and a monotone comparative-statics argument for the equilibrium inequality.

Formalization scope

Mechanisms are direct-revelation mechanisms on $[0, \bar v]^N$ , as the book reduces to in Sect. 6.2.3.1; expectations over the other customers are integrals over the joint law with customer $i$ 's coordinate overwritten by the report. Payments are assumed bounded on reports in $[0, \bar v]^N$ (not on all of $\mathbb R^N$ , where the second-price payment is unbounded) and the rules measurable. Ties in the second-price auction are broken by index, a null event, and when every customer wins the losing supremum is $0$ so the winner pays the reserve. Theorem 6.2 is stated for the second-price auction; the first-price version with reserve price, whose equilibrium (6.9) the book asserts without proof, is left out and noted. Optimality is over mechanisms satisfying conditions (i) and (ii) of Theorem 6.1 and incentive compatibility, which is the class the book compares against. The virtual value's zero $v^*$ is a parameter with $J(v^*) = 0$ rather than the maximum of (6.8), which under strict monotonicity is the same point.

Selected references

K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 6. https://doi.org/10.1007/b139000
R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
J. G. Riley and W. F. Samuelson, Optimal auctions, American Economic Review 71(3), 1981. https://www.jstor.org/stable/1802786
P. Klemperer, Auction theory: a guide to the literature, Journal of Economic Surveys 13(3), 1999. https://doi.org/10.1111/1467-6419.00083
W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. Maskin and J. Riley, Optimal multi-unit auctions, in The Economics of Missing Markets, Information, and Games, Oxford University Press, 1989.

7 thms3 active usersReviewed

Completed

Optimization Probability·Captain: naimengye

Inventory Control VIII: The Clark-Scarf Decomposition for a Serial SystemTextbook

Safety stock in a chain

Chapter 10 of Axsäter's Inventory Control turns to reorder points and safety stocks in multi-echelon systems, where the installations cannot be treated separately: a large stock downstream lets an upstream site run lean, and a long upstream lead-time argues for stock at the top. The best-known exact technique for serial systems is the decomposition of Clark and Scarf (1960), which the book presents in the infinite-horizon form of Federgruen and Zipkin (1984). It is also where the echelon stock measure comes from. The section's argument is short and self-contained, and its conclusion is a complete description of the optimal policy for a two-level serial system: order-up-to levels at both installations, one of them a newsboy solution, the other the minimizer of a convex function in which upstream shortages appear as an induced cost. It is the capstone of Chapter 10.

Setting

Installation 1 faces normally distributed period demand with mean $\mu$ and standard deviation $\sigma$ , independent across periods, so the demand over $n$ periods, $D(n)$ , is normal with mean $n\mu$ and standard deviation $\sqrt n\,\sigma$ . Installation 1 replenishes from installation 2 with lead-time $L_1$ periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time $L_2$ . Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs $e_1, e_2 \ge 0$ , so the installation holding costs are $h_1 = e_1 + e_2$ and $h_2 = e_2$ , and a shortage cost $b_1$ at installation 1; there are no ordering costs. Events in a period occur in the order: installation 2 orders, its delivery arrives, installation 1 orders, its delivery arrives, demand, cost evaluation.

Consider an arbitrary period $t$ . After ordering, installation 2 has an echelon inventory position $y_2$ , and by the standard argument its echelon stock in period $t + L_2$ is $y_2 - D(L_2)$ . Installation 1 then orders, realizing an echelon position $y_1$ that cannot exceed what is available: $y_1 \le y_2 - D(L_2)$ (Eq. 10.1). Its inventory level after the demand in period $t + L_2 + L_1$ is $y_1 - D(L_1+1)$ . The expected period costs are $C_2 = h_2\,\mathbb{E}(y_2 - D(L_2) - y_1)$ at installation 2 and $C_1 = h_1\,\mathbb{E}(y_1 - D(L_1+1))^{+} + b_1\,\mathbb{E}(y_1 - D(L_1+1))^{-}$ at installation 1, and the book reallocates the term $-h_2y_1$ to obtain

\tilde C_2(y_2) = h_2(y_2 - \mu_2'), \qquad \tilde C_1(y_1) = e_1y_1 - h_1\mu_1'' + (h_1 + b_1)\,\mathbb{E}\big(y_1 - D(L_1+1)\big)^{-},

with $\mu_2' = L_2\mu$ and $\mu_1'' = (L_1+1)\mu$ . As a function of a free $\hat y_1$ , $\tilde C_1$ is the newsboy-type function $\hat C_1$ of Eq. (10.6), minimized at the level $S_1 = \hat y_1^{*}$ given by the fractile equation (10.8). Passing everything available up to $S_1$ to installation 1, $y_1 = \min\{S_1, y_2 - D(L_2)\}$ , gives the total cost $\hat C_2(y_2)$ of Eq. (10.9), whose minimizer $S_2 = y_2^{*}$ is the order-up-to level of installation 2.

Formalization targets

Goal — the decomposition

With $S_1$ from (10.8) and $S_2$ a minimizer of $\hat C_2$ : for every $y_2$ and every allocation rule $a$ with $a(u) \le y_2 - u$ and finite expected cost,

\hat C_2(S_2) \;\le\; \mathbb{E}\big[\tilde C_2(y_2) + \tilde C_1(a(D(L_2)))\big],

and the order-up-to policy $(S_1, S_2)$ attains $\hat C_2(S_2)$ .

Supporting targets

Eq. (10.3), the stage-1 period cost through the expected backorders; the reallocation (10.4)-(10.5), which leaves the total unchanged; the closed form (10.6) of $\hat C_1$ through the loss function $G$ ; the convexity of $\hat C_1$ , its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that $\min\{S_1, y_2 - u\}$ is the cheapest feasible $y_1$ ; the identity (10.9); and the convexity of $\hat C_2$ (Problem 10.1) with the existence of its minimizer when $e_2 > 0$ .

Significance

The result itself. The decomposition reduces a two-dimensional stochastic control problem to two one-dimensional convex problems solved in sequence, from downstream to upstream, and it identifies the optimal policy class. The downstream level $S_1$ is a newsboy solution with overage cost $e_1$ , the value added, and underage cost $e_2 + b_1$ , and it is independent of the upstream installation altogether; the upstream level $S_2$ sees the downstream installation only through the induced shortage cost, the last term of (10.9). The book notes the extensions the argument admits, to more echelons, to batch ordering at the top, and, via Rosling's equivalence, to assembly systems, and its Sect. 10.1.2 adapts it, now only approximately, to distribution systems under the balance assumption. Example 10.1 shows the typical outcome: the optimal average stock at the upstream installation is slightly negative.

Formalizing it. The section's mathematics is a chain of expectations under Gaussian laws and two convexity arguments. Formalizing it fixes what "optimal" means, a per-period comparison against every allocation rule, and separates the two convexity claims the book makes in one clause each. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise allocation rule and the newsboy fractile are the same arguments as in the newsboy mission. The two places where work is needed are the identity (10.9), an expectation of a piecewise function split at $u = y_2 - S_1$ , and the convexity of $\hat C_2$ , which requires seeing that $x \mapsto \hat C_1(\min\{S_1, x\})$ is convex precisely because $S_1$ is a minimizer of the convex $\hat C_1$ (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of $D(L_2)$ , which needs the integrability of the linearly growing $\hat C_1$ . Existence of $S_2$ then follows from the growth of $\hat C_2$ at both ends, which comes from the asymptotics of the loss function: $G(z) \to 0$ as $z \to \infty$ and $G(z) + z \to 0$ as $z \to -\infty$ .

Formalization scope

$D(n)$ is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy mission, so the loss function $G$ and its closed form are reused as references. The costs are parametrized by $e_1, e_2, b_1$ with $h_1 = e_1 + e_2$ and $h_2 = e_2$ written out; $\tilde C_1$ , $\tilde C_2$ , the pre-reallocation period cost and $\hat C_2$ are Bochner integrals against these laws. Every statement assumes $\sigma > 0$ ; the goal and the convexity statements assume $e_1, e_2 \ge 0$ and $b_1 > 0$ , the book's cost signs. $L_2 = 0$ is allowed and makes $D(L_2)$ a point mass, which is the setting of the book's Problem 10.2.

$S_1$ enters as any solution of the fractile equation (10.8) and $S_2$ as any minimizer of $\hat C_2$ ; the other items show that both exist when $e_1, e_2 > 0$ . When $e_1 = 0$ the fractile is $1$ , no $S_1$ exists, and the goal is vacuous, which is faithful: the book observes that then $S_1 \to \infty$ and installation 2 never carries stock. Symmetrically, when $e_2 = 0$ and $L_2 \ge 1$ , $\hat C_2$ decreases towards its infimum without attaining it, so no $S_2$ exists and the goal is again vacuous: with free upstream holding the optimal $y_2$ is unbounded. Allocation rules are arbitrary functions of the realized $D(L_2)$ with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be $0$ and could undercut $\hat C_2(S_2)$ , which is negative in Example 10.1's stage-1 term.

What is not modelled is the infinite-horizon dynamic problem: the book's optimality claim is made period by period, and the passage to the stationary policy rests on the remark that the outside supplier has infinite supply, so the same $y_2$ can be chosen in every period. The definitions are reusable for the three-echelon extension and for the distribution system of Sect. 10.1.2; contributions formalizing Problem 10.2 ( $L_2 = 0$ ) as a first step are welcome.

Selected references

Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sect. 10.1.1. DOI 10.1007/978-3-319-15729-0
Andrew J. Clark and Herbert Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4), 1960, pp. 475-490. DOI 10.1287/mnsc.6.4.475
Awi Federgruen and Paul Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4), 1984, pp. 818-836. DOI 10.1287/opre.32.4.818
Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4), 1989, pp. 565-579. DOI 10.1287/opre.37.4.565
Geert-Jan van Houtum, Karl Inderfurth and Willem H. M. Zijm, Materials Coordination in Stochastic Multi-Echelon Systems, European Journal of Operational Research 95(1), 1996, pp. 1-23. DOI 10.1016/0377-2217(96)00080-8

10 thms3 active usersReviewed

Completed

Combinatorics·Captain: naimengye

Fundamentals of Supply Chain Theory VI: Pooling and FlexibilityTextbook

Pooling as a design principle

A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.

Setting

Risk pooling. $N$ distribution centers face normally distributed per-period demands $D_i \sim N(\mu_i, \sigma_i^2)$ with correlation coefficients $\rho_{ij}$ , and each runs a base-stock policy with holding cost $h$ and backorder cost $p$ per unit per period, so its optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over base-stock levels $S$ of $\mathbb{E}[h(S - D)^+ + p(D - S)^+]$ . Merging the centers gives one facing the total demand, normal with mean $\sum_i \mu_i$ and variance $\sigma_0^2 = \sum_i \sum_j \sigma_i \sigma_j \rho_{ij}$ (pooledVariance).

Transshipments. Two retailers $i, j$ with base-stock levels $S_i, S_j$ face independent demands. After demand is observed, under complete pooling the retailer with a surplus sends the retailer with a shortage $Y_{ji} = \min\{S_j - D_j,\ D_i - S_i\}$ units (transship), and nothing moves otherwise. The type-1 service level is the probability of no stockout, $\alpha^0_i = \Pr[D_i \le S_i]$ without and $\alpha_i = \Pr[D_i - S_i \le Y_{ji}]$ with transshipments; the type-2 service level is the fill rate, one minus expected unmet demand over expected demand, $\beta^0_i$ and $\beta_i$ likewise.

Process flexibility. A flexibility design on $n$ products and $n$ plants is a set $E$ of (product, plant) pairs, an edge $(i, j)$ meaning plant $j$ can make product $i$ . Given a demand realization $d$ and a common plant capacity $C$ , the performance $P(d, E)$ (perf) is the maximum sales obtainable by assigning production along the edges of $E$ without exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system (BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint law is invariant under permutations of the products, and $[E] = \mathbb{E}[P(D, E)]$ is the expected performance (expPerf). The named designs are the dedicated design $D_n = \{(i, i)\}$ , the long chain $C_n$ in which plant $j$ also makes product $j + 1$ (and plant $n$ makes product $1$ ), the open chain $L_k$ obtained from $C_k$ by deleting the edge $(1, k)$ , and $L^n_k$ , the open chain on the first $k$ pairs together with the dedicated edges of the rest. A 2-flexibility design (TwoFlex) is one in which every product has exactly two plants and every plant exactly two products; $C_n$ is one, and so is any union of disjoint shorter chains.

Formalization targets

Goal: Theorem 7.9

For a balanced system of size $n \ge 2$ with exchangeable demand,

C_n \in \arg\max_{A \in \mathcal{F}_2} [A],

that is, $C_n$ is a 2-flexibility design and $[A] \le [C_n]$ for every 2-flexibility design $A$ . This is long_chain_optimal.

Supporting targets

The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, $P(d, E) + P(d, E \setminus \{\alpha, \beta\}) \ge P(d, E \setminus \{\alpha\}) + P(d, E \setminus \{\beta\})$ for $E \subseteq C_n$ ; Corollary 7.6, the same in expectation; Lemma 7.7, the increments $[L^n_{k+1}] - [L^n_k]$ are nondecreasing in $k$ , ending with $[C_n] - [L^n_n]$ ; and Lemma 7.8, $[C_n] = n([L_n] - [L_{n-1}])$ .

Risk pooling, Theorem 7.1: $g^*_C \le g^*_D$ , the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality $\sqrt{\sum_i\sum_j \sigma_i\sigma_j\rho_{ij}} \le \sum_i \sigma_i$ as a separate lemma.

Transshipments, Theorems 7.2 to 7.4: $\alpha_i = \alpha^0_i + |\partial\mathbb{E}[Y_{ji}]/\partial S_i|$ , $\beta_i = \beta^0_i + \mathbb{E}[Y_{ji}]/\mathbb{E}[D_i]$ , and all four post-transshipment service levels are nondecreasing in $S_i$ .

Significance

Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.

None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.

Difficulty

The obvious approach to Theorem 7.9 is to compare $C_n$ with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of $C_n$ , and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as $C_{n_j}$ on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.

Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle $C_n$ the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.

Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge $(2, 1)$ from $L^n_{k+1}$ leaves a design that is $L^n_k$ only after the pair $1$ is moved to the end, so the argument needs the invariance of $[E]$ under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.

For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of $\mathbb{E}[Y_{ji}]$ in $S_i$ has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.

Formalization scope

perf is a supremum over a set of reals, nonempty because $y = 0$ is feasible when $d \ge 0$ and $C \ge 0$ , and bounded by $\sum_i d_i$ ; the demand is nonnegative for every outcome and the capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue integral; the demand is integrable by assumption and $P(d, E)$ is $1$ -Lipschitz in $d$ , so the integrand is integrable, and a solver must prove this measurability rather than assume it.

Exchangeability is the equality of the laws of $(D_{\sigma(i)})_i$ and $(D_i)_i$ for every permutation $\sigma$ . Designs are finite sets of pairs of Fin n; the chains are defined with finRotate, so indices wrap modulo $n$ and the closing edge of $C_n$ is $(1, n)$ in the book's numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on subsystems of sizes $n$ and $n - 1$ ; these are designs on Fin k evaluated on the first $k$ coordinates of the demand (subDemand, subPerf).

Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for which the inequality still holds, so the statement is not trivialized by that convention. The transshipment theorems take the two demand laws as probability measures on $\mathbb{R}$ with no atoms (Theorem 7.2) and finite, positive means; the quantity $Y_{ji}$ is defined for all outcomes and the service levels are probabilities and expectations under the product law.

The definition module is shared by all eleven items. Beyond the milestones, formalizing the identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural contributions.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 7. https://doi.org/10.1002/9781119584445
G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5), 1979. https://doi.org/10.1287/mnsc.25.5.498
G. Tagaras, Effects of pooling on the optimization and service levels of two-location inventory systems, IIE Transactions 21(3), 1989. https://doi.org/10.1080/07408178908966208
W. C. Jordan and S. C. Graves, Principles on the benefits of manufacturing process flexibility, Management Science 41(4), 1995. https://doi.org/10.1287/mnsc.41.4.577
D. Simchi-Levi and Y. Wei, Understanding the performance of the long chain and sparse designs in process flexibility, Operations Research 60(5), 2012. https://doi.org/10.1287/opre.1120.1082

10 thms3 active usersReviewed

Completed

Probability·Captain: naimengye

Fundamentals of Supply Chain Theory V: The Bullwhip EffectTextbook

Why orders swing more than sales

Procter & Gamble observed in the 1990s that the orders its distributors placed for diapers were far more variable than the retail sales of diapers, and that its own orders to suppliers were more variable still, although the end demand for diapers is about as stable as demand gets. The phenomenon, a growing amplification of variability as one moves upstream in a supply chain, is the bullwhip effect. Lee, Padmanabhan and Whang (1997) argued that it is not a symptom of irrational behaviour: four rational responses of an inventory manager to their own environment each produce it. Chapter 13 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) makes three of the four quantitative, following Chen, Drezner, Ryan and Simchi-Levi (2000) for demand signal processing, Lee et al. for the rationing game, and Cachon (1999) for order batching. This mission formalizes those three models and the theorems the chapter proves about them.

Setting

Demand signal processing. A retailer faces a demand process $D_t$ , $t \in \mathbb{Z}$ , that follows the stationary first-order autoregressive model

D_t = d + \rho D_{t-1} + \epsilon_t,

with a constant $d \ge 0$ , a correlation constant $-1 < \rho < 1$ , and errors $\epsilon_t$ that are independent $N(0, \sigma^2)$ variables, each independent of the demands before period $t$ . In steady state every $D_t$ has the law $N\big(d/(1-\rho),\ \sigma^2/(1-\rho^2)\big)$ . The retailer replenishes with a lead time of $L$ periods under a base-stock policy but does not know the demand parameters, so it estimates the lead-time demand from a moving average of the previous $m \ge 1$ demands:

\hat\mu^L_t = \frac{L}{m}\sum_{i=1}^m D_{t-i}, \qquad \hat\sigma^L_{et} = C\sqrt{\frac{1}{m}\sum_{i=1}^m e_{t-i}^2}, \qquad e_t = D_t - \hat\mu^1_t,

and sets the base-stock level $S_t = \hat\mu^L_t + z_\alpha \hat\sigma^L_{et}$ , where $z_\alpha$ is a safety factor. The book writes the constant in $\hat\sigma^L_{et}$ as $C_{L\rho}$ and does not give its form; here it is a free parameter $C$ . Each period the retailer orders $Q_t = S_t - S_{t-1} + D_{t-1}$ , which may be negative. In Lean the process is the structure AR1Demand, whose fields are the parameters, the errors, the demands, the recursion, the independence properties and the stationary law; muHat, err, sigmaHat, baseStock and order are the five quantities above.

Order batching. $N$ retailers face independent $N(\mu, \sigma^2)$ demands in every period and each orders once every $R \ge 1$ periods, the order being its demand over the previous $R$ periods. The supplier's order in a given period is the total ordered by the retailers whose ordering day falls in that period. Three patterns are compared: random ordering, in which each retailer's day is uniform over the $R$ days, so the number $X$ of retailers ordering on a given day is binomial $(N, 1/R)$ ; positively correlated ordering, in which all retailers order on the same day, so $X = N$ with probability $1/R$ and $0$ otherwise; and balanced ordering, in which the retailers are spread as evenly as possible, so with $N = MR + k$ , $0 \le k < R$ , $X$ is $M+1$ with probability $k/R$ and $M$ otherwise. The structure BatchOrders P N R mu sigma carries the demands, the ordering count $X$ independent of them, and supplierOrder, the sum of the last $R$ demands of retailers $1, \dots, X$ ; each pattern enters a theorem as a hypothesis on the law of $X$ .

Rationing game. Two identical retailers face single-period demand with distribution function $F$ , holding cost $h$ and stockout penalty $p$ , so the newsvendor quantity $Q^*$ satisfies $F(Q^*) = p/(h+p)$ . With probability $r$ the supplier can deliver only $A_1 < 2Q^*$ units in total and allocates them pro rata to the orders, retailer 1 receiving $A_1 Q_1/(Q_1 + Q_2)$ ; with probability $1 - r$ supply is unlimited. Retailer 1's expected cost when the retailers order $Q_1$ and $Q_2$ is

g_1(Q_1) = (1-r)\,\mathrm{nv}(Q_1) + r\,\mathrm{nv}\!\Big(\frac{A_1 Q_1}{Q_1 + Q_2}\Big),

with $\mathrm{nv}$ the newsvendor cost; this is rationingCost.

Formalization targets

Goal: Theorem 13.2, demand signal processing

\frac{\mathrm{Var}[Q_t]}{\mathrm{Var}[D_t]} \;\ge\; 1 + \Big(\frac{2L}{m} + \frac{2L^2}{m^2}\Big)(1 - \rho^m),

with equality when $z_\alpha = 0$ . This is bullwhip_signal_processing. The bound exceeds $1$ whenever $L > 0$ , whatever the value of $\rho$ : a lead time and a moving-average forecast are enough to produce the effect.

Supporting targets

The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), $\mathbb{E}[D_t] = d/(1-\rho)$ , $\mathrm{Var}[D_t] = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}[D_t, D_{t-k}] = \rho^k \mathrm{Var}[D_t]$ ; the identity $Q_t = (1 + L/m) D_{t-1} - (L/m) D_{t-m-1} + z_\alpha(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$ ; Lemma 13.1, $\mathrm{Cov}[D_{t-i}, \hat\sigma^L_{et}] = 0$ for $1 \le i \le m$ ; the vanishing of the cross term (13.12); and the variance of the demand part, $\big(1 + (2L/m + 2L^2/m^2)(1 - \rho^m)\big)\mathrm{Var}[D_t]$ .

Order batching, Theorem 13.4: under the three patterns the supplier's order has mean $N\mu$ and

\mathrm{Var}[Q^c_t] \ge \mathrm{Var}[Q^r_t] \ge \mathrm{Var}[Q^b_t] \ge N\sigma^2,

through the three variance formulas $N\sigma^2 + \mu^2 N(R-1)$ , $N\sigma^2 + \mu^2 N^2 (R-1)$ and $N\sigma^2 + \mu^2 k(R-k)$ .

The rationing game, Theorem 13.3: if $Q > 0$ is a symmetric Nash equilibrium, that is, $Q$ minimizes $g_1$ over positive order quantities when the other retailer orders $Q$ , then $Q > Q^*$ .

Significance

The three theorems are the quantitative core of the chapter. Theorem 13.2 is the single-stage building block that Theorems 13.6 and 13.7 later iterate along a serial chain, giving the product-form and the exponential lower bounds on the amplification at stage $k$ ; its comparative statics, the bound decreasing in $m$ and increasing in $L$ , are the basis of the remedies the chapter recommends (shorter lead times, smoother forecasts, sharing point-of-sale data). Theorem 13.4 ranks the ordering patterns and justifies the advice to balance ordering days when batching cannot be avoided. Theorem 13.3 shows that pro-rata rationing alone inflates orders; the book is careful to note that inflated orders are not by themselves inflated variances, and that the variance statement for this model is due to Rong, Shen and Snyder (2017).

None of these results has a machine-checked proof. The book's proofs of Theorems 13.2 and 13.4 are complete but informal, and the proof of Lemma 13.1 is omitted with a citation to Ryan's 1997 thesis; formalizing it requires a self-contained argument. The variance decomposition of $Q_t$ and the conditioning argument for Theorem 13.4 are reusable for the multistage results of Sect. 13.2.5, which are natural follow-up missions on the same definitions.

Difficulty

The obvious computation of $\mathrm{Var}[Q_t]$ expands the order into its demand part and its safety-stock part and hopes the cross term disappears. It does, but not for a reason visible in the formulas: $\hat\sigma^L_{et}$ is a square root of a sum of squares of forecast errors, a nonlinear function of $m + m$ demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and $\hat\sigma$ is an even function of them, so the covariance is the expectation of an odd function of a centred Gaussian vector. That is Lemma 13.1, and the vanishing of the cross term needs two further covariances, $\mathrm{Cov}[D_{t-1}, \hat\sigma^L_{e,t-1}]$ and $\mathrm{Cov}[D_{t-m-1}, \hat\sigma^L_{et}]$ , which the book reduces to the lemma through the recursion (the second reduction divides by $\rho$ ) but which hold for every $\rho$ by the same symmetry. A solver must set up the joint Gaussian structure of the demand vector and prove the odd-function argument; nothing in Mathlib does this directly.

The second obstacle is that the moments (13.2) to (13.4) are not assumed but derived: the structure carries the stationary law of each $D_t$ and the independence of $\epsilon_t$ from the past, and the autocovariance $\rho^k \mathrm{Var}[D_t]$ has to be obtained from the recursion by induction on the lag, with integrability supplied by the Gaussian laws.

For Theorem 13.4 the work is the conditioning on $X$ : given $X = x$ the supplier's order is a sum of $xR$ independent normals, so its conditional mean is $xR\mu$ and conditional variance $xR\sigma^2$ , and the total variance is $\mathbb{E}[\mathrm{Var}[Q \mid X]] + \mathrm{Var}[\mathbb{E}[Q \mid X]]$ . The order is defined by a sum over retailers $i < X$ , so the independence of $X$ from the demands has to be used through the indicator structure rather than through a conditional-expectation library result.

For Theorem 13.3 the argument is a first-order condition. It requires that the newsvendor cost be differentiable with derivative $(h+p)F(y) - p$ , which holds when $F$ is continuous, and that the symmetric equilibrium be an interior minimizer, which is why $Q > 0$ and the minimization over $Q_1 > 0$ are hypotheses.

Formalization scope

Time is indexed by $\mathbb{Z}$ so that $D_{t-m-1}$ exists for every $t$ . AR1Demand asserts the recursion for every outcome, the independence of the whole error family, the independence of $\epsilon_t$ from $(D_s)_{s < t}$ , and the stationary law of every $D_t$ ; these are the "steady-state" assumptions the book makes in words. The structure is satisfiable: the stationary Gaussian AR(1) process on a full-measure set of error sequences has all these properties. The constant $C_{L\rho}$ is a free real parameter $C$ ; no theorem depends on its value.

The goal divides by $\mathrm{Var}[D_t]$ , which is $\sigma^2/(1-\rho^2) > 0$ under the structure's hypotheses $\sigma > 0$ and $|\rho| < 1$ , so the ratio is a genuine quotient. Mathlib's ProbabilityTheory.variance and covariance are used; both are the ordinary real quantities for square-integrable variables, which every variable here is, $\hat\sigma^L_{et}$ included.

In BatchOrders the demands are indexed by Fin N × Fin R, the count $X$ is a natural-valued random variable bounded by $N$ and independent of the demand family, and supplierOrder sums the $R$ demands of retailers $1, \dots, X$ , the book's "without loss of generality" choice. The laws of $X$ are hypotheses on point probabilities P.real {ω | X ω = j}; with $R \ge 1$ each of the three families of hypotheses is satisfiable by a structure with the corresponding law. The subtractions $R - 1$ and $R - k$ are real.

In the rationing game the demand law is a probability measure on $\mathbb{R}$ whose distribution function is continuous and strictly increasing on $[0, \infty)$ ; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at $0$ in the theorem since $Q_1 + Q_2 > 0$ .

Beyond the ten milestones, the multistage Theorems 13.6 and 13.7 and the centralized-information bound of Theorem 13.5 are welcome as extensions on the same AR1Demand.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
H. L. Lee, V. Padmanabhan and S. Whang, Information distortion in a supply chain: the bullwhip effect, Management Science 43(4), 1997. https://doi.org/10.1287/mnsc.43.4.546
F. Chen, Z. Drezner, J. K. Ryan and D. Simchi-Levi, Quantifying the bullwhip effect in a simple supply chain: the impact of forecasting, lead times, and information, Management Science 46(3), 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
G. P. Cachon, Managing supply chain demand variability with scheduled ordering policies, Management Science 45(6), 1999. https://doi.org/10.1287/mnsc.45.6.843
Y. Rong, Z.-J. M. Shen and L. V. Snyder, The impact of ordering behavior on order-quantity variability: a study of forward and reverse bullwhip effects, Naval Research Logistics 64(1), 2017. https://doi.org/10.1002/nav.21757

12 thms3 active usersReviewed

Completed

Dynamic Programming Probability·Captain: naimengye

Markov Decision Processes III: The Average Reward Optimality Equation for Unichain ModelsTextbook

Motivation

When a system is controlled indefinitely and decisions are frequent — a router admitting packets, a queue accepting jobs, a machine being maintained — discounting future rewards is often unjustified, and what matters is the long-run average reward per period. Puterman's Chapter 8 (doi:10.1002/9780470316887) develops the theory of this criterion, and its central object is a single equation, the average reward optimality equation $0=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$ , whose unknowns are a scalar gain $g$ and a bias function $h$ . For unichain models, in which every stationary policy generates a Markov chain with one recurrent class, this equation determines the optimal gain and an optimal stationary policy. The results go back to Howard (Dynamic Programming and Markov Processes, MIT Press, 1960) for the recurrent case and to Blackwell (Discrete dynamic programming, Annals of Mathematical Statistics 33, 1962, doi:10.1214/aoms/1177704593) and Derman for the general finite case; Puterman's Section 8.4 proves them through the discounted theory of mission II, by letting the discount factor tend to one.

Setting

The model is stationary (Assumption 8.0.1): a finite set $S$ of states, for each $s$ a finite nonempty set $A_s$ of actions, a reward $r(s,a)$ and transition probabilities $p(j\mid s,a)$ , none depending on the decision epoch. A policy $\pi\in\Pi^{HR}$ may randomize and may depend on the whole history; the deterministic stationary policy $d^\infty$ applies the decision rule $d:S\to A$ at every epoch. Its transition matrix is $P_d(i,j)=p(j\mid i,d(i))$ .

For a policy $\pi$ , $v^\pi_{N+1}(s)=\mathbb E^\pi_s[\sum_{t=1}^Nr(X_t,Y_t)]$ is the expected reward over $N$ epochs. Since the limit of $N^{-1}v^\pi_{N+1}(s)$ need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards $g^\pi_+(s)$ and $g^\pi_-(s)$ , and with $g^*_\pm(s)=\sup_{\pi}g^\pi_\pm(s)$ . A policy $\pi^*$ is average optimal when $g^{\pi^*}_-(s)\ge g^\pi_+(s)$ for all $s$ and $\pi$ , the strongest of the three criteria of Section 8.1.2.

The optimality residual is $B(g,h)(s)=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$ , and the optimality equation is $B(g,h)=0$ . A decision rule is $h$ -improving when it attains $\max_{a\in A_s}\{r(s,a)+\sum_jp(j\mid s,a)h(j)\}$ at every state. A transition matrix is unichain when it consists of a single recurrent class plus a possibly empty set of transient states, and the MDP is unichain when $P_d$ is unichain for every deterministic decision rule.

Formalization targets

Goal — Theorem 8.4.5 (printed p. 361)

For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation $B(g^*,h^*)=0$ has a solution, and (d) its scalar satisfies $g^*_+(s)=g^*_-(s)=g^*$ for every $s$ ; (c) for every solution, every $h^*$ -improving decision rule gives an average optimal stationary policy.

Theorem 8.4.1 (printed p. 356)

If $B(g,h)\le 0$ then $g\ge g^*_+$ ; if $B(g,h)\ge 0$ then $g\le\sup_{d}g^{d^\infty}_-\le g^*_-$ ; if $B(g,h)=0$ then $g^*_+=g^*_-=g$ .

Theorem 8.4.3 (printed p. 358)

In a finite unichain model $B(g,h)=0$ has a solution, and every solution has the same $g$ .

Theorem 8.4.4 (printed p. 361)

If $B(g^*,h^*)=0$ and $d^*$ is $h^*$ -improving, then $(d^*)^\infty$ is average optimal.

Significance

Theorem 8.4.1(c) is what the source calls "one of the most important results for average reward models": a solution of the optimality equation with constant $g$ pins down the optimal gain under every criterion at once, so that in finite unichain models the three optimality criteria of Section 8.1.2 coincide. Theorem 8.4.3 guarantees such a solution exists, and Theorem 8.4.4 reads an optimal policy off it. Together, Theorem 8.4.5 reduces the infinite-horizon average reward problem over all history-dependent randomized policies to a finite system of equations in $(g,h)$ , which is what policy iteration, value iteration and linear programming solve in Sections 8.5 to 8.8.

The results are classical and proved. Formalizing them fixes the chain-structure hypothesis in a checkable form and pins down which criterion "average optimal" means, two places where the literature is loose. The platform's MarkovDecisionProcesses series has the finite-horizon (mission I) and discounted (mission II) models; this mission adds the undiscounted stationary model, the gains, and the unichain classification, on which Chapter 9's multichain optimality equations and Chapter 10's sensitive discount optimality can be built.

Difficulty

The obvious argument for Theorem 8.4.3 is to take the discounted optimal value $v^*_\lambda$ of mission II and let $\lambda\uparrow 1$ . It fails as stated because $v^*_\lambda$ blows up like $(1-\lambda)^{-1}$ ; what converges is the Laurent expansion $v^{d^\infty}_\lambda=(1-\lambda)^{-1}ge+h+o(1)$ of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix $P_d^*$ and the deviation matrix $H_{P_d}$ of a unichain chain. So the proof must first develop the Markov chain theory of Section 8.2 and Appendix A, choose a subsequence of discount factors along which one policy is discount optimal (possible because $D^{MD}$ is finite), and only then pass to the limit in the discounted optimality equation.

Theorem 8.4.1 looks elementary and hides the analytic step: iterating $ge\ge r_d+(P_d-I)h$ along an arbitrary history-dependent policy and dividing by $N$ requires the telescoping term $N^{-1}(P^\pi_N-I)h$ to vanish, which uses boundedness of $h$ , and requires the reduction from history-dependent randomized to Markov randomized policies (Theorem 8.1.2). For Theorem 8.4.4 the step is Corollary 8.2.7, that $r_d-ge+(P_d-I)h=0$ forces the gain of $d^\infty$ to be $g$ , which is the multiplication by $P_d^*$ that annihilates $(P_d-I)$ .

The traps are in the definitions. Recurrence and the unichain property must be stated so that the source's Example 8.4.3 comes out as the book says — the policy using $a_{1,1}$ has the absorbing state $s_2$ as its single recurrent class — and the optimality residual must use the lim sup / lim inf gains, since a definition through a limit that need not exist would be a junk value on the policies of Example 8.1.1.

Formalization scope

State and action spaces are Fintypes and admissible actions are nonempty Finsets, as in missions I and II; the stationary model is a new structure because mission II's DiscountedMDP bundles a discount factor, and carries the same data otherwise. Policies are history-dependent and randomized, so "average optimal" has its full strength; a stationary policy is the deterministic one built from a decision rule. Expected total reward is defined by the policy evaluation recursion, as in the earlier missions, rather than through a measure on trajectories.

Gains are Filter.limsup and Filter.liminf of $N^{-1}v^\pi_{N+1}(s)$ on $\mathbb R$ ; these are the source's because the sequence is bounded by $\max|r|$ , and the suprema $g^*_\pm$ over the nonempty family of policies are genuine real suprema for the same reason. The residual $B(g,h)$ is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from $i$ reaches $i$ " and unichain is "any two recurrent states communicate", the definitions of Appendix A for finite chains, applied to $P_d$ for every admissible deterministic decision rule.

Restrictions relative to the printed text, all noted in the items: Theorem 8.4.1 is stated for finite $S$ where the source says countable, since the chapter's standing assumption and the model are finite; the gain $g^{d^\infty}$ of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain $ge=g^*=g^*_+=g^*_-$ of (8.4.6) is stated through $g^*_+$ and $g^*_-$ , since $g^*$ presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and $B(g,h)=0$ with a junk maximum is impossible since every $A_s$ is nonempty. Welcome contributions beyond the milestones: Theorem 8.1.2 (reduction to Markov policies), Corollary 8.2.7 (the gain of a stationary policy from the evaluation equations), and the equivalence of the three optimality criteria in finite models.

Selected references

Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Chapter 8. doi:10.1002/9780470316887
Ronald A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
David Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962). doi:10.1214/aoms/1177704593
Cyrus Derman, Finite State Markovian Decision Processes, Academic Press, 1970.
Paul J. Schweitzer and Awi Federgruen, The functional equations of undiscounted Markov renewal programming, Mathematics of Operations Research 3 (1978). doi:10.1287/moor.3.4.308

5 thms3 active usersReviewed

Completed

Machine Learning Optimization Probability·Captain: mikedeng1

Wasserstein Distributionally Robust Optimization I: Kantorovich Duality and Strong Duality for the Worst-Case RiskTextbook

Motivation

Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional $R(P,\ell) = \mathbb{E}_P[\ell(\xi)]$ from a nominal distribution $\hat P_N$ built from $N$ training samples, then optimizes a loss function $\ell$ against $\hat P_N$ instead of the unknown true distribution $P$ . Because the optimizer adapts to the noise in $\hat P_N$ , the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around $\hat P_N$ , rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.

Setting

Fix a norm $\|\cdot\|$ on a finite-dimensional real vector space $E$ (representing $\mathbb{R}^m$ ). For $p \in [1,\infty)$ , the type- $p$ Wasserstein distance between two Borel probability measures $Q, Q'$ on $E$ is

W_p(Q,Q') = \left(\inf_{\pi \in \Pi(Q,Q')} \int_{E\times E} \|\xi-\xi'\|^p\, \pi(d\xi,d\xi')\right)^{1/p},

where $\Pi(Q,Q')$ is the set of couplings of $Q$ and $Q'$ — joint probability measures on $E \times E$ whose marginals are $Q$ and $Q'$ . The optimal $\pi$ can be read as a transportation plan moving one pile of dirt ( $Q$ ) into another ( $Q'$ ) at minimum cost, which is why $W_p$ is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.

Given $N$ training samples $\hat\xi_1,\dots,\hat\xi_N$ , the empirical distribution is $\hat P_N = \frac1N\sum_{i=1}^N \delta_{\hat\xi_i}$ . Centered at $\hat P_N$ , the Wasserstein ambiguity set of radius $\varepsilon \ge 0$ is

B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\},

where $\Xi \subseteq E$ is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function $\ell$ is

R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} \mathbb{E}_Q[\ell(\xi)],

and minimizing it over a class of admissible loss functions $\mathcal{L}$ is a distributionally robust optimization problem. $\varepsilon$ measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.

Formalization targets

Goal — Theorem 7, strong duality

R_{\varepsilon,p}(\hat P_N,\ell) = \inf_{\gamma \ge 0}\ \mathbb{E}_{\hat P_N}[\ell_\gamma(\xi)] + \gamma\varepsilon^p,\qquad \ell_\gamma(\xi) = \sup_{z\in\Xi} \ell(z) - \gamma\|z-\xi\|^p.

This is the Lagrangian dual of the worst-case risk evaluation problem, with $\gamma$ the multiplier of the Wasserstein constraint $W_p(Q,\hat P_N)\le\varepsilon$ : it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization $\ell_\gamma$ . Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which $\ell_\gamma$ is computable.

Supporting dual representations of $W_p$ — Theorems 1 and 2

W_p^p(Q,Q') = \sup\left\{\int \psi\,dQ' - \int \varphi\,dQ : \varphi,\psi \text{ bounded continuous},\ \psi(\xi)-\varphi(\xi') \le \|\xi-\xi'\|^p\right\}

W_1(Q,Q') = \sup_{\mathrm{Lip}(\varphi)\le 1} \int \varphi\,dQ - \int \varphi\,dQ'

These identify $W_p$ as a linear program's strong dual (Theorem 1) and, for $p=1$ , specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.

Upper and lower bounds — Theorems 5 and 6

R_{\varepsilon,p}(\hat P_N,\ell) \le R(\hat P_N,\ell) + \varepsilon\cdot\mathrm{Lip}(\ell)

R_{\varepsilon,p}(\hat P_N,\ell) \ge \sup\left\{\tfrac1N\textstyle\sum_i \ell(\hat\xi_i+\theta_i) : \hat\xi_i+\theta_i\in\Xi,\ \tfrac1N\textstyle\sum_i\|\theta_i\|^p\le\varepsilon^p\right\}

These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.

Exact case — Theorem 10

\Xi = \mathbb{R}^m,\ \ell \text{ convex},\ p=1 \implies R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon\,\mathrm{Lip}(\ell)

Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.

Significance

Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.

Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).

Difficulty

The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over $Q$ and the inner minimization over the multiplier $\gamma$ , and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint $W_p(Q,\hat P_N)\le\varepsilon$ via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.

Formalization scope

$E$ is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ, Borel-measurable), representing $\mathbb{R}^m$ with the paper's arbitrary fixed norm as a parameter rather than fixing the Euclidean norm. A coupling is formalized directly via MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which correctly returns $\top$ (resp. $\bot$ ) outside the feasible set rather than a finite junk value.

Two deliberate, disclosed conventions keep the extremal-value definitions faithful without extended-real integration machinery, both recorded in MODERATION_NOTES.md:

worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal, not ℝ, so an unbounded supremum is recorded as $+\infty$ rather than collapsed to Mathlib's real-valued junk value 0 on an unbounded family.
The goal theorem (7) and its Moreau-Yosida regularization restrict the loss function to bounded continuous $\ell$ (BoundedContinuousFunction E ℝ), narrower than the paper's general upper-semicontinuous, $\hat P_N$ -integrable loss class $\mathcal{L}$ (Assumption 1). This keeps $\ell_\gamma(\xi) = \sup_{z\in\Xi}\ell(z)-\gamma\|z-\xi\|^p$ a finite real number for every nonempty $\Xi$ , so the right-hand side's Bochner integral is well-posed; the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily bounded) loss class, since their statements do not require evaluating a pointwise supremum over $\Xi$ .
Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing assumption (p. 6: "we let $\Xi\subseteq\mathbb{R}^m$ be a closed set that is known to contain the support of $P$ ") for the whole worst-case-risk framework, which is used silently in the paper wherever a theorem takes $\Xi$ as an argument but was not carried into these theorems' own hypothesis lists in an earlier draft.
The goal theorem (7) additionally requires $\hat P_N$ itself supported on $\Xi$ ( $\hat P_N(\Xi^c)=0$ , the same "supported on $\Xi$ " convention ambiguitySet uses for $Q\in\mathcal P(\Xi)$ ), which the paper's framework presupposes for the nominal distribution throughout §2. Combined with $\ell$ bounded, this makes $\ell_\gamma$ bounded on the full-measure set $\Xi$ (above by $\sup\ell$ unconditionally, below by $\ell(\xi)$ itself via $z=\xi$ for $\xi\in\Xi$ ), which is what makes the right-hand side's integral genuinely well-posed rather than liable to Mathlib's non-integrable junk value $0$ .

There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and 0 < N are both required exactly where the paper's own indexing and support assumptions require them, and every extremal value uses the extended-real convention above rather than a convention that would make an inequality vacuously true.

No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only unrelated discrete/finite-type constructions); all seven definitions and six theorems are drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and .worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports directly or redefines locally per the series' reuse rule.

Selected references

Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research, 130–166. https://doi.org/10.1287/educ.2019.0198
Villani, C. (2009). Optimal Transport: Old and New. Springer. (Cited as [108] for Theorems 1 and 2.)
Smith, J. E., & Winkler, R. L. (2006). The optimizer's curse: Skepticism and postdecision surprise in decision analysis. Management Science, 52(3), 311–322. https://doi.org/10.1287/mnsc.1050.0451
Gao, R., & Kleywegt, A. J. (2016). Distributionally Robust Stochastic Optimization with Wasserstein Distance. arXiv:1604.02199.
Blanchet, J., & Murthy, K. (2019). Quantifying Distributional Model Risk via Optimal Transport. Mathematics of Operations Research, 44(2), 565–600. https://doi.org/10.1287/moor.2018.0936

13 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics+1·Captain: mikedeng1

Foundations of Machine Learning XIV: Finite Markov Decision Processes and Bellman's EquationsTextbook

Motivation

Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).

Setting

A (finite) Markov decision process consists of a finite set of states $S$ , a finite set of actions $A$ , a transition kernel $P[s'\mid s,a]$ giving the distribution over the next state $s'$ after taking action $a$ at state $s$ , and an expected reward $\mathbb E[r(s,a)]$ for that transition. A (stationary) policy $\pi:S\to\Delta(A)$ assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing $\pi$ turns the MDP into an ordinary Markov chain on $S$ : at each step the agent is at some state $s$ , draws $a\sim\pi(s)$ , receives (expected) reward $\mathbb E[r(s,a)]$ , and moves to a state drawn from $P[\cdot\mid s,a]$ . For a discount factor $\gamma\in[0,1)$ , the value of $\pi$ at $s$ is the expected discounted sum of future rewards starting from $s$ ,

V_\pi(s) = \mathbb E_{a_t\sim\pi(s_t)}\Big[\sum_{t=0}^{+\infty}\gamma^t r(s_t,a_t) \;\Big|\; s_0=s\Big],

and the state-action value function $Q_\pi(s,a)$ is the analogous quantity for taking $a$ at $s$ and then following $\pi$ . Marginalizing the raw kernel and reward over the mixed action $\pi(s)$ gives the induced transition matrix $P_{s,s'}=P[s'\mid s,\pi(s)]=\sum_a \pi(s)(a) P[s'\mid s,a]$ and induced reward vector $R_s=\mathbb E[r(s,\pi(s))]=\sum_a\pi(s)(a)\,\mathbb E[r(s,a)]$ — the objects that turn $\pi$ 's value into a genuinely linear-algebraic quantity. A policy $\pi^*$ is optimal if $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and every state $s$ ; write $V^*$ for its value function.

Formalization targets

Theorem 17.10 (goal). For a finite MDP and a fixed policy $\pi$ , the matrix $I-\gamma P$ (with $P$ the policy-induced transition matrix) is invertible, and $\pi$ 's value function is the unique solution of the Bellman equations, given in closed form by

V_\pi = (I-\gamma P)^{-1} R.

Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:

\forall s\in S,\quad V_\pi(s) = \mathbb E_{a\sim\pi(s)}[r(s,a)] + \gamma\sum_{s'} P[s'\mid s,\pi(s)]\,V_\pi(s').

Theorem 17.7 (milestone). A policy $\pi$ is optimal if and only if it places probability only on $Q_\pi$ -maximizing actions: for every $(s,a)$ with $\pi(s)(a)>0$ , $a\in \operatorname{argmax}_{a'} Q_\pi(s,a')$ .

Theorem 17.11 (milestone). The Bellman optimality operator $\Phi$ , $[\Phi(V)](s)=\max_{a} \{\mathbb E[r(s,a)]+\gamma\sum_{s'}P[s'\mid s,a]V(s')\}$ , is a $\gamma$ -contraction for $\lVert\cdot\rVert_\infty$ ; consequently, for any starting vector $V_0$ , the value-iteration sequence $V_{n+1}=\Phi(V_n)$ converges to a fixed point of $\Phi$ .

Significance

Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single $|S|\times|S|$ matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ( $O(\log(1/\epsilon))$ iterations for $\epsilon$ -accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor $\gamma<1$ , not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).

Difficulty

The obvious shortcut for Theorem 17.10 is to assert $I-\gamma P$ is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that $P$ , being row-stochastic (every row of $P$ sums to exactly $1$ , since $\pi(s)$ and $P[\cdot\mid s,a]$ are both proper distributions), has operator norm $\lVert P\rVert_\infty=1$ exactly, so $\lVert\gamma P\rVert_\infty=\gamma<1$ strictly; this rules out $1$ as an eigenvalue of $\gamma P$ , which is exactly what invertibility of $I-\gamma P$ requires. The same $\gamma<1$ fact, applied differently, drives Theorem 17.11: showing $\Phi$ is $\gamma$ -Lipschitz requires bounding $\Phi(V)(s)-\Phi(U)(s)$ by comparing the maximizing action for $V$ against the same action's value under $U$ (not $U$ 's own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if $\gamma=1$ is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.

Formalization scope

States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel asserting the required distribution property explicitly rather than assuming it silently. A policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition 17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather than one being definitionally true of the other. The trivializing formalization this rules out is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and calling the resulting identity a theorem; both would erase the mission's actual content. Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model with a termination-probability deficit rather than exact row-stochasticity, and FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted convention, so every definition here is drafted fresh rather than imported. This chunk covers §17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration); §17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a stochastic-approximation convergence substrate this mission does not build.

Selected references

Mohri, M., Rostamizadeh, A., and Talwalkar, A. Foundations of Machine Learning, 2nd ed., chapter 17. MIT Press, 2018.
Bellman, R. Dynamic Programming. Princeton University Press, 1957.
Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994.

13 thms3 active usersReviewed

Completed

Probability Statistics Stochastic Systems·Captain: mikedeng1

Stochastic Orders IV: The Increasing Convex and Increasing Concave OrdersTextbook

Comparing location and spread together

Chapter I's usual stochastic order compares "how large" two random variables tend to be; Chapter III's convex order compares "how spread out" they are, holding the mean fixed. Chapter IV's increasing convex and increasing concave orders combine the two: $X \le_{icx} Y$ says $X$ is both smaller and less variable than $Y$ in a single comparison, without forcing equal means. These are the orders a decision-maker with risk-averse (concave-utility) or risk-loving (convex-cost) preferences actually uses to rank random outcomes, since expected utility is exactly an expectation of an increasing concave or convex function. This mission formalizes both orders and their coupling characterization: the submartingale/supermartingale analogue, one chapter over, of Chapter III's Strassen martingale coupling for the plain convex order.

The increasing convex and increasing concave orders

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$ , and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the increasing convex order, written $X \le_{icx} Y$ , if

E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every increasing convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist,}

and smaller than $Y$ in the increasing concave order, $X \le_{icv} Y$ , if the same holds for every increasing concave $\varphi$ . Taking $\varphi(x)=x$ (increasing and both convex and concave) gives $E[X]\le E[Y]$ under either order — unlike the convex order, no equality of means is forced. Two equivalent tail-integral characterizations (Theorem 4.A.2) make the orders tractable: $X\le_{icx}Y$ iff $\int_x^\infty \bar F(u)\,du \le \int_x^\infty \bar G(u)\,du$ for every $x$ , and $X\le_{icv}Y$ iff $\int_{-\infty}^x F(u)\,du \ge \int_{-\infty}^x G(u)\,du$ for every $x$ , where $\bar F,\bar G$ and $F,G$ are the survival and distribution functions.

Formalization targets

Goal: the submartingale-coupling characterization (Theorem 4.A.5, increasing convex case)

X \le_{icx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]\ge\hat X\text{ a.s.}

Furthermore, $\hat X,\hat Y$ can be chosen so that $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$ ). This is the increasing-convex analogue of Chapter III's Theorem 3.A.4: instead of a martingale, $\{\hat X,\hat Y\}$ need only be a submartingale — the copy of $Y$ is, conditionally on the copy of $X$ , at least a fair randomization of it. The book states its proof is "similar to the proof of Theorem 3.A.4" and calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Companion: the supermartingale-coupling characterization (Theorem 4.A.5, increasing concave case)

The same theorem's other bracketed case: $X \le_{icv} Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$ , $\hat Y=_{st}Y$ , and $\{\hat Y,\hat X\}$ a supermartingale, $E[\hat X\mid\hat Y]\le\hat Y$ a.s. — note the swapped roles of $\hat X$ and $\hat Y$ in the conditioning relative to the increasing-convex case, not merely a flipped inequality. Drafted as a separate Lean theorem from the goal (see Formalization scope), since the two conditioning structures are genuinely different predicates, not sign-flipped rewrites of one another.

Supporting milestones

Theorem 4.A.1, the duality relation: $X\le_{icx}Y \iff -X\ge_{icv}-Y$ , and $X\le_{icv}Y\iff -X\ge_{icx}-Y$ — the increasing-order analogue of Theorem 3.A.12(a)'s duality for the plain convex order.
Theorem 4.A.2, the tail-integral characterizations above, for integrable $X,Y$ .
Theorem 4.A.8(d), closure under convolution: independent $X_i\le_{icx}Y_i$ (resp. $\le_{icv}$ ) for $i=1,\dots,m$ gives $\sum_i X_i \le_{icx} \sum_i Y_i$ (resp. $\le_{icv}$ ) — the increasing-order analogue of Chapter III's Theorem 3.A.12(d), which the book itself says "can be proven as in Theorem 3.A.12."

Significance

The increasing convex and concave orders are the natural language of expected-utility comparisons: a risk-averse agent with concave utility $u$ prefers $Y$ to $X$ exactly when $X\le_{icv}Y$ implies $E[u(X)]\le E[u(Y)]$ for every increasing concave $u$ — the order is defined precisely so that "every risk-averse agent with increasing utility agrees" collapses to one comparison. In operations research this underlies stochastic dominance of the second kind in portfolio and inventory models, and the increasing-convex order similarly formalizes "second-order stochastic dominance for costs" used to compare random cost/loss distributions under risk-loving or regret-averse preferences. The submartingale-coupling characterization is what turns the intractable "for every increasing convex $\varphi$ " quantifier into a single explicit construction, exactly as Strassen's theorem does for the plain convex order — and, being the direct chapter-IV successor to Chapter III's coupling theorem in this series, it fixes the second data point for what a "coupling-characterization" mission in this book's series looks like when the order being characterized is not symmetric between the two variables' roles.

No platform prior art exists: GET /theorems?q=increasing+convex, q=increasing+concave, and q=submartingale return zero genuinely matching hits (the one submartingale hit, a bandit subgaussian maximal inequality, uses Doob's inequality for a concentration bound, not this order). This mission restates the increasing convex/concave orders and their coupling characterization as a foundational, self-contained pair of definitions, parallel in structure to Chunk 03's convex-order mission but independently drafted (drafts cannot import each other's Lean).

Difficulty

The chief formalization risk is the one this chapter's own brief flags explicitly: the book states Theorem 4.A.5 as a single statement with bracketed alternatives (" $X\le_{icx}Y$ [ $X\le_{icv}Y$ ] iff … $\{\hat X,\hat Y\}$ is a submartingale [ $\{\hat Y,\hat X\}$ is a supermartingale] …"), and the two cases are not symmetric rewrites of each other — the conditioning variable in E[Ŷ|X̂]≥X̂ swaps to E[X̂|Ŷ]≤Ŷ in the concave case, not just a flipped inequality on the same conditioning. A Lean statement that tried to unify both cases with a single Or or a naive sign-flip would either conflate two different predicates or silently state the wrong condition for one of the two cases. The duality theorem (4.A.1) compounds this risk in the other direction: its content is exactly that $\le_{icx}$ and $\ge_{icv}$ are related (by negating the variables), so a formalization that makes this equivalence provable by unfolding definitions (rather than as a genuine ↔ between two independently-stated predicates) would trivialize the one theorem whose entire content is that relationship.

Formalization scope

Random variables are measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, matching this series' convention; IcxOrder μ ν X Y and IcvOrder μ ν X Y are drafted as two separate definitions (not one order parametrized by an Or of function classes), each quantifying over Monotone φ ∧ ConvexOn ℝ Set.univ φ (resp. ConcaveOn) with the two expectations' existence stated as explicit Integrable hypotheses inside the ∀, exactly as Chunk 03's ConvexOrder. Equality in law is ProbabilityTheory.IdentDistrib. The goal's submartingale condition uses Mathlib's conditional-expectation notation X̂ ≤ᵐ[ρ] ρ[Ŷ | m] with m the σ-algebra generated by X̂; its companion's supermartingale condition uses ρ[X̂ | m'] ≤ᵐ[ρ] Ŷ with m' generated by Ŷ instead — the conditioning variable is genuinely swapped between the two theorems, matching the book's own bracket ordering {X̂,Ŷ} vs. {Ŷ,X̂}. The "Furthermore" clause in both is kept (not dropped), via Mathlib's ProbabilityTheory.condDistrib, restated as the relevant conditional-distribution kernel's survival function being monotone at every threshold — the same shape Chapter I's UsualOrder and Chunk 03's goal theorem use, necessarily restated locally since drafts cannot import another mission's definitions.

Theorem 4.A.1 (duality) and Theorem 4.A.8(d) (convolution closure) are each drafted as a single Lean theorem with two independent conjuncts (an ∧ of two ↔s, or of two implications), one per bracketed case, since the book states both cases as the two halves of one theorem sharing every hypothesis — this is not the same shape as the goal/companion split, where the two cases have genuinely different internal structure (the swapped conditioning) rather than a shared statement instantiated at two function classes. A trivializing formalization this mission rules out: stating Theorem 4.A.1's duality by relabeling IcvOrder as IcxOrder applied to negated arguments (making the equivalence a rfl or single simp unfolding) rather than keeping the two orders as independently-defined predicates whose relationship is the theorem's actual content.

This mission draws on no platform prior art (searches for "increasing convex", "increasing concave", and "submartingale" as of 2026-09-18 return zero genuine matches — the sole submartingale hit is an unrelated bandit concentration inequality via Doob's inequality). Reusable beyond this mission: the IcxOrder/IcvOrder definition pattern and the submartingale/supermartingale coupling shape parallel Chunk 03's ConvexOrder martingale-coupling pattern closely enough that a future chapter needing "coupling characterization of a location-and-spread order" (none of the remaining chapters currently in this series' first wave) could restate the same shape with minimal adaptation.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 4 (Univariate Monotone Convex and Related Orders), §4.A. https://doi.org/10.1007/978-0-387-34675-5
This series' Chunk 03 (StochasticOrders.Convex), for the plain convex order and Strassen's martingale coupling this chapter's submartingale/supermartingale coupling directly generalizes.

7 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Supermodularity and Complementarity IV: Monotone Optimal Policies in Markov Decision ProcessesTextbook

Motivation

A Markov decision process (MDP) chooses a decision in every period of a dynamic system whose state evolves stochastically in response to the decision, so as to maximize expected discounted return. Firms use this model for inventory, pricing, and advertising decisions that respond to a randomly evolving demand state; engineers use it for maintaining or replacing equipment that degrades stochastically. A recurring practical question is qualitative rather than numerical: does the optimal decision increase with the state — should a firm price higher after a period of strong sales, or replace a machine sooner the worse its observed condition — without having to solve the dynamic program numerically for every instance of the model? Topkis's Chapter 3, Section 3.9 (Topkis, Supermodularity and Complementarity, 2011, building on Topkis [1968]) answers this by isolating the lattice-theoretic structure — supermodularity of the return function and of the transition law — under which monotone optimal policies are guaranteed on structural grounds alone. A closely related but logically independent question was studied earlier by Lehmann [1955], who characterized when a family of distributions is stochastically increasing in a parameter; Topkis generalizes Lehmann's characterization to any property of the parameter dependence whose defining set of functions forms a closed convex cone, of which stochastic monotonicity, supermodularity, and convexity are three instances (Theorem 3.9.1, Corollary 3.9.1). Serfozo [1976] independently develops related conditions for partially observed Markov decision processes, and Amir [1996] and Amir, Mirman, and Perkins [1991] give analogous monotonicity results for other classes of dynamic programming models.

Setting

Fix a finite planning horizon of $k$ periods, $i = 1, \dots, k$ . In period $i$ the state $t$ ranges over a set $T_i \subseteq \mathbb{R}^m$ ; given state $t$ , the decision $x$ is restricted to a finite, nonempty set $X_{t,i} \subseteq \mathbb{R}^n$ (finiteness guarantees that an optimal decision always exists — no continuity or compactness argument is used). Write $S_i = \{(x,t) : t \in T_i,\, x \in X_{t,i}\}$ for the set of admissible (decision, state) pairs in period $i$ . The (bounded) expected net return of choosing decision $x$ in state $t$ , period $i$ , is $r_i(x,t)$ . A discount rate $\beta \in [0,1]$ gives $\gamma = 1/(1+\beta)$ , the value in period $i$ of one unit of return in period $i+1$ . Given decision $x$ , state $t$ , and period $i$ , the state $w$ of period $i+1$ is drawn from a distribution $F(x,t,i,\cdot)$ on $\mathbb{R}^m$ .

The optimal-value function $f_i(t)$ (present value of acting optimally from state $t$ , period $i$ , onward) and the decision-value function $g_i(x,t)$ (present value of choosing $x$ in state $t$ , period $i$ , then acting optimally thereafter) are defined by backward induction from period $k$ :

g_k(x,t) = r_k(x,t), \qquad f_i(t) = \max_{x \in X_{t,i}} g_i(x,t), \qquad g_i(x,t) = r_i(x,t) + \gamma \int f_{i+1}(w)\, dF(x,t,i,w) \quad (i < k).

A subset $S$ of a Euclidean space is increasing if it is upward closed under the coordinatewise order. A family of distributions $\{F(a,\cdot) : a \in D\}$ indexed by a parameter $a$ is stochastically increasing on $D$ if the probability $\int_S dF(a,w)$ of every increasing set $S$ is a monotone (non-decreasing) function of $a$ on $D$ ; when $D$ is a sublattice, the family is stochastically supermodular on $D$ if that same probability is a supermodular function of $a$ on $D$ . A real-valued function $\varphi$ on a lattice is supermodular on a set $D$ if $\varphi(a_1) + \varphi(a_2) \le \varphi(a_1 \vee a_2) + \varphi(a_1 \wedge a_2)$ for all $a_1, a_2 \in D$ — the mission series' shared notion, defined once in chunk 02-monotonicity and reused here as Supermodularity.Monotonicity.SupermodularOn.

Formalization targets

Goal — Theorem 3.9.2 (monotone optimal policies)

g_i(x,t) \text{ supermodular on } S_i, \qquad f_i(t) \text{ supermodular on } T_i, \qquad \arg\max_{x \in X_{t,i}} g_i(x,t) \text{ increasing in } t,

together with the existence of a greatest and a least optimal decision at every state, each increasing in the state, in every period $i$ — under the hypotheses that $S_i$ is a sublattice of $\mathbb{R}^{n+m}$ , $X_{t,i}$ is expanding in $t$ , $r_i$ is increasing in $t$ (on sections) and jointly supermodular in $(x,t)$ , and $F(x,t,i,\cdot)$ is stochastically increasing in $t$ (on sections) and stochastically jointly supermodular in $(x,t)$ , for every period $i$ .

This is the weakest of the targets that is still worth stating on its own: it packages four related conclusions (parts (a)–(d) of Theorem 3.9.2) that share one hypothesis set, rather than isolating just the headline monotone-decision claim, because the book's own proof derives all four together and a solver attacking part (c) or (d) needs part (a) and (b) established first.

Supporting milestones

Lemma 3.9.4: under the monotonicity half of the goal's hypotheses alone (no supermodularity), $f_i(t)$ is increasing in $t$ for every period $i$ . This is the induction Theorem 3.9.2 reuses and strengthens.
Corollary 3.9.1(b): on a sublattice $T$ , a family of distributions is stochastically supermodular in $t$ iff $\int h(w)\,dF(t,w)$ is supermodular in $t$ for every increasing $h$ . This is what lets the goal's hypothesis " $F(x,t,i,\cdot)$ stochastically supermodular in $(x,t)$ " be converted into " $\int f_{i+1}(w)\,dF(x,t,i,w)$ supermodular in $(x,t)$ ", the step that feeds $g_i$ 's supermodularity.
Theorem 3.9.1: the general closed-convex-cone characterization of which Corollary 3.9.1(b) is the supermodularity instance (monotonicity and convexity are the other two instances, not formalized here since the goal's proof only needs the supermodularity case).

Significance

The result gives a purely structural sufficient condition — no smoothness, convexity of the decision set, or specific functional form — for monotone comparative statics in dynamic optimization: whenever the one-period return and the state transition are individually monotone and jointly supermodular in (decision, state), so is the whole multi-period value function, and so are the optimal decisions. Textbook applications include optimal advertising that decreases with prior-period sales, optimal pricing that increases with prior-period sales, and optimal maintenance of a deteriorating system, none of which need to be re-derived from scratch once the structural hypotheses are checked for the specific return and transition functions at hand.

Formalizing it contributes a genuinely new layer to the mission series and, per the paper's own triage (substrate.md), to the platform's application of Mathlib's probability-kernel infrastructure: a finite-horizon MDP with a Lebesgue–Stieltjes-style transition law and its associated stochastic-dominance vocabulary (stochastically increasing / stochastically supermodular families of distributions) did not previously exist on the platform or in this mission series, and both are reusable beyond this mission by any future formalization of dynamic programming under uncertainty. The proof itself is not open — Topkis [2011] (unchanged from the 1968/1998 original) gives a complete, elementary backward-induction argument — so what this mission produces is the formalization of a known, structurally distinctive proof technique, not a new mathematical result.

Difficulty

The naive argument — "supermodularity of $r_i$ plus supermodularity of the transition kernel obviously gives supermodularity of $g_i$ " — breaks exactly at the integral: supermodularity of $(x,t) \mapsto F(x,t,i,\cdot)$ is a statement about the whole family of distributions, not about a single number, so "the transition is jointly supermodular" has to be unpacked into "the probability of every increasing set is jointly supermodular in $(x,t)$ " before it says anything about $\int f_{i+1}(w)\,dF(x,t,i,w)$ for a specific function $f_{i+1}$ . Corollary 3.9.1(b) is exactly the step that licenses this unpacking, and it is not free: it needs Theorem 3.9.1's closed-convex-cone argument (approximating $f_{i+1}$ from below by increasing step functions and invoking monotone convergence), not a pointwise argument on $r_i$ and $F$ separately. A second place the naive argument fails is at the constraint sets: because $X_{t,i}$ only grows with $t$ rather than being fixed, monotonicity of $f_i$ (Lemma 3.9.4) needs its own induction combining that growth with monotonicity of $g_i$ — supermodularity of $g_i$ alone does not hand you monotonicity of the arg max without it.

Formalization scope

States and decisions are represented as Fin m → ℝ and Fin n → ℝ (finite-dimensional Euclidean coordinate spaces with the coordinatewise/product order, matching the book's own restriction to $\mathbb{R}^m$ and $\mathbb{R}^n$ — no abstract lattice is used where the book itself specializes). Distributions are represented as MeasureTheory.Measure on the relevant coordinate space, with IsProbabilityMeasure supplied explicitly wherever a stochastic-dominance hypothesis is used (the probability of a set is read off as (μ S).toReal, which is only faithful to $\int_S dF$ when μ is a probability measure — an unconstrained arbitrary measure would let .toReal collapse an infinite value to $0$ and make the hypothesis trivially satisfiable, a formalization this mission rules out). Integrands h are required integrable against every measure in the family wherever an integral is asserted to lie in a set V, since the Bochner integral of a non-integrable function is definitionally 0 in Lean/Mathlib and would otherwise make Theorem 3.9.1 and Corollary 3.9.1(b) trivially true. Decision sets $X_{t,i}$ are finite (Finset, not merely a bounded or compact Set) and required nonempty exactly where the book assumes it: this finiteness, not any compactness or semicontinuity argument, is what guarantees an optimal decision exists, and dropping it would silently substitute Chapter 2's compactness-based existence machinery for the different argument this section actually uses. The optimal-value and decision-value functions $f_i, g_i$ are represented as any functions satisfying the two backward-recursion equations that define them, rather than being constructed by explicit backward recursion in Lean; since the equations determine $f_i, g_i$ uniquely from $r_i$ and $F$ , this is a faithful reading of "define $f_i, g_i$ by (3.9.1) and (3.9.2)," not a weakening of the theorem. The goal's part (c) is stated using the mission series' InducedSetOrder (the Veinott/strong set order, chunk 01-lattices) and part (d) as the existence of two selection functions (greatest, least optimal decision), each monotone in the state — matching the book's "there is a greatest (least) optimal decision ... and this greatest (least) optimal decision is increasing in $t$ ." The infinite-horizon stationary extension that the book gives immediately after Theorem 3.9.2 (relying on an unproved citation to Blackwell [1965]) is out of scope for this mission.

Reusable infrastructure: the StochasticallyIncreasingOn/StochasticallySupermodularOn definitions are parametric in the ambient preorder/lattice and in the measure's target dimension, so a future mission on stochastic convexity (Corollary 3.9.1(c), not formalized here) or on Topkis's §3.10 stochastic inventory model (which explicitly depends on §3.9, per the book's own reading-order note) can reuse them without modification. Contributions extending this mission to the infinite-horizon case, or completing Corollary 3.9.1's monotonicity and convexity halves, are welcome.

Selected references

D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (unchanged from the 1998 original), Chapter 3, Section 3.9. DOI: 10.1515/9781400822539.
D. M. Topkis, "Ordered Optimal Solutions," PhD dissertation / working paper, Stanford University, 1968 (the original source for this section's results).
E. L. Lehmann, "Ordered Families of Distributions," Annals of Mathematical Statistics 26(3), 1955, pp. 399–419. https://doi.org/10.1214/aoms/1177728487
R. Serfozo, "Monotone Optimal Policies for Markov Decision Processes," Mathematical Programming Study 6, 1976, pp. 202–215.
R. Amir, "Sensitivity Analysis of Multisector Optimal Economic Dynamics," Journal of Mathematical Economics 25(1), 1996, pp. 123–141.
R. Amir, L. J. Mirman, and W. R. Perkins, "One-Sector Nonclassical Optimal Growth: Optimality Conditions and Comparative Dynamics," International Economic Review 32(3), 1991, pp. 625–644.
D. Blackwell, "Discounted Dynamic Programming," Annals of Mathematical Statistics 36(1), 1965, pp. 226–235. https://doi.org/10.1214/aoms/1177700285

8 thms3 active usersReviewed

Completed

Probability Stochastic Systems·Captain: mikedeng1

Stochastic Orders II: The Mean Residual Life OrderTextbook

Motivation

A device's mean residual life at age $t$ — its conditional expected remaining lifetime given that it has survived to $t$ — is one of the oldest and most interpretable summaries in reliability and survival analysis: it is what an insurer, a maintenance planner, or a hospital outcomes researcher actually wants to know about a unit still in service. Comparing two mean residual life functions pointwise gives the mean residual life order $\le_{mrl}$ , a natural "the survivor of $X$ is worn less, on average, than the survivor of $Y$ " comparison that is weaker than the usual stochastic order but not directly comparable to it (the book states plainly that neither implies the other in general). This mission formalizes the order's definition and its precise relationship to the stronger hazard rate order $\le_{hr}$ : under an extra monotone-ratio condition the two orders coincide, and one direction of that coincidence always holds. A third milestone gives one of the chapter's closure properties, showing that "decreasing mean residual life" (DMRL) — an aging notion used throughout reliability theory to describe units that wear out, rather than improve, with age — is preserved under adding independent noise.

Setting

Fix a probability space $(\Omega,\mu)$ and a real-valued random variable $X$ with survival function $\bar F(x) = P\{X>x\}$ and finite mean. The mean residual life function of $X$ at $t$ is

m(t) = \begin{cases} E[X-t \mid X>t], & t < t^*; \\ 0, & \text{otherwise,} \end{cases} \qquad t^* = \sup\{t : \bar F(t) > 0\}.

For a second random variable $Y$ on $(\Omega',\nu)$ with mrl function $l$ , $X$ is smaller than $Y$ in the mean residual life order, $X \le_{mrl} Y$ , if $m(t) \le l(t)$ for every $t$ . The hazard rate order, restated in this mission's own namespace (Chapter 1's version cannot be imported — see Formalization scope), is the general, absolute-continuity-free comparison $\bar F(x)\bar G(y) \ge \bar F(y)\bar G(x)$ for all $x \le y$ , where $\bar G$ is $Y$ 's survival function. A random variable $X$ is DMRL (decreasing mean residual life) if its mrl function $m$ is decreasing in $t$ .

Formalization targets

Goal — Theorem 2.A.2

\left(\frac{m(t)}{l(t)}\text{ increases in }t\right)\ \text{and}\ X \le_{mrl} Y \ \implies\ X \le_{hr} Y.

Combined with the companion milestone below, this is a genuine conditional equivalence: under the monotone-ratio hypothesis, $\le_{mrl}$ and $\le_{hr}$ coincide, and in particular $X \le_{mrl} Y \implies X \le_{st} Y$ under that condition. Without the hypothesis, the book states explicitly (the paragraph immediately preceding Theorem 2.A.1) that neither $\le_{st}$ nor $\le_{mrl}$ implies the other.

Milestones, in attack order

Theorem 2.A.1. $X \le_{hr} Y \implies X \le_{mrl} Y$ — the one-directional link that motivates the goal theorem: the hazard rate order, strictly stronger in general, always implies the mean residual life order.
Theorem 2.A.11. If $X$ is DMRL and $Z$ is a nonnegative random variable independent of $X$ , then $X \le_{mrl} X+Z$ — one of the chapter's closure properties (§2.A.3): adding independent nonnegative noise to a DMRL random variable can only increase it in the mean residual life order.

Each milestone is stated exactly as the book states it: no constant is hard-coded, no $O(\cdot)$ or asymptotic approximation is involved, and the goal's monotone-ratio hypothesis is the genuine ratio $m(t)/l(t)$ , not two separately-monotone functions (a different, unrelated condition the book itself does not state).

Significance

The mean residual life order sits at a specific point in the book's own hierarchy of orders: strictly implied by the hazard rate order (Theorem 2.A.1), and — the goal theorem — reversible into the hazard rate order under one extra monotonicity hypothesis on the ratio of the two mrl functions. This "sandwich" structure is exactly the kind of comparison-of-orders result that makes Chapter 1's usual and hazard rate orders (already formalized in Chunk 01 of this series, restated locally here since drafts cannot import each other) into a genuinely connected theory rather than a list of unrelated definitions. The DMRL closure property (Theorem 2.A.11) is separately significant: DMRL is one of the book's standard "aging" notions, used in reliability engineering to model components that wear out over time, and its preservation under adding independent noise is a basic tool for building compound reliability models (e.g. a component with an added, uncorrelated failure mode) from simpler DMRL parts.

No prior art exists on the platform for either order: GET /theorems?q=mean+residual+life returns zero hits, and GET /theorems?q=hazard+rate returns exactly one hit (DQJSQ.theorem2_ifr), an unrelated queueing-theory IFR (increasing failure rate) lemma about patience densities in a fluid queueing model, not this order — it names a different object under a coincidentally similar keyword and is not reused. This mission is a foundational island for the mean residual life order.

Difficulty

The mrl function is a genuinely two-case object: a real conditional expectation on $\{t : \bar F(t) > 0\}$ , and a hard $0$ outside that region. The goal theorem's proof (not formalized here; only the statement is a milestone) differentiates $m$ and $l$ , uses the identity $r(t) = m'(t)/m(t) + 1/m(t)$ relating the mrl function to the hazard rate, and compares the two resulting hazard-rate expressions using the ratio's monotonicity — a genuinely analytic argument, not a routine unfolding of definitions. The chief formalization difficulty is keeping the shape of $\le_{mrl}$ (a pointwise comparison of a derived function) visibly distinct from the function-class shape of $\le_{st}$ used in Chapter 1, since the book explicitly warns that conflating the two orders is a live error (neither implies the other in general) — see Formalization scope below for how each shape is kept separate.

Formalization scope

All three random variables in this mission's milestones are real-valued measurable functions on a MeasureTheory.Measure space, matching this series' Chapter 1 convention (Chunk 01). The mrl function mrl μ X t is defined as if 0 < P{X>t} then (∫ ω in {X>t}, (X ω - t) ∂μ) / P{X>t} else 0, formalizing the case split on $t < t^*$ directly via positivity of the survival probability (its defining equivalent under the survival function's monotonicity) rather than through the derived quantity $t^*$ itself. MrlOrder μ ν X Y is ∀ t : ℝ, mrl μ X t ≤ mrl ν Y t — a direct pointwise comparison of two functions, deliberately kept a different shape from Chapter 1's UsualOrder (a ∀ φ ∈ 𝒞, E[φ∘X] ≤ E[φ∘Y] function-class quantifier), since the book's own warning that $\le_{st}$ and $\le_{mrl}$ neither implies the other is a warning against treating them as interchangeable comparison shapes.

The hazard rate order is restated locally in this chapter's own namespace (StochasticOrders.MeanResidualLife.HazardRateOrder) rather than imported from Chunk 01's StochasticOrders.Usual.HazardRateOrder, because each chapter's mission is drafted and reviewed as an independent Prove2Me proposal and one draft cannot import another draft's unpublished Lean; its definition is identical in shape to Chunk 01's own restatement of the general, absolute-continuity-free survival-function form of $\le_{hr}$ (not the density-ratio form, which requires absolute continuity the book does not assume at this level of generality).

Every milestone that consumes mrl carries explicit Integrable hypotheses on the random variables involved (Integrable X μ, and Integrable Y ν or Integrable Z μ as applicable), formalizing the book's own standing "finite mean" hypothesis from §2.A.1's definition of the mrl function: without it, the Bochner integral inside mrl would return its junk value 0 for a non-integrable variable on some tail set, letting a hypothesis like MrlOrder μ ν X Y hold of a function that is not actually the book's mean residual life function. DMRL μ X is Antitone (mrl μ X), the book's own " $m(t)$ is decreasing in $t$ " in the weak, non-strict monotone sense used throughout the book for "increasing"/"decreasing".

A trivializing formalization this mission rules out: stating the goal theorem with the ratio hypothesis as two separate monotonicity conditions on $m$ and $l$ individually (rather than genuine monotonicity of the ratio $m(t)/l(t)$ on the region where $l(t)>0$ ) would be a different, strictly stronger and easier-to-satisfy hypothesis than the book's own — the milestone here states MonotoneOn (fun t => mrl μ X t / mrl ν Y t) {t | 0 < mrl ν Y t}, the genuine ratio restricted to where the denominator does not vanish, matching Theorem 2.A.2's own " $m(t)/l(t)$ increases in $t$ " verbatim.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer 2007, Chapter 2 (Mean Residual Life Orders), §2.A. https://doi.org/10.1007/978-0-387-34675-5
W. Whitt, "Uniform Conditional Stochastic Order," Journal of Applied Probability, 1980 (characterizations of IFR/DFR by the likelihood ratio order, cited by the book's remarks section as background for the chapter's aging notions).
This series' Chunk 01 (StochasticOrders.Usual), for the usual and hazard rate orders this chapter's own restated definitions parallel.

7 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

First-Order and Stochastic Optimization Methods for Machine Learning VI: The Classic Conditional Gradient MethodTextbook

Motivation

Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when $X$ is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over $X$ — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.

Setting

Fix a nonempty compact convex set $X$ in a real normed space $E$ and a convex $f:X\to \mathbb R$ with $L$ -Lipschitz gradient (Eq. (7.1.4)): $\|f'(x)-f'(y)\|_*\le L\|x-y\|$ . The classic conditional gradient (CndG) method, Algorithm 7.1, sets $x_0\in X$ , $y_0=x_0$ , and for $k=1,2,\dots$ : calls the LO oracle $x_k\in\arg\min_{z\in X}\langle f'(y_{k-1}),z\rangle$ , then sets $y_k=(1-\alpha_k)y_{k-1}+\alpha_kx_k$ for a stepsize $\alpha_k\in[0,1]$ , either the fixed schedule $\alpha_k=2/(k+1)$ (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).

Section 7.1.1.2 extends this to bilinear saddle-point problems, where $f$ itself is the (generally nonsmooth) function $f(x)=\max_{y\in Y}\{\langle Ax,y\rangle-\hat f(y)\}$ (Eq. (7.1.5)) for a compact convex $Y$ and linear operator $A$ . Since $f$ is nonsmooth, the method is applied instead to a family of smooth approximations $f_\eta$ built from a strongly convex $\omega$ on $Y$ (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter $\eta_k$ allowed to vary across iterations rather than being fixed in advance.

Formalization targets

Goal — Theorem 7.1

f(y_k) - f^* \le \frac{2L}{k(k+1)}\sum_{i=1}^k\|x_i-y_{i-1}\|^2.

Supporting milestones, in attack order

Lemma 7.1: the smoothed objective family $f_\eta$ is monotone nondecreasing in $\eta\ge0$ — the one-line fact ( $V(y)-D_Y^2\le0$ pointwise) that licenses a variable, decreasing smoothing schedule $\eta_k$ rather than a schedule fixed in advance from knowledge of the target accuracy.
Theorem 7.2: the saddle-point counterpart of the goal theorem, running the same CndG algorithm on the smoothed gradients $f_{\eta_k}'$ instead of $f'$ directly, with the explicit rate $f(y_k)-f^*\le\frac{2}{k(k+1)}\sum_{i=1}^k[i\eta_iD_Y^2+\frac{\|A\|^2}{\sigma_v\eta_i} \|x_i-y_{i-1}\|^2]$ .

Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances $\sum\|x_i-y_{i-1}\|^2$ , not a diameter-based simplification (see Difficulty).

Significance

This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based $O(LD_X^2/\varepsilon)$ complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).

No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of 2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art in MODERATION_NOTES.md).

Difficulty

The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or (7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's own proof resolves this by a single observation used for both policies at once: $f(y_k)\le f(\tilde y_k)$ for $\tilde y_k$ the point the fixed schedule $\gamma_k=2/(k+1)$ would have produced — trivially by equality under (7.1.9), or because $y_k$ is chosen to minimize $f$ over the entire line segment under (7.1.10), of which $\tilde y_k$ is one point. This mission's hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof uses and genuinely covers both policies, rather than picking one arbitrarily.

A second difficulty is not collapsing $\sum_{i=1}^k\|x_i-y_{i-1}\|^2$ into a diameter bound $kD_X^2$ inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.

Formalization scope

conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness (x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still included as a hypothesis, matching the book's own standing assumption on the problem class, even though it is not itself needed to derive the stated conclusion from the other hypotheses.

smoothed_objective_monotone and saddle_point_cndg_rate realize $f_\eta$ / $f$ via sSup of the image of $Y$ under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...} definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a "bilinear saddle-point objective" structure — no other item in this mission reuses that definition verbatim, so per this series' convention (no shared substrate bundled into a structure unless reused), it is inlined at each use.

A trivializing formalization this mission rules out: stating the LO oracle via an $\varepsilon$ -approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the chapter, not selected here).

Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of "LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object, a substantially different and more involved formalization task than the two upper-bound convergence theorems selected here; named per Hard Rule 7 rather than approximated. The d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.

Selected references

G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 7, §7.1.1. https://doi.org/10.1007/978-3-030-39568-1
M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly, 3(1-2), 1956, pp. 95-110.
M. Jaggi, "Revisiting Frank-Wolfe: projection-free sparse convex optimization," ICML, 2013 (the modern machine-learning revival of the method).

3 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

First-Order and Stochastic Optimization Methods for Machine Learning IV: Variance-Reduced Mirror Descent for Finite-Sum ProblemsTextbook

Motivation

Empirical-risk-minimization objectives in machine learning are finite sums: $\Psi(x) = \frac{1}{m}\sum_{i=1}^m f_i(x) + h(x)$ , one smooth term $f_i$ per training example (or per worker, in a distributed setting), plus a simple nonsmooth regularizer $h$ . Chapter 4's basic stochastic mirror descent handles this by sampling a single random component gradient $\nabla f_{i_t}(x)$ as an unbiased estimator of $\nabla f(x)$ — but that estimator's variance is a constant throughout the algorithm, which caps the achievable convergence rate. Variance-reduced mirror descent asks a sharper question: can an unbiased finite-sum gradient estimator be built whose variance itself vanishes as the algorithm approaches the optimum? The answer — periodic full-gradient snapshots combined with single-component corrections — is the SVRG-style idea this mission formalizes in Lan's general-norm mirror-descent framework, with an explicit, sampling-distribution-dependent constant rather than a generic $O(\cdot)$ .

Setting

Fix a closed convex set $X$ in a real normed space $E$ , and the finite-sum composite problem $\min_{x\in X}\{\Psi(x):=f(x)+h(x)\}$ (Eq. (5.3.1)), where $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ is the average of $m$ smooth convex component functions, each with $L_i$ -Lipschitz gradient $\nabla f_i$ ( $\|\nabla f_i(x)-\nabla f_i(y)\|_*\le L_i\|x-y\|$ ), and $h$ is a simple, possibly nondifferentiable convex function. $f$ is possibly $\mu$ -strongly convex, $\mu\ge0$ (Eq. (5.3.2)); this mission's goal takes $\mu=0$ (§5.3.1, "Smooth Problems Without Strong Convexity"). A fixed probability distribution $Q=\{q_1,\dots,q_m\}$ on the component indices governs the algorithm's random sampling, and

L_Q := \frac{1}{m}\max_{i=1,\dots,m}\frac{L_i}{q_i}

is the section's key aggregate smoothness constant (Eq. (5.3.4)), replacing the plain average $L$ wherever component-wise variance enters the analysis. Variance-reduced mirror descent (Algorithm 5.6) is a multi-epoch method: each epoch of length $T_s$ recomputes a full gradient $\nabla f(\tilde x)$ at a snapshot point $\tilde x$ , then runs $T_s$ inner iterations using the estimator $G_t := \big(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(\tilde x)\big)/(q_{i_t}m) + \nabla f(\tilde x)$ and the mirror-descent-with-composite-term update $x_{t+1}:=\arg\min_{x\in X}\{\gamma[\langle G_t,x\rangle+h(x)]+V(x_t,x)\}$ , where $V$ is the Bregman divergence of a fixed distance-generating function, exactly as in Chapters 3-4.

Formalization targets

Goal — Corollary 5.8

With $\theta=1$ , $\gamma=1/(16L_Q)$ , and the doubling epoch schedule $T_1=7$ , $T_s=2T_{s-1}$ (Eq. (5.3.17)),

\mathbb E[\Psi(\bar x_S)-\Psi(x^*)] \le \frac{8}{2^{S-1}}\left[\frac{11}{4}\big(\Psi(x_0)-\Psi(x^*)\big)+16L_Q\,V(x_0,x^*)\right]

for every epoch count $S\ge1$ , where $\bar x_S$ is the weighted average of the epoch snapshots (Eq. (5.3.16)).

Supporting milestones, in attack order

Lemma 5.12 — the per-component gradient-variation bound $\frac1m\sum_i\frac1{mq_i}\|\nabla f_i(x)-\nabla f_i(x^*)\|_*^2 \le 2L_Q[\Psi(x)-\Psi(x^*)]$ , the basic smoothness consequence from which the estimator's variance bound is built.
Lemma 5.13 — unbiasedness ( $\mathbb E[\delta_t]=0$ ) and two variance bounds ( $\mathbb E[\|\delta_t\|_*^2]\le 2L_Q[\dots]$ and $\le 4L_Q[\dots]$ ) for the variance-reduced estimator's error $\delta_t:=G_t-\nabla f(x_t)$ .
Lemma 5.14 — the one-step progress bound combining Lemma 5.13's variance control with the mirror-descent update's three-point inequality.
Theorem 5.6 — the general epoch-level convergence bound (with an arbitrary epoch-length schedule $T_s$ and stepsize $\gamma$ satisfying $4L_Q\gamma\le1$ ) that Corollary 5.8 instantiates.

Every constant is exactly the book's: $L_Q$ 's own sampling-distribution-dependent definition (never specialized to uniform $q_i=1/m$ ), and Corollary 5.8's explicit $8/2^{S-1}$ , $11/4$ , $16L_Q$ — not a generic $O(\cdot)$ — are all taken verbatim.

Significance

This is the series' first genuinely finite-sum result: unlike Chapters 3-4's single abstract objective $f$ , here $f$ is structurally a named average of $m$ component functions, and the sampling distribution $\{q_i\}$ over those components is a first-class free parameter of both the algorithm and the analysis (not fixed to uniform sampling) — $L_Q$ itself depends on this choice, and a formalization that hard-codes $q_i=1/m$ would understate what Lemma 5.12's own proof needs. Getting Theorem 5.6/Corollary 5.8 right also requires keeping two nested indices straight: inner iterations $t$ within an epoch, and outer epoch counts $s$ , with the convergence bound stated in terms of the epoch count $S$ alone — and keeping the two "gap" quantities $\Psi(x_0)-\Psi(x^*)$ (an objective-value gap) and $V(x_0,x^*)$ (a Bregman-divergence gap) distinct throughout, since they enter Corollary 5.8's final bound with different explicit coefficients ( $11/4$ vs. $16L_Q$ ) and neither generically bounds the other.

No result on the platform models a finite-sum objective with $m$ named component functions sampled by a general index distribution $\{q_i\}$ , a variance-reduction snapshot/anchor point, or this specific SVRG-style estimator, as of 2026-09-18 (q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, q=mirror descent finite sum — see Prior art below).

Difficulty

The central difficulty is Theorem 5.6's own epoch-weight sequence $w_s$ : the book defines $w_s:=(1-4L_Q\gamma)(T_{s-1}-1)-4L_Q\gamma T_s$ explicitly only for $s\ge2$ (Eq. (5.3.14)), yet the displayed sums $\sum_{s=1}^S w_s$ in (5.3.15)-(5.3.16) run from $s=1$ . A 2026-09-19 revision found that this, combined with the epoch snapshot $\tilde x_s$ being constrained only by membership in $X$ and not tied to the algorithm's own dynamics, made the originally drafted statements false, not merely incomplete: an adversarial, unboundedly-large- $\Psi$ , $\omega$ -independent $\tilde x_1$ together with $w_1\to\infty$ violates the stated conclusion. The fix restores the connection via an auxiliary epoch-boundary sequence and the per-epoch progress inequality Theorem 5.6's own proof derives from Lemma 5.14 (see epoch_convergence_bound's hepoch hypothesis), and resolves $w_1$ by extending (5.3.14)'s domain to $s\ge1$ via a fixed "epoch 0" length $T_0$ — w_1 is no longer left free beyond positivity. finite_sum_variance_reduced_rate instantiates $T_0:=T_1/2=3.5$ concretely, reproducing the arithmetic Corollary 5.8's own proof is internally consistent with ( $w_1 = 3/4(3.5-1)-1/4\cdot7 = 1/8$ , matching the closed form $(1/8)T_1-3/4=1/8$ ) — this was previously only a documented-but-unresolved observation, not yet a stated hypothesis.

Formalization scope

All five items are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching the mirror-descent chunks' general-norm convention (never specialized to Euclidean space or squared distance) — $V$ is a free two-point function throughout, and each $\nabla f_i$ , $\nabla f$ , $G_t$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed. This is the trivializing formalization this mission rules out: hard-coding $q_i=1/m$ (uniform sampling) or $V(x,y)=\frac12 \|x-y\|^2$ (Euclidean Bregman divergence) would understate both $L_Q$ 's dependence on the sampling distribution (the whole point of Lemma 5.12's bound) and the general-norm apparatus the rest of this book series shares.

Ψ(x_0)-Ψ(x^*) and V(x_0,x^*) are kept as two syntactically distinct terms throughout — never conflated or bounded one by the other — matching Corollary 5.8's own two separate coefficients. Corollary 5.8's own explicit constants ( $8/2^{S-1}$ , $11/4$ , $16L_Q$ ) are stated verbatim rather than left as an unspecified $O(\cdot)$ , per Hard Rule 6.

Left out of scope, for time: the gradient-computation-count complexity bound (Eq. (5.3.19), an $O(\cdot)$ statement about total oracle calls, not a convergence-rate inequality on $\Psi$ ) and §5.3.2's strongly-convex case (Theorem 5.7, a geometric-decay bound $\Delta_s\le\rho\Delta_{s-1}$ under $\mu>0$ ) are natural continuations reusing this mission's variance_reduced_progress_bound milestone, not attempted here.

Prior art

q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, and q=mirror descent finite sum were all searched on 2026-09-18. The only topically-adjacent hit across all six queries is ShiOptRates.Stochastic.variance_purchase_ classical ("Classical variance reduction is cost-neutral..."), which models plain minibatch SGD on a smooth objective with an i.i.d.-noise oracle characterized by a single scalar variance $\hat\sigma^2$ and a minibatch-size trade-off — no finite-sum structure with $m$ named component functions, no sampling distribution $\{q_i\}$ , no snapshot/anchor point $\tilde x$ , and a different question (cost-neutrality of minibatch size vs. this mission's convergence rate for a fixed variance-reduction scheme). Not reused; every item in this mission is drafted fresh.

Selected references

G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 5, §5.3. https://doi.org/10.1007/978-3-030-39568-1
R. Johnson, T. Zhang, "Accelerating stochastic gradient descent using predictive variance reduction," Advances in Neural Information Processing Systems (NeurIPS), 2013 (the SVRG estimator this section's gradient estimator generalizes to the composite mirror-descent setting).
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.

5 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

First-Order and Stochastic Optimization Methods for Machine Learning III: Stochastic Mirror DescentTextbook

Motivation

Machine learning's canonical training objective — minimize an expected or empirical risk over a data distribution — is almost never observed exactly: at each step an algorithm sees only a noisy gradient sample (a minibatch gradient, a single-example gradient, a simulation draw). Stochastic mirror descent (Nemirovski, Juditsky, Lan & Shapiro 2009) is the modern, general-norm answer to "what happens to first-order convergence guarantees when the gradient itself is a random variable": it takes the deterministic mirror-descent scheme of the previous chapter and replaces the exact subgradient with an unbiased stochastic estimate, and asks for both an expected convergence rate and, when the noise is well-behaved, an explicit probability-of-large-deviation guarantee. This is the theoretical backbone of stochastic gradient descent as used in practice.

Setting

Fix a nonempty closed convex set $X$ in a real normed space $E$ , and a convex $f:X\to\mathbb R$ with $f^*:=\min_{x\in X}f(x)$ and $x^*$ an arbitrary minimizer, exactly as in Chapter 3. A stochastic oracle $G(x,\xi)$ , queried at a point $x$ with a fresh random sample $\xi$ , returns an estimate of a subgradient $g(x)\in\partial f(x)$ : $\mathbb E[G(x,\xi)] = g(x)$ (unbiasedness), $\|g(x)\|_*\le M$ (a dual-norm Lipschitz bound, Eq. (4.1.7)), and $\mathbb E[\|G(x,\xi)-g(x)\|_*^2]\le\sigma^2$ (a second-moment/variance bound). The stochastic mirror-descent update is exactly Chapter 3's mirror-descent update with $G_t := G(x_t,\xi_t)$ in place of the deterministic $g_t$ : $x_{t+1} := \arg\min_{x\in X}\gamma_t\langle G_t,x\rangle + V(x_t,x)$ (Eq. (4.1.6)), where $V$ is the Bregman divergence of a fixed distance-generating function $\nu$ .

Formalization targets

Goal — Theorem 4.1

\mathbb E[f(\bar x^k_s)] - f^* \le \Big(\sum_{t=s}^k\gamma_t\Big)^{-1}\Big(\mathbb E[V(x_s,x^*)] + (M^2+\sigma^2)\sum_{t=s}^k\gamma_t^2\Big).

Supporting milestones, in attack order

Lemma 3.4, invoked for the stochastic update: the same three-point inequality as the deterministic mirror-descent update, restated with the stochastic gradient functional $G_t$ in place of $g_t$ — the book's own remark ("It can be easily seen that the result in Lemma 3.4 holds with $g_t$ replaced by $G_t$ ") is exactly what licenses treating this as the same algebraic fact for a fixed sample path.
Lemma 4.1: the martingale-difference deviation bound, a Chernoff-type concentration inequality for a conditionally sub-Gaussian martingale-difference sequence — the chapter's general-purpose probabilistic tool, proved independently of the optimization setting.

Every constant is exactly the book's; $M^2+\sigma^2$ (not a generic $O(\cdot)$ ) is the goal's own noise-dependent constant, taken verbatim.

Significance

This is the first mission in the series to leave the purely deterministic, real-analytic setting of Chapters 2-3 and formalize a genuinely probabilistic convergence guarantee: an expectation taken over an entire random algorithm trajectory $\xi_1,\dots,\xi_k$ , not merely over a single random variable. Getting the goal theorem's statement right requires being explicit about exactly which quantities are random (the iterates $x_t$ , hence $f(\bar x_s^k)$ and $V(x_s,x^*)$ ) and which are deterministic constants fixed in advance ( $M,\sigma,\gamma_t$ ), and about the precise mathematical content of "the stochastic gradient's bias vanishes after conditioning on the past" — Lemma 4.1 is included specifically because it is the general machine that makes that vanishing rigorous, independent of the optimization application.

No result matching stochastic mirror descent, Assumption 4's sub-Gaussian/light-tail condition, or this martingale-difference concentration lemma exists on the platform as of 2026-09-18 (q= stochastic gradient, q=stochastic mirror descent, q=martingale, q=sub-Gaussian — see Prior art below for what these queries actually returned).

Difficulty

The central difficulty is disentangling which facts in the chapter's proof genuinely need measure theory and which do not. The per-step algorithmic relations — $x_{t+1}$ 's minimality, $f$ 's subgradient inequality at $x_t$ , the dual-norm bound on $g$ — hold for every sample path individually and are formalized pointwise in $\omega$ , exactly as chunk 03-deterministic formalizes its deterministic analogues; only the second-moment bound and the final expectation inequality are genuine integrals. The one place this pointwise treatment cannot simply mirror the deterministic case is the noise cross-term $\mathbb E[\gamma_t\langle\delta_t,x_t-x^*\rangle]=0$ : in the book's proof this vanishes because $\delta_t=G_t-g(x_t)$ is conditionally mean-zero given the past and $x_t$ is a function of the past (the martingale-difference property, via the tower property of conditional expectation) — a genuinely non-pointwise fact. Rather than thread an explicit filtration through the goal theorem's own statement (which Lemma 4.1 already does, as the chapter's dedicated home for that machinery), the goal theorem takes this post-tower-property consequence directly as a named hypothesis (hcross); see Formalization scope.

Formalization scope

stochastic_mirror_iterate_three_point and stochastic_mirror_descent_bound are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching chunk 03-deterministic's general-norm milestones (mirror_iterate_three_point/mirror_descent_bound) rather than the Euclidean/inner-product specialization of that chunk's §3.1 items — Chapter 4's own stochastic mirror descent is presented directly in the general-norm framework of §3.2, with no Euclidean-only warm-up. $V$ is left a free two-point function (never hard-coded to a squared Euclidean distance), and the stochastic gradient $G_t$ and the subgradient selector $g$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed — the same trivializing formalization chunk 03-deterministic rules out (specializing $V$ to the Euclidean case) applies here and is ruled out the same way.

martingale_difference_deviation_bound (Lemma 4.1) is a standalone probabilistic result, formalized with Mathlib's MeasureTheory.Filtration and condExp machinery: the sequence $\xi_{[t]}$ 's generated filtration, $\zeta_t$ 's $\mathcal F_t$ -measurability, and the two conditional-expectation hypotheses (conditional mean zero, conditional sub-Gaussian tail) are all literal translations of the book's own E|ξ[t-1] notation.

Left out of scope, for time: Assumption 4 (the light-tail/sub-Gaussian oracle assumption), Proposition 4.1 (the large-deviation bound under Assumption 4, which chains Lemma 4.1's concentration bound with the constant stepsize policy (4.1.11) and a second Markov-inequality argument on $\sum\gamma_t^2\|\delta_t\|_*^2$ ), Lemma 4.2 and Theorem 4.2 (the smooth- $f$ case, §4.1.2, requiring a separate recursion and averaging convention $x_t^{av}$ ). All four are natural continuations reusing this mission's stochastic_mirror_iterate_three_point and/or martingale_difference_deviation_bound; a later mission or an amendment to this one could add them without touching what is here. Per Hard Rule 7 (faithfulness over coverage), a genuinely faithful formalization of Proposition 4.1 in particular — which needs Assumption 4's own conditional-MGF hypothesis threaded consistently with Lemma 4.1's, plus the constant-stepsize substitution and a second concentration argument — was judged to need more time than this session's budget allowed to do without shortcuts; it is named here rather than approximated.

Selected references

G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 4, §4.1. https://doi.org/10.1007/978-3-030-39568-1
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.
H. Robbins, S. Monro, "A stochastic approximation method," Annals of Mathematical Statistics, 22(3), 1951, pp. 400-407 (origin of stochastic approximation).

3 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization+1·Captain: mikedeng1

Introduction to Stochastic Programming III: The L-Shaped Method and Its Finite ConvergenceTextbook

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$ , then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$ , so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$ , a batch of second-stage linear programs that either certify $x$ 's second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$ . Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$ , and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$ ), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

Q(x, \xi_k) = \min_{y \ge 0} \{ q_k^\top y \mid W y = h_k - T_k x \},

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$ 's columns (where $m_2$ is $W$ 's row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$ , and when $b$ attains the true optimum of $Q(x,\xi_k)$ , LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$ .

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

Step 1 solves the current master program (the $K_1$ -feasible $x$ , plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}

\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$ ) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,

\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,

\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$ , checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$ " — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$ "; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible- $x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

6 thms3 active users

Completed

Optimization·Captain: mikedeng1

Supermodularity and Complementarity II: Topkis's Monotonicity Theorem for Parameterized OptimizationTextbook

Motivation

A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).

Setting

Let $X$ be a lattice: a partially ordered set $(X, \preceq)$ in which every pair $x, x'$ has a join $x \vee x'$ and a meet $x \wedge x'$ . A real-valued function $f : X \to \mathbb{R}$ is supermodular on $X$ if $f(x') + f(x'') \le f(x' \vee x'') + f(x' \wedge x'')$ for all $x', x'' \in X$ ; this is the same relativized notion (SupermodularOn) used, with $S = X$ , throughout chunk I of this series.

Now let $T$ also be a partially ordered set (the parameter set), and let $f : X \times T \to \mathbb{R}$ be a real-valued function of the pair $(x, t)$ . $f$ has increasing differences in $(x, t)$ if, for every $t' \prec t''$ in $T$ , the map $x \mapsto f(x, t'') - f(x, t')$ is monotone (order-preserving) in $x$ ; equivalently, the marginal gain from raising $t$ is itself increasing in $x$ . Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering $\sqsubseteq$ from chunk I: for $A, B \subseteq X$ , $A \sqsubseteq B$ holds when $a \wedge b \in A$ and $a \vee b \in B$ for all $a \in A$ , $b \in B$ .

Formalization targets

Goal — Theorem 2.8.2 (Topkis's theorem)

Let $X$ and $T$ be lattices, let $S$ be a sublattice of the product lattice $X \times T$ , and let $S_t = \{x \in X : (x, t) \in S\}$ be the section of $S$ at $t \in T$ . If $f : X \times T \to \mathbb{R}$ is supermodular on $S$ (jointly in the pair $(x, t)$ ), then

t \;\longmapsto\; \operatorname{argmax}_{x \in S_t} f(x, t)

is increasing in $t$ , with respect to $\sqsubseteq$ , on $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x, t) \neq \emptyset\}$ .

Theorem 2.8.1 (the underlying, more elementary sufficient condition)

With $S_t \subseteq X$ increasing in $t$ (with respect to $\sqsubseteq$ ), $f(x,t)$ supermodular in $x$ for each fixed $t$ , and $f(x,t)$ having increasing differences in $(x,t)$ on $X \times T$ , the same conclusion — $t \mapsto \operatorname{argmax}_{x \in S_t} f(x,t)$ increasing in $\sqsubseteq$ — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of $X \times T$ automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.

Theorem 2.8.4 (strict strengthening)

Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: $t' \prec t''$ , $x' \in \operatorname{argmax}_{x \in S_{t'}} f(x,t')$ , and $x'' \in \operatorname{argmax}_{x \in S_{t''}} f(x,t'')$ together force $x' \preceq x''$ — a genuinely stronger conclusion than $\sqsubseteq$ alone gives.

A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that $\operatorname{argmax}_{x \in X} f(x)$ is a sublattice of $X$ whenever $f$ is supermodular on $X$ — the structural fact that makes it meaningful to compare optimal-solution sets with $\sqsubseteq$ in the first place.

Significance

The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.

Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative- statics result of this shape: the closest neighboring material (order-preserving maps, MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This mission is the first formalization of Topkis's theorem on this platform and introduces the increasing-differences vocabulary (IncreasingDifferencesOn, StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs, supermodular games) reuse directly.

Difficulty

The natural first idea — differentiate $f$ in $x$ , set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and $\operatorname{argmax}_{x \in S_t} f(x,t)$ need not be a single point. The correct argument instead compares two arbitrary elements $x' \in S_{t'}$ , $x'' \in S_{t''}$ directly through the supermodularity inequality applied to the pair $(x', t')$ against $(x' \vee x'', t')$ (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from $t'$ to $t''$ inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order $\sqsubseteq$ , not a claim that some selection $t \mapsto x(t)$ is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.

Formalization scope

$X$ and $T$ are kept as abstract Lattice/PartialOrder types throughout, matching the book's own generality — Theorem 2.8.1's and 2.8.2's $\mathbb{R}^n$ / $\mathbb{R}^m$ corollary via second partial derivatives (discussed in the book's prose immediately after Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here. Supermodularity, increasing differences, and strictly increasing differences are each formalized as a single relativized definition (SupermodularOn f S, IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same declaration expresses both "supermodular on the whole lattice $X$ " (used by Theorem 2.7.1 and Theorem 2.8.1's per- $t$ hypothesis) and "jointly supermodular on a sublattice $S$ of $X \times T$ " (Theorem 2.8.2) — a formalization that instead only ever supermodularized $f(\cdot, t)$ for fixed $t$ would collapse Theorem 2.8.2's genuinely joint hypothesis into a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk brief warns against. $\operatorname{argmax}_{x \in S_t} f(x,t)$ is written out as the set of $x \in S_t$ that dominate every other element of $S_t$ under $f(\cdot, t)$ , and every conclusion is stated only for pairs $t \preceq t'$ at which both argmax sets are assumed nonempty — matching the book's own restriction to $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x,t) \neq \emptyset\}$ , since $\sqsubseteq$ holds vacuously whenever either side is empty. This mission depends on chunk I's InducedSetOrder; it introduces no reusable infrastructure beyond its own three definitions, which later missions in the series (matching, MDPs, supermodular games) are expected to import directly rather than redefine.

Selected references

Topkis, D. M., Minimizing a submodular function on a lattice, Operations Research 26(2), 1978, pp. 305–321. https://doi.org/10.1287/opre.26.2.305
Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.6–2.8.
Milgrom, P. and Shannon, C., Monotone comparative statics, Econometrica 62(1), 1994, pp. 157–180. https://doi.org/10.2307/2951479
Milgrom, P. and Roberts, J., Rationalizability, learning, and equilibrium in games with strategic complementarities, Econometrica 58(6), 1990, pp. 1255–1277. https://doi.org/10.2307/2938316

7 thms3 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: Shuze Chen

Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$ ; finite nonempty control sets $U(i)$ ; costs $g(i,u)$ ; sub-stochastic transitions $p_{ij}(u) \ge 0$ , $\sum_j p_{ij}(u) \le 1$ , the deficit being the termination probability (BertsekasSSPModel). Operators

(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$ -stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$ , every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$ ). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$ -stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$ -stage contraction, uniformly over the finitely many $m$ -stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$ -stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$ ). For the average-cost results the associated-SSP construction (stop on reaching $s$ ) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

8 thms3 active usersReviewed

Operations Research

Missions

Generalization Bounds in the Predict-then-Optimize Framework II: Margin-Based Generalization Bound for the SPO Loss under the Strength PropertyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4, second display (pp. 19–20)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Local Search Heuristics for k-Median and Facility Location Problems IV: Local Search with Multi-Copy Moves for Capacitated Facility Location Has Locality Gap 4Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Local Search Heuristics for k-Median and Facility Location Problems I: Single-Swap Local Search for k-Median Has Locality Gap 5Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Jointly Constrained Biconvex Programming II: The Convex-Envelope Branch-and-Bound Algorithm Converges to a Global SolutionResearch Paper

Motivation

Setting

Formalization targets

Goal: convergence to a global solution

Milestones

Significance

Difficulty

Formalization scope

Selected references

Jointly Constrained Biconvex Programming I: A Biconcave Function Attains Its Minimum on the BoundaryResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 274)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multi-armed Bandit Allocation Indices VI: Bandit Sampling Processes, Favourable Priors and Invariance of the IndexTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multi-armed Bandit Allocation Indices V: Restless Bandits, Indexability and Whittle Indices for Monotone ModelsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multi-armed Bandit Allocation Indices IV: The Achievable Region, Generalized Conservation Laws and the Adaptive Greedy AlgorithmTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.5

Milestones

Significance

Difficulty

Supporting dual representations of $W_p$ — Theorems 1 and 2