Completed

Optimization Probability·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains IV: Backorder Convexity and Everett's TheoremTextbook

Motivation

Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the $(s-1, s)$ policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level $s$ . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.

The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson $(s-1,s)$ model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.

Setting

A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate $\lambda > 0$ . An order is for $j$ units with probability $u_j$ , where $u_0 = 0$ and the mean order size $\bar u = \sum_j j u_j$ is finite (compound Poisson demand; simple Poisson demand is $u_1 = 1$ ). Resupply times have mean $\bar\tau > 0$ . The steady-state probability that $x$ units are in resupply is

p(0 \mid \lambda\bar\tau) = e^{-\lambda\bar\tau}, \qquad p(x \mid \lambda\bar\tau) = \sum_{j \ge 1} e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^j}{j!}\,u^{(j)}_x \quad (x \ge 1),

where $u^{(j)}_x$ is the probability that $j$ orders total $x$ units. In this mission $p(\cdot \mid \lambda\bar\tau)$ is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is $\mu = \lambda\bar\tau\bar u$ , and the book also writes $p(x \mid \mu)$ .

For a stock level $s \in \{0, 1, 2, \dots\}$ :

the ready rate is $R(s) = \sum_{x \le s} p(x \mid \lambda\bar\tau)$ ;
the expected backorders are $B(s) = \sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$ ;
the expected on-hand inventory is $\sum_{x \le s}(s - x)\,p(x \mid \lambda\bar\tau)$ ;
under simple Poisson demand the fill rate is $F(s) = \sum_{x < s} p(x \mid \lambda\bar\tau)$ .

Forward differences are $\Delta f(s) = f(s+1) - f(s)$ and $\Delta^2 f(s) = \Delta f(s+1) - \Delta f(s)$ ; discrete convexity means $\Delta^2 f \ge 0$ .

With $n$ items, unit costs $c_i > 0$ and budget $b$ , Problem 4 (3.40) is

\min \sum_i B_i(s_i) \quad \text{s.t.} \quad \sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le b,\quad s_i \in \{0,1,\dots\}.

For a multiplier $\theta > 0$ , the item-wise criterion defines $s_i^*(\theta)$ as the least $s$ with $\sum_{x \le s} p(x \mid \mu_i) \ge 1/(1 + \theta c_i)$ , and $C(\theta) = \sum_i c_i\,[s_i^*(\theta) - \mu_i + B_i(s_i^*(\theta))]$ .

Formalization targets

Goal: the Lagrangian stock levels solve Problem 4

For every $\theta > 0$ , each $s_i^*(\theta)$ exists and

\sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le C(\theta) \ \Longrightarrow\ \sum_i B_i(s_i^*(\theta)) \le \sum_i B_i(s_i)

for every vector $s$ of nonnegative integer stock levels. That is, $s^*(\theta)$ is optimal for Problem 4 at budget $b = C(\theta)$ . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.

Milestones

Section 3.3, p. 53: $\Delta F(s) = p(s \mid \lambda\bar\tau)$ and $\Delta^2 F(s) = p(s \mid \lambda\bar\tau)\,(\lambda\bar\tau/(s+1) - 1)$ , so under simple Poisson demand $F$ is discretely concave exactly on $s \ge \lfloor\lambda\bar\tau\rfloor$ (resp. $s \ge \lambda\bar\tau - 1$ for integer $\lambda\bar\tau$ ).
Section 3.3, p. 55: $\Delta B(s) = -(1 - R(s))$ and $\Delta^2 B(s) = p(s+1 \mid \lambda\bar\tau)$ .
Theorem 10 (Everett), p. 57.
Section 3.4.2, p. 60: $E[\text{On-hand}] = s - \lambda\bar\tau\bar u + B(s)$ .
Section 3.4.2, p. 61: the least $s$ with $R(s) \ge 1/(1+\theta c)$ minimizes $f(s) = (1 + \theta c)B(s) + \theta c s$ .
Section 3.4.2, p. 61: $s^*(\theta)$ and $C(\theta)$ are nonincreasing in $\theta$ .
Section 3.4.2, p. 63: at $\theta_{\max} = \max_i c_i^{-1}(1/p(0 \mid \mu_i) - 1)$ every $s_i^*(\theta_{\max}) = 0$ .
Section 3.4.3, p. 65: every solution produced by the greedy marginal-analysis rule for Problem 5 (3.41), maximum average fill rate subject to $\sum_i c_i s_i \le b$ and $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ , is optimal at the budget it uses.

Significance

The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, $s \ge \lfloor\lambda\bar\tau\rfloor$ , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.

All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.

Difficulty

The algebra of first differences is elementary; the difficulties are elsewhere. $B(s)$ is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying $\sum_x x\,p(x \mid \lambda\bar\tau)$ with $\lambda\bar\tau\bar u$ , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of $s^*(\theta)$ requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every $F_i$ is concave; dropping the floor constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ makes it false.

Formalization scope

Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields $\lambda, \bar\tau > 0$ , an order-size distribution $u$ with $u_0 = 0$ , $u_j \ge 0$ , $\sum_j u_j = 1$ , and summable $j u_j$ (the finite mean is added: without it $B$ is infinite). Expected on-hand inventory is the finite sum $E[(s - X)^+]$ . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).

Pinnings and deviations, each stated in the item's Formalization Note:

$\theta > 0$ and $c > 0$ . The book allows $\theta \ge 0$ in (3.38); at $\theta = 0$ the threshold $1$ is never reached and $f = B$ has no minimizer.
Theorem 10 without convexity and for an arbitrary set $S$ : the book assumes $f, g$ convex, but its proof does not use it and the applications are to integer vectors (labelled generalization).
$B$ 's identities for compound Poisson demand. The book derives them under simple Poisson demand and uses them for compound demand on p. 61; strict convexity and strict decrease are stated only for simple Poisson demand, as in the book.
Optimality is always against every feasible vector, never an infimum; the greedy procedure is a relation on sequences, covering every tie-breaking rule.
Problem 5 keeps the constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ .

A trivializing formalization is ruled out: the goal is stated for the book's own backorder function $B$ built from the compound Poisson law, not for an arbitrary convex function nor for a $B$ defined through its differences.

Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 3, pp. 47–65. https://doi.org/10.1007/b138879
H. Everett III, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Operations Research 11(3):399–417, 1963. https://doi.org/10.1287/opre.11.3.399
B. L. Fox and D. M. Landi, Searching for the multiplier in one-constraint optimization problems, Operations Research 18(2):253–262, 1970. https://doi.org/10.1287/opre.18.2.253
G. J. Feeney and C. C. Sherbrooke, The (s−1, s) inventory policy under compound Poisson demand, Management Science 12(5):391–411, 1966. https://doi.org/10.1287/mnsc.12.5.391

13 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Introduction to the Scenario Approach II: Violation Guarantees after Discarding k ConstraintsTextbook

Motivation

Decisions under uncertainty are often required to satisfy a constraint $\theta \in \Theta_\delta$ that depends on a random parameter $\delta$ , and requiring it for every possible $\delta$ is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of $\delta$ by $N$ independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.

Enforcing all $N$ sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards $k$ of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.

Setting

A decision $\theta$ ranges over $\mathbb R^d$ (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain $\Theta$ and a linear cost $c^{\mathsf T}\theta$ . An uncertain parameter $\delta$ takes values in a measurable space $\Delta$ with probability $\mathbb P$ , and each $\delta$ determines a closed convex constraint set $\Theta_\delta$ . The violation probability of a decision is

V(\theta) = \mathbb P\{\delta \in \Delta : \theta \notin \Theta_\delta\}.

Given independent samples $\delta_1,\dots,\delta_N$ with joint law $\mathbb P^N$ , the scenario program minimizes $c^{\mathsf T}\theta$ over $\theta \in \Theta \cap \bigcap_{i=1}^N \Theta_{\delta_i}$ . For a set $I$ of indexes, the program without the constraints in $I$ minimizes the same cost over $\Theta \cap \bigcap_{i \notin I} \Theta_{\delta_i}$ ; its solution is written $\theta^*_I$ . A removal procedure selects, as a function of the whole sample, a set of $k$ indexes, and $\theta^*_k$ denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the $k$ removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that $\Theta$ and every $\Theta_\delta$ are convex and closed, and Assumption 3.6, that for every sample size $m$ and every sample the scenario program has exactly one solution.

Formalization targets

Goal: Theorem 3.9

For $N \ge d$ , under Assumptions 3.4 and 3.6, for every removal procedure and every $\varepsilon \in [0,1]$ ,

\mathbb P^N\{V(\theta^*_k) > \varepsilon\} \le \binom{k+d-1}{k} \sum_{i=0}^{k+d-1} \binom Ni \varepsilon^i (1-\varepsilon)^{N-i}.

The bound depends on the problem only through $d$ , and on the removal procedure not at all. For $k = 0$ it is Theorem 3.7.

Milestones

Theorem 3.7 (no removal): $\mathbb P^N\{V(\theta^*) > \varepsilon\} \le \sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ , used for the program with the $N-k$ kept constraints.
Eq. (5.11): up to a zero probability set, the event $\{V(\theta^*_k) > \varepsilon\}$ is contained in the union over all $k$ -element index sets $I$ of the events " $\theta^*_I$ violates all constraints in $I$ and $V(\theta^*_I) > \varepsilon$ ".
Eq. (5.13): for a fixed $I$ , the probability of that event equals $\int_{(\varepsilon,1]} \alpha^k F_V(d\alpha)$ , where $F_V$ is the law of $V(\theta^*_I)$ .
Eq. (5.14) and Theorem 3.9 for $d = 2$ : the book's complete proof in the plane.
Eqs. (3.15)–(3.17) and the conclusion of Section 3.3.1: with the explicit level $\varepsilon_k$ of (1.9), the right-hand side of (3.13) is at most $\beta$ .
Theorem 1.2: with probability at least $1-\beta$ , $V(\theta^*_k) \le \varepsilon_k$ , where

\varepsilon_k = \frac{k}{N} + \left[\frac{\sqrt k}{N} + \frac{\sqrt k+1}{N}\left((d-1)\ln(k+d-1) + \frac{d-1}{\sqrt k} + \ln\frac1\beta\right)\right].

Significance

Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of $k$ before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when $k/N$ is held fixed, the violation exceeds the empirical risk $k/N$ by a margin of order $\ln N/\sqrt N$ , only slightly worse than the $1/\sqrt N$ rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).

Theorem 3.9 is proved in the literature for general $d$ (Campi and Garatti, 2011); the textbook proves it for $d = 2$ . To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.

Difficulty

The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to $\theta^*_k$ directly. The argument must pass through all $\binom Nk$ fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor $\binom Nk$ and does not give (3.13). For a fixed index set, the probability that the $k$ removed scenarios are all violated involves the distribution of $V(\theta^*_I)$ , which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function $\alpha \mapsto \alpha^k$ is needed. In general dimension the combinatorial constant $\binom{k+d-1}{k}$ comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d), samples of size $m$ are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:

