Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed $G$ , let $R$ be the algorithm's internal fair random bits, and let $v(G,R)$ be its nonnegative rational output. A ratio $\alpha$ requires

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record

1 prover on it3 of 3 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record

1 prover on it3 of 3 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Convex Optimization Operations Research Probability·Captain: mikedeng1

Stochastic Convex Programming: Basic Duality 2: With a Bounded Second-Stage Set the Intrinsic First-Stage Problem Coincides with the One Induced by P and Recourse Is AttainedResearch Paper

Motivation

Two-stage stochastic programming with recourse models a decision taken in two steps: a first-stage decision $x_1$ is fixed before a random outcome $s$ is observed, and a recourse decision $x_2(s)$ is taken afterwards, once $s$ is known. The model goes back to Dantzig (1955) and Beale (1955) and is the basic template of stochastic optimization in operations research: capacity planning before demand is known, production before prices are revealed, reservoir management before inflows are observed.

When the outcome space is not finite, the recourse is a function $x_2(\cdot)$ , and the problem must specify the class of functions it ranges over. Rockafellar and Wets (Pacific J. Math. 62 (1976) 173–195) develop the duality theory of the convex case with recourse functions that are measurable and essentially bounded ( $\mathcal L^\infty$ ), the setting in which the dual multipliers and their interpretation as prices become available. Their §3 asks whether that restriction loses anything: whether minimizing over $\mathcal L^\infty$ recourses gives the same first-stage problem as minimizing, scenario by scenario, the best attainable second-stage cost.

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. The data are closed convex nonempty sets $C_1\subseteq\mathbb R^{n_1}$ , $C_2\subseteq\mathbb R^{n_2}$ , finite convex functions $f_{10},f_{1i}$ on $\mathbb R^{n_1}$ ( $i=1,\dots,m_1$ ), and functions $f_{20}(s,x_1,x_2)$ , $f_{2i}(s,x_1,x_2)$ ( $i=1,\dots,m_2$ ), finite and jointly convex in $(x_1,x_2)$ for each $s$ , and measurable in $s$ for each $(x_1,x_2)$ , summable for $i=0$ and bounded for $i\ge1$ . These are the paper's standing assumptions.

With $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$ , the essential objective of the problem $\mathbf P$ is

f(x_1,x_2)=F_1(x_1,0)+\int_S F_2\big(s,x_1,x_2(s),0\big)\,\sigma(ds),

where $F_1(x_1,u_1)=f_{10}(x_1)$ if $x_1\in C_1$ and $f_{1i}(x_1)\le u_{1i}$ for all $i$ , and $+\infty$ otherwise, and $F_2(s,x_1,x_2,u_2)=f_{20}(s,x_1,x_2)$ if $x_2\in C_2$ and $f_{2i}(s,x_1,x_2)\le u_{2i}$ for all $i$ , and $+\infty$ otherwise. Integrals of extended-real functions follow the paper's convention (2.4): the ordinary integral (real or $-\infty$ ) when the integrand is majorized by a summable function, and $+\infty$ otherwise.

Two first-stage problems are compared:

the first-stage problem induced by $\mathbf P$ minimizes $J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2)$ ;
the intrinsic first-stage problem $\mathbf Q$ minimizes $j(x_1)=F_1(x_1,0)+\int_S q(s,x_1)\,\sigma(ds)$ , where $q(s,x_1)=\inf_{x_2\in\mathbb R^{n_2}}F_2(s,x_1,x_2,0)$ is the optimal recourse cost in scenario $s$ .

The hypothesis of the general result uses $\rho(s,x_1)=\inf\{|x_2|\mid F_2(s,x_1,x_2,0)<+\infty\}$ , the Euclidean distance from the origin to the feasible recourses ( $+\infty$ if there are none), and calls $x_1$ intrinsically feasible when $j(x_1)<+\infty$ . A normal convex integrand $h$ on $S\times\mathbb R^n$ is lower semicontinuous, convex and proper in $z$ for each $s$ , with a measurability condition given by a sequence of measurable functions dense in each $\operatorname{dom}h(s,\cdot)$ .

Formalization targets

Goal: Theorem 2 (p. 187)

If $C_2$ is bounded, then for every $x_1\in\mathbb R^{n_1}$

j(x_1)=J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2),\qquad \inf\mathbf Q=\inf\mathbf P,

the two first-stage problems have the same minimizers, and the infimum over $x_2\in\mathcal L^\infty_{n_2}$ is attained for each $x_1$ .

Theorem 1 (p. 186)

If $\rho(\cdot,x_1)$ is essentially bounded for every intrinsically feasible $x_1$ , then $j(x_1)=J(x_1)$ for all $x_1$ , $\inf\mathbf Q=\inf\mathbf P$ , and the minimizers coincide. Boundedness of $C_2$ is a special case of this hypothesis.

Milestones

(2.1): $F(x,u)=F_1(x_1,u_1)+\int_S F_2(s,x_1,x_2(s),u_2(s))\,\sigma(ds)$ (p. 180);
Proposition 1: for a normal convex integrand, $\inf_{z\in\mathcal L^p_n}\int_S h(s,z(s))\,\sigma(ds)=\int_S\inf_z h(s,z)\,\sigma(ds)$ whenever the left side is not $+\infty$ (p. 181);
Proposition 2: $F_2$ is a normal convex integrand (p. 182);
Proposition 4: $q(\cdot,x_1)$ is measurable (p. 185);
(3.5)–(3.6): $j\le f$ , hence $\inf\mathbf Q\le\inf\mathbf P$ (p. 186);
the feasible-recourse multifunction (3.10) is measurable, $\rho$ is measurable, and the nearest feasible point is a measurable selection (p. 187);
Theorem 1 (p. 186);
with $C_2$ bounded, the argmin multifunction of $F_2(s,x_1,\cdot,0)$ is nonempty, compact, measurable and has a measurable selection (p. 188).

The Corollary of Theorem 2 (p. 188), that $x_1$ minimizes $\mathbf Q$ iff some $(x_1,x_2)$ minimizes $\mathbf P$ , is included as a further statement.

Significance

The theorem justifies the modelling choice behind the paper's duality theory: when the second-stage constraint set is bounded, restricting recourse to essentially bounded measurable functions changes neither the optimal value nor the optimal first-stage decisions, and an optimal recourse function exists for every first stage. The duality theory of the companion mission (Theorem 3 of the same paper) is developed in that $\mathcal L^\infty$ setting, so the two results together describe the problem completely in the bounded case. Proposition 1, the interchange of infimum and integral for normal integrands, is a basic tool of stochastic programming and of the calculus of variations, used well beyond this paper.

The results are proved in the 1976 paper, relying on Rockafellar's earlier work on normal integrands and measurable selections. None of them has a machine-checked proof. Mathlib has the Lebesgue and Bochner integrals, $\mathcal L^p$ spaces and the measurable-selection prerequisites in partial form; it has no normal integrands, no extended-real integral convention of this kind, and no interchange theorem. A formal development produces those as reusable components.

Difficulty

The inequality $j\le J$ is immediate. The reverse inequality requires, from the pointwise infima $q(s,x_1)$ , a single recourse function $x_2(\cdot)$ that is measurable, essentially bounded and nearly optimal in almost every scenario. Choosing a near-minimizer separately for each $s$ gives no measurability at all: the content is a measurable choice, and that needs the normality of $F_2$ and the measurability of the multifunctions of feasible and of optimal recourses. Essential boundedness is a second, independent obstacle: without a bound on $\rho$ every feasible recourse may be unbounded, and the infimum over $\mathcal L^\infty$ can then exceed $j$ . Attainment in Theorem 2 needs, in addition, compactness of the argmin sets, which comes from the boundedness of $C_2$ and lower semicontinuity.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; indices $i=1,\dots,m$ are Fin m; $\mathcal L^\infty_n$ and $\mathcal L^p_n$ are Mathlib's Lp (Fin n → ℝ) p σ, so recourse functions are almost-everywhere classes and the second-stage constraints hold almost surely. $\sigma$ is a probability measure in every theorem. All extended-real quantities ( $F$ , $F_1$ , $F_2$ , $f$ , $J$ , $q$ , $j$ , $\rho$ , $\inf\mathbf P$ , $\inf\mathbf Q$ ) take values in EReal, and every infimum is the complete-lattice infimum, so an empty infimum is $+\infty$ . The integral convention (2.4) is the published definition DupacovaWets.Consistency.expect: $+\infty$ when the positive part has infinite integral (for a measurable function, exactly when it has no summable majorant), and otherwise the difference of the lower Lebesgue integrals of the positive and negative parts. $|\cdot|$ in $\rho$ is the Euclidean length, not the sup norm. "Gives the minimum" is "has value $\le$ the value at every point". Measurability of a multifunction is the published definition DupacovaWets.Consistency.IsMeasurableMultifunction ( $\{s\mid\Gamma(s)\cap K\ne\emptyset\}$ measurable for every closed $K$ ). The standing assumptions are fields of the structure Problem.

The integral of an extended-real function must not be replaced by a Bochner integral of its real part, which would turn $\pm\infty$ values into $0$ and make $j$ meaningless; and the infima must not be real sInf, which returns $0$ on unbounded sets.

Reusable beyond this mission: the notion of a normal convex integrand on a finite-dimensional space, and Proposition 1. Contributions of measurable-selection infrastructure (Kuratowski–Ryll-Nardzewski type theorems, measurability of distance functions of closed-valued multifunctions) are welcome as supporting lemmas. The mission "Stochastic Convex Programming: Basic Duality 1" formalizes the duality theorem of the same paper on the same model.

Selected references

R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
R. T. Rockafellar, Measurable dependence of convex sets and functions on parameters, Journal of Mathematical Analysis and Applications 28 (1969) 4–25. https://doi.org/10.1016/0022-247X(69)90104-8
R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
G. B. Dantzig, Linear programming under uncertainty, Management Science 1(3–4) (1955) 197–206. https://doi.org/10.1287/mnsc.1.3-4.197

15 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

Motivation

A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.

This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.

Setting

A store offers a subset $S$ of the variants $N=\{1,\dots,n\}$ of a category. Each variant $j$ has an MNL preference $v_j>0$ , and the option of buying nothing has preference $v_0>0$ . A customer facing $S$ buys variant $j\in S$ with probability

q_j(S)=\frac{v_j}{\sum_{i\in S}v_i+v_0}.

Variants are labelled so that $v_1\ge v_2\ge\cdots\ge v_n$ , and the most-popular sets are $A_i=\{1,\dots,i\}$ .

The retailer sells at price $p$ and buys at unit cost $c$ , with $0<c<p$ , and stocks $x_j$ units of each variant before the season. The critical fractile is $z=\Phi^{-1}(1-c/p)$ , with $\Phi$ the standard normal distribution function. Two models of aggregate demand $Y_j$ are considered, both with store volume $\lambda>0$ :

Independent population model. $Y_j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$ , where $\sigma>0$ and $0\le\beta<1$ . The optimal expected profit $\max_{x\ge0}\sum_{j\in S}E[p\min\{x_j,Y_j\}-cx_j]$ equals

\pi_I(S,v)=(p-c)\lambda\sum_{j\in S}q_j-\frac{p\sigma\lambda^\beta e^{-z^2/2}}{\sqrt{2\pi}}\sum_{j\in S}q_j^\beta .

Trend-following population model. All customers make the same choice, so $Y_j=\lambda$ with probability $q_j$ and $Y_j=0$ otherwise. The optimal expected profit is

\pi_T(S,v)=\sum_{j\in S}(pq_j-c)^+\lambda .

The assortment problem is $\max_{S\subseteq N}\pi(S,v)$ for $\pi=\pi_I$ or $\pi=\pi_T$ .

For Lemma 1, fix $S$ and let $\delta\ge0$ be the preference of a variant added to it: $f(\delta)=\sum_{j\in S}v_j+\delta+v_0$ , $g_I$ and $g_T$ are the numerators of the profit after the addition, and $h_I=g_I/f$ , $h_T=g_T/f$ .

Formalization targets

Goal: Theorem 1 (p. 1503)

For each demand model there is a most-popular set that is optimal among all $2^n$ assortments:

\exists\,i\in\{0,\dots,n\}\ \forall S\subseteq N:\ \pi_I(S,v)\le\pi_I(A_i,v),\qquad \exists\,i\in\{1,\dots,n\}\ \forall S\subseteq N:\ \pi_T(S,v)\le\pi_T(A_i,v).

The paper prints $i\in\{1,\dots,n\}$ for both models. In the independent model the empty assortment can be the unique optimum (when $\pi_I(A_1,v)<0$ , for instance at small $\lambda$ ), so $i=0$ is allowed there; the trend-following range is the printed one.

Milestones

(4)–(7): under normal demand, $x^*_j=\lambda q_j+z\sigma(\lambda q_j)^\beta$ is the optimal stocking vector and the optimal profit is $\pi_I(S,v)$ .
(8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$ .
Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$ .
Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$ .
§3.1: $h(v_j)=\pi(S\cup\{j\},v)$ for $j\notin S$ , and $h(0)=\pi(S,v)$ .

Significance

The search over assortments is a priori a search over $2^n$ subsets. Theorem 1 cuts it to the $n+1$ nested sets $A_0\subset A_1\subset\cdots\subset A_n$ , so the optimal assortment is found by comparing $n+1$ numbers. The result is not obvious: the paper's example ( $n=8$ , $v_1=v_2=10$ , $v_8=1$ ) shows that $\{1,8\}$ can beat $\{1,2\}$ , so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.

The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the $\beta=0$ boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.

Difficulty

The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term $\sum q_j^\beta$ is concave in the shares, so profit is not monotone or submodular in $S$ in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference $\delta$ to be quasi-convex in $\delta$ . That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio $g/f$ with $f$ affine and proving $g_I$ convex, which in turn needs concavity of $(\sum_{j\in S}v_j^\beta+\delta^\beta)(\sum_{j\in S}v_j+\delta+v_0)^{1-\beta}$ . The exchange argument must also handle ties among the $v_j$ , which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity $E(Z-z)^+=\varphi(z)-z(1-\Phi(z))$ , neither of which is in Mathlib in this form.

Formalization scope

Variants are Fin n, 0-based: the paper's variant $j$ is index $j-1$ , $A_i$ is the set of indices below $i$ , and the paper's $v_1$ is the first entry v ⟨0, _⟩. The no-purchase preference $v_0$ is a separate real v0, never a variant. Preferences are strictly positive and the sorting $v_1\ge\cdots\ge v_n$ is the hypothesis Antitone v.
Standing hypotheses: $0<c<p$ , $\lambda>0$ , $\sigma>0$ , $0\le\beta<1$ ; the goal also assumes $n\ge1$ (the trend-following range $1\le i\le n$ needs it).
$z$ is defined from $p$ and $c$ as the least $x$ with $\Phi(x)\ge1-c/p$ , $\Phi$ the c.d.f. of Mathlib's gaussianReal 0 1; a separate theorem states $\Phi(z)=1-c/p$ and uniqueness.
Powers are Real.rpow, so $0^0=1$ . At $\beta=0$ this keeps (7) correct ( $\sum_{j\in S}q_j^0=|S|$ ), but $h_I(0)=\pi_I(S,v)$ then fails; that one clause carries $\beta>0$ . The goal keeps $0\le\beta<1$ .
The positive part $(\cdot)^+$ is max · 0. In (11), $\lambda$ multiplies both terms; the printed (11) has it on the sum only, which would break $h_T(v_j)=\pi_T(S\cup\{j\},v)$ unless $\lambda=1$ .
"Optimal" means $\pi(S,v)\le\pi(A_i,v)$ for every $S\subseteq N$ , including $S=\emptyset$ . A formalization that maximizes only over prefix sets, assumes the optimum nonempty or the profit nonnegative, treats $z$ as a free real unrelated to $p$ and $c$ , or drops one of the two demand models, is a different and weaker statement and does not count.
In milestone 1 the order-up-to levels $x^*_j$ are assumed nonnegative, the formal content of the paper's assumption $\lambda^{1-\beta}q_j\gg\sigma q_j^\beta$ .

Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.

Selected references

G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (reprinted SIAM Classics in Applied Mathematics 10, 1994). https://doi.org/10.1137/1.9781611971255
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 5: Full-Batch LPT Is Within 4/3 − 1/(3m) of the Optimal Makespan on Parallel Batch MachinesResearch Paper

Motivation

Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.

This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio $4/3 - 1/(3m)$ on $m$ machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.

Setting

There are $n$ jobs with processing times $p_j > 0$ , all available at time $0$ , and $m \ge 1$ identical batch processing machines. Each machine processes up to $B \ge 1$ jobs at the same time. A batch is a set of at most $B$ jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,

p(P) = \max_{j \in P} p_j .

A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time $0$ . The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written $P/B/C_{\max}$ , and $C^*$ denotes its optimal value, over every way of forming batches (any sizes up to $B$ , any grouping) and every assignment. For $B = 1$ it is the classical problem $P//C_{\max}$ .

Algorithm BLPT.

Rank the jobs in nonincreasing order of processing time and cut the ranked list into successive groups of $B$ jobs, the last possibly smaller.
Order these batches in nonincreasing order of batch time and assign each in turn to a machine with least current load.

$C(\mathrm{BLPT})$ is the resulting makespan.

For the optional lateness result, each job also has a due date $d_j \ge 0$ . The maximum lateness of a schedule is $L_{\max} = \max_j (C_j - d_j)$ , $L$ is its value under BLPT, $L^*$ its optimum and $d_{\max} = \max_j d_j$ .

Formalization targets

Goal: Proposition 3 (p. 773)

C(\mathrm{BLPT}) \le \left(\frac43 - \frac1{3m}\right) C^* .

It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.

Milestones

Proposition 2 (p. 772). With the jobs re-indexed longest first, some optimal schedule has batches of consecutive jobs, all full except possibly the one containing the last job. In other words, its batches are exactly the groups formed in Step 1 of BLPT.
The reduction (§5, p. 772). $C^*$ equals the optimal makespan of $P//C_{\max}$ on the aggregate jobs $p(B_1), \dots, p(B_{\lceil n/B\rceil})$ .
Graham's LPT bound, as quoted (p. 772). For jobs $q_0 \ge \dots \ge q_{M-1} \ge 0$ on $m$ machines, list scheduling in that order has makespan at most $(4/3 - 1/(3m))$ times the optimum.
Proposition 5 (p. 773, further result).

\frac{L - L^*}{L^* + d_{\max}} \le \left(\frac13 - \frac1{3m}\right) + \frac{d_{\max}}{L^* + d_{\max}} .

Significance

Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on $B$ , whereas arbitrary batch list scheduling only gets $B + 1 - 1/m$ (Proposition 1 of the same paper). For one machine the factor is $1$ , so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for $P//C_{\max}$ transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to $L^* + d_{\max}$ because $L^*$ may be negative.

All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.

Difficulty

The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, $C^*$ ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.

Formalization scope

Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.

Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). $C^*$ is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.

Explicit readings of the paper's phrases:

"rank jobs in decreasing order" is any list of all jobs that is nonincreasing in p;
the batches of Step 1 are List.toChunks B of that list;
"order the batches in nonincreasing order of $p(B_k)$ " is any permutation of those chunks that is nonincreasing in batch time;
every statement is quantified over both choices;
"assign them to the machines as they become free" is least-loaded list scheduling with the published lowest-index tie rule. With no idle time, the machine that becomes free first is a least-loaded one, and the tie rule does not change the multiset of loads;
" $1/3m$ " is $1/(3m)$ ;
"optimal solution" in Proposition 2 is a valid batching with an assignment whose makespan equals $C^*$ , and "consecutive, all full except the one containing the highest indexed job" is "equal, up to order, to the chunks of the ranked list";
schedules on each machine run in list order without idle time, and every processing order is a reordering of the list. For $L^*$ this covers every semi-active schedule.