$d \ge 1$ , $d \le N$ , $k \le N$ and $\varepsilon \in [0,1]$ ;
Assumption 3.6 for every $m$ , including $m = 0$ , and for every sample (not almost every);
the removed constraints are violated with probability one (∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for $1 \le k < N$ (on a sample with all $\delta_i$ equal a kept constraint coincides with a removed one) and would make the results vacuous;
measurability, which the book glosses over (p. 33): the constraint relation $\{(\theta,\delta) : \theta \in \Theta_\delta\}$ is jointly measurable, the solution map of the scenario program with $m$ constraints is measurable for every $m$ , and $\theta^*_k$ is measurable;
for Theorem 1.2 and Section 3.3.1: $k \ge 1$ (formula (1.9) divides by $\sqrt k$ ), $N \ge 1$ , $\beta \in (0,1)$ ; Section 3.3.1 additionally assumes $\varepsilon_k \le 1$ , the range in which its chain of inequalities holds.

Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for $d = 2$ only, as in the book.

A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict $V(\theta^*_k) > \varepsilon$ ; a statement for one fixed rule, or with $\theta^*_k$ unconstrained, would be a different theorem.

A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size $N-k$ , the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general- $d$ counting argument of the cited paper, are welcome.

Selected references

M. C. Campi and S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
M. C. Campi and S. Garatti, A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, Journal of Optimization Theory and Applications 148(2), 257–280, 2011. https://doi.org/10.1007/s10957-010-9754-6
M. C. Campi and S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 1211–1230, 2008. https://doi.org/10.1137/07069821X
G. C. Calafiore and M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

13 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Introduction to the Scenario Approach IV: The FAST Algorithm Keeps the Beta Bound and Adds a Factor (1−ε)^{N₂}Textbook

Motivation

The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample $N$ instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in $N$ and in the number $d$ of optimization variables. To reach a failure level $\varepsilon$ with confidence $1-\beta$ , the number of scenarios grows roughly like $\frac{2}{\varepsilon}\big(\ln\frac1\beta+d-1\big)$ (Theorem 1.1 of the book). The product of $d$ and $1/\varepsilon$ is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.

FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number $N_1$ of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers $N_2$ further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.

Timeline:

2006, Calafiore and Campi: violation bounds for the solution of convex scenario programs.
2008, Campi and Garatti: the exact binomial bound, tight for fully supported problems (Theorem 3.7 of the book).
2014, Carè, Garatti and Campi: FAST and its two-stage bound, Eq. (8.5).
2018, Campi and Garatti's textbook, §8.3, the source of this mission.

Setting

Let $\Delta$ be a measurable space carrying a probability measure $\mathbb P$ , and let $\ell(\nu,\delta)$ be a real loss of a decision $\nu\in\mathbb R^{d-1}$ under the uncertain parameter $\delta\in\Delta$ . As a standing assumption of the book, $\ell(\cdot,\delta)$ is convex for every $\delta$ .

Given scenarios $\delta_1,\dots,\delta_m$ drawn independently from $\mathbb P$ , the scenario program (1.4) is

\min_{\nu\in\mathbb R^{d-1}}\ \Big[\max_{i=1,\dots,m}\ \ell(\nu,\delta_i)\Big].

Its solution is $\nu^*$ and its optimal value $\ell^*$ . Assumption 3.6 requires that for every $m$ and every sample the solution exist and be unique. The pair $(\nu,\ell)$ has $d$ components, and $d$ is the number that enters every bound.

The risk (Definition 8.2) of a decision $\nu$ with cost level $\ell$ is

R(\nu,\ell)=\mathbb P\{\delta\in\Delta:\ \ell(\nu,\delta)>\ell\},

the probability that a new instance costs more than promised. It is the violation $V(\nu,\ell)$ of the epigraphic constraint $\ell\ge\ell(\nu,\delta)$ .

FAST takes $N_1+N_2$ independent scenarios. It solves (1.4) with the first $N_1$ of them, obtaining $\nu^*_{N_1}$ . In the detuning step it then sets

\ell^*_F=\max_{i=1,\dots,N_1+N_2}\ \ell(\nu^*_{N_1},\delta_i),

the smallest level that covers every scenario seen. The output is $(\nu^*_F,\ell^*_F)$ with $\nu^*_F=\nu^*_{N_1}$ .

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

For every $\varepsilon\in[0,1]$ ,

\mathbb P^{N_1+N_2}\{V(\nu^*_F,\ell^*_F)>\varepsilon\}\ \le\ (1-\varepsilon)^{N_2}\sum_{i=0}^{d-1}\binom{N_1}{i}\varepsilon^i(1-\varepsilon)^{N_1-i}.

No relation between $N_1$ and $d$ is required. When $N_1<d$ the sum equals $1$ and the bound reads $(1-\varepsilon)^{N_2}$ .

Milestone: Theorem 3.7 for program (1.4)

The first stage is an ordinary scenario program with $N_1$ scenarios. For $N\ge d$ ,

\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\ \le\ \sum_{i=0}^{d-1}\binom{N}{i}\varepsilon^i(1-\varepsilon)^{N-i},

that is, $R(\nu^*,\ell^*)$ is dominated by a $B(d,N-d+1)$ distribution (recalled on p. 90).

Milestone: the $N_2$ rule

For $\varepsilon,\beta\in(0,1)$ , $N_2\ge\frac1\varepsilon\ln\frac1\beta$ makes the right-hand side of (8.5) at most $\beta$ (p. 95).

Significance

The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With $N_1=Kd$ (the book suggests $K\approx20$ ) and $N_2\ge\frac1\varepsilon\ln\frac1\beta$ , the total number of scenarios is $Kd+\frac1\varepsilon\ln\frac1\beta$ . This is additive in $d$ and $1/\varepsilon$ rather than multiplicative, and the added $N_2$ scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: $\ell^*_F$ is in general higher than the value a classical scenario program with the same confidence would return.

Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The $N_2$ rule is an elementary but explicit sample-size certificate.

Difficulty

The obvious route treats the detuning step as a fresh scenario program with $N_1+N_2$ scenarios and applies Theorem 3.7 to it. That fails: $\nu^*_F$ is not the solution of that program, and Theorem 3.7 with $N_1+N_2$ scenarios gives a bound that is not of the product form (8.5). The level $\ell^*_F$ depends on all $N_1+N_2$ scenarios at once, including those that determined $\nu^*_{N_1}$ , and the map $c\mapsto R(\nu,c)$ is monotone but need not be continuous, so the event $V(\nu^*_F,\ell^*_F)>\varepsilon$ is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.

Formalization scope

Lean representation:

The decision space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin n); the book's $d$ is written $n+1$ , never with natural-number subtraction.
A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same $\mathbb P$ defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.
The maximum in (1.4) and in $\ell^*_F$ is Finset.sup' over a nonempty index set. $\ell^*_F$ runs over all $N_1+N_2$ scenarios, not over the $N_2$ new ones only.
The risk is (P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event $V>\varepsilon$ of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.
The first-stage solution is a map νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.

Hypotheses the book leaves implicit, stated explicitly:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (standing assumption, p. 6).
Existence and uniqueness of the solution (Assumption 3.6) for every $m\ge1$ and every sample. The program with no scenario has no minimum, so $m=0$ is excluded.
$N_1\ge1$ , since the first stage needs a scenario.
$\varepsilon\in[0,1]$ ; for $\varepsilon>1$ the factor $(1-\varepsilon)^{N_2}$ can be negative.
The loss is jointly measurable in $(\nu,\delta)$ and the first-stage solution map is measurable. The book glosses over measurability (p. 6, footnote 1; p. 33).

A formalization that bounds only the $N_2$ new scenarios is ruled out, because $\ell^*_F$ is defined as a maximum over all $N_1+N_2$ scenarios. So is one that takes $\ell^*_F$ as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.

A complete development needs the scenario program in loss form, product-measure conditioning on $\Delta^{N_1}\times\Delta^{N_2}$ , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018, §8.3 and Theorem 3.7. https://doi.org/10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, FAST—Fast Algorithm for the Scenario Technique, Operations Research 62(3):662–671, 2014. https://doi.org/10.1287/opre.2014.1257
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3):1211–1230, 2008. https://doi.org/10.1137/07069821X
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5):742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

6 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory IV: PASTA and the Formulas of Palm CalculusTextbook

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

14 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory III: Stationary Regimes of Stochastic RecurrencesTextbook

Stationary Regimes of Stochastic Recurrences

Background

Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence

W_{n+1} = h(W_n, ξ_n),

driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this mission is about both.

Exact sampling, and what "exact" means

§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a stationary law π, and the classical way to sample it is to run the chain and wait. That gives a sample whose law converges to π and is never equal to it.

Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state, all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started further and further in the past. Once two chains meet they stay together, so eventually all r coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function preserves a partial order with a least and a greatest state, and a single uniform sequence drives every chain, the two extremal chains funnel all the others and their coalescence suffices.

Neither theorem is a statement about a program. Each says that a random variable is almost surely finite, and that another has a distribution equal to π.

Renovating events: sufficient, and then necessary

§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a finite random index.

Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime, reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences with a constant initial condition, strong backwards coupling produces renovating events. So the method characterises stability rather than merely detecting it.

The saturation rule

§2.11 treats the multidimensional case, where the state is a vector and the natural models are monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks it: under homogeneity, monotone and non-expansive are the same property. That is what puts these models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not depend on the initial condition.

The goal

Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues fed by the external stream, measure the departure intensity µ of the saturated system, and declare the network stable when λ < µ. The book is careful that this saturation rule "does not hold for all systems".

Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:

If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1.    If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.

Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.

Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.

What this mission provides

Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.

Formalization scope

The standing assumptions of §2.5.1 (p.104) are part of every §2.5.4 statement: (P⁰, θ) is ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.
Theorem 2.5.4 is stated for {W_n^{[C]}}, the sequence its proof on p.119 builds the renovating events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary 2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the page prints W_n.
Theorem 2.11.2 carries all four limits, a.s. and in expectation, for every integrable ℝ^K-valued random initial condition Y, under the book's linear lower bound E[X_n^{[0]}] > −Cn.
The goal is stated on the Palm space of a stationary ergodic marked point process: T_0 = 0, T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four framework assumptions for every point process. γ(0) is the a.s. limit of Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service, and dropping the link between the points and θ makes the second implication false. Neither is done.
Stating only one of the goal's two implications, or collapsing them into an equivalence, would be a different theorem. Both implications are stated, with the gap between ≥ 1 and > 1 left open.

12 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory II: The Loynes Stability Theorem and CouplingTextbook

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

13 thms2 active usersReviewed

Analysis Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

13 thms2 active usersReviewed

Completed

Analysis Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory I: The Swiss Army Formula of Palm CalculusTextbook

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of `P⁰_N`

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

11 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Linear Programming: Foundations and Extensions V: Convergence Rates of the Path-Following MethodTextbook

Motivation

Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.

Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ . The primal problem is to maximize $c^Tx$ subject to $Ax + w = b$ , $x, w \ge 0$ ; the dual is to minimize $b^Ty$ subject to $A^Ty - z = c$ , $y, z \ge 0$ . A primal–dual point is a quadruple $(x, w, y, z)$ with $x, z \in \mathbb{R}^n$ , $w, y \in \mathbb{R}^m$ ; it is strictly positive, $(x, w, y, z) > 0$ , if every component is. Write $X, W, Y, Z$ for the diagonal matrices of $x, w, y, z$ and $e$ for the all-ones vector. The norms are $\|v\|_1 = \sum_j |v_j|$ and $\|v\|_\infty = \max_j |v_j|$ .

At a point $(x, w, y, z)$ the three measures of progress are the primal infeasibility $\rho = b - Ax - w$ , the dual infeasibility $\sigma = c - A^Ty + z$ , and the complementarity $\gamma = z^Tx + y^Tw$ . Fix parameters $0 < \delta < 1$ and $0 < r < 1$ . One iteration of the method, from a strictly positive point, sets $\mu = \delta\gamma/(n+m)$ , takes any solution $(\Delta x, \Delta w, \Delta y, \Delta z)$ of the Newton system

A\Delta x + \Delta w = \rho, \quad A^T\Delta y - \Delta z = \sigma, \quad Z\Delta x + X\Delta z = \mu e - XZe, \quad W\Delta y + Y\Delta w = \mu e - YWe,

computes the step length

\theta = r\left(\max_{i,j}\left\{\left|\tfrac{\Delta x_j}{x_j}\right|, \left|\tfrac{\Delta w_i}{w_i}\right|, \left|\tfrac{\Delta y_i}{y_i}\right|, \left|\tfrac{\Delta z_j}{z_j}\right|\right\}\right)^{-1} \wedge 1 \qquad (18.7)

(with $\theta = 1$ when all ratios vanish), and moves to $(x + \theta\Delta x, w + \theta\Delta w, y + \theta\Delta y, z + \theta\Delta z)$ . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts $^{(k)}$ denote the quantities at the $k$ -th iterate, and $\theta^{(k)}$ is the step length computed there.

Formalization targets

Goal: Theorem 18.1 with the explicit constant

If $t > 0$ , $M$ is real, and for all $k \le K$ one has $\theta^{(k)} \ge t$ , $\|x^{(k)}\|_\infty \le M$ , $\|y^{(k)}\|_\infty \le M$ , then for all $k \le K$ , with $\tilde t = t(1-\delta)$ ,

\|\rho^{(k)}\|_1 \le (1-t)^k\|\rho^{(0)}\|_1, \qquad \|\sigma^{(k)}\|_1 \le (1-t)^k\|\sigma^{(0)}\|_1, \qquad \gamma^{(k)} \le (1-\tilde t)^k \left(\gamma^{(0)} + \frac{M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)}{\delta t}\right).

Milestones

The one-step identities for the infeasibilities, $\tilde\rho = (1-\theta)\rho$ (18.8) and $\tilde\sigma = (1-\theta)\sigma$ (18.9); the one-step complementarity estimate

\tilde\gamma \le (1 - (1-\delta)\theta)\gamma + M\|\rho\|_1 + M\|\sigma\|_1 \qquad (18.10)

under $\|x\|_\infty, \|y\|_\infty \le M$ ; and the recursion $\gamma^{(k)} \le (1-\tilde t)\gamma^{(k-1)} + M(1-t)^{k-1}(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ (18.11). Two unnumbered statements complete the picture: every iteration has $0 < \theta \le 1$ and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies $|b^Ty - c^Tx| \le \gamma + \|\sigma\|_1\|x\|_\infty + \|\rho\|_1\|y\|_\infty$ (§18.5.3).

Significance

Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor $1 - t$ per iteration while the complementarity, and hence (by the duality-gap estimate) the gap $b^Ty - c^Tx$ , falls only by $1 - \tilde t$ . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.

All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.

Difficulty

The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term $\theta^2(\Delta y^T\rho - \sigma^T\Delta x)$ that has no sign. Bounding it requires relating the size of the step $\theta\Delta$ to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon $K$ is what makes the statement non-trivial.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, $A$ is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case $\theta = 1$ when all ratios vanish, since Lean's r / 0 = 0 would otherwise give $\theta = 0$ . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current $+\ \theta \cdot$ direction. The hypotheses $0 < \delta < 1$ , $0 < r < 1$ (pp. 272–273) are stated in every theorem; $M$ is an arbitrary real number and $K$ a natural number. As in the book, the hypotheses of Theorem 18.1 range over $k \le K$ , so the iteration from index $K$ is part of the data.

Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant $\bar M < \infty$ ". Because $K$ is fixed, that existential is satisfied trivially by $\max_{k \le K}\gamma^{(k)}/(1-\tilde t)^k$ , and a statement with $\exists \bar M$ would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): $\bar M = \gamma^{(0)} + M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)/(\delta t)$ . Eq. (18.11) is stated with the book's $\tilde M = M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ written out.

The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 18, pp. 269–283. https://doi.org/10.1007/978-1-4614-7630-6
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

14 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$ . Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$ , and arc $(i,j)$ carries a cost $c_{ij}$ . The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$ , $-1$ in row $i$ , and $0$ elsewhere. The network flow problem (14.1) is

\text{minimize } c^{T}x\quad\text{subject to}\quad Ax=-b,\ x\ge 0 .

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$ . A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$ , and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$ , a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$ , $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$ , $t\notin C$ , and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$ .

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .

Milestones

Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .

Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
Theorem 15.1, Max-Flow Min-Cut (p. 234):

\max\{x_{ts}\}=\min_C \kappa(C),

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$ , bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
"Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
A basis is $m-1$ linearly independent columns of the $(m-1)$ -row matrix $\tilde A$ , the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$ , and for $k=0<n$ the claim is false. No connectedness is assumed.
For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

7 thms2 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$ , $T_{iG}\ge 1$ is the first passage time to $G$ . The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$ . The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$ . The mean first passage time is $m_{iG}=E[T_{iG}]$ , infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$ . A state $i$ is positive recurrent when $m_{ii}<\infty$ , and the steady state probability is $\pi_i=m_{ii}^{-1}$ . On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$ . The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ . Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$ , and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$ , a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$ . The quantities of $\Gamma_N$ are written $m_{iG}(N)$ , $c_{iG}(N)$ , $\pi_i(N)$ and $J(i)(N)$ . An AS is conforming (for a $z$ standard $\Gamma$ ) if, for large $N$ , $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$ . It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$ .

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$ :

P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$ .

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$ ,

\text{every ATAS that sends excess probability to } G \text{ is conforming},

and if $G\subseteq R$ it is also conforming on $R$ . No rate of convergence and no constants are involved, and $G$ need not contain $z$ .

Milestones

Proposition C.4.2: for fixed $t$ , $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$ ; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$ .
Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$ .
Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$ .
Proposition C.4.6: on a positive recurrent class, convergence of $\pi$ , of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$ , of $c_{zz}$ and of all $c_{iG}$ are equivalent.
Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$ , and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$ .

Further results

Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$ , the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$ .
Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$ , the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$ . First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$ , a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$ , and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$ , $c_{iG}$ , $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$ . $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$ , the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$ . $\Gamma_N$ is built as an MC on the subtype of $S_N$ , and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$ . Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ( $N<N_0$ or a state outside $S_N$ ). For fixed states this affects finitely many $N$ , and all statements are limits, $\liminf$ s or eventual equalities. All convergence is in $[0,\infty]$ . The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$ .

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$ , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$ , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics·Captain: mikedeng1

Theory of Games and Economic Behavior VI: Splitting Sets and the Decomposition Partition of a GameTextbook

Motivation

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$ -person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$ ; and every splitting set is a union of blocks of $\Pi_\Gamma$ . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$ ). Write $-S = I - S$ . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .

For $J \subseteq I$ with complement $K = I - J$ , the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$ -constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$ , for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ( $\ominus$ , $I$ ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( $K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$ ); and the two extreme cases (43:J) ( $\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ( $\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$ . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$ , since a pair $S \subseteq J' \cup J''$ , $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$ .

Formalization scope

Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$ ; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$ ). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$ , and $v$ is a function Finset ι → ℝ.
Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$ ); every other statement holds without it. (43:E) assumes $J \neq \ominus$ , since the book's constituent is a game and has at least one player.
Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$ , $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$ -constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$ .
No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$ , or complements taken in an ambient type larger than $I$ , would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

16 thms2 active usersReviewed

Completed

Convex Optimization Information Theory Linear algebra+1·Captain: naimengye

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$ , and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$ ? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$ , which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$ , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$ . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$ , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$ , sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$ , and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$ , write $F_T c = \sum_{j \in T} c_j v_j$ . A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$ ; with this convention $F_T c$ is just the product $Fc$ . Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$ .

Definition 1.1. For an integer $S$ , the $S$ -restricted isometry constant $\delta_S$ is the smallest quantity such that

(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$ . The $S, S'$ -restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$ . The paper writes $\theta_S$ for $\theta_{S,S}$ . These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$ , and $F$ a real $p \times m$ matrix with $FA = 0$ . Let $S \ge 1$ satisfy

\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}

If $y = Af + e$ where $e$ is supported on a set of size at most $S$ , then $f$ is the unique minimizer of $(P_1')$ .

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$ , and let $c$ be supported on a set $T$ with $|T| \le S$ . Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$ .

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$ ), and the two dual sparse reconstruction properties, Lemma 2.1 ( $\ell^2$ version) and Lemma 2.2 ( $\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$ , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$ , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$ . Given such a $w$ , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$ ; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ( $T_0 \cup T_n$ ) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$ , are what Lemma 2.1 gives for a set of size $S$ ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$ ; the mission states the lemma with $\theta_{S,S'}$ , which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$ , and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$ ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$ . The definitions are total in $S, S'$ , and each theorem carries the paper's domain conditions ( $S \ge 1$ , and $2S \le m$ , $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$ , so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$ ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$ " is a positive function of the real number $\delta_S$ , quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$ , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$ ) belong to a separate mission.

Selected references

E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

9 thms2 active usersReviewed

Dynamic Programming Markov Chain·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains II: The Single-Unit Single-Customer DecompositionTextbook

Motivation

A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.

1960, Clark and Scarf proved optimality of echelon base-stock policies for finite-horizon serial systems by dynamic programming, decomposing the cost into one term per echelon (Management Science 6(4)).
1984, Federgruen and Zipkin gave a lower-bound argument for the infinite-horizon average-cost case (Operations Research 32(4)); Chen and Song (2001) used it for Markov-modulated demand (Operations Research 49(2)).
2008, Muharremoglu and Tsitsiklis introduced the single-unit single-customer approach: every unit of stock is paired with one future customer, and the inventory problem splits into countably many independent two-action problems (Operations Research 56(5)).

This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).

Setting

A single item is reviewed in periods $n = 1, \dots, N$ . An exogenous, time-homogeneous Markov chain $s_n$ on a finite set $\Sigma$ is observed at the start of period $n$ ; given $s_n = s$ , the demand $D_n \in \{0,1,2,\dots\}$ has law $\kappa(s,\cdot)$ and is independent of $s_{n+1}$ . Excess demand is backordered.

Every unit of demand is a customer, and customers are indexed in arrival order, the $v_0$ initially waiting customers first. A customer's distance is $0$ once served, $1$ while waiting, and $2, 3, \dots$ for future customers in the order they will arrive. Units are indexed by location: $0$ (used), $1$ (on hand), $2, \dots, m$ (in transit) and $m+1$ (at the supplier, which holds countably many units). The state is

x_n = \big(s_n, (z_{1n}, y_{1n}), (z_{2n}, y_{2n}), \dots\big),

with $z_{jn}$ the location of unit $j$ and $y_{jn}$ the distance of customer $j$ . In period $n$ : units in transit move one location closer and the released units move from $m+1$ to $m$ (so an order is on hand $m-1$ periods later); the demand $D_n$ brings the customers at distances $2, \dots, D_n+1$ to distance $1$ and moves the others $D_n$ steps closer; units on hand serve waiting customers, lowest indices first; then $h$ is charged per unit on hand and $b$ per waiting customer, with $0 < h < b$ . The criterion is the expected cost over the $N$ periods, discounted by $\alpha \in (0,1]$ .

A policy for the whole system $\mathcal S$ chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit $j$ only ever serves customer $j$ . The subsystem $\mathcal S_w$ is unit $w$ with customer $w$ under commitment, with state $x^w_n = (s_n, z_{wn}, y_{wn})$ and actions Release and Hold. The set $R^*_n(s,y)$ contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance $y$ , and the critical distance is

y^*(n,s) = \max\{\, y : R^*_n(s,y) \ni \mathit{Release} \,\}.

Formalization targets

Goal: Theorem 5 (p. 29)

Every policy that, in each period $n$ and Markov state $s_n$ , releases the lowest-indexed units at the supplier to raise the inventory position to

y^*(n, s_n) - 1

is optimal for $\mathcal S$ among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.

Milestones

Lemma 1 (p. 26): some monotone policy is optimal, every monotone policy is committed, and so some committed policy is optimal.
Theorem 4 (p. 27): the optimal cost of $\mathcal S$ is the sum over $w$ of the optimal costs of $\mathcal S_w$ ,

V^{\mathcal S}_1(s, x_1) = \sum_{w} V_1\big(s, (z_{w1}, y_{w1})\big),

and managing every subsystem independently and optimally is optimal for $\mathcal S$ . 3. Lemma 2 (p. 28): $R^*_n(s, y+1) = \{\mathit{Release}\}$ implies $\mathit{Release} \in R^*_n(s, y)$ . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if $y \le y^*(n,s)$ , is optimal for every subsystem.

Significance

The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.

The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:

Lemma 1 is asserted as "clearly" true;
Lemma 2's proof by contradiction covers only uniquely optimal releases, while the critical distance policy also needs the case of ties;
the passage from the subsystem policy to the inventory position (Theorem 5) is an "intuitive argument".

A formal development makes each of these precise.

Difficulty

The obvious argument says that costs are linear, so the cost of $\mathcal S$ is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit $j$ with customer $j$ holds only under monotone policies, and a general policy for $\mathcal S$ observes the whole infinite state $x_n$ , not just $x^w_n$ . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.

The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment $\{1, \dots, y^*\}$ when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last $m-1$ periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.

Formalization scope

Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.

Model. Model bundles the chain, the demand law, $m$ , $h$ , $b$ and $\alpha$ with the standing assumptions $1 \le m$ , $0 < h < b$ , $0 < \alpha \le 1$ , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in $[0,\infty]$ .

Subsystem. Subsystem defines a subsystem, its optimal cost, $R^*_n$ , $y^*(n,s)$ and the critical distance policy.

System. System defines $\mathcal S$ with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.

Conventions and pinnings:

Indexing. Units and customers are indexed from $0$ ; Lean index $j$ is the book's $j+1$ .
Policy class. Policies are Markov: functions of the period, the Markov state and the configuration, as on p. 25.
Optimality. Optimal means attaining the infimum over all policies for $\mathcal S$ . Restricting the class to monotone or base-stock policies would make Theorem 5 circular and is ruled out.
Starting states. The book's "any starting state $x_1$ " is the configuration built on pp. 23–24 from $v_0$ and the stock at locations $1, \dots, m$ . For arbitrarily labelled states Theorem 4 is false.
Critical distance. $y^*(n,s)$ is a supremum in $\mathbb N \cup \{\infty\}$ . Where it is $\infty$ (a released unit cannot arrive before the horizon), Theorem 5 leaves the policy free.
Distance 0. Lemma 2 and the optimality of $R_n$ are stated for customers at distance at least 1. At distance 0 with the unit at the supplier (a configuration committed policies never reach), both are false as printed.

Corrections to the book:

$h > 0$ is added. With $h = 0$ an optimal policy with finite orders need not exist, so Theorem 5 fails.
Chain structure is pinned. The chain's ergodicity is unused on a finite horizon and omitted. The conditional independence of $D_n$ and $s_{n+1}$ given $s_n$ is added as a reading of "given $s_n$ , the distribution of $D_n$ is known".
Vacuous corner. If some state's demand has infinite mean, every policy may cost $\infty$ and the optimality statements hold vacuously.

Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).

Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in $[0,\infty]$ .

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Section 2.2, pp. 22–31. https://doi.org/10.1007/b138879
A. Muharremoglu and J. N. Tsitsiklis, A single-unit decomposition approach to multiechelon inventory systems, Operations Research 56(5), 2008. https://doi.org/10.1287/opre.1080.0620
A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and J.-S. Song, Optimal policies for multiechelon inventory problems with Markov-modulated demand, Operations Research 49(2), 2001. https://doi.org/10.1287/opre.49.2.226.13528

8 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Introduction to the Scenario Approach III: The Risks of the Empirical Costs Follow an Ordered Dirichlet DistributionTextbook

Motivation

A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads

\min_{\nu\in\mathbb R^{d-1}}\Big[\max_{i=1,\dots,N}\ell(\nu,\delta_i)\Big],

where $\ell(\nu,\delta)$ is the cost of a decision $\nu$ when the uncertain parameter takes the value $\delta$ , and $\delta_1,\dots,\delta_N$ are independent draws from an unknown probability $\mathbb P$ . The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value $\ell^*$ , and it does so without any knowledge of $\mathbb P$ .

That guarantee concerns a single number, $\ell^*$ . Two scenario programs with the same $N$ and the same optimal value can look very different at the solution: in one, most sampled costs lie just below $\ell^*$ ; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.

Timeline:

2008: Campi and Garatti prove that the violation of the scenario solution is dominated by a beta distribution $B(d,N-d+1)$ , with equality for fully supported problems (doi:10.1137/07069821X).
2015: Carè, Garatti and Campi prove that the risks of all empirical costs from index $d$ on have a joint ordered Dirichlet law (doi:10.1137/130928546).
2018: the book states the result as Theorem 8.4 and draws the probability box from it.

Setting

Let $\Delta$ be a measurable space with a probability $\mathbb P$ , and $\ell:\mathbb R^{d-1}\times\Delta\to\mathbb R$ a cost that is convex in $\nu$ for every $\delta$ (a standing assumption of the book). For a sample $(\delta_1,\dots,\delta_N)$ of independent draws from $\mathbb P$ , let $\nu^*$ be the solution of the program above and $\ell^*=\max_i\ell(\nu^*,\delta_i)$ its optimal value.

Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, $\ell^*_1\ge\ell^*_2\ge\dots\ge\ell^*_N$ ; so $\ell^*_1=\ell^*$ .

Risk (Definition 8.2). For a decision $\nu$ and a level $\ell$ , $R(\nu,\ell)=\mathbb P\{\delta:\ell(\nu,\delta)>\ell\}$ . The risk of the $k$ -th empirical cost is $R_k=R(\nu^*,\ell^*_k)$ , and $R_1\le R_2\le\dots\le R_N$ .

Nondegeneracy (Definition 8.3). For every $N\ge d$ , with probability $1$ , $\ell^*_d\ne\ell^*_{d+1}\ne\dots\ne\ell^*_N$ . Costs with index below $d$ are excluded because several scenarios typically attain the maximum at $\nu^*$ .

Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, $\min t$ subject to $t\ge\ell(\nu,\delta_i)$ , the constraint of scenario $i$ is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every $m\ge d$ the program with $m$ scenarios has exactly $d$ support constraints with probability $1$ .

The ordered Dirichlet distribution with parameters $(d,1,\dots,1)$ is the law on $\{0\le\alpha_d\le\dots\le\alpha_N\le1\}$ with density $\frac{N!}{(d-1)!}\alpha_d^{d-1}$ .

Formalization targets

Goal: Theorem 8.4

Under nondegeneracy, for $N\ge d$ and all $\varepsilon_d,\dots,\varepsilon_N$ ,

\mathbb P^N\{R_d\le\varepsilon_d,\dots,R_N\le\varepsilon_N\}=\frac{N!}{(d-1)!}\int_0^{\varepsilon_d}\alpha_d^{d-1}\int_0^{\varepsilon_{d+1}}\!\!\cdots\int_0^{\varepsilon_N}\mathbf 1_{\{0\le\alpha_d\le\dots\le\alpha_N\le1\}}\,\mathrm d\alpha_N\cdots\mathrm d\alpha_d .

This is an identity of joint distribution functions, not a bound, and it does not depend on $\ell$ or $\mathbb P$ .

Milestones

Theorem 3.7 for the min-max program: $\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for $\varepsilon\in[0,1]$ .
Fully supported problems: $\ell^*=\ell^*_d$ with probability $1$ .
Marginal of $R_d$ (a corollary of the goal): $\mathbb P^N\{R_d\le\varepsilon\}=1-\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ , the beta law $B(d,N-d+1)$ .

Significance

The result. The theorem controls the whole distribution function of the cost $\ell(\nu^*,\delta)$ of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of $R_d,\dots,R_N$ yields, with a prescribed confidence $1-\beta$ , a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of $\ell(\nu^*,\delta)$ , computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since $\ell^*\ge\ell^*_d$ makes the risk of $\ell^*$ at most $R_d$ .

Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.

Difficulty

The obvious attempt treats $R_d,\dots,R_N$ as the order statistics of the uniform variables $1-F(\ell(\nu^*,\delta_i))$ . That works only for $d=1$ , when the decision space is a point and the costs are independent. For $d\ge2$ the decision $\nu^*$ is itself a function of the whole sample, so the sampled costs at $\nu^*$ are neither independent nor identically distributed, and the $d$ -th cost is tied to the scenarios that determine the solution. The factor $\alpha_d^{d-1}$ and the constant $N!/(d-1)!$ encode exactly this dependence. Any argument must account for which scenarios are active at $\nu^*$ without assuming full support, since the theorem holds whether or not $\ell^*=\ell^*_d$ .

Formalization scope

The decision space is EuclideanSpace ℝ (Fin n) and the book's $d$ is $n+1$ ; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with $k$ counted from $1$ ; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box $\prod_k[0,\varepsilon_k]$ intersected with the ordered simplex, stated for all real $\varepsilon_k$ . The solution map $\omega\mapsto\nu^*$ is a hypothesis-constrained function, never an arbitrary map.

Implicit hypotheses of the book pinned down in the binders:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (p. 6).
Existence and uniqueness of the solution of the program for every sample size $m\ge1$ and every sample; the book's Assumption 3.6 says "every $m$ ", but the program with no scenario has no solution.
Nondegeneracy for every sample size $m\ge d$ , not only for the $N$ of the theorem, as Definition 8.3 is written.
Joint measurability of $(\nu,\delta)\mapsto\ell(\nu,\delta)$ and measurability of the solution map (measurability is glossed over in the book, p. 6 footnote 1 and p. 33).
$N\ge d$ , and $\varepsilon\in[0,1]$ in the binomial-form statements.

A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by $\ell(\nu,\delta)=\|\nu-\delta\|^2$ with a continuous law on $\mathbb R^{n}$ , and for $d=1$ by any cost independent of $\nu$ with an atomless law.

A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the $d=1$ case of the goal, and of auxiliary facts about kthLargest are all welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018. doi:10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, Scenario min-max optimization and the risk of empirical costs, SIAM J. Optim. 25(4):2061–2080, 2015. doi:10.1137/130928546
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19:1211–1230, 2008. doi:10.1137/07069821X

10 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization IV: Descent and Stationary Cluster Points of the Proximal Gradient MethodResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4

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

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

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

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

Milestones

In the order of the paper's proof:

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

13 thms2 active usersReviewed

Optimization·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization III: For Semi-Algebraic Problems the ADMM Sequence Converges and Has Finite LengthResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) is a standard method for problems of the form $\min_x h(x)+P(\mathcal Mx)$ , in which a smooth loss $h$ is composed with a structured, possibly nonsmooth regularizer $P$ through a linear map $\mathcal M$ . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the $\ell_0$ constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective $\mathcal M$ . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the $x$ -block.