Proposition 5 adds the hypothesis $d_j \ge 0$ , which the paper's proof uses but does not print. It also makes $L^* + d_{\max}$ positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.

A statement with $C^*$ restricted to consecutive batches, a sorry-free bound obtained from a degenerate $m = 0$ or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any $P//C_{\max}$ work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.

Selected references

C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039
A. H. G. Rinnooy Kan, L. Stougie, Stochastic Integer Programming, Ch. 8 of Y. Ermoliev, R. J.-B. Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer, 1988 (source of the reused list-scheduling definitions). https://doi.org/10.1007/978-3-642-61370-8

10 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Scenarios and Policy Aggregation in Optimization Under Uncertainty 2: A Limit of Locally Optimal Progressive Hedging Steps Is a Stationary Point of the Nonconvex ProblemResearch Paper

Motivation

Multistage decision problems under uncertainty are often modelled by a finite set of scenarios: each scenario $s$ fixes one possible future, and for it a deterministic problem can be solved. What makes the problem stochastic is the requirement that decisions may depend only on information available at the time they are taken. Rockafellar and Wets (WP-87-119, 1987; journal version Math. Oper. Res. 16 (1991) 119–147) proposed the progressive hedging algorithm, which solves the scenario problems separately with a penalty and a price term and blends their solutions step by step into a single policy that respects the information constraints. The method is a standard decomposition scheme of stochastic programming and is implemented in solver libraries such as PySP and mpi-sppy.

For convex problems the paper proves convergence through the theory of the proximal point algorithm. Many practical scenario models are not convex (integer-like penalties, nonconvex costs). For that case the paper proves one result, Theorem 6.1: the algorithm cannot be expected to find a global minimum, but whenever it converges, its limit is a stationary point. This mission formalizes that result.

Setting

Let $S$ be a finite set of scenarios with probabilities $p_s>0$ , $\sum_s p_s=1$ . A decision is a vector $x=(x_1,\dots,x_T)\in\mathbb R^n$ , split into blocks $x_t$ taken at times $t=1,\dots,T$ . For each scenario there is a scenario subproblem

(P_s)\qquad\text{minimize } f_s(x)\ \text{over } x\in C_s\subseteq\mathbb R^n .

Throughout, every $C_s$ is nonempty and closed, every $f_s$ is locally Lipschitz, and the sets $\{x\in C_s\mid f_s(x)\le\alpha\}$ are bounded.

A policy is a map $X:S\to\mathbb R^n$ . Policies form a space $\mathcal E$ with inner product $\langle X,Y\rangle=\sum_s p_s X(s)\cdot Y(s)$ and norm $\|X\|=\langle X,X\rangle^{1/2}$ . For each time $t$ the scenarios are partitioned into bundles $A\in\mathcal A_t$ of scenarios indistinguishable at time $t$ . A policy is implementable, $X\in\mathcal N$ , when each $X_t$ is constant on every bundle of $\mathcal A_t$ ; it is admissible, $X\in\mathcal C$ , when $X(s)\in C_s$ for all $s$ . The aggregation operator $J$ replaces $X_t(s)$ by its conditional expectation over the bundle of $s$ ; $K=I-J$ , and $\mathcal M=\{W\mid JW=0\}=\mathcal N^\perp$ . With $F(X)=\sum_s p_s f_s(X(s))$ the problem is

(P)\qquad\text{minimize } F(X)\ \text{over } X\in\mathcal C\cap\mathcal N .

Progressive hedging with parameter $r>0$ keeps $X^\nu\in\mathcal C$ and $W^\nu\in\mathcal M$ . It sets $\hat X^\nu=JX^\nu$ , computes $X^{\nu+1}(s)$ for every $s$ from

(P^\nu_s)\qquad\text{minimize } f_s(x)+x\cdot W^\nu(s)+\tfrac12 r|x-\hat X^\nu(s)|^2\ \text{over } x\in C_s ,

and updates $W^{\nu+1}=W^\nu+rKX^{\nu+1}$ . In the nonconvex case, $X^{\nu+1}(s)$ is only required to be $\delta$ -locally optimal: optimal among the points of $C_s$ within Euclidean distance $\delta$ of it, for a fixed $\delta>0$ .

$\partial g(x)$ denotes Clarke's generalized gradient of a locally Lipschitz $g$ and $N_C(x)$ Clarke's normal cone to a closed set $C$ .

Formalization targets

Goal: Theorem 6.1

If $X^\nu\to X^*$ and $W^\nu\to W^*$ , then $X^*\in\mathcal N\cap\mathcal C$ , $W^*\in\mathcal M$ and

-W^*(s)\in\partial f_s(X^*(s))+N_{C_s}(X^*(s))\qquad\text{for all } s\in S;

moreover $X^*$ is a local minimizer of $(\tilde P)$ , which is (P) with $f_s$ replaced by $\tilde f_s(x)=f_s(x)+\tfrac12 r|x-X^*(s)|^2$ , and $-W^*(s)\in\partial\tilde f_s(X^*(s))+N_{C_s}(X^*(s))$ .

Milestones

(6.4)–(6.5): each $X^{\nu+1}$ is optimal for $(P^\nu)$ , minimize $F(X)+\langle X,W^\nu\rangle+\tfrac12 r\|X-\hat X^\nu\|^2$ over $\mathcal C$ , on the $\|\cdot\|$ -ball of radius $\delta'=\delta\min_s p_s^{1/2}$ .
$W^*\in\mathcal M$ , $KX^\nu\to0$ and $X^*\in\mathcal N$ .
(6.6): $X^*$ is locally optimal for $(P^*)$ , minimize $F(X)+\langle X,W^*\rangle+\tfrac12 r\|X-X^*\|^2$ over $\mathcal C$ .
$X^*$ is locally optimal for $F(X)+\tfrac12 r\|X-X^*\|^2=E\{\tilde f_s(X(s))\}$ over $\mathcal C\cap\mathcal N$ .
(6.2): $\partial\tilde f_s(X^*(s))=\partial f_s(X^*(s))$ , from $\partial\tilde f_s(x)=\partial f_s(x)+r(x-X^*(s))$ .
Theorem 4.1: at a local minimizer of (P) satisfying the constraint qualification "the only $W\in\mathcal M$ with $-W(s)\in N_{C_s}(X^*(s))$ for all $s$ is $W=0$ ", some $W^*\in\mathcal M$ satisfies the conditions above; in the convex case these conditions imply global optimality.

Significance

Theorem 6.1 is the paper's only guarantee outside convexity. It says that progressive hedging, run with local solvers on nonconvex scenario subproblems, cannot converge to a point that fails the first-order conditions, and that the limiting price system $W^*$ is a Lagrange multiplier for the nonanticipativity constraint $X\in\mathcal N$ . It needs no constraint qualification, unlike the general necessary condition of Theorem 4.1: the multiplier is produced by the algorithm. This is the basis for using progressive hedging as a heuristic for nonconvex and mixed-integer stochastic programs.

The result is proved in the paper; to our knowledge it has not been machine-checked. A complete formalization would give checked statements of the scenario model ( $J$ , $K$ , $\mathcal N$ , $\mathcal M$ with the weighted inner product), of the algorithm with inexact local subproblem solutions, and of Clarke's optimality conditions for problems with separable structure. The convex convergence theory of the same paper is the subject of the companion mission Scenarios and Policy Aggregation in Optimization Under Uncertainty 1.

Difficulty

The local optimality of $X^{\nu+1}(s)$ is relative to a ball centred at the iterate, which moves. Passing to the limit requires a radius that is uniform in $\nu$ and in the norm of $\mathcal E$ ; this is what $\delta'$ provides, and it only covers points strictly inside the limiting ball: a point of $\mathcal C$ at distance exactly $\delta'$ from $X^*$ may lie outside every ball around the iterates. The step from local optimality to the multiplier condition uses Clarke's necessary condition for minimization over a closed set and the sum rule for a Lipschitz function plus a smooth one; neither is in Mathlib. Theorem 4.1 needs, in addition, a calculus rule for normal cones of an intersection under a qualification condition, and the transfer of Clarke's objects between $\mathcal E$ with the weighted inner product and the individual scenario spaces.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). A policy is a function S → EuclideanSpace ℝ (Fin n). The weighted inner product and norm of $\mathcal E$ are explicit definitions (ip, pnorm); Lean's built-in norm on policies (the sup norm) is used only for topological notions: convergence of the iterates and "locally optimal" without a radius, which do not depend on the norm. The radii $\delta'$ are in the weighted norm, the radius $\delta$ in the Euclidean norm of $\mathbb R^n$ . Time blocks are a monotone map from coordinates to periods; bundles are the classes of a setoid on $S$ for each period. The standing assumptions are fields of the model structure, so every theorem carries them. Indices are 0-based and sequences are indexed by $\nu=0,1,2,\dots$ ; the run starts from $X^0\in\mathcal C$ and $W^0\in\mathcal M$ . Theorem 4.1 is stated in its decomposed form (4.4), scenario by scenario.

Clarke's generalized gradient and normal cone are the published platform definitions ClarkeGradients.Shared.generalizedGradient (convex hull of limits of gradients) and ClarkeGradients.FlowInvariance.normalCone (closure of the cone generated by the generalized gradient of the distance function); for locally Lipschitz functions and closed nonempty sets these are the objects the paper uses.

Formalizations that trivialize the statement are excluded: Theorem 6.1 carries no convexity hypothesis and no constraint qualification, the $\delta'$ -balls are not measured in the sup norm, and the run predicate is satisfiable (the model files come with a sanity check exhibiting a run).

Useful infrastructure, reusable beyond this mission: Clarke's necessary condition for local minimization of a Lipschitz function over a closed set, the sum rule with a $C^1$ function, products of normal cones, and basic facts about $J$ (an orthogonal projection onto $\mathcal N$ for the weighted inner product). Contributions of any of these are welcome.

Selected references

R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, IIASA Working Paper WP-87-119, 1987. https://pure.iiasa.ac.at/id/eprint/2933/
R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, Mathematics of Operations Research 16(1), 119–147, 1991. https://doi.org/10.1287/moor.16.1.119
F. H. Clarke, Generalized gradients and applications, Transactions of the AMS 205, 247–262, 1975. https://doi.org/10.1090/S0002-9947-1975-0367131-6
F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309

11 thms2 active usersReviewed

Completed

Machine Learning Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 1: WM Makes at Most log(w_init/w_fin)/log(2/(1+β)) Mistakes on Any SequenceResearch Paper

Motivation

In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.

Setting

A finite pool has $n$ members, each of which predicts either $0$ or $1$ on every trial. The true label on trial $t$ is $\rho_t\in\{0,1\}$ , and member $i$ predicts $x_{t,i}\in\{0,1\}$ . The master prediction is $\lambda_t\in\{0,1\}$ . Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.

Each member begins with a strictly positive real weight $w_{0,i}$ . Before trial $t$ , let $w_{t,i}$ be its current weight. For $b\in\{0,1\}$ , let $q_{t,b}$ be the sum of weights of members predicting $b$ . WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor $\beta$ with $0\le\beta<1$ ; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.

Write $W_t=\sum_i w_{t,i}$ for the total pool weight at a trial boundary. Thus $W_0=w_{\mathrm{init}}$ and $W_T=w_{\mathrm{fin}}$ after $T$ trials. Let $m$ count the trials with $\lambda_t\ne\rho_t$ . The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.

Formalization targets

The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,

W_{t+1}\le \frac{1+\beta}{2}W_t.

Across the whole sequence, with $m$ master mistakes, the corresponding estimate is

W_T\le W_0\left(\frac{1+\beta}{2}\right)^m.

The goal is the paper's Theorem 2.1, retaining its explicit constant:

m\le \frac{\log(W_0/W_T)} {\log\!\left(2/(1+\beta)\right)} \qquad\text{when }W_T>0.

The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for $\beta=0$ . The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.

Significance

The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The $\beta=0$ case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.

The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.

Difficulty

The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When $\beta=0$ , a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.

Formalization scope

The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and $\beta$ are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require $0\le\beta<1$ and strictly positive initial member weights. The goal additionally requires $W_T>0$ , while the two weight inequalities permit $W_T=0$ . Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.

The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.

A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within scope.

Selected references

Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

4 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 3: Dynamic Program DP3 Minimizes the Number of Tardy Equal-Length Jobs on a Batch Machine with Agreeable Release and Due DatesResearch Paper

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$ . Job $j$ has release time $r_j$ , due date $d_j$ , and processing time $p_j$ . In the main problem every processing time equals a common value $p$ . A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$ . Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$ . For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$ . For $1\le i\le j$ , it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$ . A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$ . The main target is

U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$ . The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$ , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$ , with an empty range giving $+\infty$ . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

9 thms2 active usersReviewed

Combinatorics Markov Chain Probability·Captain: mikedeng1

Coalescents With Multiple Collisions 1: A Coalescent on Partitions of ℕ With k-Fold Merger Rates λ_{b,k} Exists Iff λ_{b,k} = ∫ x^{k−2}(1−x)^{b−k} Λ(dx)Research Paper

Motivation

A coalescent models a collection of ancestral lineages merging as time runs backward. If every event joins exactly two lineages, a single pairwise merger rate describes the finite system. Pitman’s 1999 paper asks which rates permit an event to join any number of blocks, while still giving one process on partitions of all positive integers. This matters when a sample of any finite size must be a restriction of the same population model: specifying a chain separately at every sample size is insufficient unless the chains agree when labels are removed. The paper supplies an exact answer in terms of a finite measure on the unit interval. See Pitman (1999), Theorem 1 and §3.1.

Setting

Let $\mathcal P_n$ be the partitions of $[n]=\{1,\ldots,n\}$ and $\mathcal P_\infty$ the partitions of the positive integers. A partition records which labels belong to the same block. The map $R_n$ restricts a partition to $[n]$ . A partition $\pi$ refines $\pi'$ when every block of $\pi$ is contained in a block of $\pi'$ . Thus blocks can merge as time grows, but never split.

A $\mathcal P_\infty$ -valued process is a coalescent here when its paths refine with time and each finite restriction $R_n$ has right-continuous step-function paths. For a partition of $[n]$ with $b$ blocks, each unordered choice of $k$ blocks, $2\le k\le b$ , merges into one block at rate $\lambda_{b,k}$ . Different choices are different possible transitions, each with that rate; the rate is not multiplied by the number of choices. The finite chain’s generator $Q_n$ records these transition rates, with each diagonal entry the negative sum of the other entries in its row. Its transition matrix after time $t$ is $\exp(tQ_n)$ .

An array $(\lambda_{b,k})$ is consistent when, for every $n<m$ and every initial partition of $[m]$ , restricting the $m$ -label chain to $[n]$ gives the same process law as the $n$ -label chain started at the restricted partition. A finite nonnegative Borel measure $\Lambda$ on $[0,1]$ supplies a rate array through an integral. The point mass at zero is included: because $0^0=1$ for natural powers, it gives pairwise mergers while higher-order merger rates vanish. These definitions follow Pitman (1999), pp. 1871–1872 and Lemma 18.

Formalization targets

Characterization of admissible rates

The goal is the existence-and-rates part of Theorem 1. For every nonnegative array $(\lambda_{b,k}:2\le k\le b)$ , a coalescent with these finite-chain merger rates exists from every $\pi\in\mathcal P_\infty$ if and only if there is a finite nonnegative measure $\Lambda$ on $[0,1]$ such that

\lambda_{b,k}=\int_{[0,1]}x^{k-2}(1-x)^{b-k}\,\Lambda(dx) \qquad(2\le k\le b).

The statement asks for one measure representing every rate in the infinite array, and a process from every initial partition. It fixes neither a particular measure nor a sample size. This is Theorem 1, equation (1).

Supporting claims

The milestone list follows §3.1: adjacent-size restrictions suffice to check consistency; consistency is equivalent to

\lambda_{b,k}=\lambda_{b+1,k}+\lambda_{b+1,k+1} \qquad(2\le k\le b);

and the nonnegative normalized array relation

\mu_{i,j}=\mu_{i+1,j}+\mu_{i,j+1},\qquad \mu_{0,0}=1,

is equivalent to a representation $\mu_{i,j}=\mathbb E[X^i(1-X)^j]$ for $X\in[0,1]$ . The final milestone states the uniqueness as well as the existence of the representing measure: equation (1) is a bijection between consistent arrays and finite measures. These are the claims in Lemma 18 and its proof, p. 1882.

Significance

The characterization turns an infinite family of nonnegative rates into one finite measure, and says exactly when finite chains at different sample sizes can be restrictions of a common partition process. The bijection also makes the measure identifiable from the rates. Without consistency, a chain specified at one size can change its law when an unobserved extra label is added; there would be no single process on $\mathcal P_\infty$ with those restrictions.

Pitman proved these results in 1999. The mission concerns machine-checking their statements and, eventually, their proofs. The current Lean items are open theorems with compiled statements; they do not yet have machine-checked proofs. The reusable part of a complete development would include finite partition generators, restriction of continuous-time Markov chains, and the moment representation for normalized nonnegative arrays. These tools also apply to other consistent families of random combinatorial structures.

Difficulty

Checking that each $Q_n$ defines a finite-state chain does not by itself construct a process on partitions of all integers. Deleting one label can change which apparent merger occurs in the smaller chain, so the rates must satisfy a precise identity across adjacent sizes. Even once those identities hold, the conclusion requires one joint law whose finite restrictions agree for all sizes and times, with right-continuous paths. The representation step must recover a genuine finite measure, including possible mass at zero, and must prove uniqueness; a mere numerical fit for finitely many entries cannot establish the theorem.

Formalization scope

The Lean partition type is Setoid (Fin n) at finite size and a type synonym of Setoid ℕ at infinite size. The paper’s positive labels are shifted to zero-based labels, preserving their order. The measurable structure on infinite partitions is generated by pairwise equivalence coordinates, equivalently by finite restrictions; finite partition spaces use the discrete measurable structure. The process path predicate requires refinement at every pair of ordered times and right continuity of every finite restriction. Finite-chain laws are specified at all finite collections of times through $\exp(tQ_n)$ , so a process cannot qualify merely by having the right initial state or a single marginal.

The measure is represented on $\mathbb R$ with zero mass outside $[0,1]`; integrals are over$ [0,1] $. Finiteness is explicit, preventing a nonintegrable Bochner integral from acquiring Lean’s default value. Natural-number exponents retain$ x^0=1 $at$ x=0 $. The rate array is read only for$ 2\le k\le b$, and the zero measure is allowed. The Fin 0 restriction is an additional tautological boundary case introduced by Lean’s natural numbers. The process sample space is a small Lean type, and the law is a probability measure on it.

Only the characterization sentence of Theorem 1 is targeted. Its later assertions about the strong Markov property, Feller semigroup, Skorohod path-space law, and weak continuity of the law map are outside this mission. Contributions toward those properties would need further path-space infrastructure. The formalized foundations and milestones can also support the paper’s Poisson construction and its later results, but those are separate targets.

Selected references

Jim Pitman, Coalescents with multiple collisions, Annals of Probability 27(4), 1870–1902, 1999. DOI: 10.1214/aop/1022874819.

7 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Inequalities on Partially Ordered Spaces 3: Ornstein's d̄-Distance of Stationary Real Processes Equals ∫ω⁰dP + ∫ω⁰dQ − 2 sup{∫ω⁰dR : R ≺ P, R ≺ Q}Research Paper

Motivation

Two stationary random sequences can have identical distributions at each individual time while differing in their dependence across time. Comparing only their one-time marginals therefore misses a feature relevant to stochastic-process comparison. Ornstein's $\bar d$ measures the cost of matching two whole stationary processes: it minimizes the expected discrepancy at one time over joint laws that are themselves stationary. Kamae, Krengel, and O'Brien use stochastic order to replace that optimization over pairs of processes with an optimization over a single common lower process in Theorem 8 of their 1977 paper. This mission formalizes that identity and the stationary coupling results supporting it.

Setting

A two-sided path with values in a space $E$ is a sequence $\omega=(\omega^n)_{n\in\mathbb Z}$ . The shift $T$ sends $\omega$ to the path whose coordinate $n$ is $\omega^{n+1}$ . A probability law $P$ on paths is stationary, written $P\in\mathcal S_T$ , when $P\circ T^{-1}=P$ . A law $\nu$ on pairs of paths is jointly stationary, written $\nu\in\mathcal S_S$ , when it is invariant under $S(\omega_1,\omega_2)=(T\omega_1,T\omega_2)$ . Its first and second marginals are denoted $\nu_1$ and $\nu_2$ . These are the objects defined at the start of Section 8.

When $E$ has a partial order, paths are ordered coordinatewise: $\omega_1\leq\omega_2$ means $\omega_1^n\leq\omega_2^n$ for every integer $n$ . For probability laws on any such space, write $P\prec Q$ if $\int f\,dP\leq\int f\,dQ$ for every bounded, measurable, increasing real function $f$ . Thus stochastic order compares laws through all bounded increasing observations, including observations that depend on several time coordinates. The paper introduces this order on a partially ordered Polish space whose order graph is closed and whose measurable sets are Borel sets in Section 1.

For real-valued paths, $\omega^0$ is the value at time zero. If the time-zero values under stationary laws $P$ and $Q$ are integrable, define Ornstein's distance by

\bar d(P,Q)=\inf_{\substack{\nu\in\mathcal S_S\\\nu_1=P,\,\nu_2=Q}} \int |\omega_1^0-\omega_2^0|\,\nu(d\omega_1,d\omega_2).

The stationary constraint on $\nu$ is part of the definition. It asks for a matching of the full processes, even though the cost is evaluated at one coordinate. The paper notes that this formula is equivalent to Ornstein's original definition for the processes considered here on p. 910.

Formalization targets

The ordered special case is Lemma 3: if $P\prec Q$ , then

\bar d(P,Q)=\int\omega^0\,Q(d\omega)-\int\omega^0\,P(d\omega).

The main target is Theorem 8, equation (18). For stationary real process laws $P,Q$ with finite first moments at time zero,

\bar d(P,Q)= \int\omega^0\,P(d\omega)+\int\omega^0\,Q(d\omega) -2\sup_{\substack{R\in\mathcal S_T\\R\prec P,\,R\prec Q}} \int\omega^0\,R(d\omega).

The supremum ranges over stationary laws of whole paths, ordered on the full coordinatewise path space. The milestone list includes Theorem 7's stationary monotone coupling, Lemmas 2 and 3, and three claims made inside the proof of Theorem 8: the triangle inequality $\bar d(P,Q)\le\bar d(P,R)+\bar d(R,Q)$ , which the paper asserts without proof ("since $\bar d$ is a distance"), the attainment of the infimum defining $\bar d$ , and the fact that the law of the coordinatewise minimum of an optimal stationary coupling lies below both $P$ and $Q$ . These are the statements from the paper that delimit the target.

Significance

The identity expresses a distance defined through stationary joint distributions using only stationary laws below both inputs in stochastic order. It therefore links a coupling cost to an order-theoretic optimization. In the ordered case, Lemma 3 evaluates the distance directly from the difference of means. The authors point out that the general formula replaces an infimum over laws on a product path space by a supremum over laws on one path space on p. 911.

The 1977 results are proved on paper; these mission statements are open Lean proof targets. A completed formalization would supply reusable definitions for stationary path laws, stationary couplings, stochastic order on path spaces, and $\bar d$ , together with checked statements about their interaction. It would also make the closed-order and first-moment conditions explicit at every point where a subsequent result uses them. The separate mission for Theorem 1 contains the general coupling characterization that the paper invokes in Theorem 7.

Difficulty

The cost in $\bar d$ inspects only time zero, but admissibility of a coupling involves every time coordinate at once. An arbitrary coupling of the time-zero marginals need not extend to a stationary coupling of the two processes. The stationary-coupling existence statement must preserve both full path marginals and the coordinatewise order. On the optimization side, taking an infimum in the real numbers is justified only after the coupling class is shown nonempty and its costs are finite; attaining the infimum requires more than those two facts. These are the obstacles made explicit by Theorem 7 and the proof of Theorem 8.

Formalization scope

The Lean path space is $\mathbb Z\to E$ , with Mathlib's product topology, Borel measurable structure, and coordinatewise order. The shift sends coordinate $n$ to the old coordinate $n+1$ . For Theorem 7, $E$ carries the paper's standing assumptions: it is Polish, its order is a closed partial order, and its measurable structure is Borel. Measurability of quantified functions is explicit, following the paper's convention that sets and functions under discussion are measurable. Theorem 8 and its Section 8 milestones specialize to $E=\mathbb R$ .

The real-valued definition of $\bar d$ takes the infimum over jointly stationary probability couplings with the specified full path marginals. Under the target's finite-first-moment hypotheses, the product coupling makes this class nonempty, every displayed cost is integrable, and costs are bounded below by zero. The goal states the supremum with an explicit finite least upper bound. It considers common lower laws with an integrable time-zero coordinate: such laws give the finite values intended by the paper, and this restriction does not remove the optimal value. These choices exclude totalized integrals and default real infima or suprema from supplying a spurious identity. Theorem 7's support condition is concentration on the closed set of ordered path pairs.

Reusable contributions include general facts about stationary measures on countable products, measurable coordinatewise order and meet maps, and stationary coupling compactness. The target specifically requires the order to test bounded increasing functions on the full path space; replacing it with a comparison of time-zero marginals would give a different claim. Likewise, dropping the joint stationarity constraint from the definition of $\bar d$ would turn it into the Kantorovich (Wasserstein-1) distance of the time-zero marginals, a different and in general smaller quantity; the formalization keeps that constraint. The source is the published Annals of Probability version; throughout this mission printed page $=$ PDF page $+898$ .

Selected references

T. Kamae, U. Krengel, and G. L. O'Brien, Stochastic Inequalities on Partially Ordered Spaces, The Annals of Probability 5(6), 899–912, 1977. DOI: 10.1214/aop/1176995659.

13 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 2: Wendel's Formula E[exp(−λ/V_n)] = e^{−λ} φ_α(λ)^{n−1} ψ_α(λ)^{−n} for PD(α, 0)Research Paper

Motivation

A random discrete distribution is a random sequence of nonnegative numbers summing to $1$ . Ranked in decreasing order, $V_1\ge V_2\ge\cdots$ , such sequences model the relative sizes of species in a population, of cycles of a random permutation, of excursion intervals of a Markov process, and of atoms of random measures used as priors in Bayesian nonparametrics. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ is the main family of such laws; Pitman and Yor (Ann. Probab. 1997) derived its properties from a stable subordinator.

The special case $\mathrm{PD}(\alpha,0)$ , $0<\alpha<1$ , describes the ranked lengths of the excursion intervals of a stable( $\alpha$ ) subordinator's range, or of a Bessel process away from zero, up to time $1$ . A basic question about it is the law of a single ranked term $V_n$ . The answer goes through the Laplace transform of $1/V_n$ :

Darling (1952) found the characteristic function of the limit of $S_n/X_{(n,1)}$ (sum over maximum of i.i.d. heavy-tailed variables), which is that of $1/V_1$ .
Lamperti (1961) derived the corresponding Laplace transform from renewal theory, for $n=1$ .
Wendel (1964) obtained the transform for every $n\ge2$ from the range of a stable subordinator.
Pitman and Yor (1997), Proposition 11, explained the formula through an exact decomposition of $1/V_n$ into independent, infinitely divisible pieces.

Setting

Fix $0<\alpha<1$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent, with $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha,n\alpha)$ on $(0,1)$ . Form the stick-breaking sequence $\tilde V_1=\tilde Y_1$ and $\tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ for $n\ge2$ , and let $V_1\ge V_2\ge\cdots$ be its terms in decreasing order. The law of $(V_n)$ is $\mathrm{PD}(\alpha,0)$ (Definition 1 of the paper, with $\theta=0$ ).

From $(V_n)$ define $R_n=V_{n+1}/V_n$ , $A_0=0$ and, for $n\ge1$ ,

A_n=\frac{V_1+\cdots+V_n}{V_{n+1}},\qquad \Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n}.

For $\lambda\ge0$ the paper's two Laplace exponents are

\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1\left(1-e^{-\lambda x}\right)x^{-\alpha-1}\,dx,

and $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

The proof represents $(V_n)$ through a Poisson random measure (PRM) $\Lambda_\alpha$ on $(0,\infty)$ with $\Lambda_\alpha(x,\infty)=Cx^{-\alpha}$ : its ranked points $\Delta_1>\Delta_2>\cdots$ satisfy $X_n:=C\Delta_n^{-\alpha}=\varepsilon_1+\cdots+\varepsilon_n$ with $\varepsilon_i$ i.i.d. standard exponential, and $V_n=\Delta_n/\sum_m\Delta_m$ .

Formalization targets

Goal: Proposition 11

For every $n\ge1$ ,

\frac1{V_n}=1+A_{n-1}+\Sigma_n\quad\text{a.s.},

where (i) $A_{n-1}$ is distributed as the sum of $n-1$ independent copies of $A_1$ , with $E[e^{-\lambda A_{n-1}}]=\phi_\alpha(\lambda)^{n-1}$ ; (ii) $\Sigma_n$ is distributed as the sum of $n$ independent copies of $\Sigma_1$ , with $E[e^{-\lambda\Sigma_n}]=\psi_\alpha(\lambda)^{-n}$ ; (iii) $A_{n-1}$ and $\Sigma_n$ are independent.

Milestones

Proposition 10 (iii): $X_n=LV_n^{-\alpha}$ , with $L=\lim nV_n^\alpha$ , are the arrival times of a unit Poisson process, and $V_n=X_n^{-1/\alpha}/\sum_mX_m^{-1/\alpha}$ .
Lemma 24 (i)–(ii): $C\Delta_n^{-\alpha}$ is gamma $(n)$ ; the ratios $\Delta_i/\Delta_n$ , $i<n$ , are the order statistics of $n-1$ i.i.d. variables of density $\alpha x^{-\alpha-1}$ on $(1,\infty)$ , independent of $(\Delta_n,\Delta_{n+1},\dots)$ .
(66): $P(A_1\in dx)=\alpha x^{-\alpha-1}dx\,1(x>1)$ .
(67): $E[e^{-\lambda\Sigma_n}\mid\Delta_1,\dots,\Delta_n]=\exp\left(-\Delta_n^{-\alpha}\int_0^1(1-e^{-\lambda u})\Lambda_\alpha(du)\right)$ .
Proposition 8: the $R_n$ are independent and $R_n\sim\mathrm{beta}(n\alpha,1)$ .
(34): $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

Consequence: Corollary 12 (Wendel's formula)

E\left[\exp(-\lambda/V_n)\right]=e^{-\lambda}\,\phi_\alpha(\lambda)^{n-1}\,\psi_\alpha(\lambda)^{-n}\qquad(\lambda\ge0).

Significance

The result. Proposition 11 turns $1/V_n$ into the sum of the constant $1$ and two independent variables, each a sum of i.i.d. pieces with explicit Laplace exponents. Wendel's formula (38) is a one-line consequence, and since $1/V_n>0$ it determines the law of $V_n$ . The same decomposition is reused later in the paper: Proposition 26 combines (35) and (67) into a conditional form of (38) given $R_1,\dots,R_{n-1}$ and $X_n$ , which the paper uses in later calculations.

Formalizing it. All results here are proved in the paper; none is machine-checked. A formal proof needs the Poisson representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10, itself resting on Perman–Pitman–Yor 1992), elementary but non-trivial facts about Poisson arrival times (gamma laws, order statistics, independence of ratios), and a conditional Laplace functional of a Poisson process. Each milestone is a self-contained target; Lemma 24 and (67) are statements about Poisson arrival times only and do not mention Poisson–Dirichlet laws.

Difficulty

The identity $1/V_n=1+A_{n-1}+\Sigma_n$ is algebra once $\sum_mV_m=1$ . The content is in the laws. On the stick-breaking side, the $V_n$ are the order statistics of a dependent sequence, and neither $A_{n-1}$ nor $\Sigma_n$ has an evident structure: the ranking destroys the independence of the $\tilde Y_n$ . The proof passes to the Poisson side, where the ranked points of a PRM have tractable conditional laws, and then must transport the conclusions back through a representation that holds only in distribution. Part (ii) requires a conditional computation (67) given $n$ points, followed by integration against a gamma law; part (iii) requires the mutual independence of all the ratios $R_n$ , an infinite family.

Formalization scope

The Lean development lives in namespace PoissonDirichlet.Wendel; its definitions file contains every object above.

Sequences are 0-based: V ω k is $V_{k+1}$ , Aseq (V ω) k is $A_k$ , Sigseq (V ω) k is $\Sigma_{k+1}$ , ratio (V ω) k is $R_{k+1}$ . Exponents $n-1$ and $n$ become k and k + 1.
$\mathrm{PD}(\alpha,0)$ is Definition 1 with $\theta=0$ . The law of $(\tilde Y_n)$ is a probability measure on sequences with independent coordinates of the stated beta laws. " $V$ has law $\mathrm{PD}(\alpha,0)$ " means $P(V\in s)$ equals the mass of the preimage of $s$ under the ranked stick-breaking map, for every measurable $s$ . Ranked values are defined with the extended cardinal Set.encard.
$A_n$ and $\Sigma_n$ are the $V$ -quotients of (31)–(32), not the $R$ -expressions; $\phi_\alpha,\psi_\alpha$ are the integrals (33)–(34), not Laplace transforms.
"Distributed as the sum of $m$ independent copies of $X$ " is equality with the $m$ -fold convolution power of the law of $X$ , the Dirac mass at $0$ when $m=0$ .
Every statement carries $0<\alpha<1$ except Lemma 24, which holds for all $\alpha>0$ .
The local time $L$ of (24) is a random variable with the hypothesis that $nV_n^\alpha\to L$ almost surely; this is its definition.
The PRM is used only through its ranked points, encoded by arrival times: $\Delta_n=(C/X_n)^{1/\alpha}$ with $X_n=\varepsilon_1+\cdots+\varepsilon_n$ , $\varepsilon_i$ i.i.d. standard exponential. This is the paper's own (27)–(28). In (67) the $\varepsilon_i$ are also assumed measurable, so that the conditioning $\sigma$ -algebra is a sub- $\sigma$ -algebra.
Lemma 24 (iii) is not stated; its only use is (67), which is stated. Corollary 12 states only the formula (38).

The formalization does not use Measure.map of a possibly non-measurable map in any definition: every equality of laws for such maps is stated through preimages. It does not use Set.ncard or limUnder. Every Laplace transform is the integral of a function with values in $(0,1]$ , and both exponent integrals are integrable under the stated parameter range, so no statement holds because an integral takes the junk value $0$ .

Useful infrastructure beyond this mission: arrival times of a Poisson process and their gamma and order-statistic laws; convolution powers of measures on $\mathbb R$ ; the Laplace functional of a Poisson random measure. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992.
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964.
J. Lamperti, A contribution to renewal theory, Proc. Amer. Math. Soc. 12:724–731, 1961.
D. A. Darling, The influence of the maximum term in the addition of independent random variables, Trans. Amer. Math. Soc. 73:95–107, 1952.

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 2: Branch and Bound with the Two-Machine Lower Bound Finds a Sequence of Least Mean Completion TimeResearch Paper

Motivation

In a two-machine flow shop, each of $n$ jobs is processed first on machine $A$ and then on machine $B$ , and the order of the jobs is to be chosen. For the makespan (the finishing time of the last job), Johnson (1954) gave an exact sorting rule. For the sum (equivalently, the mean) of the completion times, no such rule is known: the problem is NP-hard in the strong sense (Garey, Johnson and Sethi, 1976), and exact methods search the $n!$ sequences implicitly.

Ignall and Schrage (1965) were among the first to apply branch and bound to sequencing. They view the $n!$ sequences as the leaves of a tree of partial sequences, keep a list of partial sequences ranked by a lower bound, and always extend the most promising one. For the two-machine mean-completion-time problem they introduced a lower bound, built from two relaxations (one where machine $A$ is the bottleneck, one where machine $B$ is), that became the template for many later flow-shop bounds.

Setting

There are $n\ge1$ jobs; job $i$ has processing time $a_i$ on machine $A$ and $b_i$ on machine $B$ . A sequence is a permutation $\sigma$ of the jobs, processed in that order on both machines with every operation started as early as possible. The completion time $d_i(\sigma)$ of job $i$ is the time machine $B$ finishes it, and the objective is $\sum_{i=1}^n d_i(\sigma)$ .

A node $J_r$ is a partial sequence of $r$ jobs; $\bar J_r$ is the set of the $n-r$ jobs not in it; $k$ is the last job of $J_r$ and $d_k$ its completion time; $d_i$ ( $i\in J_r$ ) are the completion times of the jobs of $J_r$ . For an ordering $(i_1,\dots,i_{n-r})$ of $\bar J_r$ ,

T_r=\sum_{p=1}^{n-r}\Big[\sum_{j\in J_r}a_j+(n-r-p+1)a_{i_p}+b_{i_p}\Big],

and for an ordering $(j_1,\dots,j_{n-r})$ of $\bar J_r$ ,

S_r=\sum_{p=1}^{n-r}\Big[\max\Big(d_k,\sum_{j\in J_r}a_j+\min_{i\in\bar J_r}a_i\Big)+(n-r-p+1)b_{j_p}\Big].

$\hat T_r$ and $\hat S_r$ are their minima over all orderings of $\bar J_r$ , and the lower bound of the node is

LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r).

The procedure starts with a list holding only the empty node. A step removes the first node, creates one child for every unscheduled job by appending it, and inserts the children into the list ranked by $LB$ (a new node goes before old nodes with equal bound). It stops the first time the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the procedure finds a sequence of least mean completion time

For all real data, (i) the procedure reaches a list whose first node $P$ is terminal, and (ii) whenever that happens, the sequence $\sigma^\ast$ formed by $P$ and its one unscheduled job satisfies

\sum_{i=1}^n d_i(\sigma^\ast)\le\sum_{i=1}^n d_i(\sigma)\qquad\text{for every sequence }\sigma .

Milestones

For $1\le r\le n-1$ and every sequence $\sigma$ beginning with $J_r$ : $T_r$ of the order in which $\sigma$ processes $\bar J_r$ is at most $\sum_{i\in\bar J_r}d_i(\sigma)$ , hence so is $\hat T_r$ (pp. 405–406).
An ordering of $\bar J_r$ by increasing $a_i$ attains $\hat T_r$ (p. 406).
An ordering of $\bar J_r$ by increasing $b_j$ attains $\hat S_r$ (p. 406).
The analogue of 1 for $S_r$ and $\hat S_r$ (p. 406).
$LB(J_r)\le\sum_i d_i(\sigma)$ for every $\sigma$ beginning with $J_r$ (p. 406).
At depth $n-1$ , $LB$ equals the value of the node's unique completion (labelled: what the stopping rule of p. 402 needs).
Without delays, job $i_p$ completes at $\sum_{J_r}a_j+a_{i_1}+\dots+a_{i_p}+b_{i_p}$ and $\sum_{\bar J_r}d_i=T_r$ (pp. 405–406).
The three-job example of p. 408: 1–2 is optimal for jobs 1, 2, while 3–2–1 is optimal for all three.

Significance

The goal is the correctness of the paper's algorithm for the two-machine problem: the sequence it returns is optimal, not merely good, and it returns one for every input. The lower-bound milestones are the paper's own justification of its bound, and the sorting milestones show that the bound is computable in $O(n\log n)$ per node rather than by a minimization over $(n-r)!$ orderings.

On the formal side, no item on the platform treats flow-shop lower bounds or branch and bound over sequences; the nearest is the branch-and-bound mission for jointly constrained biconvex programs (BiconvexProg.BranchBound, Al-Khayyal and Falk 1983), an unrelated algorithm over boxes. The paper's arguments are short and informal ("it should be evident"); the formalization makes explicit that the $S_r$ bound holds for every order and every input, which the paper derives only by analogy with $T_r$ . The published definitions of Johnson's as-soon-as-possible schedule (from the Johnson 1954 missions) are reused for the completion times.

Difficulty

The two halves of the bound are relaxations of different kinds. $T_r$ ignores waiting on machine $B$ ; $S_r$ ignores idle time on machine $B$ after its first job of $\bar J_r$ and replaces that job's machine- $A$ time by the smallest one. The paper's description of $S_r$ as "the sum of the completion times" when $\min b\ge\max a$ is not an identity, since $\min a$ replaces $a_{j_1}$ ; only the inequality is true, and it has to be proved for the given order directly. The sorting claims are rearrangement inequalities, with the coefficient $n-r-p+1$ decreasing in the position.

The goal is a statement about all $n!$ sequences, while the procedure only ever looks at the nodes on its list, whose length changes at every step. The tempting one-line justification, that the first terminal node has the smallest bound, says nothing by itself about sequences that are not descendants of nodes still on the list, nor about whether the bound of a terminal node is the value of its sequence; and termination of the search has to be shown, not assumed.

Formalization scope

Jobs are Fin n (the paper's $1,\dots,n$ shifted to $0,\dots,n-1$ ); processing times are arbitrary reals, with no sign condition; all statements are true without one.
Completion times of a full sequence come from Johnson's asapC2 (referenced definition JohnsonFlowShop.TwoStage.asapStart2). The objective is the sum of the completion times; the paper's mean differs by the fixed factor $1/n$ .
A node is a list of jobs; "a sequence begins with $J_r$ " means $J_r$ is a prefix of its list of jobs.
$\hat T_r$ and $\hat S_r$ are defined as minima over all orderings of $\bar J_r$ , not by a sorted order; that sorting attains them is milestones 2 and 3. Defining them by sorting would make those milestones true by definition.
At the root ( $r=0$ ) $d_k$ is read as $0$ ; the root is never ranked, and the lower-bound milestones are stated for $1\le r\le n-1$ .
Terminal nodes are at depth $n-1$ . The paper says "a node that has scheduled all $n$ jobs"; its own example stops at a node with three of four jobs, and its node counts end at level $n-1$ .
Explicit readings: "is a lower bound" means $\le$ the objective of every sequence beginning with the node; "will exceed" means $\ge$ ; "the problem is solved: that node's sequence is an optimal one" means termination plus optimality over all $n!$ sequences.
A trivializing formalization is ruled out: the bound is not taken over an unrestricted or empty set of orderings (the set of orderings of $\bar J_r$ is nonempty), optimality is over all permutations rather than over the nodes the run visits, and termination is part of the goal.
Not formalized: the reduction to permutation schedules (the paper's footnote on p. 401 asserts it for mean completion time without proof, and no platform item proves it), dominance discarding (pp. 403–405), the jobset generator, Tables I–III and the 9-job examples.

Proofs of any milestone, and reusable lemmas on as-soon-as-possible two-machine schedules (completion times of a prefix, monotonicity in the start time), are welcome.

Selected references

E. Ignall and L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
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 and 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
A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Job Matching, Coalition Formation, and Gross Substitutes 6: When Workers Are Alike in Production, Gross Substitutes Is Equivalent to Nonincreasing Returns to WorkersResearch Paper

Motivation

Kelso and Crawford's 1982 Econometrica paper studies a labor market in which firms hire sets of heterogeneous workers at individually negotiated salaries. Their existence results for the core and for competitive equilibrium, and the convergence of their salary-adjustment process, all rest on one hypothesis about each firm's technology, the gross-substitutes condition (GS): raising some workers' salaries never makes a firm drop a worker whose salary did not change. The condition has since become central to matching with contracts, ascending auctions and the theory of discrete convexity (Hatfield and Milgrom 2005; Fujishige and Yang 2003). It is defined through the firm's demand correspondence rather than through the production function, so its economic content is not obvious.

Section 6 of the paper explains that content. Its first result, Theorem 6, says that when workers are alike in production, (GS) is exactly the familiar requirement of nonincreasing returns to workers. This mission formalizes Theorem 6, the two halves of its proof, and the companion claim that with two heterogeneous workers (GS) is equivalent to subadditivity.

Setting

Fix a finite set $W$ of $m$ workers and a single firm. Its production technology is a function $y : 2^W \to \mathbb{R}$ ; $y(C)$ is the gross product when the firm hires the set $C$ . A salary vector $s \in \mathbb{R}^W$ assigns to each worker $i$ the salary $s_i$ the firm must pay to hire him or her. The firm's net profit is

\pi(C; s) = y(C) - \sum_{i \in C} s_i ,

and $C$ is demanded at $s$ , written $C \in M(s)$ , if it maximizes $\pi(\,\cdot\,; s)$ over all subsets of $W$ (problem (A) of the paper). The technology satisfies (GS) if for all salary vectors $s \le \tilde s$ and every $C \in M(s)$ there is $\tilde C \in M(\tilde s)$ with

T(C) = \{\, i \in C : \tilde s_i = s_i \,\} \subseteq \tilde C .

Workers are alike in production when the product depends only on how many are hired: $y(C) = \bar y(|C|)$ for some $\bar y : \mathbb{N} \to \mathbb{R}$ . The workers remain distinct individuals, since their salaries can differ. The function $\bar y$ has nonincreasing returns to workers (DR) if

\bar y(w + 1) - \bar y(w) \le \bar y(w) - \bar y(w - 1) \qquad \text{for every integer } w,\ 1 \le w \le m - 1 .

A technology $y$ is subadditive if $y(C \cup D) \le y(C) + y(D)$ for disjoint $C, D \subseteq W$ .

In the Lean development these are profit, IsDemanded, GrossSubstitutesOn y Set.univ, DR (Fintype.card W) ybar and Subadditive y, in the namespace KelsoCrawford.Returns.

Formalization targets

Goal: Theorem 6 (p. 1499)

For every $\bar y : \mathbb{N} \to \mathbb{R}$ ,

\text{(DR) for } \bar y \text{ on } \{0, \dots, m\} \iff C \mapsto \bar y(|C|) \text{ satisfies (GS) on } \mathbb{R}^W .

Milestones

(DR) implies (GS) (proof of Theorem 6, p. 1499).
If (DR) fails, (GS) fails (proof of Theorem 6, pp. 1499–1500): if for some $w$ with $1 \le w \le m - 1$

\bar y(w + 1) - \bar y(w) > \bar y(w) - \bar y(w - 1), \tag{19}

then $C \mapsto \bar y(|C|)$ violates (GS). 3. Two workers (p. 1500), off the goal's path: if $|W| = 2$ and $y(\emptyset) = 0$ , then $y$ satisfies (GS) if and only if $y$ is subadditive, that is $v_1 + v_2 \ge v_{12}$ .

Significance

The result itself. Theorem 6 gives a production-side reading of (GS): restricted to identical workers it is nonincreasing returns, so (GS) can be viewed as the generalization of that convexity condition to heterogeneous workers. The paper uses this reading to explain why something like (GS) is needed for existence: without it the core and the competitive equilibrium may fail to exist, as the example of Section 6 shows (mission 7 of this series). The two-worker claim locates the boundary further: with two workers (GS) is subadditivity, while with three or more subadditivity is no longer enough.

Formalizing it. Nothing of this paper was on Prove2Me before this series. Theorem 6 is a proved result in the paper. This draft provides compiling Lean statements of both directions, with (GS) in the paper's own form (real salary vectors and the set $T(C)$ ), and of the two-worker characterization; their proofs remain open. A completed mission would provide machine-checked proofs of those statements. The statements fix the boundary conventions exactly (which $w$ are constrained, what happens with zero or one worker), which the informal argument leaves implicit. The definitions of profit, demand and (GS) are the same as in the other missions of the series (1–5 and 7), so proofs here are reusable there.

Difficulty

For (DR) $\Rightarrow$ (GS), the natural argument sorts workers by salary and observes that a profit-maximizing firm hires the $w^*$ cheapest workers. With ties among salaries this description is not literally true (any $w^*$ cheapest workers will do), and after a salary increase the new optimal size and the new ranking change at once; showing that some new maximizer keeps every worker whose salary stayed fixed requires a careful exchange argument rather than a monotone comparison of indices. For the converse, a single failure of (DR) must be turned into an explicit pair of salary vectors; the construction must make one worker strictly demanded before the change and strictly undemanded after it, which requires controlling every competing set, not only the sets of the critical sizes $w$ and $w + 1$ . The two-worker characterization requires a case analysis over the four candidate demands at every salary pair, including ties.

Formalization scope

Workers form an arbitrary finite type W with m = Fintype.card W; a technology is a function Finset W → ℝ, and "alike in production" is the technology fun C => ybar C.card with ybar : ℕ → ℝ. Salaries are arbitrary real vectors W → ℝ, and (GS) is required on all of $\mathbb{R}^W$ (Set.univ), the continuous version that Theorem 6 is about. A discrete market can satisfy (GS) on its salary grid while its continuous version does not, so the discrete version is a different statement and is not targeted here. (DR) is written for natural numbers with 1 ≤ w and w + 1 ≤ m, so that w - 1 never truncates. For $m \le 1$ it is vacuous, and no lower bound on $m$ is imposed. Neither (MP) nor (NFL), $\bar y(0) = 0$ , is assumed in Theorem 6: the paper uses neither, and adding them would weaken the theorem. The two-worker claim keeps the paper's normalization $y(\emptyset) = 0$ and uses its general definition of subadditivity over disjoint pairs.

A trivializing formalization would restrict (GS) to a single salary vector, quantify demand over a subfamily of sets, or replace "some demanded set contains $T(C)$ " by "the given set does", and is ruled out by the definitions above, which follow the paper's (A) and (GS) word for word. The read-out of the goal as two milestones is the paper's own split of its proof.

Infrastructure needed: finite sums over Finset, sorting of a finite salary vector, and elementary facts on concave sequences. Contributions that would be reusable beyond this mission include a general lemma that concave functions of cardinality yield gross-substitutes demand, and the link between (GS) and M $^\natural$ -concavity of set functions (Murota's gross-substitutes axioms are on Prove2Me as Shuze Chen's DiscreteConvex_MConvexFunctionsC_MNatGS, a related but different object: one price per good and integer bundles). Proofs of either direction, of the two-worker claim, or of intermediate lemmas are welcome.

Selected references

A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6) (1982), 1483–1504. https://doi.org/10.2307/1913392
V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2) (1981), 437–450. https://doi.org/10.2307/1913320
S. Fujishige and Z. Yang, A note on Kelso and Crawford's gross substitutes condition, Mathematics of Operations Research 28(3) (2003), 463–469. https://doi.org/10.1287/moor.28.3.463.16393
J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4) (2005), 913–935. https://doi.org/10.1257/0002828054825466
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Monotone Comparative Statics I: The Argmax Is Monotone Nondecreasing in (t, S) If and Only If f Is Quasisupermodular in x and Has the Single Crossing Property in (x; t)Research Paper

Why monotone comparative statics matters

An optimization problem often changes when a parameter changes: a price rises, a constraint expands, or a strategic environment shifts. Comparative statics asks whether the optimal choice moves in a predictable direction. The usual numerical tools, such as derivatives, can be unavailable when choices form a discrete set or the objective is neither smooth nor concave. Milgrom and Shannon's Monotonicity Theorem gives a condition expressed entirely through order and preference comparisons. It applies to individual optimization problems and supplies the order argument used later in their paper for games with strategic complementarities.

Their 1994 paper moves beyond cardinal conditions such as supermodularity and increasing differences. Those conditions imply useful comparative statics, but they can change under a strictly increasing transformation of the objective even though every argmax set stays the same. Quasisupermodularity and single crossing describe the comparisons that actually govern the argmax. The theorem characterizes these conditions through the behavior of optimizers over all constraint sets, rather than giving only a sufficient test. The historical relationship and the claims in this paragraph are described in Milgrom and Shannon, Sections 1–2.

Ordered choices, constraints, and preferences

Let $X$ be a lattice: a partially ordered choice set in which every two choices $x,y$ have a meet $x\wedge y$ and a join $x\vee y$ . Let $T$ be a partially ordered parameter set and $f:X\times T\to\mathbb R$ an objective. For any constraint set $S\subseteq X$ , define the possibly empty maximizer set

M(t,S)=\operatorname{argmax}_{x\in S}f(x,t)=\{x\in S: f(y,t)\le f(x,t)\text{ for every }y\in S\}.

The strong set order, written $A\le_s B$ , compares subsets of the lattice by requiring $a\wedge b\in A$ and $a\vee b\in B$ for every $a\in A$ and $b\in B$ . It can compare feasible sets as well as sets of optimizers. On singleton sets it agrees with the order on $X$ . It also holds vacuously if either set is empty; it is reflexive at $S$ exactly when $S$ is a sublattice. These are the paper's conventions on page 159.

A function $g:X\to\mathbb R$ is quasisupermodular if, for every $x,y\in X$ , both

g(x\wedge y)\le g(x)\Rightarrow g(y)\le g(x\vee y),\qquad g(x\wedge y)<g(x)\Rightarrow g(y)<g(x\vee y)

hold. The single crossing property of $f$ in $(x;t)$ requires, whenever $x''<x'$ and $t''<t'$ , that a weak or strict preference for $x'$ over $x''$ at $t''$ remains respectively weak or strict at $t'$ . The strict version sends even a weak preference at $t''$ to a strict one at $t'$ . These definitions are given on pages 160 and 162.

Formalization targets

Theorem 4: the monotonicity equivalence

The main target is Theorem 4 on page 162:

\bigl[\forall t\le t',\ S\le_s S': M(t,S)\le_s M(t',S')\bigr] \quad\Longleftrightarrow\quad \bigl[\forall t,\ f(\cdot,t)\text{ is quasisupermodular on }X\bigr] \land\bigl[f\text{ has single crossing in }(x;t)\bigr].

The milestone list records the two necessity claims and the sufficiency claim separately, using the three corresponding passages of the paper's proof. The goal keeps both directions together. It imposes no restriction on which subsets may be used as constraints.

Consequences and the stronger selection statement

Corollary 1 characterizes quasisupermodularity alone through monotonicity as the constraint set changes, with no varying parameter. Corollary 2 says that the maximizers over a sublattice themselves form a sublattice. The reflexivity remark identifies when $S\le_s S$ holds. Theorem 4′ uses the strict single crossing property and a nondecreasing feasible-set correspondence $S:T\to 2^X$ to conclude that every selection of maximizers is nondecreasing. These nearby results share the definition layer with the main theorem and give distinct targets for the formal development.

What the result supplies

The equivalence turns an order property of an entire family of optimization problems into two properties of the objective. In particular, its converse shows that if every feasible-set comparison produces monotone maximizers, then quasisupermodularity and single crossing are forced. This matters for problems where an analyst can reason about choice behavior more directly than about algebraic properties of $f$ . The corollaries also separate the effects of constraints and parameters and describe the structure of the optimal-choice set. The paper develops these consequences on pages 162–163.

The theorem is proved in the paper. The remaining work here is a machine-checked Lean proof of the ordinal characterization, its two directions, and the adjacent consequences. Published Prove2Me definitions already encode the strong set order, and its Topkis series covers related cardinal hypotheses such as supermodularity and increasing differences. This mission adds the paper's quasisupermodularity and single crossing predicates and seeks formal proofs of the distinct ordinal results. The separate characterization and linear-perturbation results of the same paper are targets of the other missions in this series.

Where the proof is difficult

The obstacle is the interaction of two orders. An increase in $t$ changes preferences, while an increase in $S$ changes which choices can be compared. A pointwise claim that an optimizer rises does not follow from either order condition alone, particularly when maximizers tie or are incomparable. The main theorem concerns sets of maximizers under the strong set order, so both the meet and join of optimizers at two parameter–constraint pairs must land in the correct maximizing sets. Conversely, observing monotonicity for one fixed feasible set cannot establish quasisupermodularity; the equivalence relies on monotonicity across every constraint set. The weak and strict preference clauses have different roles, so replacing either by the other changes the target. These are the distinctions visible in Theorem 4 and its proof.

Formalization scope

Lean represents $X$ with Lattice, $T$ with PartialOrder, and $f:X\to T\to\mathbb R$ in curried form. No finiteness, total order, topology, measurability, or maximizer-attainment hypothesis is imposed. The paper's product order for product lattices is Lean's usual componentwise order. The imported Supermodularity.Lattices.InducedSetOrder is exactly the paper's strong set order, including its behavior on empty sets. The definition argmaxOn returns the set of points in $S$ whose objective value bounds every value attained in $S$ ; it may be empty.

Quasisupermodularity is encoded with a reusable set argument but applied to Set.univ in every theorem here, so the property concerns the whole lattice. Single crossing compares strictly ordered choices and strictly ordered parameters and preserves both weak and strict preferences. ArgmaxMonotone compares weakly ordered parameters and all constraint sets under the strong set order. Theorem 4′ encodes a selection on an arbitrary domain $D\subseteq T$ where maximizers actually exist; it makes no global existence assertion. For Corollary 2, an arbitrary parameter is fixed and its objective is written $g:X\to\mathbb R$ .

These choices rule out easy specializations that would change the theorem: taking $X$ to be a chain, restricting quasisupermodularity to a selected feasible set, demanding nonempty argmax sets, or dropping strict preference clauses. The reusable development consists of the maximizer-set definition, the two ordinal predicates, and their relation to the published strong set order. Contributions proving the goal, its three proof-direction milestones, the corollaries, and the selection theorem all fit this scope.

Selected references

Paul Milgrom and Chris Shannon, Monotone Comparative Statics, Econometrica 62(1), 1994, 157–180. DOI: 10.2307/2951479.

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Potential Games 1: A Game Is an Exact Potential Game If and Only If I(γ, u) = 0 on Every Simple Closed Path of Length 4Research Paper

Why this question matters

In a strategic game, each player evaluates a change in their own strategy using that player's own payoff. These incentives need not point in a common direction. A potential game is a case in which one real-valued function records every player's payoff change under a unilateral deviation. This common function lets questions about incentives be expressed as questions about one object on the space of strategy profiles. Monderer and Shapley's 1996 paper introduced several kinds of potential and gave a local characterization of the exact kind. The characterization is the subject of this mission.

The local test matters because the defining condition appears to require finding an unknown potential on the entire profile space. Theorem 2.8 says that a condition on four-step cycles already determines whether such a function exists, even when individual strategy sets are infinite. The paper compares this characterization with the familiar idea that a conservative field has zero integral around closed curves; here the “integral” is a finite sum of payoff changes along unilateral deviations (Monderer and Shapley, pp. 130–131).

Games, deviations, and path sums

Let $N$ be a finite set of players. For each player $i\in N$ , let $Y^i$ be a strategy set, and let $Y=\prod_{i\in N}Y^i$ be the set of pure strategy profiles. The payoff of player $i$ is a function $u^i:Y\to\mathbb R$ . If $y\in Y$ , the notation $(y^{-i},x)$ means the profile obtained by replacing only player $i$ 's strategy with $x\in Y^i$ . The strategy sets themselves are not required to be finite in this section of the paper (p. 127).

An exact potential is a function $P:Y\to\mathbb R$ such that, for every $i$ , every opponents' profile $y^{-i}$ , and every $x,z\in Y^i$ ,

u^i(y^{-i},x)-u^i(y^{-i},z) =P(y^{-i},x)-P(y^{-i},z).

A game admitting such a function is an exact potential game. The paper uses the shorter term “potential game” for this class when the adjective is clear (pp. 127–128, equation (2.2)).

A path $\gamma=(y_0,\ldots,y_L)$ is a sequence in which each step changes exactly one player's strategy to a different value. Write $i_k$ for the unique player who moves from $y_{k-1}$ to $y_k$ . The path sum of the payoff vector $u$ is

I(\gamma,u)=\sum_{k=1}^{L} \bigl(u^{i_k}(y_k)-u^{i_k}(y_{k-1})\bigr).

The path is closed when $y_0=y_L$ . It is simple closed when, in addition, the vertices $y_0,\ldots,y_{L-1}$ are pairwise distinct. Its length is $L$ , the number of steps and the number of vertices before the final return. These definitions follow pp. 128, 130–131.

Formalization targets

Theorem 2.8: four equivalent conditions

For a game with finitely many players, Theorem 2.8 asserts the equivalence of all four claims:

\begin{aligned} &\Gamma\text{ has an exact potential};\\ &I(\gamma,u)=0\quad\text{for every finite closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every finite simple closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every simple closed path }\gamma\text{ of length }4. \end{aligned}

The last condition is a local criterion, but the goal keeps the full four-way equivalence of the published theorem, p. 131. The milestone list follows five claims in its Appendix A proof: vanishing path sums from a potential, path independence, construction of a potential from vanishing closed-path sums, the local exchange of two different players' moves, and the reduction from all closed paths to length-four simple cycles (pp. 138–139).

Related results in the same development

Corollary 2.9 expresses the length-four test directly as a zero sum of payoff changes around four corners obtained by varying two players' strategies. Lemma 2.7 says that two exact potentials for the same game differ by one additive constant. Both are included as supporting statements from the same definition layer, although they are not milestones in the attack path for Theorem 2.8 (pp. 130–131).

What the result provides

Theorem 2.8 turns existence of a global function into a test on local cycles. Corollary 2.9 makes those cycles visible in payoff tables: fixing all but two players, the alternating sum around each two-player rectangle must vanish. For finite strategy sets this gives a direct finite collection of conditions; for infinite strategy sets the theorem remains a mathematical characterization without claiming a finite algorithm (Monderer and Shapley, p. 131).

The original paper proves these statements. The formalization work is to represent games, paths, path sums, and the four-way equivalence in Lean, then supply machine-checked proofs. The present mission contains compiled statements with open proofs. Its definition modules are also reusable for the paper's other results about potentials, improvement paths, and congestion games.

Where the proof is difficult

The challenging direction is that zero sums on simple length-four cycles force zero sums on every closed path. A closed path may repeat vertices and may involve more than two players. A direct appeal to the local condition does not cover such a path. The Appendix A argument uses changes to a path's sequence of deviators, and its informal treatment of adjacent moves by the same player leaves a boundary case: the two moves can cancel, so replacing them by one move would create a null step, which the definition of a path excludes. A formal proof must account for this case while preserving the paper's exact statement (pp. 138–139).

Formalization scope

Lean represents the finite player set by a finite type $\iota$ and a profile by a dependent function $y:\prod_{i:\iota}Y^i$ . Strategy sets $Y^i$ remain arbitrary types. The operation $(y^{-i},x)$ is a one-coordinate update. A finite path stores $L+1$ vertices and its deviator at each of the $L$ steps; the step condition determines that deviator uniquely. Closed paths of length zero are allowed and have sum zero. The paper prints $n$ , the number of players, as the upper limit of the path sum on p. 130, although its summands are indexed by path steps. The Lean definition sums over all $L$ steps, as the surrounding definition and later equations require.

The four-cycle hypothesis quantifies only over simple closed paths of exactly four genuine steps. It is not replaced by all four-step walks or by cycles with null or simultaneous deviations. The goal retains all four clauses rather than only its shortest equivalence. Corollary 2.9 explicitly requires the two varying players to be distinct; this is implicit in the paper's four-corner construction. No finite-strategy assumption is imposed on Theorem 2.8, Corollary 2.9, or Lemma 2.7.

The development needs ordinary finite sums, dependent functions, coordinate updates, and finite-indexed paths. Its path and potential definitions are intended as an interface for later work. Contributions proving any of the five source-backed milestones, the goal, or the two related statements are within scope.

Selected references

Dov Monderer and Lloyd S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. DOI: 10.1006/game.1996.0044.

10 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 1: Under PD(α, 0) the Ratios V_{n+1}/V_n Are Independent with beta(nα, 1) LawsResearch Paper

Motivation

Random partitions describe a population split into species, clusters, or types. If the species frequencies are put in decreasing order, the first frequency is the largest species, the second is the next largest, and so on. The Poisson–Dirichlet distribution gives a family of laws for these ranked frequencies. Its two parameters connect different random partition models, while the one-parameter case $\mathrm{PD}(\alpha,0)$ has a particularly direct description through ratios of neighboring frequencies. Pitman and Yor state that these ratios are independent and have explicit beta distributions, even though the ranked frequencies themselves have a complicated joint law (Pitman and Yor 1997, Proposition 8).

The result matters when a statistic of a random partition depends on the relative sizes of its largest components. A ratio $V_{n+1}/V_n$ describes the gap between two successive ranked species without requiring their total scale. An independent sequence of such ratios also gives a way to generate the entire ranked sequence. The paper records this converse immediately after Proposition 8 as Corollary 9 (Pitman and Yor 1997, p. 862).

Setting

Fix $0<\alpha<1$ . A beta $(a,b)$ distribution is a probability distribution on $(0,1)$ with density proportional to $x^{a-1}(1-x)^{b-1}$ . Let $\widetilde Y_n$ , for $n=1,2,\ldots$ , be independent beta $(1-\alpha,n\alpha)$ random variables. They break an initial mass of one into successive stick lengths

\widetilde V_n=\widetilde Y_n\prod_{i=1}^{n-1}(1-\widetilde Y_i).

Sort these lengths in decreasing order, counting repeated values separately, and write the resulting sequence as $V_1\geq V_2\geq\cdots$ . The law of this ranked sequence is $\mathrm{PD}(\alpha,0)$ , the $\theta=0$ case of Definition 1 in the paper (Pitman and Yor 1997, p. 857). The paper's broader definition takes $0\leq\alpha<1$ and $\theta>-\alpha$ , with beta $(1-\alpha,\theta+n\alpha)$ stick factors. This mission retains that general definition so later statements use the same object, but its theorems concern $\theta=0$ and $0<\alpha<1$ .

Define the adjacent ranked ratio $R_n=V_{n+1}/V_n$ . The source proves that the ranked masses are strictly positive almost surely under the Poisson–Dirichlet law, so these ratios have their ordinary probabilistic meaning (Pitman and Yor 1997, Proposition 2). The random sequence $R_1,R_2,\ldots$ is different from the independent stick factors $\widetilde Y_n$ : the latter are defined before ranking, whereas each $R_n$ compares consecutive masses after ranking.

Formalization targets

Goal: Proposition 8

For a sequence $(V_n)$ with $\mathrm{PD}(\alpha,0)$ law, the variables $R_n=V_{n+1}/V_n$ are mutually independent, and each has beta $(n\alpha,1)$ distribution. The equivalent cumulative distribution formula is part of the target:

\mathbb P(R_n\leq r)=r^{n\alpha}\qquad(n\geq1,\ 0\leq r\leq1).

The exponent and beta parameter use the paper's one-based $n$ . Independence concerns the full infinite family, rather than only pairs of ratios (Pitman and Yor 1997, Proposition 8, equations (21)–(22)).

Supporting targets

Proposition 10(i) establishes a local-time limit $L=\lim_{n\to\infty}nV_n^\alpha$ , both almost surely and in $L^p$ for every real $p\geq1$ . Proposition 10(iii) identifies the transformed sequence $X_n=LV_n^{-\alpha}$ with the arrival times of a unit-rate Poisson process: it has the joint law of partial sums of independent standard exponential variables. The proposition also recovers $V_n$ by normalizing $X_n^{-1/\alpha}$ . Finally, the proof of Proposition 8 states that consecutive Poisson arrival ratios $X_n/X_{n+1}$ are independent beta $(n,1)$ variables (Pitman and Yor 1997, pp. 862, 870). These are the three curated milestones. Corollary 9 is included as a companion: independent beta $(n\alpha,1)$ ratios, inserted into the paper's convergent series and finite products, produce a $\mathrm{PD}(\alpha,0)$ sequence.

Significance

Proposition 8 converts a statement about the order statistics of infinitely many dependent masses into an explicit product law for their ratios. It gives direct distributional information about every neighboring pair in a Poisson–Dirichlet partition. Together with Corollary 9, it specifies both how to read the ratios from a ranked partition and how to reconstruct a ranked partition from ratios. The formulas can therefore serve as a common interface for calculations and simulation involving $\mathrm{PD}(\alpha,0)$ (Pitman and Yor 1997, Propositions 8–10).

The mathematical results in this mission were proved in the 1997 paper; the open work here is a machine-checked Lean proof of their stated forms. Such a development would add reusable facts about infinite beta sequences, ranked stick lengths, Poisson arrival times, and their joint laws. The independent-arrival-ratio statement is useful beyond the Poisson–Dirichlet setting because its assumptions only concern standard exponential increments.

Difficulty

The stick factors are independent before their lengths are sorted, but sorting is a global operation: a particular ranked mass may have come from any stick index. Their independence therefore does not directly give independence of adjacent ranked ratios. Even a marginal calculation for one ratio does not establish mutual independence of the entire sequence. The local-time and arrival-time assertions in Proposition 10 encode the extra structure needed to state the joint result. The real technical burden is to relate the distribution obtained from ranked stick lengths to the distribution of an infinite Poisson arrival sequence, while retaining the almost-sure limits and normalization stated by the authors.

Formalization scope

Lean represents every sequence as a function $\mathbb N\to\mathbb R$ , with index $k=0$ denoting the paper's first index $n=1$ . stick implements equation (4); ranked defines the $(k+1)$ -st largest nonnegative length by upper-level-set cardinality, counted with multiplicity. It uses extended cardinality so an infinite upper-level set cannot be assigned cardinality zero. IsStickLaw records independence and the beta $(1-\alpha,\theta+(k+1)\alpha)$ coordinate laws. HasPD describes the distribution of the ranked stick sequence by probabilities of measurable preimages. This commits the mission to Definition 1 rather than a ratio construction of $\mathrm{PD}(\alpha,0)$ .

All mission theorems require $0<\alpha<1$ , and every source probability space is a probability measure. Ratios and negative real powers occur only as random quantities whose bases are positive almost surely under that law. Their exceptional values on null sets do not affect the distributional claims. The local time is identified by its almost-sure defining limit, rather than by a default value assigned when a limit fails. The $L^p$ clause uses the norm of the approximation error. The Poisson arrival law is stated jointly on measurable sets of infinite real sequences; it is not reduced to one-dimensional exponential marginals. These choices rule out vacuous interpretations through a nonmeasurable Measure.map, a finite-cardinality default on an infinite set, a junk integral, limUnder at a nonexistent limit, or a dropped parameter range.

The development needs Mathlib's beta and exponential measures, infinite product and independence APIs, measurable sequence spaces, real powers, infinite sums, and $L^p$ norms. Results about ranked values and arrival ratios would be reusable in later Poisson–Dirichlet missions. Contributions that establish these source statements at full strength, or their necessary measurable and summability infrastructure, fit the scope.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Annals of Probability 25(2):855–900, 1997. DOI: 10.1214/aop/1024404422.

5 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Large Deviations of Sums of Independent Random Variables 1: The Fuk–Nagaev Inequality P(S_n ≥ x) ≤ ΣP(X_i > y_i) + P_4, P_5 or P_6 for Truncated Moments of Order t ≥ 2Research Paper

Motivation

How likely is a sum of independent random variables to exceed a large level $x$ ? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in $x$ . Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds $P(S_n\ge x)$ by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.

The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), $P(S_n\ge x)\le c_t^{(1)}A_t^+x^{-t}+\exp\{-c_t^{(2)}x^2/B_n^2\}$ , is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.

Setting

Let $X_1,\dots,X_n$ be independent real random variables on a probability space, with distribution functions $F_i(u)=P(X_i<u)$ , and let $S_n=X_1+\dots+X_n$ . Fix a level $x>0$ , truncation levels $Y=\{y_1,\dots,y_n\}$ (positive numbers), and a number $y\ge\max_iy_i$ .

The truncated summands are $\tilde X_i=X_i$ if $X_i\le y_i$ and $\tilde X_i=0$ if $X_i>y_i$ , with sum $\tilde S_n=\sum_i\tilde X_i$ . The paper writes $\mu(\cdot,\cdot)$ , $B^2(\cdot,\cdot)$ and $A(t;\cdot,\cdot)$ for sums of truncated means, second moments and absolute moments of order $t$ , the arguments being the truncation levels. The three used here are

\mu(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u\,dF_i(u),\qquad B^2(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u^2\,dF_i(u),\qquad A(t;0,Y)=\sum_{i=1}^n\int_{0\le u\le y_i}|u|^t\,dF_i(u).

For $t\ge2$ , $0<\alpha<1$ and $\beta=1-\alpha$ , write $L=\log\big(\beta xy^{t-1}/A(t;0,Y)+1\big)$ and define

P_4=\exp\Big\{\beta\frac xy-\Big(\big(1-\tfrac\alpha2\big)\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},\qquad P_5=\exp\Big\{\Big(\beta-\frac{t\alpha}2\Big)\frac xy-\Big(\beta\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},

P_6=\exp\Big\{-\frac{\alpha x\,(\alpha x/2-\mu(-\infty,Y))}{e^tB^2(-\infty,Y)}\Big\}.

Finally $A_t^+=\sum_i\int_{u\ge0}u^t\,dF_i(u)$ and $B_n^2=\sum_i\operatorname{Var}X_i$ .

In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.

Formalization targets

Goal: Theorem 1.3 (p. 749)

Suppose $t\ge2$ , $0<\alpha<1$ , $\beta=1-\alpha$ and $B^2(-\infty,Y)<\infty$ . Write (1.4) for $\max[t,L]\ge\alpha xy/(e^tB^2(-\infty,Y))$ and (1.6) for $\max[t,L]<\alpha xy/(e^tB^2(-\infty,Y))$ . Then

\text{(1.4)}\implies P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+P_6,\qquad \text{(1.6)}\implies P(S_n\ge x)<\sum_{i=1}^nP(X_i>y_i)+P_4,

and if (1.6) holds together with $\beta\ge t\alpha/2$ or $\beta x\ge\mu(-\infty,Y)$ , then $P(S_n\ge x)<\sum_iP(X_i>y_i)+P_5$ . The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.

Milestones

The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for $P(\tilde S_n\ge x)$ ; the equivalence of (1.4) with $h_1\le\max[t/y,h_2]$ ; (1.19), $P(\tilde S_n\ge x)\le P_6$ under (1.4); $P(\tilde S_n\ge x)<P_4$ under (1.6); and (1.20), $P(\tilde S_n\ge x)<P_5$ .

Corollaries

Corollary 1.7 (1.23): for $\mathbb EX_i=0$ , $\beta=t/(t+2)$ , $\alpha=1-\beta$ ,

P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+\exp\Big\{-\frac{\alpha^2x^2}{2e^tB^2(-\infty,Y)}\Big\}+\Big(\frac{A(t;0,Y)}{\beta xy^{t-1}}\Big)^{\beta x/y}.

Corollary 1.8 (1.24): for $\mathbb EX_i=0$ , $A_t^+<\infty$ , $t\ge2$ ,

P(S_n\ge x)\le\Big(1+\frac2t\Big)^tA_t^+x^{-t}+\exp\Big\{-\frac{2e^{-t}x^2}{(t+2)^2B_n^2}\Big\}.

Significance

Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters $y_i$ , $y$ , $\alpha$ let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums ( $t$ -th moment inequalities of Rosenthal type follow by integrating it in $x$ ), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.

The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants $(1+2/t)^t$ and $2(t+2)^{-2}e^{-t}$ .

Difficulty

The obvious argument, Chernoff's bound applied to $S_n$ , fails at once: without exponential moments $\mathbb Ee^{hS_n}$ is infinite for every $h>0$ . Truncating the summands repairs this, but the bound then depends on the choice of the exponent $h$ , and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, $t/y$ and the minimisers $h_1$ , $h_2$ of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.

The corollaries need a separate step: Corollary 1.7 requires $\mu(-\infty,Y)\le0$ , which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for $P(X_i>\beta x)$ with the truncated moment $A(t;0,Y)$ so that the two polynomial terms add to exactly $A_t^+/(\beta x)^t$ .

Formalization scope

The summands are X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index $i$ stands for the paper's $i+1$ . $x>0$ , $y_i>0$ , $y\ge y_i$ and $y>0$ are hypotheses ( $y>0$ follows from the others when $n\ge1$ ).
Every integral $\int_E\varphi(u)\,dF_i(u)$ is the expectation of $\varphi(X_i)$ over the event $\{X_i\in E\}$ , with the endpoints of $E$ copied from the page. Powers with exponent $t$ are real powers; $A(t;0,Y)$ uses $|u|^t$ .
Added hypotheses. Finiteness of $B^2(-\infty,Y)$ is assumed as integrability of $X_i^2$ on $\{X_i\le y_i\}$ for each $i$ ; Lemma 1.4 assumes $X\in L^2$ (its $\beta=\mathbb EX^2$ is a number); Corollary 1.8 assumes each $X_i\in L^2$ , since Mathlib's variance is $0$ outside $L^2$ . On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by $0$ and the statements would become false.
Degenerate values. On the page $A(t;0,Y)=0$ makes $L=+\infty$ , so (1.4) holds. Lean's division by $0$ would make $L=0$ ; condition (1.4) is therefore the definition cond_1_4, which includes the case $A(t;0,Y)=0$ , and (1.6) is cond_1_6, which requires $A(t;0,Y)>0$ . For $A\ge0$ the two are exact complements. If $B^2(-\infty,Y)=0$ , $P_6$ and the exponential term of (1.23) take the page's limiting value $0$ , and so does the exponential term of (1.24) when $B_n^2=0$ ; Lean's $x/0=0$ would otherwise make them $1$ .
Ruled out. Stating the goal for the truncated sum $\tilde S_n$ instead of $S_n$ , or only the moment-generating-function bound, would replace the theorem by a step of its proof; the goal is about $P(S_n\ge x)$ , with the strict inequalities of (1.7) and (1.7a) kept strict.
Lemma 1.4 uses $\beta$ for $\mathbb EX^2$ ; it is unrelated to $\beta=1-\alpha$ of Theorem 1.3.
Reusable beyond this mission: Lemma 1.4 (a cumulant bound for variables bounded above) and the truncation inequality (1.8). Contributions welcome on any milestone, and on the corollaries independently of the goal.

Selected references

S. V. Nagaev, Large deviations of sums of independent random variables, Ann. Probab. 7(5):745–789, 1979. https://doi.org/10.1214/aop/1176994938
D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory Probab. Appl. 16(4):643–660, 1971. https://doi.org/10.1137/1116071

16 thms2 active usersReviewed

Completed

Control Theory Operations Research Stochastic Systems·Captain: mikedeng1

Distributed Scheduling Based on Due Dates and Buffer Priorities 2: Under Last Buffer First Serve the Number of Parts Stays Bounded, Eventually by (λc(ε)+γ)/(1−ρ−λε)Research Paper

Motivation

Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).

LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.

Timeline:

1990: Kumar and Seidman exhibit instability of clearing policies on a reentrant line with spare capacity.
1991: Lu and Kumar prove stability of FBFS (Theorem 1) and of LBFS (Theorems 2–3) under deterministic bursty arrivals. They also prove it for least slack and earliest due date (Theorem 4, Corollary 1), and show that a buffer priority policy can be unstable (Example 1).
1996: Dai and Weiss prove stability of the fluid models of FBFS and LBFS on reentrant lines (Math. Oper. Res. 21(1)), which by Dai's fluid limit theorem gives positive Harris recurrence for the stochastic versions.

Setting

A nonacyclic flow line has $S$ service centers; center $\sigma$ has $m_\sigma \ge 1$ identical machines, each processing one part at a time. Every part follows the same route through buffers $b_1, \dots, b_l$ : in buffer $b_i$ it waits at center $\sigma_i$ , then needs $\tau_i > 0$ units of uninterrupted processing on one machine of that center. A center may serve several buffers.

Parts are released into $b_1$ ; part $\pi$ is released at time $\alpha(\pi)$ and exits at time $e(\pi)$ , when its service at $b_l$ ends. Finitely many parts may be present at time $0$ , in any buffer, some already in service. With $u(t)$ the number of releases in $[0,t]$ , the arrivals are bursty with rate $\lambda$ and burst $\gamma$ if

u(t)-u(s)\le \lambda(t-s)+\gamma\qquad(0\le s\le t).\tag{1}

The work per machine that one part brings to center $\sigma$ is $w_\sigma=\sum_{i:\sigma_i=\sigma}\tau_i/m_\sigma$ , and the load is $\rho=\lambda\overline w$ with $\overline w=\max_\sigma w_\sigma$ . The capacity condition is $\rho<1$ (3). Also $\overline\tau=\max_j\tau_j$ , and $w^{(k)}$ is the maximum per-machine work brought to a center by a part in $b_k$ , counting only buffers $b_k,\dots,b_l$ (6).

Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from $b_i$ only if every buffer $b_j$ of its center with $j>i$ is empty. The number of parts in the system at time $t$ is $x(t)$ .

Formalization targets

Goal: Theorem 3, Stability of LBFS

Under (1) and (3), for every $\varepsilon>0$ with $1-\rho-\lambda\varepsilon>0$ ,

x(t)\le\max\Big\{(1+\rho+\lambda\varepsilon)x(0)+\lambda c(\varepsilon)+\gamma,\ \frac{2(\lambda c(\varepsilon)+\gamma)}{1-\rho-\lambda\varepsilon}\Big\}\quad(t\ge0),

\limsup_{t\to\infty}x(t)\le\frac{\lambda c(\varepsilon)+\gamma}{1-\rho-\lambda\varepsilon}.

Here $c(\varepsilon)$ is the explicit constant of the delay estimate. The paper prints the second bound as $\lambda c(\varepsilon)+\gamma/(1-\rho-\lambda\varepsilon)$ ; its proof establishes the form above, which is the one posed.

Milestones

The delay estimate behind the goal, in the order of its proof:

the base case (8) for the last buffer;
the one-step comparison (11) with the part just ahead;
the induction claim (10) for every truncated line $B^{(k)}=\{b_k,\dots,b_l\}$ : a part in $B^{(k)}$ with $x$ parts ahead exits within $c^{(k)}(\varepsilon)+(w^{(k)}+\varepsilon)x$ ;
Theorem 2, the contractive estimate

e(\pi)-\alpha(\pi)\le c(\varepsilon)+(\overline w+\varepsilon)x\qquad(\varepsilon>0),

for a part that finds $x$ parts in the system on release.

Then the Pipeline Property $e(\pi)-\alpha(\pi)\le\overline wx+o(x)$ , order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay $e(\pi)-\alpha(\pi)$ is bounded.

Significance

Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate $\overline w+\varepsilon$ : the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.

The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).

Difficulty

The obvious argument fails because under LBFS parts released later do interfere with a part $\pi$ : they occupy machines nonpreemptively at the low-priority buffers $\pi$ must still pass. So the delay of $\pi$ cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems $B^{(k)}$ , nested with an induction on the position of $\pi$ in its buffer. The constant $c^{(k)}(\varepsilon)$ is recomputed at every level from $c^{(k+1)}(\varepsilon/2)$ , so $\varepsilon$ is halved at each level. A formal proof must also handle what the paper treats informally:

the order in which parts leave buffers when several arrive at the same instant;
parts already in service at time $0$ ;
an empty system between busy periods.

Formalization scope

All declarations are in the namespace ReentrantScheduling.LBFS.

Buffers are 0-based in Lean: the paper's $b_i$ is index $i-1$ .
A run lists its parts in a fixed line order: parts present at time $0$ first (deeper buffers first, then earlier service start), then released parts by release time. This order breaks ties between simultaneous arrivals, and "parts ahead of $\pi$ " means the parts in the system that precede $\pi$ in it.
Service start times are in WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.
All counts (capacity, nonidling, (1), $x(t)$ ) are Set.encard, never Set.ncard, which would count an infinite set as $0$ and make the capacity rule vacuous.
The constants $c^{(k)}(\varepsilon)$ of (8)–(9) are explicit definitions that depend only on the line and $\varepsilon$ . A constant chosen after the run would let it depend on the arrivals or the initial state.
Theorem 3's bounds are inequalities in $[0,\infty]$ ; the lim sup is taken there, so it cannot be a junk value of an unbounded real function.
The standing assumptions of §II are hypotheses or part of the run predicate: nonidling, nonpreemptive, head-of-buffer service, $m_\sigma\ge1$ , $l\ge1$ . The positivity $\tau_i>0$ is pinned: the paper leaves it implicit.
Every theorem quantifies over all admissible LBFS runs. The empty run and nontrivial runs satisfy the hypotheses.

The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of $x(t)$ ).

Not posed here:

Example 1, which is already on the platform as QueueingStability.LuKumar.theorem31;
Theorem 4 and Corollary 1 (least slack, earliest due date), whose proof modifications the paper leaves to the reader;
Theorem 5 (several flow lines), whose proof is a sketch.

Selected references

S. H. Lu and P. R. Kumar, Distributed Scheduling Based on Due Dates and Buffer Priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
P. R. Kumar and T. I. Seidman, Dynamic Instabilities and Stabilization Methods in Distributed Real-Time Scheduling of Manufacturing Systems, IEEE Transactions on Automatic Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
J. G. Dai and G. Weiss, Stability and Instability of Fluid Models for Reentrant Lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Monte Carlo Bounding Techniques for Determining Solution Quality in Stochastic Programs: The Expected Sample-Average Optimal Value Is a Lower Bound on z* That Improves with Sample SizeResearch Paper

Motivation

Most stochastic programs that arise in practice, such as two-stage stochastic linear programs with recourse, have far too many scenarios to be solved exactly. The standard remedy is sample-average approximation: draw $n$ independent observations of the random data, replace the expectation by the sample mean, and solve the resulting deterministic problem. A candidate solution $\hat x$ found this way, or by any heuristic, comes with no guarantee. To judge it one needs a bound on its optimality gap $Ef(\hat x,\tilde\xi)-z^*$ , and estimating $Ef(\hat x,\tilde\xi)$ is routine; what is missing is a lower bound on the unknown optimal value $z^*$ .

Mak, Morton and Wood (Oper. Res. Lett. 24 (1999)) show that the optimal value of the sample-average problem supplies exactly this: its expectation never exceeds $z^*$ , and it can only move closer to $z^*$ as the sample size grows. The result requires almost no structure of the problem, and it underlies the batch-means confidence intervals on the optimality gap used throughout the stochastic programming literature, including the single- and two-replication procedures of Bayraksan and Morton (2006).

Timeline.

1960: Madansky's wait-and-see bound $z^*\ge E\min_{x\in X}f(x,\tilde\xi)$ (Management Sci. 6), the case $n=1$ of the result.
1998: Norkin, Pflug and Ruszczyński use stochastic lower bounds of this kind inside a branch-and-bound method (Math. Programming 83); the paper notes that they verified the monotonicity independently.
1999: Mak, Morton and Wood prove $Ez_n^*\le z^*$ (Theorem 1) for arbitrary $X$ and $Ez_n^*\le Ez_{n+1}^*$ (Theorem 2), and build confidence intervals on the optimality gap from them.

Setting

Let $\tilde\xi$ be a random vector with distribution $\mu$ on a measurable space $\Xi$ , let $X\subseteq\mathbb R^d$ be a deterministic feasible set, and let $f:\mathbb R^d\times\Xi\to\mathbb R$ . The stochastic program is

\mathrm{SP}\qquad z^*=\min_{x\in X}Ef(x,\tilde\xi),\qquad x^*\in\arg\min_{x\in X}Ef(x,\tilde\xi).

Let $\tilde\xi^1,\tilde\xi^2,\dots$ be independent and identically distributed (i.i.d.) from the distribution of $\tilde\xi$ , defined on a probability space $(\Omega,P)$ . The sample-average problem of size $n\ge1$ is

\mathrm{SP}_n\qquad z_n^*=\min_{x\in X}\frac1n\sum_{i=1}^n f(x,\tilde\xi^i),\qquad x_n^*\in\arg\min_{x\in X}\frac1n\sum_{i=1}^n f(x,\tilde\xi^i).

Its optimal value $z_n^*$ is a random variable. All the $z_m^*$ are built on the same sequence: $z_n^*$ uses its first $n$ terms and $z_{n+1}^*$ its first $n+1$ . Throughout, $Ef(x,\tilde\xi)$ is assumed to exist for every $x\in X$ .

For the proof structure the mission also uses the leave-one-out values

z_{n,(i)}^*=\min_{x\in X}\frac1n\sum_{\substack{j=1\\j\ne i}}^{n+1}f(x,\tilde\xi^j),\qquad i=1,\dots,n+1,

the sample-average optimal values of the $n+1$ subsamples of size $n$ of the first $n+1$ observations.

Formalization targets

Goal: the lower bound improves with the sample size

Ez_n^*\ \le\ Ez_{n+1}^*\ \le\ z^*\qquad(n\ge1),

stated in the Introduction (p. 48) as the paper's main claim, with no assumption on $X$ or on $f(\cdot,\tilde\xi)$ beyond the existence of the relevant expectations and of optimal solutions.

Milestones

Theorem 1 (p. 49): $Ez_n^*\le z^*$ .
Proof of Theorem 2 (p. 50), pathwise: $\frac1{n+1}\sum_{i=1}^{n+1}z_{n,(i)}^*\le z_{n+1}^*$ .
Proof of Theorem 2 (p. 50): $E z_{n,(i)}^*=Ez_n^*$ for every $i$ .
Theorem 2 (p. 50): $Ez_{n+1}^*\ge Ez_n^*$ .

Companion statements

The remark after Theorem 1 (p. 49): $E\min_{x\in X}\mathcal F(x,\cdot)\le z^*$ for any unbiased estimator $\mathcal F(x,\cdot)$ of $Ef(x,\tilde\xi)$ .
The wait-and-see bound (p. 50), $z^*\ge E\min_{x\in X}f(x,\tilde\xi)$ .
Display (9) (p. 52): for $\hat x\in X$ and $G_n=\frac1n\sum_i f(\hat x,\tilde\xi^i)-z_n^*$ , $G_n\ge0$ and $EG_n\ge Ef(\hat x,\tilde\xi)-z^*$ .

Significance

Theorem 1 turns any sampling-based solver into a source of statistical lower bounds on $z^*$ : averaging independent replications of $z_n^*$ gives a confidence interval for a lower bound, and display (9) combines it with an upper-bound estimator into an estimator of the optimality gap that is nonnegative by construction. Theorem 2 justifies increasing the sample size: the bias $z^*-Ez_n^*$ is nonincreasing in $n$ . Both results are used, often without proof, in the analysis of sample-average approximation and of the gap-estimation procedures built on it.

The results are proved, in this paper and in textbooks (e.g. Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming). To our knowledge none of them is machine-checked. On Prove2Me, a special case of Theorem 1 under continuity, compactness and a square-integrable envelope is posed but unproved (SolutionQuality.SRP.display1_negative_bias), and the wait-and-see inequality is proved for finitely many scenarios in an extended-real model (StochasticProg.ValueOfInfo.prop1_ws_le_rp_le_eev). This mission states the general versions, for arbitrary feasible sets and integrable costs, on a measure-theoretic i.i.d. model.

Difficulty

Theorem 1 is short on paper; in a formal setting its difficulty is bookkeeping: minima over arbitrary sets and expectations of possibly non-integrable functions both need explicit hypotheses to mean what the paper means. Theorem 2 is harder. The natural first attempt compares $z_n^*$ and $z_{n+1}^*$ on the same sample path, but no pathwise inequality holds in either direction: one extra observation can raise or lower the sample-average optimum. The monotonicity holds only in expectation, so any argument must use the joint law of the infinite i.i.d. sequence, including the law of its subsequences, and measurability of $z_n^*$ as a function of the sample path.

Formalization scope

The model is the published definition file SolutionQuality.SRP.Setting: decisions lie in EuclideanSpace ℝ (Fin d), $\mu$ is a probability measure on $\Xi$ , the sample is an i.i.d. sequence ξ : ℕ → Ω → Ξ (the paper's $\tilde\xi^i$ is ξ (i-1)), and $z^*$ , $z_n^*$ , $G_n$ and the optimality gap are its optValue, saaValue, gapEstimate and optGap. The mission adds skipIndex, the leave-one-out value looValue and the path law pathLaw.

Committed conventions:

$X$ is an arbitrary set: no convexity, closedness or compactness, and $f(\cdot,\xi)$ has no continuity (p. 49: "X need not be convex …").
Minima are conditionally complete infima (sInf), and expectations are Bochner integrals. Both take the value $0$ $0$ on bad inputs, so every statement carries the hypotheses that keep them genuine:
- integrability of $f(x,\cdot)$ for $x\in X$ (the first-moment half of the paper's standing assumption; the second moments are not used and are omitted);
- attainment of $z^*$ (the paper's $x^*\in\arg\min$ );
- almost-sure attainment of every $\mathrm{SP}_m$ (the paper's $x_m^*\in\arg\min$ ), stated for the law of the sample path, or almost-sure boundedness below where that suffices;
- integrability of $z_n^*$ and $z_{n+1}^*$ (" $Ez_n^*$ exists");
- measurability of $z_n^*$ as a function of the sample path (" $z_n^*$ is a random variable"), for Theorem 2 only. It holds, e.g., for countable $X$ or for $f(\cdot,\xi)$ continuous on $X$ ; it fails for arbitrary $X$ and $f$ , which is why it is assumed.
$n\ge1$ throughout, since the empty sample mean is $0$ .

These hypotheses are disclosed in each statement and are satisfiable: a sanity instance with $X$ a singleton satisfies all of them. A formalization that dropped the integrability of $z_n^*$ , or that allowed $z_0^*$ , would make the goal false or vacuous, and one that assumed continuity and compactness would restate the special case already on the platform; neither is in scope.

A complete development needs: the expectation of a sample mean under an i.i.d. law; the identification of the law of fun j => ξ (skipIndex i j) · with Measure.infinitePi (fun _ => μ) (Mathlib's iIndepFun_iff_map_fun_eq_infinitePi_map); and the averaging identity behind the leave-one-out decomposition. The reindexing lemma for i.i.d. sequences is reusable well beyond this mission. Proofs of the milestones, and alternative arguments for Theorem 2, are welcome.

Selected references

W.-K. Mak, D. P. Morton, R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Operations Research Letters 24 (1999) 47–56. https://doi.org/10.1016/S0167-6377(98)00054-6
A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960) 197–204. https://doi.org/10.1287/mnsc.6.2.197
V. I. Norkin, G. Ch. Pflug, A. Ruszczyński, A branch and bound method for stochastic global optimization, Mathematical Programming 83 (1998) 425–450. https://doi.org/10.1007/BF02680569
G. Bayraksan, D. P. Morton, Assessing solution quality in stochastic programs, Mathematical Programming 108 (2006) 495–514. https://doi.org/10.1007/s10107-006-0720-x
A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

7 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 3: The Partition Job Shop on Two Machines Has a Schedule of Finish Time 5T, Preemptive or Not, Iff a Partition ExistsResearch Paper

Motivation

A job shop is the basic model of a factory floor in which every job follows its own route through the machines. Minimizing the time at which the last job is finished (the finish time, or makespan) is one of the central problems of deterministic scheduling theory, and the question of which special cases admit efficient algorithms has organized much of the field since the 1950s.

For two machines the picture is sharp. Jackson (1956) showed that a two-machine job shop in which every job has at most two operations is solved by a simple rule extending Johnson's flow-shop algorithm (Jackson, Naval Research Logistics Quarterly 3, 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 105). Once a single job may have three operations, the non-preemptive problem becomes NP-complete: Lenstra, Rinnooy Kan and Brucker showed this for $n-1$ jobs with one nonzero task each and one job with three (Annals of Discrete Mathematics 1, 1977; a 1975 Mathematisch Centrum report is the paper's reference [1]). Gonzalez and Sahni (Operations Research 26(1), 1978) extended this boundary to preemptive schedules, in which a task may be interrupted and resumed later: even then the two-machine problem is NP-complete, already when only two jobs have three nonzero tasks. This mission formalizes that reduction, Lemma 5 together with Corollary 2 of their paper.

Timeline:

1956: Jackson, two-machine job shop with at most two operations per job, solved in $O(n\log n)$ .
1975/1977: Lenstra, Rinnooy Kan and Brucker, the non-preemptive two-machine job shop NP-complete with $n-1$ one-task jobs and one three-task job.
1976: Garey, Johnson and Sethi, the non-preemptive two-machine job shop NP-complete even when problem size is measured by the sum of the task lengths (Mathematics of Operations Research 1, 1976).
1978: Gonzalez and Sahni, the preemptive two-machine job shop NP-complete (Lemmas 5 and 6), and the non-preemptive case again by the same reduction (Corollary 2).

Setting

A job shop has processors $P_1, \dots, P_m$ and jobs $1, \dots, n$ . Job $i$ is a finite sequence of tasks; task $j$ of job $i$ must be processed on a given processor $k$ for $t_{k,i,j} \ge 0$ time units, and for every job, task $j \ge 2$ can begin only after task $j-1$ has been completed. Schedules start at time $0$ . A preemptive schedule assigns to every task a finite set of time intervals $[s, f)$ on its processor, of total length $t_{k,i,j}$ , such that intervals on the same processor do not overlap and every interval of task $j$ begins after task $j-1$ of the same job is completed. A non-preemptive schedule processes each task in a single interval. If $f_i(S)$ is the time at which job $i$ is completed, the finish time is $\mathrm{FT}(S) = \max_i f_i(S)$ .

PARTITION: a multiset $\{a_1, \dots, a_n\}$ of nonnegative integers has a partition if some index set $u$ satisfies $\sum_{i \in u} a_i = \tfrac12 \sum_{i=1}^n a_i$ .

From $a_1, \dots, a_n$ , with $T = \sum_i a_i$ , the paper builds the two-processor job shop $\mathrm{JS}$ with $n+2$ jobs:

job $i \le n$ : tasks $(P_2, a_i)$ , $(P_1, a_i)$ ;
job $n+1$ : tasks $(P_1, T/2)$ , $(P_2, T/2)$ , $(P_1, 3T)$ ;
job $n+2$ : tasks $(P_2, 3T)$ , $(P_1, T/2)$ , $(P_2, T/2)$ .

Each processor carries load exactly $5T$ . In Lean, the instance is JS a : JobShopLTAS.Core.Instance 2 (n + 2), a schedule is S : Schedule (JS a) (a finite set of pieces), and the predicates are S.IsPreemptive, S.IsNonPreemptive and S.FinishedBy (5 * T a).

Formalization targets

Goal: Lemma 5 and Corollary 2

For every $n$ and every $a : \mathrm{Fin}\,n \to \mathbb N$ ,

\bigl(\exists\, S \text{ preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a) \quad\text{and}\quad \bigl(\exists\, S \text{ non-preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a).

Milestones

Lemma 5(a): a partition yields a non-preemptive schedule of finish time exactly $5T$ (the paper's Figure 3).
Observations (i)–(ii) in the proof of Lemma 5(b): in any preemptive schedule with $\mathrm{FT} \le 5T$ , task $t_{2,n+1,2}$ is completed by $2T$ and $t_{2,n+2,1}$ by $4T$ ; no part of $t_{1,n+1,3}$ runs before $T$ and no part of $t_{1,n+2,2}$ before $3T$ .
Lemma 5(b): without a partition, every preemptive schedule has $\mathrm{FT} > 5T$ .
Lemma 5: the preemptive equivalence.
Corollary 2: the non-preemptive equivalence.

Significance

The result places the boundary of tractability for two-machine job shops exactly: at most two operations per job is solvable in $O(n\log n)$ , while two jobs with three operations make the problem NP-complete, and allowing preemption does not help. The same instance serves both schedule types, because its optimum is $5T$ in either model exactly when a partition exists.

The theorem is classical and fully proved on paper; no machine-checked proof is known to exist. Formalizing it requires a precise model of preemptive schedules, which the paper treats informally, and makes explicit an argument (the "no idle time" step of Lemma 5(b)) that the paper compresses into a few sentences. The schedule model built here is shared with the other job-shop missions of this series.

Difficulty

Direction (a) is a concrete schedule and is bookkeeping. Direction (b) is the substance. The tempting argument "each processor has load $5T$ , so a schedule of finish time $5T$ has no idle time, hence some set of short jobs fills exactly $[0, T/2]$ on $P_2$ " is incomplete for preemptive schedules: the short jobs may be split into many pieces spread over the whole horizon, and $U$ , the set of short jobs that touch $P_1$ during $[0, T]$ , is defined by pieces rather than by whole tasks. Making the counting argument rigorous requires measuring idle time on each processor across arbitrary finite unions of intervals and tying the amount of processing done on $P_1$ before $T$ to the completed first tasks on $P_2$ .

Formalization scope

Processing times are real numbers; the PARTITION data are natural numbers cast to $\mathbb R$ ; $T$ is the real sum. Processors are Fin 2 with $P_1 = 0$ , $P_2 = 1$ ; jobs and tasks are 0-based, so the paper's job $n+1$ is job n and job $n+2$ is job n + 1.
Job-shop data reuse the published JobShopLTAS.Core.Instance. Schedules are finite sets of pieces (task, start, end) with positive length, following the paper's footnote 1 (p. 40). A task of length zero has no pieces and is completed when its predecessor is; it never blocks a processor.
A non-preemptive schedule is a preemptive one with at most one piece per task. "Finish time $\le \tau$ " is ∀ j, S.jobFinish j ≤ τ; "finish time $> 5T$ " is the existence of a job finishing after $5T$ ; "finish time $5T$ " in Lemma 5(a) is $\le 5T$ together with a job finishing at exactly $5T$ .
Complexity wording not formalized. "Partition $\alpha$ preemptive JOFT" and "Partition $\alpha$ nonpreemptive JOFT" (polynomial reducibility), "NP-complete", and Lemma 6 ("JOFT is in NP") are not stated. What is stated is the equivalence that the paper's proofs establish for the instance they construct, with the explicit constant $\tau = 5T$ .
The PARTITION condition is written $2\sum_{i\in u} a_i = \sum_i a_i$ in $\mathbb N$ , avoiding truncated division.
A trivializing formalization is ruled out: the schedule notion requires every task to receive its full processing time, so the empty schedule is feasible only when $T = 0$ (and then the empty index set is a partition), and the finish-time bound is over every job, so no statement holds by an unattained supremum or a default value.
Welcome contributions: a proof of Lemma 5(a) by an explicit piece schedule; infrastructure for measuring busy and idle time of a processor in a finite piece schedule, reusable for Lemma 7 (mission 4) and the preemptive flow-shop missions; the proof of Lemma 5(b).

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
M. R. Garey, D. S. Johnson, R. Sethi, Complexity of Flow Shop and Job Shop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
J. R. Jackson, An Extension of Johnson's Results on Job Lot Scheduling, Naval Research Logistics Quarterly 3(3), 201–203, 1956. https://doi.org/10.1002/nav.3800030307
R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

11 thms2 active usersReviewed

Graph Theory Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms IV: A Uniform Flow of Size Ω(𝒮/log n) on Paths of Length O(C_max log n/(n𝒮))Research Paper

Motivation

Communication networks must route many source–destination demands through shared edges. A multicommodity flow describes how much of each demand can be carried simultaneously without exceeding an edge's capacity. In an undirected network, a cut bounds the traffic that can pass between two groups of vertices, but many commodities can interfere even when no single cut is obviously restrictive. Leighton and Rao showed that the uniform concurrent flow is within a logarithmic factor of the corresponding sparsest-cut bound Leighton and Rao, 1999.

For routing, flow value alone is incomplete: a feasible flow can use long detours. Section 2.5 of the same paper establishes that a flow of the guaranteed size can be carried on paths whose number of edges is also controlled. The result supports the paper's discussion of low-congestion, low-dilation routing in communication networks, where a long route can increase latency or complicate scheduling even if every edge has sufficient capacity Leighton and Rao, 1999, §2.5.

Setting

Let $V$ be a finite set of $n\ge2$ vertices. An undirected capacitated network has a symmetric capacity $C(u,v)\ge0$ for each pair, with $C(u,u)=0$ . A pair is an edge when its capacity is positive. Parallel physical edges can be combined by adding their capacities. The network is connected: every nonempty proper subset $U\subsetneq V$ has positive cut capacity $C(U,\bar U)=\sum_{u\in U,v\notin U}C(u,v)$ , where $\bar U=V\setminus U$ .

The uniform multicommodity flow problem gives one unit of demand to each unordered pair of distinct vertices. Equivalently, it gives demand $1/2$ to each ordered pair $(s,t)$ with $s\ne t$ Leighton and Rao, 1999, footnote 2. A concurrent flow of value $\lambda$ routes the fraction $\lambda$ of every demand. Traffic in both directions of an undirected edge shares that edge's capacity. The demand crossing $U$ is $|U|\,|\bar U|$ , so the uniform min-cut, also called the sparsest-cut value, is

\mathcal S=\min_{\varnothing\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.

For a flow path, length means its number of edges. A separate nonnegative symmetric distance function $d$ assigns lengths to edges; its total weight is $W=\sum_e C(e)d(e)$ . Given a hop budget $L$ , let $d_L(u,v)$ be the smallest $d$ -length of a walk from $u$ to $v$ using at most $L$ edges. The value is $\infty$ if no such walk exists. The maximum capacity incident to one vertex is $C_{\max}=\max_v\sum_u C(v,u)$ . The paper uses $\log n=\log_2n$ and $\ln n$ for the natural logarithm Leighton and Rao, 1999, footnote 3.

Formalization targets

A large uniform flow with short paths

Theorem 18 asserts the existence of absolute constants $c_1,c_2>0$ such that every network in the setting above admits a concurrent uniform flow of value $\lambda$ whose every route has at most $L$ edges, with

\lambda\ge c_1\frac{\mathcal S}{\log_2 n},\qquad L\le c_2\frac{C_{\max}\log_2 n}{n\mathcal S}.

The constants precede the choice of network: they cannot depend on its size or capacities. The goal gives an actual flow and integer hop limit, not only a lower bound on a supremum Leighton and Rao, 1999, Theorem 18.

The dual and geometric estimates

The short-path linear-programming dual uses $d_L$ in its distance constraint, $\frac12\sum_{u,v}d_L(u,v)\ge1$ , and minimizes $W$ . Lemma 19 partitions a network into components with both edge-radius at most $\Delta C/W$ and distance-radius at most $\Delta$ , while the capacity between components is at most $4W\log_2n/\Delta$ . Corollary 20 finds a component with at least $2n/3$ vertices when $0<W\le\mathcal S/(36\log_2n)$ . Lemma 21 bounds the sum of $L/4$ -restricted distances from any such large set to its complement by $6W/(n\mathcal S)$ , provided $L\ge12C_{\max}\ln n/(n\mathcal S)$ . These are the mission's milestones, in source order Leighton and Rao, 1999, pp. 808–809.

Significance

Theorem 18 places simultaneous lower and upper guarantees on a routing solution: it carries a substantial fraction of every uniform demand, while each route uses a bounded number of edges. Its hop guarantee is stronger than simply knowing that the unconstrained maximum flow is large. The result is one of the paper's inputs for reasoning about routing paths with low congestion and dilation; the paper also says analogous short-path results extend to product and directed flow problems, without presenting all their details Leighton and Rao, 1999, p. 811.

The known mathematical result has a published proof; this mission asks for machine-checked statements and proofs. A complete development would establish the hop-indexed flow model, the restricted shortest-path duality, and the two-radius partition estimates in Lean. The network, proper-cut, and extended-distance interfaces can be reused in later work on sparse cuts and length-constrained routing. No machine-checked proof of this exact theorem is claimed here.

Difficulty

The ordinary approximate max-flow/min-cut theorem controls the amount of concurrent traffic but does not bound the number of edges on each route. Restricting routes changes the dual: a shortest path that exceeds the hop budget is unavailable, and some vertex pairs have no allowed path at all. Assigning such a pair distance zero would alter the dual constraint. The geometric estimates must control both hop count and $d$ -length on the same connecting paths, since bounds witnessed by two unrelated paths cannot be combined into one short route Leighton and Rao, 1999, §2.5.

Formalization scope

The vertex type is finite and has at least two members. Capacities are real, symmetric and nonnegative; zero-capacity pairs are absent from the graph. Connectivity is the paper's standing cut assumption. The min-cut ranges over nonempty proper subsets, so no expression divides by a zero cardinality. Demands use the paper's ordered-pair $1/2$ convention. A short flow is a nonnegative commodity–hop–arc array whose equations inject, conserve and absorb traffic; the capacity constraint combines both directions and all hops. The maximum flow is a supremum over feasible values. Its use is confined to the positive-demand finite setting, where the feasible set is nonempty and bounded.

Restricted distances take values in extended nonnegative reals, so an empty family of allowed walks has value $\infty$ . The radius predicate requires one walk inside a component to meet both bounds. $\log_2$ appears in Theorem 18, Lemma 19 and Corollary 20; Lemma 21's threshold uses $\ln$ . For expressions dividing by $W$ , the formal statements require $W>0$ ; this makes the printed radius meaningful. The explicit companion theorem uses the hop limit $\lfloor L\rfloor$ for the paper's real $L$ , which is what "at most $L$ edges" means; Lemma 21 keeps $L$ real. The polynomial-time search claim is outside this existence formalization. A definition making every restricted distance zero, or quantifying its asymptotic constants after the network, would make the goal a different theorem.

Contributions may include finite-flow and linear-programming duality, path decomposition for the hop-indexed formulation, the partition estimate, the large-component corollary, or the restricted-distance estimate. The same finite graph and extended-distance definitions may serve subsequent missions.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, Journal of the ACM 46(6):787–832, 1999. DOI: 10.1145/331524.331526.

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms V: On a 3-Regular c-Expander the Uniform Max-Flow Is at Most 6𝒮/(c(⌊log n⌋ − 2))Research Paper

Motivation

A multicommodity flow problem asks to route many source–sink demands through one capacitated network at the same time. Its min-cut (sparsest cut) is the smallest ratio, over all cuts, of the capacity crossing the cut to the demand separated by it. Routing is always limited by every cut, so the max-flow never exceeds the min-cut. For a single commodity the two are equal (Ford–Fulkerson); for many commodities they are not, and the size of the gap governs a large family of approximation algorithms for graph partitioning, layout and routing problems.

Leighton and Rao (J. ACM 46 (1999), extended abstract FOCS 1988) proved that for uniform problems, where every pair of nodes demands one unit, the gap is at most $O(\log n)$ (their Theorem 2). This mission formalizes the other half: Section 2.1 of the paper, A bad example, which shows that the $\log n$ is necessary. On a 3-regular expander graph the max-flow is a $\Theta(\log n)$ factor smaller than the min-cut, so Theorem 2 cannot be improved beyond the constant.

Timeline. Ford and Fulkerson (1956) and Elias–Feinstein–Shannon (1956): single-commodity max-flow equals min-cut. Hu (1963): equality for two commodities. Leighton and Rao (1988, journal 1999): uniform and product problems have an $O(\log n)$ gap, and expanders show it is tight. Klein, Agrawal, Ravi and Rao (1990) and later Linial–London–Rabinovich (Combinatorica 1995) and Aumann–Rabani (1998): an $O(\log k)$ gap for general demands with $k$ commodities, tight by the same expander example.

Setting

Let $V$ be a finite set of $n$ nodes. A network assigns a capacity $C(u,v)\ge0$ to every pair, symmetric and zero on the diagonal. For $U\subseteq V$ with complement $\bar U$ , the cut capacity $C(U,\bar U)$ is the total capacity of the pairs with one end in $U$ and the other in $\bar U$ .

In the uniform multicommodity flow problem (UMFP) every pair of distinct nodes is a commodity with unit demand. Its max-flow $f$ is the largest fraction such that $f$ units of every commodity can be routed simultaneously without exceeding any capacity (concurrent flow). Its min-cut is

\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.

Section 2.1 takes a 3-regular $n$ -node graph $G$ with unit edge capacities, so that $C(U,\bar U)=|\langle U,\bar U\rangle|$ is the number of edges between $U$ and $\bar U$ , and assumes that $G$ is a $c$ -edge-expander:

|\langle U,\bar U\rangle|\ \ge\ c\,\min\{|U|,|\bar U|\}\qquad\text{for all }U\subseteq V,

for a constant $c>0$ . Families of such graphs exist for a sufficiently small $c$ (Margulis 1973; a random 3-regular graph has the property with high probability). Throughout, $\log$ is $\log_2$ .

Formalization targets

Goal: the gap on an expander

For a 3-regular $c$ -edge-expander with unit capacities and $n\ge 8$ ,

f\ \le\ \frac{6\,\mathcal S}{c\,\bigl(\lfloor\log n\rfloor-2\bigr)} .

This is the final display of §2.1 (pp. 794–795), with the floor that the argument actually supports (see Formalization scope). It leaves the expander family unspecified: it holds for every graph with the two properties.

Milestones, in the order the argument uses them

$\mathcal S\ge c/(n-1)$ for the expander (p. 794).
In a 3-regular graph, at most $n/2$ nodes lie within distance $\lfloor\log n\rfloor-3$ of any node.
Hence at least half of the source–sink pairs are at distance at least $\lfloor\log n\rfloor-2$ .
A uniform flow of fraction $f$ uses capacity at least $\tfrac12\binom n2 f(\lfloor\log n\rfloor-2)$ , and the total capacity is $3n/2$ .
Hence $f\le 3n/\bigl(\binom n2(\lfloor\log n\rfloor-2)\bigr)=6/\bigl((n-1)(\lfloor\log n\rfloor-2)\bigr)$ .

Companions: Theorem 1

Theorem 1 (p. 795) states that for any $n$ there is an $n$ -node UMFP with $f\le O(\mathcal S/\log n)$ . It is stated twice: conditionally on a family of 3-regular $c$ -expanders (the form §2.1 proves), and unconditionally, with one constant $K$ for all $n\ge2$ .

Significance

The result shows that the $O(\log n)$ max-flow min-cut gap of Leighton and Rao's Theorem 2 is tight up to the constant, and, through the same example, that the $O(\log k)$ bound for general demands is tight. Every approximation algorithm that rounds a multicommodity flow, or its dual, to a cut loses a $\Theta(\log n)$ factor in the worst case for this reason; improving on it, as Arora, Rao and Vazirani did (J. ACM 2009) with an $O(\sqrt{\log n})$ approximation for sparsest cut, requires a stronger relaxation than the flow LP.

The result is classical and proved. To our knowledge it has no machine-checked proof. Formalizing it requires the concurrent-flow LP, the uniform sparsest cut, graph distance balls in bounded-degree graphs and a counting argument that converts path lengths into capacity usage; each of these is reusable. The unconditional Theorem 1 additionally needs the existence of bounded-degree expanders on every number of nodes, which is a substantial formalization project in its own right.

Difficulty

The min-cut bound and the ball bound are elementary. The central step is milestone 4: turning "the shortest path of a commodity has at least $\ell$ edges" into "the commodity uses at least $f\ell$ units of capacity". In an arc-flow formulation a commodity is a conservation-respecting function on arcs, not a set of paths, so the step needs either a path decomposition of each commodity's flow or a weak-duality argument with unit edge lengths. The obvious attempt, summing the conservation equations directly, gives only the net flow across one cut and loses the factor $\ell$ .

The unconditional Theorem 1 is hard for a different reason: the paper cites the existence of 3-regular expanders and does not prove it, and the theorem asks for every $n$ , including odd $n$ , where no 3-regular graph exists.

Formalization scope

Nodes are a Fintype $V$ with decidable equality and $n=|V|$ . A network is a symmetric nonnegative real capacity function with zero diagonal; the unit-capacity network of a simple graph $G$ has $C(u,v)=1$ on edges and $0$ elsewhere. Commodities are ordered pairs $(s,t)$ , $s\ne t$ , each with demand $\tfrac12$ (the paper's footnote 2), so each unordered pair carries one unit; a flow is a nonnegative arc flow per commodity, and both directions of an edge share its capacity. The max-flow is the supremum of feasible fractions. The min-cut ranges over nonempty proper $U$ only: at $U=\emptyset$ or $V$ the ratio is $0/0$ , which Lean reads as $0$ and which would make $\mathcal S=0$ .

Conventions and added hypotheses:

The floor. The page writes $\log n-2$ . Its argument shows that far pairs have distance at least $\lfloor\log n\rfloor-2$ , which differs from $\log n-2$ for non-integer $\log n$ . The goal and milestones state $\lfloor\log n\rfloor-2$ (Nat.log 2 n), a different constant in the same $\Theta(\log n)$ .
$n\ge 8$ makes $\lfloor\log n\rfloor-2\ge1$ , so the bound divides by a positive number.
Graph distance is the extended distance, $\infty$ between components, never Lean's junk value $0$ .
Regularity is SimpleGraph.IsRegularOfDegree 3.
Theorem 1 requires the network to be connected (the paper's standing assumption, p. 789); a disconnected network has $f=\mathcal S=0$ and would make the statement empty. Its constant is quantified before $n$ .
Polynomial-time claims are not formalized.

The hypotheses of the goal are satisfiable: the 3-cube $Q_3$ ( $n=8$ ) is 3-regular and a $1$ -edge-expander. Contributions welcome: the arc-flow path-length lemma, the ball bound for bounded-degree graphs, and an existence theorem for 3-regular expanders.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9(4):325–332, 1973.
N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
S. Arora, S. Rao and U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM 56(2):5, 2009. https://doi.org/10.1145/1502793.1502794

7 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Globally Convergent Inexact Newton Methods II: Trust Region Limit Points Are Stationary Points of ‖F‖, and Near a Zero Where F′ Is Invertible the Full Newton Step Is Eventually TakenResearch Paper

Motivation

Solving a system of nonlinear equations $F(x)=0$ , with $F:\mathbf R^n\to\mathbf R^n$ continuously differentiable, is a basic task in numerical analysis and optimization: it is the inner step of interior-point and sequential quadratic programming methods, of implicit time-stepping for differential equations, and of equilibrium computations in operations research. Newton's method converges fast near a solution at which the derivative $F'$ is invertible, but from a poor starting point it may fail. Trust region methods are a standard globalization: each step minimizes the norm of the local linear model $F(x_k)+F'(x_k)s$ over a ball $\|s\|\le\delta_k$ , and the radius $\delta_k$ is shrunk or enlarged according to how well the model predicted the actual decrease of $\|F\|$ (Moré and Sorensen 1983; Dennis and Schnabel 1983, §6.4).

Eisenstat and Walker (1994) developed a general global convergence theory for inexact Newton methods, in which steps only reduce the linear model's norm by a factor $\eta_k<1$ and must also give sufficient decrease of $\|F\|$ . Their §4, Application 1, shows that this theory also covers trust region methods. This mission formalizes that application.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbf R^n$ ; the norm need not be Euclidean), and $F:E\to E$ continuously differentiable with derivative $F'(x)$ . For a point $x_k$ and a step $s$ , the actual reduction and predicted reduction are

\operatorname{ared}_k(s)=\|F(x_k)\|-\|F(x_k+s)\|,\qquad \operatorname{pred}_k(s)=\|F(x_k)\|-\|F(x_k)+F'(x_k)s\|.

A point $x$ is a stationary point of $\|F\|$ if $\|F(x)\|\le\|F(x)+F'(x)s\|$ for every $s$ : no step decreases the norm of the linear model. A point $x_*$ is a limit point of $(x_k)$ if every ball around $x_*$ contains $x_k$ for infinitely many $k$ .

Algorithm TR is given $x_0$ , $\bar\delta_0>0$ , $0<t\le u<1$ and $0<\theta_{\min}<\theta_{\max}<1$ . At iteration $k$ it sets $\delta_k=\bar\delta_k$ and picks a step

s_k\in\arg\min_{\|s\|\le\delta_k}\|F(x_k)+F'(x_k)s\|.\tag{4.5}

While $\operatorname{ared}_k(s_k)<t\cdot\operatorname{pred}_k(s_k)$ , it replaces $\delta_k$ by $\theta\delta_k$ for some $\theta\in[\theta_{\min},\theta_{\max}]$ and picks a new $s_k$ by (4.5). Then $x_{k+1}=x_k+s_k$ , and the next initial radius satisfies $\bar\delta_{k+1}\ge\delta_k$ if $\operatorname{ared}_k(s_k)\ge u\cdot\operatorname{pred}_k(s_k)$ , and $\bar\delta_{k+1}\ge\theta_{\min}\delta_k$ otherwise. The algorithm does not break down if it generates an infinite sequence of iterates.

Formalization targets

Goal: Theorem 4.4

If Algorithm TR does not break down, then

\text{every limit point } x_* \text{ of } (x_k) \text{ is a stationary point of } \|F\|,

and if $x_*$ is a limit point with $F'(x_*)$ invertible, then

F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=-F'(x_k)^{-1}F(x_k)\ \text{for all sufficiently large }k.

The statement has no constants, and it holds for every choice the algorithm leaves open: the minimizer in (4.5), the factors $\theta$ , and the new radii.

Milestones

Corollary 3.7. Any sequence with $\operatorname{pred}_k(s_k)\ge0$ and $\operatorname{ared}_k(s_k)\ge t\cdot\operatorname{pred}_k(s_k)$ , $s_k=x_{k+1}-x_k$ , for which $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ near a limit point $x_*$ , converges to $x_*$ .
Lemma 4.2. If $F'(x_*)$ is invertible, then for some $\Gamma>0$ , $\epsilon_*>0$ , every minimizer $s$ of (4.5) with any radius $\delta>0$ and $\|x-x_*\|<\epsilon_*$ satisfies $\|s\|\le\Gamma\{\|F(x)\|-\|F(x)+F'(x)s\|\}$ (4.6).
Lemma 4.3. If $x_*$ is not a stationary point of $\|F\|$ , then (4.6) holds for radii $0<\delta\le\delta_*$ and $x$ near $x_*$ .
Lemma 4.1. For a run of Algorithm TR, if $\|s_k\|\le\Gamma\cdot\operatorname{pred}_k(s_k)$ (4.1) holds for every trial step of iterations with $x_k$ near a limit point $x_*$ and $k$ large, then $x_k\to x_*$ and $\liminf_k\delta_k>0$ .

An extra item, Corollary 3.6, states that such a sequence with $\sum_k\operatorname{relpred}_k(s_k)$ divergent has $F(x_k)\to0$ , where $\operatorname{relpred}_k(s_k)=\operatorname{pred}_k(s_k)/\|F(x_k)\|$ (or $1$ if $F(x_k)=0$ ).

Significance

Theorem 4.4 is a global convergence result that assumes neither bounded level sets, nor the existence of a solution, nor an inner-product norm. It separates two conclusions: without any regularity, the only possible accumulation points are stationary points of $\|F\|$ ; at an accumulation point where $F'$ is invertible, the method finds a solution, converges to it, and eventually takes the full Newton step. The paper assumes only continuous differentiability, which does not by itself give a quadratic convergence rate. Lemmas 4.2 and 4.3 are local facts about minimizers of the linear model's norm over a ball and apply to any method that uses such steps.

The result is proved in the paper. As far as we know, none of it is formalized: Mathlib has the Fréchet derivative, the inverse function theorem and invertible continuous linear maps, but no trust region or inexact Newton convergence theory. This mission produces machine-checked versions of the paper's statements for an arbitrary norm, together with a reusable vocabulary (actual/predicted reduction, stationary points of $\|F\|$ , model minimizers, trust region runs) for later formalizations of trust region and Levenberg–Marquardt type methods.

Difficulty

The obvious argument shows that $\|F(x_k)\|$ decreases, so it converges, and then tries to conclude that the predicted reductions tend to zero. That step fails without control on the radii: if $\delta_k\to0$ , small predicted reductions say nothing about stationarity, and the steps could shrink while the iterates still wander. The central difficulty is to show that near a non-stationary or regular limit point the radii stay bounded away from zero, while at the same time proving that the whole sequence converges to that limit point, not just a subsequence. Under an arbitrary norm the model minimizer is not unique and the model norm is not smooth, so arguments based on gradients of $\frac12\|F\|_2^2$ do not apply.

Formalization scope

$\mathbf R^n$ with an arbitrary norm is a finite-dimensional real normed space E; $F'$ is fderiv ℝ F, and "continuously differentiable" is ContDiff ℝ 1 F.
A run of Algorithm TR is the predicate IsTRRun. Iteration $k$ records the number $m_k$ of while-loop passes, the factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$ , and trial steps $s_{k,0},\dots,s_{k,m_k}$ , each a minimizer of (4.5) for its radius. Trials $j<m_k$ fail the test $\operatorname{ared}\ge t\cdot\operatorname{pred}$ , and trial $m_k$ passes it. "Does not break down" is the existence of such a run. Any minimizer in (4.5) may be chosen.
"Limit point" is MapClusterPt. "Sufficiently near $x_*$ and $k$ sufficiently large" is: there exist $\rho>0$ and $K$ such that the property holds for $k\ge K$ with $\|x_k-x_*\|<\rho$ . "Whenever $k$ is sufficiently large" is ∀ᶠ k in atTop.
" $F'(x_*)$ invertible" is (fderiv ℝ F xstar).IsInvertible. $F'(x_k)^{-1}$ is ContinuousLinearMap.inverse, which is the true inverse for all large $k$ .
" $\liminf\delta_k>0$ " is "eventually $\delta_k\ge c$ for some $c>0$ "; " $\sum\operatorname{relpred}$ divergent" is ¬ Summable.
In Lemma 4.1, (4.1) is required for every trial step $s_{k,j}$ of iterations with $x_k$ near $x_*$ and $k$ large: in Algorithm TR the symbol $s_k$ takes the value of each trial step, and the proof on p. 403 applies (4.1) to trial steps. Requiring it for the accepted step alone would make the lemma false. Lemmas 4.2 and 4.3 are stated with $\Gamma>0$ .
No statement assumes $F(x_*)=0$ , $x_k\to x_*$ , bounded level sets, a Euclidean norm or a Lipschitz derivative: those are conclusions or absent from the paper. A run predicate that forced zero steps or zero radii would make the convergence claims trivial; IsTRRun forces neither, and it has a run with nonzero steps (for $F=\mathrm{id}$ on $\mathbf R$ ).

Needed infrastructure: the continuity of $x\mapsto F'(x)^{-1}$ near an invertible point (Lemma 1.1 of the paper), a uniform linearization bound $\|F(y)-F(x)-F'(x)(y-x)\|\le\varepsilon\|y-x\|$ near a point (Lemma 1.2), and the telescoping argument of Theorem 3.5. These are reusable well beyond this mission. Contributions are welcome on each milestone separately, and on general lemmas about minimizers of $\|a+Ls\|$ over a ball.

Selected references

S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM Journal on Optimization 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
J. J. Moré and D. C. Sorensen, Computing a Trust Region Step, SIAM Journal on Scientific and Statistical Computing 4(3) (1983) 553–572. https://doi.org/10.1137/0904038
J. E. Dennis Jr. and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Prentice-Hall 1983; SIAM reprint 1996. https://doi.org/10.1137/1.9781611971200
R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM Journal on Numerical Analysis 19(2) (1982) 400–408. https://doi.org/10.1137/0719025

7 thms2 active usersReviewed

Completed

Control Theory Dynamical Systems Operations Research·Captain: mikedeng1

Dynamic Instabilities and Stabilization Methods in Distributed Real-Time Scheduling of Manufacturing Systems 4: A Run-Truncating Priority-Queue Supervisor Keeps Every Buffer Bounded When ρₘ < 1Research Paper

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$ , with level $x_{p,i}(t)\ge 0$ . Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$ , and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$ . Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$ , the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}

and thresholds $z_{p,i}\ge0$ . It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$ ; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$ ; when a run ends and $Q_m\ne\emptyset$ , the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$ , the backlog of part type $p$ for machine $\mu_{p,i}$ .

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$ , every supervised trajectory, from every initial state, satisfies

\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$ , that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$ .
A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$ ) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$ .
Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$ .

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$ ; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$ , with a set-up paid at each.

Formalization scope

Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$ . Time is real with $t\ge0$ . Set-up times satisfy $\delta_{b,b}=0$ : a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$ , and at exactly $1/\tau_b$ while $b$ is nonempty.
Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$ . The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$ , are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$ .
Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$ . Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$ : with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$ , never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$ .
Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$ . A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085

8 thms2 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

On Tail Probabilities for Martingales 2: For |X_n| ≤ 1 and E{X_n | ℱ_{n−1}} = 0, the Conditional Variance W_a Used to Cross a Satisfies E exp[−f(λ)W_a] ≥ exp[−λ(a+1)]Research Paper

Motivation

Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process $Q_\lambda(T_n, S_n)$ is a supermartingale and $R_\lambda(T_n, S_n)$ a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound $P\{W_a \ge b\} < 5(a+1)/b^{1/2}$ , Lévy's theorem that $\sup_n S_n = \infty$ almost surely on $\{\sum V_i = \infty\}$ (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space and $\mathcal F_0 \subset \mathcal F_1 \subset \cdots$ an increasing sequence of sub- $\sigma$ -fields of $\mathcal F$ . Let $X_1, X_2, \dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$ , satisfying the standing condition (1.1):

|X_n| \le 1 \quad\text{and}\quad E\{X_n \mid \mathcal F_{n-1}\} = 0 \qquad (n \ge 1).

The conditional variance of the $n$ -th step is $V_n = \operatorname{Var}\{X_n \mid \mathcal F_{n-1}\}$ . The partial sums are $S_n = X_1 + \cdots + X_n$ and the intrinsic time is $T_n = V_1 + \cdots + V_n$ , with $S_0 = T_0 = 0$ .

For a real $\lambda$ , let $f(\lambda) = e^{-\lambda} - 1 + \lambda$ (positive for $\lambda > 0$ ), and $R_\lambda(v, y) = \exp\{\lambda y - f(\lambda) v\}$ .

A stopping time is a random variable $\sigma$ with values in $\{0, 1, 2, \dots, \infty\}$ such that $\{\sigma = n\} \in \mathcal F_n$ for every $n$ ; it is uniformly bounded if $\sigma \le N$ everywhere for some integer $N$ .

Fix a level $a > 0$ . The crossing time $\tau_a$ is the least $n$ with $S_n \ge a$ , and $\tau_a = \infty$ if there is none. The crossing variance is

W_a = T_{\tau_a} = \sum_{i=1}^{\tau_a} V_i \in [0, \infty],

the total conditional variance the process needs to cross the level $a$ if it crosses, and otherwise the total conditional variance $\sum_{i \ge 1} V_i$ , which may be infinite.

Formalization targets

Goal: Theorem (1.8)

For every $\lambda > 0$ and $a > 0$ ,

E\{\exp[-f(\lambda) W_a]\} \ge \exp[-\lambda(a+1)],

with the convention $\exp[-f(\lambda)\cdot\infty] = 0$ .

Milestones

The two-point cases of (3.7): for $X$ taking only the values $-1$ and $a > 0$ (Case 1), or only $-b$ and $a$ with $0 < b \le 1$ (Case 2), with $E(X) = 0$ and $\lambda \ge 0$ ,

E\{\exp(\lambda X)\} \ge \exp\{f(\lambda) \operatorname{Var} X\}.

Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$ .
Proposition (3.6): under (1.1), $E\{R_\lambda(T_\sigma, S_\sigma)\} \ge 1$ for every $\lambda \ge 0$ and every uniformly bounded stopping time $\sigma$ .
From (4.2): $S_n \le a + 1$ for $n \le \tau_a$ , and for every $n$ ,

1 \le E\{\exp[\lambda S_{\tau_a\wedge n} - f(\lambda)T_{\tau_a\wedge n}]\} \le \exp[\lambda(a+1)]\cdot E\{\exp[-f(\lambda)T_{\tau_a\wedge n}]\}.

Significance

The result. Theorem (1.8) says that the Laplace transform of $W_a$ cannot be small, so $W_a$ cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.

Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in $[0,\infty]$ . The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).

Difficulty

The obvious route is optional stopping at $\tau_a$ itself. It fails: $\tau_a$ is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at $\tau_a \wedge n$ , use the overshoot bound $S_{\tau_a \wedge n} \le a + 1$ (which relies on $X_n \le 1$ ), and pass to the limit $n \to \infty$ in a way that sends the integrand to $0$ on $\{W_a = \infty\}$ ; the limit exchange needs $T_n \to W_a$ in $[0, \infty]$ and $f(\lambda) > 0$ . A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where $E\exp(\lambda X)$ may be infinite; the usual convexity bounds go in the opposite direction.

Formalization scope

The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.

Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index $1$ ; $X_0$ is never read. Measurability is " $X_n$ is $\mathcal F_n$ -strongly measurable for $n \ge 1$ ", and the two parts of (1.1) are assumed almost surely. $V_n$ is Mathlib's condVar of $X_n$ given $\mathcal F_{n-1}$ ; under (1.1) every $X_n$ is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is $\infty$ ). $\tau_a$ is WithTop ℕ-valued and $W_a$ is $[0,\infty]$ -valued (ℝ≥0∞), built from the nonnegative parts of the $V_i$ , which agree with $V_i$ almost surely. The integrand of the goal is the function that equals $e^{-f(\lambda) W_a}$ on $\{W_a < \infty\}$ and $0$ on $\{W_a = \infty\}$ ; replacing it by $\exp(-f(\lambda)\cdot\mathrm{toReal}(W_a))$ , which is $1$ on $\{W_a = \infty\}$ , would formalize a strictly weaker statement and is ruled out. In (3.7), where $\exp(\lambda X)$ need not be integrable, the expectation is a lower Lebesgue integral in $[0,\infty]$ , and $X$ is assumed square-integrable so that $\operatorname{Var} X$ is finite.

Corrected misprints. Definition (1.2)(e) prints $R_\lambda(v,y) = \exp\{\lambda h - f(\lambda) v\}$ ; $h$ is read as $y$ . The display in (4.2) prints the last factor without its expectation sign; the $E$ is restored.

Ranges. The goal uses $\lambda > 0$ and $a > 0$ as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for $\lambda \ge 0$ as on p. 107.

Lemma (3.1) ( $g(x) = (e^x - 1 - x)/x^2$ is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that $R_\lambda(T_n, S_n)$ is a submartingale, and Corollary (1.9) as a follow-up.

Selected references

David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1), 1975, 100–118. https://doi.org/10.1214/aop/1176996452
Paul Lévy, Théorie de l'addition des variables aléatoires, Gauthier-Villars, 1937 (Theorem 68, p. 247, cited in (4.5)).

10 thms2 active usersReviewed

Dynamical Systems Operations Research Probability+1·Captain: mikedeng1

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$ . For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$ . His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$ . Kingman's conditions (§1.1–1.2) are:

S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ ;
S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$ ;
S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$ ;
S₃′: $E(x_{01}^+)<\infty$ , where $x^+=\max(x,0)$ .

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$ .

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$ . A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$ -valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,

with $\log 0=-\infty$ . Expectations of $[-\infty,\infty)$ -valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$ , defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$ .

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$ , then

\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|

exists in $-\infty\le\xi<\infty$ with probability one, and

E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

(1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$ .
Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$ .
Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$ .
Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$ , then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$ . For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$ , as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$ -algebra on $\mathfrak B\times\mathfrak B$ , so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$ . The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$ -algebra, not equality of one-dimensional marginals.
S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
$\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$ ; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$ , and is ruled out.
$\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$ , and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

8 thms2 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

On the Generalized “Birth-and-Death” Process 3: Given the Mean Growth n̄_t, the Rates λ = (n̄′/n̄)⁺, μ = (n̄′/n̄)⁻ Uniquely Minimize Var(n_t) for All tResearch Paper

Motivation

In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?

Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.

Setting

The process starts with one ancestor. At time $t$ , each member gives birth at rate $\lambda(t)$ and dies at rate $\mu(t)$ ; the rates are nonnegative. Let $n_t$ be the population size and $\bar n_t$ its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.

Define the integrated net death rate and the fluctuation by

\rho_{\lambda,\mu}(t)=\int_0^t\bigl(\mu(\tau)-\lambda(\tau)\bigr)\,d\tau, \qquad V_{\lambda,\mu}(t)=e^{-2\rho_{\lambda,\mu}(t)} \int_0^t e^{\rho_{\lambda,\mu}(\tau)} \bigl(\lambda(\tau)+\mu(\tau)\bigr)\,d\tau.

Kendall's equations (13) and (14c) identify $\bar n_t=e^{-\rho_{\lambda,\mu}(t)}$ and $V_{\lambda,\mu}(t)=\operatorname{Var}(n_t)$ for the one-ancestor process. A pair $(\lambda,\mu)$ is admissible here when both rates are continuous and nonnegative on $[0,\infty)$ . It has mean $\bar n$ when $e^{-\rho_{\lambda,\mu}(t)}=\bar n_t$ for every $t\ge0$ . In particular, the initial value is $\bar n_0=1$ . These definitions let the mission quantify over every admissible rate pair with the prescribed mean.

For a positive continuously differentiable mean curve, write $g(t)=\bar n_t'/\bar n_t$ . The minimum-fluctuation rates are $\lambda_*(t)=\max\{g(t),0\}$ and $\mu_*(t)=\max\{-g(t),0\}$ . When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.

Formalization targets

The goal is the simultaneous variance bound

V_{\lambda_*,\mu_*}(t)\le V_{\lambda,\mu}(t) \quad\text{for every }t\ge0 \text{ and every admissible }(\lambda,\mu)\text{ with mean }\bar n.

The statement also establishes that $(\lambda_*,\mu_*)$ is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for $a>1$ and $b>0$ , $\bar n_t=a/(1+(a-1)e^{-bt})$ has minimum-fluctuation death rate zero and birth rate $b(1-\bar n_t/a)$ .

Significance

The result distinguishes mean growth from population risk. Fixing $\lambda-\mu$ fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.

The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of $\rho$ because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.

Difficulty

The constraint imposed by a given mean fixes the difference $\lambda-\mu$ but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum $\lambda(t)+\mu(t)$ does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.

Formalization scope

The Lean development represents rates and the prescribed mean as functions $\mathbb R\to\mathbb R$ . Every stochastic claim is restricted to $t\ge0$ ; the integrals are oriented interval integrals from zero. Both rates are continuous on all of $\mathbb R$ and nonnegative on nonnegative time. The mean is $C^1$ , positive on all of $\mathbb R$ , and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining $g$ , $\lambda_*$ and $\mu_*$ continuous without changing any comparison on $[0,\infty)$ . These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.

Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of $\bar n$ . The goal uses positive and negative parts of $g$ and therefore covers any positive $C^1$ curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of $\lambda+\mu$ .

The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.

Selected references

D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.

6 thms2 active usersReviewed