Setting

Fix $\mathcal M:\mathbb R^n\to\mathbb R^m$ linear, $h:\mathbb R^n\to\mathbb R$ twice continuously differentiable with bounded Hessian, and $P:\mathbb R^m\to(-\infty,+\infty]$ proper (finite somewhere) and closed (lower semicontinuous). For $\beta>0$ the augmented Lagrangian is

L_\beta(x,y,z)=h(x)+P(y)-\langle z,\mathcal Mx-y\rangle+\tfrac\beta2\|\mathcal Mx-y\|^2 .

The ADMM produces $(x^t,y^t,z^t)_{t\ge0}$ from arbitrary $(x^0,z^0)$ by

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

Assumption 1 with $\mathcal T_1=0$ asks for $\sigma,\delta>0$ , $\gamma\in(0,1)$ and symmetric maps $\mathcal Q_1,\mathcal Q_2,\mathcal Q_3$ with $\mathcal M\mathcal M^*\succeq\sigma\mathcal I$ , $\mathcal Q_1\succeq\nabla^2h(x)\succeq\mathcal Q_2$ and $\mathcal Q_3\succeq[\nabla^2h(x)]^2$ for all $x$ , $\mathcal Q_2+\beta\mathcal M^*\mathcal M\succeq\delta\mathcal I$ , and $\delta\mathcal I\succ\frac{2}{\sigma\beta\gamma}\mathcal Q_3$ .

The limiting subdifferential $\partial f(x)$ of $f$ consists of limits $v$ of regular subgradients $v^t$ at points $x^t\to x$ with $f(x^t)\to f(x)$ . A point $x$ is stationary if $0\in\nabla h(x)+\mathcal M^*\partial P(\mathcal Mx)$ .

A set in $\mathbb R^N$ is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations $p_i=0$ and strict inequalities $g_j<0$ ; a function is semi-algebraic if its graph is. A proper $f$ has the KL property at $\hat x\in\operatorname{dom}\partial f$ if there are $\eta>0$ , a neighbourhood $V$ of $\hat x$ and a continuous concave $\varphi:[0,\eta)\to\mathbb R_+$ with $\varphi(0)=0$ , $\varphi\in C^1(0,\eta)$ , $\varphi'>0$ , such that $\varphi'(f(x)-f(\hat x))\,\operatorname{dist}(0,\partial f(x))\ge1$ whenever $x\in V$ and $f(\hat x)<f(x)<f(\hat x)+\eta$ . A KL function is proper, closed, and KL at every point of $\operatorname{dom}\partial f$ .

In the Lean development $L_\beta$ is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space $\mathbb R^n\times\mathbb R^m\times\mathbb R^m$ with the Euclidean inner product.

Formalization targets

Goal: Theorem 3 (p. 13)

Under the standing assumptions and Assumption 1 with $\mathcal T_1=0$ , if $h$ and $P$ are semi-algebraic and the ADMM sequence has a cluster point $(x^*,y^*,z^*)$ , then

(x^t,y^t,z^t)\to(x^*,y^*,z^*),\qquad 0\in\nabla h(x^*)+\mathcal M^*\partial P(\mathcal Mx^*),\qquad \sum_{t}\|x^{t+1}-x^t\|<\infty .

No constants are fixed: every parameter is quantified exactly as in the paper.

Milestones

(35): some $w\in\partial L_\beta(x^{t+1},y^{t+1},z^{t+1})$ has $\|w\|\le C\|x^{t+1}-x^t\|$ for $t\ge1$ .
(36): $L_\beta(x^t,y^t,z^t)-L_\beta(x^{t+1},y^{t+1},z^{t+1})\ge D\|x^{t+1}-x^t\|^2$ for $t\ge1$ .
(39): $L_\beta(x^t,y^t,z^t)\to L_\beta(x^*,y^*,z^*)$ .
Finite termination when $L_\beta$ reaches its limit value.
(41): the one-step KL estimate.
Remark 4(1): the goal with " $L_\beta$ is a KL function" in place of semi-algebraicity.
$L_\beta$ is semi-algebraic when $h$ and $P$ are.
Proper closed semi-algebraic functions are KL functions, with $\varphi(s)=cs^{1-\theta}$ .

Milestones 6, 7 and 8 together imply the goal.

Significance

The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the $x$ -trajectory, for a nonconvex ADMM without any convexity of $h$ or $P$ . Semi-algebraicity covers the paper's applications: polynomial losses, the $\ell_0$ constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of $L_\beta$ , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).

Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.

Difficulty

The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires $L_\beta$ to drop by a multiple of $\|x^{t+1}-x^t\|^2+\|y^{t+1}-y^t\|^2+\|z^{t+1}-z^t\|^2$ , while the ADMM only guarantees a drop proportional to $\|x^{t+1}-x^t\|^2$ (Remark 4(2)). The relative-error bound (35) is likewise in terms of the $x$ -step alone, and relating the $y$ - and $z$ -blocks back to the $x$ -block uses the surjectivity of $\mathcal M$ and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in $x$ .

The semi-algebraic part has a separate difficulty: showing that $L_\beta$ is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ its adjoint. $P$ and $L_\beta$ take values in EReal, never passed through toReal except where the value is provably finite. $\succeq$ is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with $\phi=0$ ; argmin steps are "value at most the value anywhere", with no uniqueness; $y^0$ is unconstrained. The triple space is the nested $L^2$ product, so its inner product is the sum of the block inner products.

The KL inequality is stated for every $v\in\partial f(x)$ , which encodes $\operatorname{dist}(0,\emptyset)=+\infty$ . Writing it with Metric.infDist 0 (∂f x) would give $\operatorname{dist}(0,\emptyset)=0$ and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of $\operatorname{dom}\partial f$ , only on a neighbourhood and only for values in $(f(\hat x),f(\hat x)+\eta)$ ; $\varphi$ is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. $\eta$ is a positive real, which is equivalent to the paper's $\eta\in(0,\infty]$ .

The hypotheses $\phi=0$ and $\mathcal T_1=0$ are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.

Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.

Selected references

G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://arxiv.org/abs/1407.0753 (v6 is the cited version)
H. Attouch, J. Bolte, P. Redont, A. Soubeyran, Proximal alternating minimization and projection methods for nonconvex problems: an approach based on the Kurdyka–Łojasiewicz inequality, Math. Oper. Res. 35(2), 2010. https://doi.org/10.1287/moor.1100.0449
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4), 2007. https://doi.org/10.1137/050644641
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

17 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Global Convergence of Splitting Methods for Nonconvex Composite Optimization II: The Proximal ADMM Sequence Is Bounded Under CoercivityResearch Paper

Motivation

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

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

Setting

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

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

The augmented Lagrangian is

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (p. 11)

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

9 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Reinforcement Learning·Captain: mikedeng1

Approximately Optimal Approximate Reinforcement Learning II: Near-Optimality of a Policy with Small Policy AdvantageResearch Paper

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$ ; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$ , a finite nonempty action set $A$ , transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$ ), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$ , and a discount factor $0\le\gamma<1$ . A stochastic policy $\pi(a;s)$ is, for each state $s$ , a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$ .

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$ , where $s_0=s$ , $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$ . The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$ . The discounted future state distribution from $\mu$ is

d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu),\qquad s_0\sim\mu,

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$ .

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$ : the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$ . For nonnegative $f,g$ on $S$ , $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

\eta_{\tilde\mu}(\pi^*)-\eta_{\tilde\mu}(\pi)\le\frac{\varepsilon}{1-\gamma}\left\|\frac{d_{\pi^*,\tilde\mu}}{d_{\pi,\mu}}\right\|_\infty\le\frac{\varepsilon}{(1-\gamma)^2}\left\|\frac{d_{\pi^*,\tilde\mu}}{\mu}\right\|_\infty.

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$ ; taking $\tilde\mu=D$ , the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$ , $\pi$ and any starting distribution $\mu$ ,

\eta_\mu(\tilde\pi)-\eta_\mu(\pi)=\frac{1}{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}\big[A_\pi(s,a)\big].

The states are weighted by the future state distribution of the new policy $\tilde\pi$ , the advantage is that of the old policy $\pi$ .

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$ , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$ ), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$ . Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$ ) and P s a s' (the paper's $P(s';s,a)$ ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$ , $0\le\gamma<1$ , $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: " $X\le K\|f/g\|_\infty$ " is " $X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$ ". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$ ; no full-support assumption is made on $\mu$ or $\tilde\mu$ . The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ , which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$ ; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$ . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$ , and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477

10 thms2 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Optimal Two- and Three-Stage Production Schedules with Setup Times Included 2: Johnson's Rule for Three MachinesResearch Paper

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$ , $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$ . It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$ , $s^2_i + B_i \le s^3_i$ . The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$ .

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$ . Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$ , Johnson defines

K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,

the sums running over the items in the first $u$ (resp. $v$ ) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$ , then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .

Milestones

Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$ , so that

\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$ , so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$ . 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$ , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$ .

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$ , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$ , so the empty instance has makespan $0$ . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$ , $H_{v+1}$ . Statements with maxima over positions assume $n \ge 1$ .

Hypotheses made explicit or corrected:

$\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$ , as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$ , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

13 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Robustness and Generalization I: A Generalization Bound for Robust AlgorithmsResearch Paper

Why algorithmic robustness

A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.

Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.

Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.

Setting

Throughout, $\mathcal Z$ is a measurable space of samples and $\mathcal H$ is an arbitrary set of hypotheses. A loss $l : \mathcal H \times \mathcal Z \to \mathbb R$ satisfies $0 \le l(h,z) \le M$ for a constant $M$ . A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$ , and a learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$ , written $\mathbf s \mapsto \mathcal A_{\mathbf s}$ .

For a probability measure $\mu$ on $\mathcal Z$ , the expected error and the training error of the learned hypothesis are

\mathcal L(\mathcal A_{\mathbf s}) = \mathbb E_{z\sim\mu}\, l(\mathcal A_{\mathbf s}, z), \qquad l_{\mathrm{emp}}(\mathcal A_{\mathbf s}) = \frac1n \sum_{i=1}^n l(\mathcal A_{\mathbf s}, s_i).

Definition 2 (p. 396). For $K \in \mathbb N$ and $\epsilon(\cdot) : \mathcal Z^n \to \mathbb R$ , the algorithm $\mathcal A$ is $(K, \epsilon(\cdot))$ -robust if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$ such that for every $\mathbf s \in \mathcal Z^n$ ,

\forall s \in \mathbf s,\ \forall z \in \mathcal Z,\ \forall i:\quad s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).

The partition is chosen once, before the training set. Only the tolerance $\epsilon(\mathbf s)$ may depend on $\mathbf s$ .

For a partition $C_1,\dots,C_K$ , the cell count $|N_i|$ is the number of training points in $C_i$ . The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.

Formalization targets

Goal: Theorem 1 (p. 396)

Let $\mathcal A$ be $(K,\epsilon(\cdot))$ -robust and let $\mathbf s$ consist of $n \ge 1$ i.i.d. draws from $\mu$ . Then for every $\delta > 0$ , with probability at least $1-\delta$ ,

|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.

The constants are the paper's and are kept as printed. $K$ , $\epsilon(\cdot)$ , $M$ , $n$ , $\delta$ , $\mu$ and the algorithm are all universally quantified.

Milestones (proof of Theorem 1, pp. 396–397)

Bretagnolle–Huber–Carol inequality for the multinomial vector of cell counts. For every $\lambda \ge 0$ ,

\Pr\Big\{\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \ge \lambda\Big\} \le 2^K \exp\Big(\frac{-n\lambda^2}{2}\Big).

Eq. (3). With probability at least $1-\delta$ ,

\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \le \sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.

Eq. (4). For a partition witnessing robustness and for every training set $\mathbf s$ , deterministically,

|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big|.

Significance

Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:

Corollary 1: an adaptive number of cells;
Corollaries 2 and 3: covering-number instances;
Theorem 4: a pseudo-robust version;
the Markovian case.

Its complexity term depends only on the number of cells $K$ , not on any capacity measure of $\mathcal H$ . This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, $K$ is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.

Theorem 1 is a published result with a short proof. What a formalization adds:

a machine-checked statement of the robustness notion, pinning down which quantifier comes first;
a formal proof of the multinomial concentration step, which the paper takes from van der Vaart and Wellner rather than proving;
a reusable interface for the covering-number examples.

A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.

Difficulty

The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of $\mu$ -measure zero, where the conditional expectation in the paper's chain is undefined.

The main obstacle is the probabilistic step. The quantity $\sum_i ||N_i|/n - \mu(C_i)|$ is an $\ell_1$ deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the $K$ coordinates gives a bound whose deviation level grows linearly in $K$ . That is not $2^K e^{-n\lambda^2/2}$ , and it does not give the constant $\sqrt{2K\ln 2}$ of Theorem 1. The difficulty is to obtain the exact exponential rate $2^K e^{-n\lambda^2/2}$ for the $\ell_1$ deviation as a whole, with no loss in the constant.

Formalization scope

Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and $\mu(C_i)$ enters as a real number.

"With probability at least $1-\delta$ " is encoded as an upper bound $\delta$ on the outer measure, under $\mu^n$ , of the set of training sets where the inequality fails. This needs no measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$ .

The paper ignores measurability. The formalization restores it: every $l(h,\cdot)$ is measurable and every cell is a measurable set. Together with $0 \le l \le M$ this makes the expected error a genuine expectation.

The theorems assume $n \ge 1$ . The Bretagnolle–Huber–Carol step assumes $\lambda \ge 0$ , because the printed inequality is false for $\lambda < 0$ . No upper bound on $\delta$ is imposed: for $\delta > 2^K$ the radicand is negative, the square root evaluates to $0$ , and the statements remain true.

Two trivializing readings of Definition 2 are ruled out:

The partition may not depend on the training set. In IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a $\{0,1\}$ -valued loss would be $(2,0)$ -robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.
The tolerance may not depend on the test point, and the condition is required for every $z \in \mathcal Z$ , not only for $z$ equal to a training point.

Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).

Selected references

H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2
O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
H. Xu, C. Caramanis and S. Mannor, Robustness and Regularization of Support Vector Machines, Journal of Machine Learning Research 10 (2009) 1485–1510. https://www.jmlr.org/papers/v10/xu09b.html
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

7 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Optimization·Captain: mikedeng1

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?

Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.

Setting

A Bayesian routing game $\Gamma(\lambda)$ has a single origin–destination pair, a finite set of edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ (each route a set of edges), and a finite set of network states $\mathcal S$ . Travelers of total demand $D>0$ are split into populations $i\in\mathcal I$ , one per TIS; population $i$ has size $\lambda^iD$ , where the size vector $\lambda$ lies in the simplex $\Delta=\{\lambda:\lambda^i\ge0,\ \sum_i\lambda^i=1\}$ . Each population receives a signal (its type) $t^i$ from a finite set $\mathcal T^i$ ; states and type profiles $t=(t^i)_i$ are drawn from a common prior $\pi\in\Delta(\mathcal S\times\mathcal T)$ . Edge $e$ in state $s$ has cost $c^s_e(w)$ at load $w$ , positive, strictly increasing and differentiable.

A strategy profile $q$ assigns to each population and type a split $q^i_r(t^i)\ge0$ of its demand over routes, with $\sum_rq^i_r(t^i)=\lambda^iD$ ; these form the polytope $\mathcal Q(\lambda)$ . It induces route flows $f_r(t)=\sum_iq^i_r(t^i)$ and edge loads $w_e(t)=\sum_{r\ni e}f_r(t)$ . A traveler of population $i$ with signal $t^i$ forms the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ and evaluates the expected route cost $\mathbb E[c_r(q)\mid t^i]=\sum_{s,t^{-i}}\sum_{e\in r}\beta^i(s,t^{-i}\mid t^i)\,c^s_e(w_e(t))$ . A Bayesian Wardrop equilibrium (BWE) is a $q\in\mathcal Q(\lambda)$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is

C^{i*}(\lambda)=\sum_{t^i\in\mathcal T^i}\Pr(t^i)\min_{r\in\mathcal R}\mathbb E[c_r(q^*)\mid t^i].

The weighted potential is $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$ , and $\Psi(\lambda)=\min_{q\in\mathcal Q(\lambda)}\Phi(q)$ is its equilibrium value. In route-flow form, $\widehat\Phi(f)$ is the same expression in terms of $f$ ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand $D$ , nonnegativity) and one information impact constraint per population, $\widehat J^i(f)\le\lambda^iD$ , where $\widehat J^i(f)=D-\sum_r\min_{t^i}f_r(t^i,\widehat t^{-i})$ measures how much of the demand reacts to population $i$ 's signal. Let $\mathcal F^\dagger$ be the set of minimizers of $\widehat\Phi$ subject to (14a)–(14c) only, and

\Lambda^\dagger=\{\lambda\in\Delta:\ \exists f^\dagger\in\mathcal F^\dagger,\ \widehat J^i(f^\dagger)\le\lambda^iD\ \ \forall i\}.

In the two-stage game, travelers first choose a TIS, inducing $\lambda$ , and then play $\Gamma(\lambda)$ . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:

\lambda^i>0\ \Longrightarrow\ C^{i*}(\lambda)=\min_{j\in\mathcal I}C^{j*}(\lambda)\qquad\forall i\in\mathcal I.\tag{31}

Formalization targets

Goal: Theorem 4

For every $\lambda\in\Delta$ and every BWE of $\Gamma(\lambda)$ ,

(31)\ \text{holds}\iff\lambda\in\Lambda^\dagger .

With the existence of a BWE for every $\lambda\in\Delta$ , this is the paper's statement that the set of equilibrium adoption rates is $\Lambda^\dagger$ .

Milestones

Theorem 1. $q$ is a BWE of $\Gamma(\lambda)$ iff $q$ minimizes $\Phi$ over $\mathcal Q(\lambda)$ ; the equilibrium edge load $w^*(\lambda)$ is unique.
Proposition 2. A route flow in the flow polytope $\mathcal F(\lambda)$ ((14a)–(14c) plus all information impact constraints) is an equilibrium flow iff it minimizes $\widehat\Phi$ over $\mathcal F(\lambda)$ .
Lemma 5. $\Psi$ is convex on $\Delta$ , and with $z^{ij}=e_i-e_j$ and $V^{ij*}=C^{j*}-C^{i*}$ ,

\lim_{\epsilon\to0^+}\frac{\Psi(\lambda+\epsilon z^{ij})-\Psi(\lambda)}{\epsilon}=-D\,V^{ij*}(\lambda).

Proposition 5. $\Lambda^\dagger$ is convex, $\Lambda^\dagger=\operatorname{argmin}_{\lambda\in\Delta}\Psi(\lambda)$ , and the equilibrium edge load equals the size-independent load $w^\dagger$ of $\mathcal F^\dagger$ iff $\lambda\in\Lambda^\dagger$ .

A separate item states the existence of a BWE for every $\lambda\in\Delta$ .

Significance

The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On $\Lambda^\dagger$ the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.

Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).

Difficulty

The direction " $\lambda\in\Lambda^\dagger$ implies (31)" is not a pointwise statement about costs: it follows from $\Lambda^\dagger$ being the argmin of $\Psi$ together with the formula linking directional derivatives of $\Psi$ to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with $\lambda$ ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors ( $\lambda^i=0$ ) that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity $\Lambda^\dagger=\operatorname{argmin}\Psi$ needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.

Formalization scope

The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, $D>0$ , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of $\mathbb R$ , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).

Conventions: size vectors range over the probability simplex; $\Psi$ is the infimum of $\Phi$ over $\mathcal Q(\lambda)$ and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); $C^{i*}$ is the last form of the paper's (7), well defined when $\lambda^i=0$ ; $\widehat J^i$ is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; $\mathcal F^\dagger$ and similar sets are argmin sets. Lemma 5 is stated for the directions $z^{ij}$ with $\lambda^j>0$ (otherwise $\lambda+\epsilon z^{ij}$ leaves the simplex); $\lambda^i=0$ is allowed.

A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and $\Lambda^\dagger$ is defined by (30) from the flow problem (28), not as the argmin of $\Psi$ , so the goal is not a restatement of Proposition 5.

Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope $\mathcal F(\lambda)$ ), are welcome.

Selected references

M. Wu, S. Amin, A. E. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999 (preprint: https://arxiv.org/abs/1808.10590)
W. H. Sandholm, Potential games with continuous player sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
A. V. Fiacco, J. Kyparisis, Convexity and concavity properties of the optimal value function in parametric nonlinear programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986. https://doi.org/10.1007/BF00938592

9 thms2 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program II: Stability of the Deterministic Equivalent Convex ProgramResearch Paper

Motivation

A two-stage stochastic linear program with fixed recourse chooses a first-stage decision $x$ before a random vector $\xi$ is observed, and then pays for a cheapest corrective action $y$ once $\xi$ is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.

Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of $x$ (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.

Setting

The data are a random element $\xi=(c,q,p,T)$ with $c\in\mathbb R^n$ , $q\in\mathbb R^{\bar n}$ , $p\in\mathbb R^{\bar m}$ and $T$ an $\bar m\times n$ matrix, distributed according to a probability measure $\mu$ . The recourse matrix $W$ ( $\bar m\times\bar n$ ), the first-stage matrix $A$ ( $m\times n$ ) and $b\in\mathbb R^m$ are fixed. The recourse function is

Q(x,\xi)=\min\{q(\xi)y \mid Wy=p(\xi)-T(\xi)x,\ y\ge0\},

equal to $+\infty$ if the second-stage program is infeasible and $-\infty$ if it is unbounded.

The weak covariance condition (Definition 2.2) requires $c_j$ , $q_jp_i$ and $q_jt_{ik}$ to be integrable for all indices; it does not require $q$ , $p$ or $T$ themselves to be integrable. The paper also assumes throughout that $W$ has full row rank (p. 312).

Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and $(+\infty)+(-\infty)=+\infty$ . The expected recourse is $\mathcal Q(x)=E_\xi\{Q(x,\xi)\}$ and the objective is

Z(x)=\bar c\,x+\mathcal Q(x),\qquad \bar c=E_\xi\{c(\xi)\}.

The induced constraints are $K_2=\bigcap_{\zeta\in\tilde\Xi_{p,T}}\{x : p-Tx\in\operatorname{pos}W\}$ , where $\operatorname{pos}W=\{Wy:y\ge0\}$ and $\tilde\Xi_{p,T}$ is the support of the distribution of $(p,T)$ . The fixed constraints are $K_1=\{x: Ax=b,\ x\ge0\}$ , and $K=K_1\cap K_2$ . The deterministic equivalent program (8.2) is to minimize $Z$ over $K$ .

A convex program of the form $\min\{f(x) : Ax=b,\ x\ge0,\ x\in D\}$ with finite value $v$ is stable (Definition 8.1(iv)) if there is $\pi\in\mathbb R^m$ with $v\le f(x)+\pi(b-Ax)$ for all $x\in D$ , $x\ge0$ . Equivalently, the dual obtained by perturbing $b$ is solvable and has no duality gap.

Formalization targets

Goal: Theorem 8.11 (p. 337)

If the weak covariance condition holds, $W$ has full row rank, $K_2$ is a polyhedron and the program is finite, $v=\inf_K Z\in\mathbb R$ , then

\exists\,\pi\in\mathbb R^m:\quad v\le Z(x)+\pi\,(b-Ax)\quad\text{for all }x\in K_2,\ x\ge0 .

Milestones

Corollary 7.3 (p. 328). The value $t\mapsto\min\{cx\mid Ax=t,\ x\ge0\}$ is a finite maximum of affine functions on $\operatorname{pos}A$ , or $-\infty$ on all of $\operatorname{pos}A$ .
Proposition 7.5 (p. 329). $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ for each $\xi$ in the support, concave polyhedral in $q$ , and convex polyhedral in $(p,T)$ .
Theorem 7.6 (p. 329). $Z$ is convex on $K$ , and it is either finite on $K$ or identically $-\infty$ on $K$ .
Theorem 7.7 (pp. 329–330). If $Z>-\infty$ on $K$ , then $|Z(x)-Z(x^0)|\le\bar B\|x-x^0\|$ on $K$ (Euclidean norm).
Lemma 8.9 (p. 337). A finite program $\min\{f(x): Ax=b,\ x\ge0\}$ whose objective is convex and Lipschitz on a polyhedral domain is stable.

Significance

Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function $\phi(u)=\inf\{Z(x) : Ax=b-u,\ x\in K_2\cap\mathbb R^n_+\}$ at $u=0$ , and hence a bounded rate of change of the optimal value under perturbations of $b$ . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically $-\infty$ on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.

The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on $K_2$ for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.

Difficulty

The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of $Q(\cdot,\xi)$ . It fails unless that constant is integrable, and the weak covariance condition, not integrability of $\xi$ , is what has to deliver this, uniformly over the finitely many second-stage bases.

For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of $Z$ has curved boundary, the perturbation function can have infinite slope at $0$ ; the polyhedral hypothesis on $K_2$ is what excludes this.

Formalization scope

Types. Vectors are Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper ( $c$ , $q$ , $\pi$ ) enter through dotProduct. The law $\mu$ is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). $Q$ is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.
The integral. $\mathcal Q$ is written as lintegral of the positive part minus lintegral of the negative part, with $+\infty$ whenever the positive part is $+\infty$ . This is the paper's $(+\infty)+(-\infty)=+\infty$ ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be $0$ for non-integrable integrands and make every expected-cost statement trivial, and it is not used. $\bar c$ is a Bochner integral, legitimate because Definition 2.2 makes each $c_j$ integrable.
Readings of informal words.
- "Has first moments" is Integrable.
- "Convex polyhedron" means finitely many weak linear inequalities; $\emptyset$ and $\mathbb R^n$ are included.
- "Finite convex (concave) polyhedral function on $S$ " means equal on $S$ to the maximum (minimum) of finitely many affine functions. The $x$ and $(p,T)$ parts of Proposition 7.5 are stated as a dichotomy with the identically $-\infty$ case; the $q$ part is stated, as Corollary 7.4 gives it, as finite concave polyhedral on $\operatorname{pos}(W^T,-W^T,I)$ when the recourse problem is feasible.
- "Convex" for the extended-real $Z$ (Theorem 7.6) is ConvexOn of toReal on the finite branch.
- "Bounded on $K$ " (Theorem 7.7) is read as $Z>-\infty$ on $K$ , the proof's own reading. Finiteness on $K$ is part of the conclusion.
- "Convex and Lipschitz on a polyhedron" (Lemma 8.9) means the objective's domain is the polyhedron.
- "The program is finite" means the infimum over $K$ is a real number.
- "Stable" is the Kuhn–Tucker form above: a multiplier compared against the primal value, not merely a solvable dual. The latter would allow a duality gap.
Standing assumptions. Full row rank of $W$ appears in Theorems 7.7 and 8.11, where the proof uses square nonsingular submatrices of $W$ . It is omitted from Theorem 7.6 and Corollary 7.3 (Theorem 7.2's rank assumption), where it is not needed; this makes those statements stronger.
Corrections to the page. Theorem 8.11 is printed with " $K$ is polyhedral", $K=K_1\cap K_2$ , and read literally it is false. Take $T(\xi)$ uniform on the unit circle, $p\equiv1$ , $W=(1)$ , $q\equiv0$ , $c\equiv(-1,0)$ and $K_1=\{x_2=1,\ x\ge0\}$ . Then $K_2$ is the unit disk and $K=\{(0,1)\}$ is polyhedral with finite value $0$ , but no multiplier exists. The goal therefore assumes " $K_2$ is polyhedral", as the sentence before Lemma 8.9 and the proof require. In the dual (8.3) the page writes $c$ for $\bar c$ .
Ruled out. A statement of stability as "the dual supremum is attained" without equality to the primal value is not the goal, and neither is a hypothesis making $K$ empty or $Z$ identically $-\infty$ : the finiteness hypothesis excludes both.
Infrastructure. The needed pieces are Minkowski–Weyl for polyhedra (PointedCone.FG/DualFG in Mathlib), LP duality with $\pm\infty$ values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.

Selected references

R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
R. M. Van Slyke and R. J.-B. Wets, A duality theory for abstract mathematical programs with applications to optimal control theory, J. Math. Anal. Appl. 22(3):679–706, 1968 (cited by Wets for Definition 8.1 and the dual (8.3)).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 3. https://doi.org/10.1007/978-1-4614-0237-4

10 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program I: The Induced Feasibility Region Is a Closed Convex Polyhedron When T Is FixedResearch Paper

Motivation

A two-stage stochastic program with recourse is a linear program in which a decision $x$ is taken before a random vector $\xi$ is observed, and a corrective (recourse) decision $y$ is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in $x$ alone, and the first question is which $x$ are admissible at all: the random second-stage constraints induce constraints on $x$ that are not written down anywhere in the data.

Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix $W$ is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix $T$ is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.

Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every $x$ feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random $W$ . The 1974 survey collects these results in the form formalized here.

Setting

The data are a fixed real $\bar m \times \bar n$ matrix $W$ and a random vector $\xi = (c, q, p, T)$ with $c \in \mathbb{R}^n$ , $q \in \mathbb{R}^{\bar n}$ , $p \in \mathbb{R}^{\bar m}$ and $T$ an $\bar m \times n$ matrix. The law of $\xi$ is a probability measure $\mu$ on the product space, and its support $\tilde\Xi$ is the smallest closed set of measure one. The recourse function is

Q(x,\xi) = \min\{\, q(\xi)y \mid Wy = p(\xi) - T(\xi)x,\ y \ge 0 \,\},

equal to $+\infty$ when the program is infeasible and $-\infty$ when it is unbounded below. The expected recourse $\mathcal Q(x) = E_\xi\{Q(x,\xi)\}$ uses the paper's integral: the sum of the positive part $\int Q^+ d\mu \in [0,+\infty]$ and the negative part $-\int Q^- d\mu \in [-\infty,0]$ , with $(+\infty) + (-\infty) = +\infty$ .

The weak covariance condition (Definition 2.2) asks that $c_j$ , $q_j p_i$ and $q_j t_{ik}$ be integrable for all $i, j, k$ . Write $\operatorname{pos} W = \{Wy \mid y \ge 0\}$ . The candidate feasibility sets for the induced constraints are

$K_2^\mu$ : the $x$ for which, with probability one, some $y \ge 0$ solves $Wy = p(\xi) - T(\xi)x$ ;
$K_2^p$ : the $x$ for which such a $y$ exists for every $\xi \in \tilde\Xi$ ;
$K_2^s = \{x \mid \mathcal Q(x) < +\infty\}$ ;
$K_2 = \bigcap_{\zeta \in \tilde\Xi_{p,T}} K_2(\zeta)$ , where $\tilde\Xi_{p,T}$ is the support of the law of $(p,T)$ and $K_2(\zeta) = \{x \mid p - Tx \in \operatorname{pos} W\}$ for $\zeta = (p,T)$ .

A convex polyhedron is a set $\{x \mid Gx \ge \alpha\}$ given by finitely many linear inequalities; $\emptyset$ and $\mathbb{R}^n$ are polyhedra.

Formalization targets

Goal: Theorem 4.10

If $T$ is fixed and $\xi$ satisfies the weak covariance condition, then

K_2 = \{x \in \mathbb{R}^n \mid Gx \ge \alpha\} \quad \text{for some finite system } G, \alpha,

so $K_2$ is a closed convex polyhedron. The number of inequalities is not fixed in advance, and $K_2$ may be empty.

Milestones

Theorem 4.1. Under weak covariance, $K_2^\mu = K_2^p = K_2^s$ .
Corollary 4.5. Under weak covariance, $K_2 = K_2^p = K_2^\mu = K_2^s$ .
Theorem 4.6. For every set $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$ , $K_2 = \bigcap_{\zeta \in \Sigma} K_2(\zeta)$ .
Theorem 4.7. $K_2$ is closed and convex; if the closed positive hull $\operatorname{pos}(\tilde\Xi_{p,T})$ is a convex polyhedral cone, $K_2$ is a convex polyhedron.

Significance

Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of $(p, T)$ . This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when $p(\xi)$ has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.

The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).

Difficulty

Two steps resist the obvious approach. First, $K_2^p \subseteq K_2^s$ needs an integrable upper bound for the positive part of $Q(x,\cdot)$ on the whole support. $Q$ is only piecewise linear in $\xi$ , can equal $-\infty$ , and $q$ , $p$ , $T$ are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra $K_2(\zeta)$ , and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of $p$ is the content of the goal, and the resulting system may be inconsistent, in which case $K_2 = \emptyset$ .

Formalization scope

Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is $\mathbb{R}^n \times \mathbb{R}^{\bar n} \times \mathbb{R}^{\bar m} \times \mathbb{R}^{\bar m \times n}$ with its Borel structure, and $\mu$ is a probability measure on the whole space (the paper's sample space $\Xi$ only carries $\mu$ ). Readings fixed by the formalization:

"has first moments" (Def. 2.2) is Integrable with respect to $\mu$ .
The integral is the paper's: two lower Lebesgue integrals, returning $+\infty$ whenever the positive part diverges. Mathlib's EReal subtraction ( $\top - \top = \bot$ ) and the Bochner integral of toReal (zero for non-integrable functions) would both make $K_2^s$ wrong and are not used.
"support" is Mathlib's Measure.support; $\tilde\Xi_{p,T}$ is the support of the pushforward under the (continuous, hence measurable) projection onto $(p,T)$ .
" $T$ is fixed" means $T(\xi) = T_0$ with probability one, a weaker hypothesis than pointwise constancy.
"convex polyhedron" is the solution set of finitely many weak linear inequalities, the number of them existentially quantified; "convex polyhedral cone" is the conic hull of finitely many vectors; "closed positive hull" is the closure of the conic hull.
Full row rank of $W$ is the paper's standing assumption (p. 312) and is carried as a hypothesis of Theorem 4.1, Corollary 4.5 and Theorem 4.10; it is inessential for them.
Theorem 4.6 is stated as "for every $\Sigma$ with the same closed positive hull as $\tilde\Xi_{p,T}$ ". The literal statement fails: a closed half-plane has no extreme points, so the "inverse of convex closure" would give $\Sigma = \emptyset$ and an intersection equal to $\mathbb{R}^n$ .
The set on p. 314 (iii) is printed $K_2^p$ .

A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral $\mathcal Q$ would make $K_2^s = \mathbb{R}^n$ . Neither is used.

A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of $\operatorname{pos} W$ (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.

Selected references

R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
R. M. Van Slyke and R. J.-B. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Ch. 3. https://doi.org/10.1007/978-1-4614-0237-4

8 thms2 active usersReviewed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Computing Optimal (s, S) Inventory Policies III: Selecting an (s, S) Policy That Is Optimal for Every Starting StockResearch Paper

Motivation

The periodic-review inventory model with a fixed ordering cost is one of the basic models of operations research. When every order incurs a set-up cost $K$ in addition to holding and shortage costs, the optimal replenishment rule over an infinite horizon is, under standard convexity assumptions, a stationary $(s, S)$ policy: whenever the stock falls below the reorder point $s$ , order up to the level $S$ . Existence of such an optimal policy goes back to Scarf (1960) and Iglehart (1963). Knowing that an optimal $(s, S)$ policy exists does not say how to find one, and the average cost of an $(s, S)$ policy is neither convex nor unimodal in $(s, S)$ .

Veinott and Wagner (Management Science 11 (1965) 525–552) gave an exact algorithm. It proceeds in three steps: (i) compute integers $\underline{s} \le \bar{s} \le \underline{S} \le \bar{S}$ bounding an optimal policy; (ii) find the set $\mathcal S$ of all policies within those bounds that minimize the cost for starting stocks below $\underline{s}$ ; (iii) choose from $\mathcal S$ a policy that is optimal for every starting stock. This mission formalizes the theory behind Step iii. It is the third mission of a series on the paper: mission I treats the renewal closed form of the discounted cost, mission II the bounds of Step i.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent non-negative integer random variables with common distribution $\varphi$ and finite mean. Following the paper's Eq. (2), the unit purchase cost and the holding and penalty costs are combined into a single function $G_\alpha : \mathbb Z \to \mathbb R$ , assumed convex with $G_\alpha(y) \to \infty$ as $|y| \to \infty$ ; the set-up cost is $K \ge 0$ and $\alpha$ is the discount factor.

A stationary $(s, S)$ policy, with integers $s \le S$ , sets the stock after ordering to

Y_t = S \text{ if } X_t < s, \qquad Y_t = X_t \text{ if } X_t \ge s,

and the stock evolves as $X_{t+1} = Y_t - \xi_t$ from $X_1 = x$ . Its discounted cost is

f(x \mid s, S) = \sum_{t \ge 1} \alpha^{t-1} E\bigl[K\delta(Y_t - X_t) + G_\alpha(Y_t)\bigr],

where $\delta(z) = 1$ for $z > 0$ and $\delta(0) = 0$ , and its equivalent average cost is $a_\alpha(x \mid s, S) = (1-\alpha) f(x \mid s, S)$ .

A policy $(s', S')$ is optimal for a set $\mathfrak X$ of integers if, for each $x \in \mathfrak X$ , it minimizes $a_\alpha(x \mid s, S)$ over all $(s, S)$ policies; it is optimal if it is optimal for every integer $x$ . Under a fixed policy, $x'$ is accessible from $X_1 = x$ if $\Pr(X_t = x' \mid X_1 = x) > 0$ for some $t > 1$ .

Below the reorder point the cost does not depend on the starting stock; its value is written $\mathcal L_\alpha(S, D)$ with $D = S - s$ . The bounds are: $\underline{S}$ the smallest minimizer of $G_\alpha$ ; $\bar{S}$ the smallest integer $\ge \underline{S}$ with $G_\alpha(\bar{S}+1) \ge G_\alpha(\underline{S}) + \alpha K$ (21); $\underline{s}$ the smallest integer with $G_\alpha(\underline{s}) \le G_\alpha(\underline{S}) + K$ (22); $\bar{s}$ the smallest integer with $G_\alpha(\bar{s}) \le G_\alpha(\underline{S}) + (1-\alpha)K$ (23). The candidate set $\mathcal S$ consists of the policies with $\underline{s} \le s \le \bar{s}$ , $\underline{S} \le S \le \bar{S}$ that minimize $\mathcal L_\alpha(S, S-s)$ among such policies.

Formalization targets

Goal: Theorem 2 (p. 543)

For $0 < \alpha < 1$ and $(s^i, S^i), (s^j, S^j) \in \mathcal S$ : if $(s^i, S^i)$ is optimal and every $x'$ with

\min(s^i, s^j) \le x' < \max(s^i, s^j)

is accessible from $S^j$ under $(s^j, S^j)$ , then $(s^j, S^j)$ is optimal.

Milestones

§3, p. 533. For $x < s$ , $f(x \mid s, S) = K + f(S \mid s, S)$ .
Theorem 1, p. 542. For $0 \le \alpha < 1$ and $s \le s'$ : if $a_\alpha(x \mid s, S) = a_\alpha(x \mid s', S')$ for all $x < s'$ , then equality holds for all $x$ .
Lemma 1, p. 543. For $0 < \alpha < 1$ : if $(s, S)$ is optimal for $X_1 = x$ , it is optimal for every $x'$ accessible from $x$ .

Significance

Theorem 2 turns the final selection step of the algorithm into a reachability check on the demand distribution: a policy of $\mathcal S$ is certified optimal without comparing average costs at every starting stock. Its corollaries give checkable sufficient conditions; for example (Corollary 2.2) if $\varphi(k) > 0$ for $k = 1, \dots, s^n - s^1$ , the policy of $\mathcal S$ with the largest reorder point is optimal, which covers Poisson and negative binomial demand. Theorem 1 separately reduces the comparison of two policies to finitely many starting stocks.

The results are proved in the paper (Section 4 and Appendix §3). No machine-checked version is known: the platform has no discrete $(s, S)$ inventory chain, no discounted cost of a stationary policy on $\mathbb Z$ , and no accessibility notion for such a chain. The mission produces these objects together with the paper's selection theory on top of them.

Difficulty

Theorem 1 needs a renewal decomposition at the first passage of the stock below $s'$ , carried out for expectations over an unbounded integer state space with a discounted infinite sum. Lemma 1 is the delicate step. The paper's argument compares the $(s, S)$ policy with a hybrid policy that follows $(s, S)$ until the stock first reaches $x'$ and then switches to an optimal policy; the inequality "the hybrid cannot be better than the optimal policy" requires that some stationary $(s, S)$ policy is optimal among all ordering policies, including non-stationary ones. That existence result is cited by the paper (Section 2), not proved there. A proof of Lemma 1 within the class of $(s, S)$ policies alone does not go through, because the hybrid policy is not an $(s, S)$ policy.

Formalization scope

All objects live in the namespace VeinottWagnerSS.Selection. The model is the structure Model: the demand distribution φ : PMF ℕ with finite mean, K ≥ 0, and G : ℤ → ℝ convex (non-decreasing forward differences) and tending to $+\infty$ at both ends. The unit cost $c$ , the function $L$ and the lead time $\lambda$ do not appear (the paper's own reduction, Eq. (2), p. 529). Stock levels are integers. stateLaw is the law of $X_{t+1}$ , obtained by iterated PMF.bind; fCost is the expected discounted cost of that chain as a real series, which converges absolutely for $0 \le \alpha < 1$ because every $Y_t$ lies in $[s, \max(x, S)]$ . aCost is $(1-\alpha)$ times fCost. Accessible uses the law of $X_t$ with $t > 1$ strictly. Optimality is among $(s, S)$ policies (p. 536); the class of general ordering policies is not formalized.

The bounds $\underline{s}, \bar{s}, \underline{S}, \bar{S}$ are infima of sets of integers; under the standing assumptions and $\alpha < 1$ these sets are nonempty and bounded below, so each bound is the least integer the paper describes. $\mathcal L_\alpha(S, D)$ is defined as $a_\alpha(S - D - 1 \mid S - D, S)$ , the cost at the starting stock just below $s$ ; that this is the common value for every $x < s$ is milestone 1.

The standing assumptions are kept in every statement, including Theorem 1 and milestone 1, which do not need them; Lemma 1 and Theorem 2 are true only because of them. No printed slip was found in the three results.

Trivializing formalizations are excluded: $f$ is the expected cost of the stock process, not a closed formula or a fixed point of a recursion, so milestone 1 is not definitional; the bounds are the least integers of (21)–(23), not arbitrary integers, so $\mathcal S$ is determined by the data; the goal does not assume that $(s^j, S^j)$ is optimal below $\max(s^i, s^j)$ , and Lemma 1 assumes optimality only at the single starting stock $x$ .

Useful contributions beyond the milestones: summability lemmas for fCost, the Markov (one-step) equation for fCost, the first-passage decomposition, and, for Lemma 1, a formalization of general ordering policies with the existence of an optimal stationary $(s, S)$ policy. The chain and cost definitions are reusable for other $(s, S)$ results of the paper (Theorem 3, Corollaries 2.1 and 2.2).

Selected references

A. F. Veinott, Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

6 thms2 active usersReviewed

Operations Research

Missions

Analysis and Algorithms for Service Parts Supply Chains IV: Backorder Convexity and Everett's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: the Lagrangian stock levels solve Problem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Introduction to the Scenario Approach II: Violation Guarantees after Discarding k ConstraintsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.9

Milestones

Significance

Difficulty

Formalization scope

Selected references

Introduction to the Scenario Approach IV: The FAST Algorithm Keeps the Beta Bound and Adds a Factor (1−ε)^{N₂}Textbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

Milestone: Theorem 3.7 for program (1.4)

Milestone: the N2N_2N2​ rule

Significance

Difficulty

Formalization scope

Selected references

Elements of Queueing Theory IV: PASTA and the Formulas of Palm CalculusTextbook

PASTA and the Formulas of Palm Calculus

Background

The goal

Why it earns its place: Pollaczek–Khinchin

The rest of the chapter

What this mission provides

Formalization scope

Elements of Queueing Theory III: Stationary Regimes of Stochastic RecurrencesTextbook

Stationary Regimes of Stochastic Recurrences

Background

Exact sampling, and what "exact" means

Renovating events: sufficient, and then necessary

The saturation rule

The goal

What this mission provides

Formalization scope

Elements of Queueing Theory II: The Loynes Stability Theorem and CouplingTextbook

The Loynes Stability Theorem and Coupling

Background

The goal

The route, and what it produces on the way

Three extensions

Formalization scope

What this mission provides

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Ergodic theory, quoted

Predictability, and why PASTA can be stated

The goal

Palm probability meets stochastic intensity

What this mission provides

Formalization scope

Elements of Queueing Theory I: The Swiss Army Formula of Palm CalculusTextbook

The Swiss Army Formula of Palm Calculus

Background

The goal

The local meaning of P⁰_N

What this mission provides

Formalization scope

Linear Programming: Foundations and Extensions V: Convergence Rates of the Path-Following MethodTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 18.1 with the explicit constant

Milestones

Milestone: the $N_2$ rule

The local meaning of `P⁰_N`

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)