Operations Research

Linear Optimization Optimization·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 2: τᵏ Stays Bounded Below If (LP) Has an Optimum, and Otherwise κᵏ Stays Bounded Below and τᵏ/θᵏ Is BoundedResearch Paper

Motivation

Interior-point methods for linear programming are usually analysed under two assumptions: a strictly feasible starting point is known, and the problem has an optimal solution. In practice neither is known in advance. The homogeneous self-dual embedding of Ye, Todd and Mizuno (Math. Oper. Res. 19(1), 1994) removes both assumptions. It embeds a standard-form linear program and its dual into one artificial program that always has an obvious interior starting point. A solution of the artificial program either yields optimal solutions of the original pair or certifies that one of them is infeasible. The embedding underlies the infeasibility detection of several interior-point LP and conic solvers.

The paper's main result is an $O(\sqrt n L)$ iteration bound. Section 4, "Analysis of the output", asks a different, practical question: what can be read off the iterates if the algorithm is stopped early, at an approximate solution? Theorem 8 answers it. This mission formalizes Theorem 8 and the results its proof uses.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ . The primal and dual programs are

\text{(LP)}\ \min\{c^Tx : Ax=b,\ x\ge0\},\qquad \text{(LD)}\ \max\{b^Ty : A^Ty\le c\},

with dual slack $s=c-A^Ty$ . An optimal solution pair is an optimal $\bar x$ of (LP) together with an optimal $(\bar y,\bar s)$ of (LD).

Write $e$ for the all-ones vector and set $\bar b=b-Ae$ , $\bar c=c-e$ , $\bar z=c^Te+1$ . The homogeneous self-dual program (HLP), in the paper's normalization $y^0=0$ , $x^0=s^0=e$ , has variables $(y,x,\tau,\theta,s,\kappa)$ with $y\in\mathbb R^m$ , $x,s\in\mathbb R^n$ , $\tau,\theta,\kappa\in\mathbb R$ :

\begin{array}{rl} \min & (n+1)\theta\\ \text{s.t.} & Ax-b\tau+\bar b\theta=0,\\ & s=-A^Ty+c\tau-\bar c\theta\ \ge0,\\ & \kappa=b^Ty-c^Tx+\bar z\theta\ \ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(n+1),\qquad x\ge0,\ \tau\ge0. \end{array}

$\mathcal F_h$ is its feasible set and $\mathcal F_h^0$ the subset with $x,\tau,s,\kappa>0$ . A self-complementary solution is an optimal solution of (HLP). A strictly self-complementary one also has $\theta=0$ and $(x+s;\tau+\kappa)>0$ . For a point of (HLP) put $\mu=(x^Ts+\tau\kappa)/(n+1)$ , and for $\beta\in(0,1)$ let

\mathcal N(\beta)=\Bigl\{z\in\mathcal F_h^0 : \Bigl\|\begin{pmatrix}Xs\\ \tau\kappa\end{pmatrix}-\mu e\Bigr\|_2\le\beta\mu\Bigr\}.

The predictor–corrector algorithm with $\beta=1/4$ starts at $z^0=(0,e,1,1,e,1)$ . At even $k$ (predictor step) it solves the Newton system (11)–(12) with target $\gamma\mu^k=0$ and moves along the direction by the largest step that stays in $\mathcal N(2\beta)$ (13). At odd $k$ (corrector step) it solves the system with target $\mu^k$ and takes a full step.

Formalization targets

Goal: Theorem 8 (p. 63)

For every predictor–corrector sequence $(y^k,x^k,\tau^k,\theta^k,s^k,\kappa^k)$ :

if (LP) possesses an optimal solution, then for every optimal pair $\bar x,(\bar y,\bar s)$

\tau^k\ge\frac{1-2\beta}{e^T\bar x+e^T\bar s+1}\quad\text{for all }k;

otherwise there is a fixed $\varepsilon>0$ , independent of $k$ , with

\kappa^k\ge\frac{(1-2\beta)\varepsilon}{n+1},\qquad \frac{1-2\beta}{2(n+1)}\le\frac{1-2\beta}{\kappa^k}\le\frac{\tau^k}{\theta^k}\le\frac{1+2\beta}{\kappa^k}\le\frac{(n+1)(1+2\beta)}{(1-2\beta)\varepsilon}

for all $k$ .

Milestones

In the order the proof uses them:

the predictor-step and corrector-step claims from the proof of Theorem 6 (p. 62);
the iterates lie in $\mathcal N(2\beta)$ (p. 63);
Theorem 2 (iv): the optimal value of (HLP) is $0$ and $(n+1)\theta=x^Ts+\tau\kappa$ on $\mathcal F_h$ (stated for general $x^0,s^0>0$ , $y^0$ );
equation (9): $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$ ;
an optimal pair scaled by $\alpha=(n+1)/(e^T\bar x+e^T\bar s+1)$ is a self-complementary solution;
the orthogonality identity $(x^k)^Ts^*+(s^k)^Tx^*+\kappa^k\tau^*=(n+1)\theta^k$ ;
Theorem 2 (v), existence of a strictly self-complementary solution;
Theorem 3 (i) and (ii), reading such a solution back into (LP) and (LD);
the bound $\kappa^k\le(n+1)+(n+1)\theta^k\le2(n+1)$ .

Significance

Theorem 8 is a stopping criterion. Either $\tau^k$ stays bounded away from zero, which happens exactly when (LP) has an optimal solution, or $\tau^k$ and $\theta^k$ go to zero at the same rate while $\kappa^k$ stays bounded away from zero. An implementation can therefore watch $\tau^k/\theta^k$ and $\kappa^k$ and decide the status of (LP) from an approximate iterate, without the exact rounding procedure needed for the $O(\sqrt nL)$ bound. The bounds hold for real data, with no integrality and no bit length.

Theorem 8 has a published proof on one page, building on the self-duality facts of §2 and the Mizuno–Todd–Ye step analysis. None of it is machine-checked. A complete development would give a verified account of the homogeneous self-dual embedding, including:

the skew-symmetric orthogonality argument;
Goldman–Tucker strict complementarity for (HLP);
the predictor–corrector neighborhood invariants.

These are the ingredients of every analysis of the embedding. Homogeneous self-dual programs appear on Prove2Me in other conventions (Vanderbei's (22.4) and (22.21), Matoušek's (SD)), but their statements concern different programs: no artificial variable $\theta$ , no normalizing row. They do not formalize any statement here.

Difficulty

The two branches of Theorem 8 rest on facts of different depth.

The first branch needs only an optimal pair of (LP)/(LD), lifted into (HLP), and the identity $(x^k)^Ts^*+(s^k)^Tx^*+\kappa^k\tau^*=(n+1)\theta^k$ .
The "otherwise" branch needs an optimal solution of (HLP) with $\kappa^*>0$ . Its existence is not elementary. It comes from strict complementarity (Theorem 2 (v)) together with the characterization of Theorem 3 (i). Strict complementarity for linear programs is the Goldman–Tucker theorem, which Mathlib does not contain.
The neighborhood invariants behind "the sequence is in $\mathcal N(2\beta)$ " are the Mizuno–Todd–Ye estimates. They need the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ of the Newton directions and a careful quadratic bound on $\|D_xd_s\|$ .

The obvious first idea is to treat Theorem 8 as a consequence of Theorem 6. It fails: Theorem 8 is about every iterate of an infinite run and uses no iteration count. The constant $\varepsilon$ depends on the instance and is not explicit.

Formalization scope

Data. Real data A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ, c : Fin n → ℝ, with no rank assumption and no integrality. (LP)/(LD) feasibility and optimality are built on the published general-form LP definition LinearOptimization_DualLP. "(LP) has a solution (feasible and bounded)" in Theorem 3 is read as "(LP) has an optimal solution".
Points. A point of (HLP) is a structure with fields y x τ θ s κ. The slacks $s,\kappa$ are pinned to the constraint expressions. (HLP) is defined for general $(x^0,y^0,s^0)$ ; the instance (7) is obtained by substitution. Optimality means minimizing the objective over $\mathcal F_h$ , not " $\theta=0$ ", so Theorem 2 (iv) is not built into the definition.
Norm. The norm in $\mathcal N(\beta)$ is the Euclidean norm on $\mathbb R^{n+1}$ , written out explicitly.
Constants. $\beta=1/4$ is a named constant. The statements show $1-2\beta$ and $1+2\beta$ as printed.
The iteration. It is a relation IsPCSequence: $z^0=(0,e,1,1,e,1)$ , and each step is $z^{k+1}=z^k+\alpha d$ for some solution $d$ of (11)–(12). The relation is needed because $d_y$ is not unique when $A$ is rank-deficient.
Step size. The predictor step size must be the greatest element of the set in (13), as printed. On an instance where that maximum is not attained, no predictor–corrector sequence exists and Theorem 8 holds vacuously there. A sorry-free check shows that $z^0\in\mathcal N(1/4)$ for all data, so the sequence does start.
The two branches. They are two implications with complementary hypotheses, "(LP) has an optimal solution" and its negation. The negation covers infeasible and unbounded (LP) alike.
Quantifiers. The first branch quantifies over all optimal pairs. In the second, $\exists\varepsilon>0$ precedes $\forall k$ .
Divisions. The chain keeps the printed divisions. All denominators ( $\kappa^k$ , $\theta^k=\mu^k$ ) are positive on $\mathcal N(2\beta)$ , so Lean's $x/0=0$ convention plays no role.
Ruled out. A formalization in which $\varepsilon$ may depend on $k$ , or in which the first branch asserts the bound for only some optimal pair, would make Theorem 8 trivial or weaker. Both are excluded.

Needed infrastructure: LP duality and Goldman–Tucker strict complementarity for real standard-form programs, and the skew-symmetric orthogonality lemma. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the central-path limit) for the existence of $\kappa^*>0$ , are welcome.

Selected references

Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$ -Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
S. Mizuno, M. J. Todd, Y. Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
O. Güler, Y. Ye, Convergence behavior of interior-point algorithms, Mathematical Programming 60, 215–228, 1993. https://doi.org/10.1007/BF01580610
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, 53–97, 1956. https://doi.org/10.1515/9781400881987-005

17 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Semidefinite Programming 2: If Every Step Lowers the Potential φ by δ > 0, Then After k ≥ (ν√n log(1/ε) + ψ(x⁽⁰⁾, Z⁽⁰⁾))/δ Steps the Duality Gap Is at Most ε Times Its Initial ValueResearch Paper

Motivation

Semidefinite programs optimize a linear objective while requiring an affine matrix to be positive semidefinite. They include familiar linear and quadratic optimization models and arise in engineering and combinatorial optimization. Vandenberghe and Boyd's survey develops their duality theory and describes interior point methods that work with primal and dual matrices simultaneously. The question in this mission is quantitative: if a method lowers a particular potential by a fixed amount at each step, how quickly does its primal-dual objective gap shrink? Vandenberghe and Boyd, pp. 49, 76–77.

The paper uses the potential to combine two kinds of progress. One term records the size of the duality gap; another records how far the current matrices are from a central pair. Decreasing the gap alone does not ensure the matrices remain well positioned for the next step, so the potential accounts for both quantities. Theorem 5.1 turns a per-step decrease in this scalar into an explicit bound on the gap after $k$ steps. The theorem concerns any sequence meeting that decrease condition; it does not prescribe a particular search direction or step-selection algorithm. Vandenberghe and Boyd, pp. 76–77.

Setting

Fix a vector $c\in\mathbb R^m$ and symmetric real $n\times n$ matrices $F_0,F_1,\ldots,F_m$ . For $x\in\mathbb R^m$ , define the affine matrix

F(x)=F_0+\sum_{i=1}^{m}x_iF_i.

The primal problem minimizes $c^Tx$ subject to $F(x)\succeq0$ . A dual-feasible matrix $Z$ satisfies $Z\succeq0$ and $\operatorname{Tr}(F_iZ)=c_i$ for every $i=1,\ldots,m$ . Here $\succeq0$ means positive semidefinite; $\succ0$ means positive definite. The pair $(x,Z)$ is strictly feasible if both $F(x)\succ0$ and $Z\succ0$ , with the dual equations still satisfied. Section 4 also assumes that $F_1,\ldots,F_m$ are linearly independent. Vandenberghe and Boyd, pp. 49, 63, 70.

For a feasible pair, the duality gap is the difference between the primal objective $c^Tx$ and the dual objective $-\operatorname{Tr}(F_0Z)$ . Equation (32) identifies it as

\eta=c^Tx+\operatorname{Tr}(F_0Z)=\operatorname{Tr}(F(x)Z).

For a strictly feasible pair, define the deviation from centrality and the potential by

\psi(x,Z)=-\log\det(F(x)Z)+n\log\eta-n\log n,

\varphi(x,Z)=\nu\sqrt n\,\log\eta+\psi(x,Z),\qquad \nu\ge1.

The logarithm is natural. The matrix size $n$ determines the $\sqrt n$ factor; it is distinct from the number $m$ of decision variables. These are the explicit formulas on p. 76, where the paper also expresses $\psi$ through a central pair. Vandenberghe and Boyd, pp. 64, 75–76.

Formalization targets

The first milestones establish the gap identity, the expanded determinant formula for $\varphi$ , and nonnegativity of $\psi$ with its stated equality condition. The final milestone bounds the gap by the potential:

\eta\le\exp\!\left(\frac{\varphi(x,Z)}{\nu\sqrt n}\right).

For the goal, let $(x^{(j)},Z^{(j)})$ , $j=0,\ldots,k$ , be strictly feasible pairs and suppose a fixed $\delta>0$ gives the decrease stated in equation (56) at every step $j<k$ :

\varphi(x^{(j+1)},Z^{(j+1)})\le\varphi(x^{(j)},Z^{(j)})-\delta.

The goal theorem, Theorem 5.1, says that for $0<\varepsilon<1$ and

k\ge\frac{\nu\sqrt n\log(1/\varepsilon)+\psi(x^{(0)},Z^{(0)})}{\delta},

one has the boundary-correct gap estimate

\operatorname{Tr}(F(x^{(k)})Z^{(k)})\le\varepsilon\operatorname{Tr}(F(x^{(0)})Z^{(0)}).

The paper prints a strict inequality in the last display. Its stated non-strict threshold permits equality, as explained under Formalization scope. Vandenberghe and Boyd, p. 77, (56) and Theorem 5.1.

Significance

The theorem converts a local numerical guarantee into a global bound on an optimization certificate. Because the gap is the difference between primal and dual objectives, shrinking it gives a quantitative measure of progress toward optimality for every strictly feasible iterate. The expression records the dependence on matrix size, desired relative gap, starting deviation, and guaranteed potential decrease. It leaves the mechanism that achieves the decrease open, so different potential reduction methods can use the same conclusion. Vandenberghe and Boyd, pp. 64, 76–77.

The target here is a machine-checked statement and proof of this known 1996 result, together with its four supporting facts. The draft declarations compile as statements; their proofs remain open. A complete development would make the determinant, trace, positive-definiteness, and sequence reasoning reusable for other matrix optimization arguments. It would also record the boundary correction precisely rather than carrying forward a strict sign that fails at equality.

Difficulty

The substantive matrix claim is $\psi(x,Z)\ge0$ . The product $F(x)Z$ need not be symmetric, even though both factors are positive definite, so directly applying a result about symmetric matrix eigenvalues to the product is not automatic. The nonnegativity and its equality case must respect the positivity and determinant conventions used by the explicit formula. The later exponential bound and iteration statement depend on those facts and on keeping each logarithm in its positive domain. Vandenberghe and Boyd, p. 76.

Formalization scope

Lean uses Fin m for the $m$ variable matrices, indexed from zero, with $F_0$ as a separate argument; Fin n indexes matrix rows and columns. Matrix.IsHermitian represents real symmetry. Matrix.PosSemidef and Matrix.PosDef represent the paper's matrix inequalities $\succeq0$ and $\succ0$ , including symmetry. The matrix size satisfies $n\ge1$ . Traces, determinants, natural logarithms, and $\sqrt n$ are the corresponding Mathlib operations. All statements involving $\psi$ or $\varphi$ require strict feasibility, so the real logarithm's default value on nonpositive inputs cannot decide a theorem. The paper's linearly independent $F_1,\ldots,F_m$ are an explicit hypothesis on the Section 4 and 5 statements. Vandenberghe and Boyd, pp. 49, 70, 76–77.

The definition of $\psi$ uses the explicit second formula on p. 76. The central pair in the preceding formula is not represented; its existence is introduced on p. 75 without a proof there. The p. 76 prose describes $\psi\ge0$ for feasible pairs, but its finite real logarithmic formula and the potential reduction iterates use strictly feasible pairs. The milestone states that domain explicitly. In Theorem 5.1 strict feasibility is assumed for the iterates $j=0,\ldots,k$ and equation (56) for the steps $j<k$ only, so the statement covers a method that stops after $k$ steps. The fixed $\delta$ is positive, and $\nu\ge1$ and $0<\varepsilon<1$ are explicit.

The paper's strict conclusion is false at its own inclusive threshold. Take $m=n=1$ , $F_0=0$ , $F_1=c=Z^{(j)}=1$ , $x^{(j)}=e^{-j}$ , $\nu=\delta=1$ , and $\varepsilon=e^{-1}$ . Then $\psi=0$ , each decrease is exactly one, and at $k=1$ the gap equals $\varepsilon$ times its initial value. The goal therefore uses $\le$ , the strongest statement valid at the printed threshold. This correction is recorded in the theorem's description and moderation notes. Vandenberghe and Boyd, p. 77, Theorem 5.1.

A complete proof needs Mathlib's matrix order, determinant and trace identities, logarithm and exponential facts, and an arithmetic-geometric mean statement for positive eigenvalues. Matrix lemmas and the deviation inequality are welcome contributions alongside the final sequence bound. The definitions preserve the paper's full potential and feasible domain; replacing $\psi$ by zero or dropping the $\sqrt n$ factor would change the target.

Selected references

Lieven Vandenberghe and Stephen Boyd, Semidefinite Programming, SIAM Review 38(1), 49–95, 1996. DOI: 10.1137/1038003.

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

Potential Games 3: A Finite Game Has the Finite Improvement Property If and Only If It Has a Generalized Ordinal PotentialResearch Paper

Motivation

In a strategic game, players may repeatedly change their own choices when a change raises their payoff. This gives a simple model of decentralized adjustment: each move uses the current profile and one player's immediate incentive. The central question is whether such adjustment can continue forever. Monderer and Shapley introduced the finite improvement property (FIP) to state that every sequence of strict unilateral improvements ends. Their 1996 paper, pp. 128–130, relates that dynamic property to a real-valued function on the game's strategy profiles.

An ordinal potential records each player's strict preference between two of their strategies when the other players' strategies are fixed. Such a function is useful because it assigns one common direction to the players' individual choices. The paper gives a two-player game $G_1$ that has the FIP but no ordinal potential, then introduces a weaker, generalized ordinal potential and proves that it captures exactly the finite games with the FIP (Monderer and Shapley, pp. 129–130). This mission isolates that characterization from the paper's other results about exact potentials and congestion games.

Setting

Let $N$ be a finite set of players. Player $i\in N$ has a strategy set $Y^i$ , and a strategy profile $y\in Y=\prod_{i\in N}Y^i$ selects one strategy for each player. The payoff function $u^i:Y\to\mathbb R$ gives player $i$ 's payoff at a profile. Write $(y^{-i},x)$ for the profile obtained by replacing player $i$ 's strategy in $y$ by $x\in Y^i$ . A finite game has finite $Y^i$ for every player. These are the paper's conventions at the start of §2 (p. 127).

A path is a sequence of profiles in which each step changes exactly one player's strategy to a different strategy. It is an improvement path when the moving player strictly increases their payoff at every step. The game has the FIP if no infinite improvement path exists. Thus the property concerns paths of any length and every allowed choice of deviator, rather than the behavior of one selected update rule (p. 128).

An ordinal potential $P:Y\to\mathbb R$ satisfies

u^i(y^{-i},x)>u^i(y^{-i},z)\quad\Longleftrightarrow\quad P(y^{-i},x)>P(y^{-i},z)

for every player $i$ , opponents' profile $y^{-i}$ , and $x,z\in Y^i$ . A generalized ordinal potential replaces this equivalence by the forward implication only. The two notions are distinct, as the game $G_1$ on p. 129 shows (equations (2.1) and (2.3), pp. 127, 129).

Formalization targets

Goal: Lemma 2.5

For every finite game $\Gamma$ ,

\Gamma\text{ has the FIP}\quad\Longleftrightarrow\quad \Gamma\text{ admits a generalized ordinal potential}.

This is Lemma 2.5, p. 129. It specifies a precise characterization rather than choosing a particular potential or a particular update schedule.

Supporting statements

The milestone list follows the paper's statements: Lemma 2.3 says a finite ordinal potential game has the FIP; the proof of Lemma 2.5 says the finite-improvement reachability relation is transitive under the FIP; and it concludes that the whole strategy-profile set can be represented by a real function increasing along that relation (pp. 128–130). Corollary 2.6 and the explicit game $G_1$ record the boundary between ordinal and generalized ordinal potentials: under its distinct-payoff condition a finite game with the FIP has an ordinal potential, while $G_1$ shows that condition cannot simply be omitted (pp. 129–130). Lemma 2.1 and Corollary 2.2 concern equilibria: an ordinal potential game has the same pure equilibria as the game in which every player receives the potential, so a maximizer of the potential is an equilibrium, and every finite ordinal potential game has a pure-strategy equilibrium (p. 128).

Significance

The goal connects a property of all possible strict improvement paths to the existence of a single real-valued certificate on profiles. In a finite game, such a certificate describes a common direction for unilateral payoff gains, regardless of which improving player moves next. The distinction between ordinary and generalized ordinal potentials matters: an ordinary potential must also preserve indifference, whereas the FIP alone does not require that (Monderer and Shapley, p. 129).

The characterization is proved in the paper; the remaining work in this mission is a Lean proof of its faithful finite-game statement. The local platform index used for this proposal has no published theorem expressing this characterization. The definitions of improvement paths and improvement reachability can also support other formal results about game dynamics. The game $G_1$ serves as a concrete check on the strict distinction between the two potential notions.

Difficulty

The payoff vector itself does not give an immediate numerical order on whole profiles: each step compares one player's payoff, and the next step may involve another player. Finiteness rules out an endlessly increasing sequence only after a suitable profile-level ordering has been established. The converse direction therefore requires more than observing that each individual move helps its deviator. The paper's $G_1$ also rules out replacing the generalized potential in the goal with an ordinary ordinal one (p. 129).

Formalization scope

Players form a finite Lean type ι with decidable equality; each player's strategies form a type Y i. A theorem about a finite game additionally assumes every Y i is finite. These types may be empty: in that case there is no strategy profile, and the corresponding FIP and potential statements retain their ordinary quantified meaning. No nonemptiness assumption is inserted into Lemma 2.5. Corollary 2.2 alone assumes every strategy set nonempty, which the page takes for granted: without it there is no profile and no equilibrium. An equilibrium point is a pure Nash equilibrium in the sense of the published definition AGT.IsPureNash (no player gains strictly by a unilateral deviation), and "P admits a maximal value in Y" in Lemma 2.1 is read as "P attains its maximum on Y". The finite player assumption follows the standing convention on p. 127; the finite strategy assumption is added only where the source says “finite game.”

The expression $(y^{-i},x)$ is Function.update y i x. IsStep requires one coordinate to change to a different value. HasFIP forbids an infinite natural-number-indexed path of strict payoff improvements, so it cannot be satisfied merely because each separately described finite path has finite length. A finite path stores its deviator at each step; the genuine-step condition determines that deviator uniquely. The same path bundle contains the paper's path sum and closed-path predicates for consistency across this paper's missions, although only finite improvement paths are used here. The relation ImprovesTo u x y means that a finite strict improvement path leads from $y$ to a distinct $x$ .

The necessary development comprises the two potential predicates, path and FIP definitions, the finite improvement relation, the transitivity and representation milestones, and the goal characterization. Contributions that prove these statements or simplify their proof dependencies are within scope. A definition that checks only finite paths, allows null steps, or confuses the one-way condition (2.3) with the two-way condition (2.1) would change the result.

Selected references

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

13 thms3 active usersReviewed

Completed

Machine Learning Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

Motivation

In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).

The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).

Setting

Fix a finite nonempty pool of $n$ forecasters and a finite sequence of $t$ trials. At trial $j$ , expert $i$ predicts $x_i^{(j)}\in[0,1]$ , and after the master predicts, a label $\rho^{(j)}\in[0,1]$ is revealed. Expert $i$ has weight $w_i^{(j)}$ before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are

s^{(j)}=\sum_{i=1}^{n}w_i^{(j)},\qquad \gamma^{(j)}=\frac{\sum_{i=1}^{n}w_i^{(j)}x_i^{(j)}}{s^{(j)}}.

WMC predicts $\gamma^{(j)}$ . Its loss on the trial is the absolute error $|\gamma^{(j)}-\rho^{(j)}|$ , and its total absolute loss is $m=\sum_{j=1}^{t}|\gamma^{(j)}-\rho^{(j)}|$ . Write $w_{\mathrm{init}}=s^{(1)}$ and $w_{\mathrm{fin}}=s^{(t+1)}$ for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).

WMC updates on every trial. For $0\le\beta<1$ , it multiplies each weight by a factor $F_i^{(j)}$ in the interval

\beta^{|x_i^{(j)}-\rho^{(j)}|}\le F_i^{(j)}\le 1-(1-\beta)|x_i^{(j)}-\rho^{(j)}|, \qquad w_i^{(j+1)}=F_i^{(j)}w_i^{(j)}.

The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention $0^0=1$ is used when $\beta=0$ and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).

Formalization targets

Theorem 5.2: WMC total loss

For every run with positive final total weight, the target is the paper's explicit inequality

m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{1-\beta}.

The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes $w_{\mathrm{fin}}>0$ ; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).

Supporting numbered results

Lemma 5.1 states $\beta^r\le1+r(\beta-1)$ for $\beta\ge0$ and $0\le r\le1$ , ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which $\beta=0$ and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).

Significance

The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit $1/(1-\beta)$ constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).

The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.

Difficulty

A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at $\beta=0$ : an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.

Formalization scope

The pool is Fin n with $n>0$ and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents $w^{(1)}$ and w t represents the weights after all $t$ trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in $[0,1]$ , $0\le\beta<1$ , and a permitted factor for every expert on every trial.

The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in 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.

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics·Captain: mikedeng1

Potential Games 2: Every Finite Potential Game Is Isomorphic to a Congestion GameResearch Paper

Motivation

Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.

Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.

Setting

A game in strategic form $\Gamma$ has a finite set of players $N = \{1, \dots, n\}$ , for each player $i$ a strategy set $Y^i$ , the profile set $Y = \times_{i\in N} Y^i$ , and payoff functions $u^i : Y \to \mathbb{R}$ . For a profile $y$ and $x \in Y^i$ , $(y^{-i}, x)$ is $y$ with player $i$ 's strategy replaced by $x$ . The game is finite if every $Y^i$ is finite.

A function $P : Y \to \mathbb{R}$ is a potential for $\Gamma$ (condition (2.2) with unit weights) if

u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z) \qquad \text{for all } i,\ y^{-i},\ x, z \in Y^i,

and $\Gamma$ is a potential game if it has a potential (IsPotential, IsPotentialGame).

A congestion model $C(N, M, (\Sigma^i)_{i\in N}, (c_j)_{j\in M})$ has players $N$ , a finite set of facilities $M$ , for every player a set $\Sigma^i$ of strategies, each a nonempty subset of $M$ , and for every facility $j$ a vector $c_j$ , where $c_j(k)$ is the payoff to each user of $j$ when exactly $k$ players use it. The associated congestion game has strategy sets $\Sigma^i$ and payoffs

v^i(A) = \sum_{j\in A^i} c_j\big(\sigma_j(A)\big), \qquad \sigma_j(A) = \#\{i \in N : j \in A^i\}. \tag{3.1}

Two games with the same players are isomorphic (IsIsomorphic) if there are bijections $g^i : Y^i_1 \to Y^i_2$ with $u^i_1(y) = u^i_2(g^1(y^1), \dots, g^n(y^n))$ for every player $i$ and profile $y$ .

Formalization targets

Goal: Theorem 3.2

\text{Every finite potential game is isomorphic to a congestion game.}

Formally: for every finite set of players, finite strategy sets $Y^i$ and payoffs $u$ admitting a potential, there are $m \in \mathbb{N}$ and a congestion model on the facilities $\{1, \dots, m\}$ , all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to $\Gamma$ .

Milestones

The milestones follow Appendix B of the paper.

Lemma B.1 (p. 139): with $x^r(j) = c_j(r)$ and $x(B) = \sum_{j\in B} x(j)$ , $v^i(A) = x^1(A(i)\cap A(-i)^c) + x^2\big(\bigcup_{k\neq i}[A(i)\cap A(k)\cap A(-\{i,k\})^c]\big) + \cdots + x^n\big(\bigcap_{k} A(k)\big)$ .
The invariance of $u^i - P$ (p. 141): $u^i(a^{-i}, a^i) - P(a^{-i}, a^i)$ does not depend on $a^i$ .
The $M_1$ identity and (B.2) (p. 141): on the facility set $M = \times_i \{0,1\}^{K(i)}$ , $A^1_{m_1}\cap\cdots\cap A^n_{m_n}\cap M_1 = \{\varepsilon(m)\}$ , so $x^n(A^1_{m_1}\cap\cdots\cap A^n_{m_n}) = P(a^1_{m_1}, \dots, a^n_{m_n})$ .
(B.6) (p. 141): $x^1(A^i_{m_i}\cap A(-i)^c) = x^1(\varepsilon(m^i)) = u^i(a) - P(a)$ .

Significance

Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.

Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.

Difficulty

The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load $1$ and load $n$ , by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of $u^i$ that player $i$ cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.

The construction as printed does not cover one player: with $n = 1$ the vectors $x^1$ and $x^n$ are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.

Formalization scope

Players form a finite type ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). $(y^{-i}, x)$ is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.
The congestion model is the published CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family $\Sigma^i$ and latency j k is the paper's $c_j(k)$ , an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at $0$ and above $n$ never enter (3.1).
The congestion game as a game in strategic form is congestionPayoff G, whose strategy set for player $i$ is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.
In the goal the facility set is Fin m for an existentially quantified $m$ , and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal $u$ , would make the goal a different, weaker statement; the formal goal does neither.
The Appendix B construction (FacilityConstruction) indexes the coordinates of player $i$ by $Y^i$ itself instead of $K(i) = \{1, \dots, k(i)\}$ ; $m^i = (m_k)_{k\neq i}$ is passed as a full profile whose $i$ -th coordinate is ignored; $x^n$ and $x^1$ select a representative by choice, the chosen $i$ -th coordinate playing the role of the arbitrary $a^i$ in (B.4).
Misprints corrected: in Lemma B.1, $x^r(j) = c_j(m)$ is read $c_j(r)$ , and the " $\cdots$ " as the general term $x^r(\bigcup_{S\ni i, |S| = r}[\bigcap_{k\in S}A(k)\cap A(-S)^c])$ ; in (B.6), $A(-i)$ is read $A(-i)^c$ and $P^i(a)$ as $P(a)$ .

Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.

Selected references

D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2 (1973), 65–67. https://doi.org/10.1007/BF01737559
E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler and T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38 (2008), 1602–1623. https://doi.org/10.1137/070680096 (source of the platform's Rosenthal potential identity)

13 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.

Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). Examples are $\mathbb{R}^n$ and products of finite chains, ordered componentwise.

A function $f : X \to \mathbb{R}$ is supermodular on a set $S \subseteq X$ if

f(x) + f(y) \le f(x \vee y) + f(x \wedge y) \qquad \text{for all } x, y \in S.

It is quasisupermodular (p. 162) if for all $x, y \in X$

$f(x) \ge f(x \wedge y)$ implies $f(x \vee y) \ge f(y)$ , and
$f(x) > f(x \wedge y)$ implies $f(x \vee y) > f(y)$ .

A function $h : \mathbb{R} \to \mathbb{R}$ is strictly increasing if $r < s$ implies $h(r) < h(s)$ . A function $f$ is supermodularizable if $h \circ f$ is supermodular on $X$ for some strictly increasing $h$ .

For $x_1, x_2 \in X$ the set $\{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}$ is closed under $\vee$ and $\wedge$ ; it is the sublattice generated by $x_1$ and $x_2$ and has at most four points.

Quasisupermodularity depends only on the order of the values of $f$ , so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.

Formalization targets

Goal: Theorem 8 (p. 165)

$f : X \to \mathbb{R}$ is quasisupermodular if and only if there is $g : \mathbb{R} \times X \times X \to \mathbb{R}$ such that (i) $r \mapsto g(r, x_1, x_2)$ is strictly increasing for every $(x_1, x_2) \in X^2$ , and (ii) for every $x_1, x_2 \in X$ ,

x \mapsto g(f(x), x_1, x_2) \ \text{ is supermodular on } \{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}.

Milestones

Invariance (p. 164): if $f$ is quasisupermodular and $g$ strictly increasing, $g \circ f$ is quasisupermodular.
Supermodularizable implies quasisupermodular (pp. 164–165): if $h$ is strictly increasing and $h \circ f$ is supermodular on $X$ , then $f$ is quasisupermodular.
Lemma (p. 165): if $f$ is quasisupermodular on $L = \{x, x', x \vee x', x \wedge x'\}$ , then $h \circ f$ is supermodular on $L$ for some strictly increasing $h : \mathbb{R} \to \mathbb{R}$ .
Example 1 (p. 165): the function on $\{0,1\} \times \{0,1,2,3\}$ with rows $(1,2,2,1)$ and $(3,4,5,3)$ is quasisupermodular but not supermodularizable.

The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on $(x_1, x_2)$ .

Significance

Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.

On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of $\mathbb{R}$ that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.

Difficulty

The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values $a, b, c, d$ of $f$ at $x, x \vee x', x \wedge x', x'$ need not satisfy $a + d \le b + c$ , and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing $h$ of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which $x$ and $x'$ are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair $(x, x')$ .

Formalization scope

Lattices are Mathlib's Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.
Quasisupermodularity is a draft definition QuasiSupermodularOn g S, relativized to a set $S$ ; the paper's notion on $X$ is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of $S$ .
Supermodularity is the published definition Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.
"Strictly increasing" is StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.
The transformation $g : \mathbb{R} \times X \times X \to \mathbb{R}$ of Theorem 8 is curried, g : ℝ → X → X → ℝ; it may depend on $(x_1, x_2)$ but not on $x$ . Transformations are defined on all of $\mathbb{R}$ , as printed, not only on the values of $f$ .
The Lemma's four-point lattice is formalized as the subset $\{x, x', x \vee x', x \wedge x'\}$ of an ambient lattice, with both notions relativized to it; the subset is closed under join and meet, so this is the page's statement, including the degenerate cases.
Example 1's domain is Fin 2 × Fin 4 with the product order.

Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps $\mathbb{R} \to \mathbb{R}$ with prescribed values on finitely many points.

Selected references

P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
M. Li Calzi, Generalized Symmetric Supermodular Functions, Working Paper, Stanford University, 1990 (listed so in the paper's references; the text on p. 165 cites it as Li Calzi (1991)).

8 thms3 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 2: Kesten's Theorem for R = Q + MR — Unique Stationary Law, Power Tails with Explicit C±, and C₊ + C₋ > 0 iff Q ≢ (1 − M)cResearch Paper

Motivation

The random difference equation

R \overset{\mathcal L}{=} Q + MR,\qquad R \text{ independent of } (Q,M),

describes the stationary state of the affine recursion $R_n = Q_n + M_n R_{n-1}$ driven by independent copies of a random pair $(Q,M)$ . It appears wherever a quantity is multiplied by a random factor and then receives a random increment: the discounted value of a stream of random cash flows (a perpetuity), the stationary volatility of ARCH and GARCH models in financial econometrics (de Haan, Resnick, Rootzén and de Vries 1989), random walks in random environment, and the stationary laws of random coefficient autoregressions. In all of these, the question that matters for risk is the size of the tail $P(R>t)$ .

Timeline:

1973. Kesten proves, in a multivariate setting, that the stationary solution has power-law tails, $P(R>t)\sim C_+t^{-\kappa}$ , where $\kappa$ solves $\mathbf E|M|^\kappa=1$ ; the constants are not identified, and the proof of the key renewal step (his Theorem 4) runs to nine pages.
1979. Vervaat gives a full account of existence, uniqueness and moments of the solution in dimension one.
1980–1981. Grincevičius proves a maximal inequality of Lévy type for the partial sums of the recursion.
1986. Letac formulates a general principle for existence and uniqueness of solutions of random equations $R\overset{\mathcal L}{=}\Psi(R)$ .
1991. Goldie proves an implicit renewal theorem (Theorem 2.3, the subject of the first mission of this series) and deduces from it a new proof of Kesten's one-dimensional theorem, with explicit formulas for the constants $C_\pm$ and a necessary and sufficient condition for them not to vanish (Theorem 4.1).
2016. Buraczewski, Damek and Mikosch survey the theory, in which Kesten's theorem in Goldie's form is the central result.

Setting

Let $(Q,M)$ be a pair of real random variables with joint law $\mu$ on $\mathbb R^2$ . No independence between $Q$ and $M$ and no sign condition on either is assumed. A probability law $\rho$ on $\mathbb R$ is a law for $R$ satisfying (1.1) if the law of $Q+MR$ equals $\rho$ when $R$ has law $\rho$ and is independent of $(Q,M)$ .

A law on $\mathbb R$ is arithmetic if it is concentrated on a lattice $\{n\lambda:n\in\mathbb Z\}$ for some $\lambda>0$ , and nonarithmetic otherwise. For $\kappa>0$ , the conditions of Lemma 2.2 on $M$ are

\mathbf E|M|^\kappa = 1,\qquad \mathbf E|M|^\kappa\log^+|M|<\infty,

and that the conditional law of $\log|M|$ given $M\ne0$ is nonarithmetic. Under them

m := \mathbf E|M|^\kappa\log|M| \in (0,\infty).

With $x^+=x\vee0$ and $x^-=(-x)\vee0$ , the constants of Theorem 4.1 are, when $M\ge0$ a.s.,

C_\pm = \frac{\mathbf E\big(((Q+MR)^\pm)^\kappa-((MR)^\pm)^\kappa\big)}{\kappa m},

and otherwise $C_+=C_-=\frac{1}{2\kappa m}\mathbf E\big(|Q+MR|^\kappa-|MR|^\kappa\big)$ , where $R$ has the stationary law and is independent of $(Q,M)$ .

Formalization targets

Goal: Theorem 4.1

Assume the conditions of Lemma 2.2 and $\mathbf E|Q|^\kappa<\infty$ . Then there is a unique law $\rho$ for $R$ satisfying (1.1); the expectations defining $C_\pm$ are finite; and

\lim_{t\to\infty} t^\kappa P(R>t) = C_+,\qquad \lim_{t\to\infty} t^\kappa P(R<-t) = C_-,

with $C_\pm$ as above. Finally

C_++C_->0 \iff P\big(Q=(1-M)c\big)<1 \ \text{ for each fixed } c\in\mathbb R.

Milestones

In the order the proof uses them:

Corollary 2.4: the implicit renewal theorem with the moment conditions (2.16)–(2.17) and constants (2.18)–(2.20), for a general random function $\Psi$ in place of $t\mapsto Q+Mt$ .
Lemma 9.4: tail-difference integrals against $t^{\kappa-1}dt$ versus moment differences.
The elementary inequalities (9.26)–(9.27).
(4.8): for $\kappa>1$ , $\mathbf E|R|^{\kappa-1}<\infty$ with an explicit bound.
(2.16)–(2.17) for $\Psi(t)=Q+Mt$ : the moment differences are integrable.
Proposition 4.2 (Grincevičius's maximal inequality) and its consequence (4.6).
The lower bound $P(|\Pi_n|>e^t\text{ for some }n)\ge\delta e^{-\kappa t}$ for the products $\Pi_n=M_1\cdots M_n$ .
Under the condition $P(Q=(1-M)c)<1$ for each $c$ , $t^\kappa P(|R|>t)$ stays bounded away from $0$ .

Significance

The result. Theorem 4.1 identifies the tail exponent of the stationary solution as the root $\kappa$ of $\mathbf E|M|^\kappa=1$ , which depends on $M$ alone, and expresses the tail constants as expectations under the stationary law. The constants yield the bounds of Corollary 4.3 and closed forms when $\kappa$ is an integer (Corollaries 4.4, 4.5). The dichotomy between $M\ge0$ a.s. (different left and right constants) and $P(M<0)>0$ (equal constants) is visible only through these formulas. The positivity criterion tells when the power tail is really there: it fails exactly when the recursion has a deterministic fixed point $c$ . Tail estimates for GARCH processes, perpetuities in insurance mathematics and random walks in random environment are applications of this statement.

Formalizing it. The theorem has been proved since 1973 and in the present form since 1991; it is open only as a formalization. No machine-checked proof of Kesten's theorem, of the implicit renewal theorem, or of the underlying nonarithmetic key renewal theorem on the whole line is known to this mission. The work consists of formalizing Goldie's proof, which assembles the implicit renewal theorem with moment estimates, a maximal inequality and a Cramér–Lundberg-type lower bound for a random walk with negative drift.

Difficulty

The obvious argument is to write $R=\sum_{k\ge1}\Pi_{k-1}Q_k$ and estimate the tail of each term. It fails because $\mathbf E|M|^\kappa=1$ makes every term contribute tails of the same order $t^{-\kappa}$ , and the sum of infinitely many such contributions is exactly what has to be computed; termwise bounds give the right exponent at best, not the limit or the constant. A second natural idea, applying the renewal theorem directly to $P(R>t)$ , needs integrability of a tail difference that is not evident, because $\mathbf E|R|^\kappa$ is infinite whenever $C_++C_->0$ ; the moment differences $((Q+MR)^+)^\kappa-((MR)^+)^\kappa$ must be controlled without either term being integrable. The positivity half is a separate problem: the formula for $C_\pm$ is a difference of two infinite-looking quantities, and showing it is positive requires a lower bound on the tail that does not come from the formula.

Formalization scope

Everything is stated in terms of laws. The joint law of $(Q,M)$ is a probability measure $\mu$ on $\mathbb R\times\mathbb R$ (first coordinate $Q$ , second $M$ ); a law for $R$ satisfying (1.1) is a probability measure $\rho$ on $\mathbb R$ that equals the image of $\mu\otimes\rho$ under $((q,m),r)\mapsto q+mr$ , and uniqueness is among all probability measures on $\mathbb R$ , with no moment restriction. Expectations involving $R$ and $(Q,M)$ are integrals against $\mu\otimes\rho$ , which is what makes $R$ independent of $(Q,M)$ . The conditions of Lemma 2.2 are stated for the law of $M$ , with $\mathbf E|M|^\kappa$ and $\mathbf E|M|^\kappa\log^+|M|$ as lower Lebesgue integrals and the conditional law of $\log|M|$ taken given $M\neq0$ . " $P(R>t)\sim C_+t^{-\kappa}$ " is the limit statement $t^\kappa P(R>t)\to C_+$ , which the paper prescribes and which includes $C_+=0$ . Milestones on sequences use independent copies $(Q_n,M_n)$ on an arbitrary probability space carrying them, stored 0-based.

The statement does not reduce to a trivial one: the ratio form $P(R>t)/(C_+t^{-\kappa})\to1$ (undefined when $C_+=0$ ), existence of some fixed point without uniqueness, the positivity criterion as a one-way implication, and tail limits asserted for an arbitrary random variable rather than for the stationary law are all excluded. One correction to the source is built in: Lemma 9.4's (9.17) is printed as an equality, which fails for independent identically distributed non-degenerate $X$ , $Y$ ; the inequality the proof establishes is stated.

A complete development needs: convolution and image measures of products on $\mathbb R^2\times\mathbb R$ ; the key renewal theorem on the whole line for nonarithmetic laws with positive mean (the content of the first mission of this series); existence and uniqueness for contractive random affine maps; Lévy-type maximal inequalities; and ladder-height estimates for random walks with negative drift whose steps may equal $-\infty$ . The renewal-theoretic and random-walk components are reusable well beyond this mission. Contributions of any milestone, and of supporting lemmas such as the moment bounds for perpetuities, are welcome.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Annals of Applied Probability 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
L. de Haan, S. I. Resnick, H. Rootzén and C. G. de Vries, Extremal behaviour of solutions to a stochastic difference equation with applications to ARCH processes, Stochastic Processes and their Applications 32(2):213–224, 1989. https://doi.org/10.1016/0304-4149(89)90076-8
D. Buraczewski, E. Damek and T. Mikosch, Stochastic Models with Power-Law Tails: The Equation X = AX + B, Springer, 2016. https://doi.org/10.1007/978-3-319-29679-1

13 thms3 active usersReviewed

Optimization Probability·Captain: mikedeng1

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Inventory pooling lets several locations serve their combined demand from one stock of goods. Classical newsvendor analysis predicts lower optimal cost when pooling reduces demand variation, but the reduction can vanish when demands are perfectly correlated. Xuanming Su asks whether that conclusion survives when managers make noisy stocking decisions rather than always choose the optimum. In the published 2008 article, Bounded Rationality in Newsvendor Models, the decision noise follows a continuous logit model, in which better quantities are chosen more often. Proposition 7 gives conditions under which pooling strictly lowers expected cost, including a case where classical pooling has no cost gain. Su, 2008

The question matters for multilocation inventory systems because an order quantity is a decision as well as a response to demand. Pooling changes both the distribution of demand faced by the system and the number of independently chosen orders. A comparison based only on optimal costs leaves the second change out. This mission isolates the paper's mathematical claim about the combined effect of demand and decision variation. Su, 2008, §9

Setting

There are $n$ locations. Demand at location $i$ is normally distributed with mean $\mu_i$ and standard deviation $\sigma_i$ . The total demand has normal law with mean $\mu_T=\sum_i\mu_i$ and standard deviation $\sigma_T$ . An order of $x$ against a realized demand $D$ incurs holding cost $h(x-D)^+$ for unsold units and backlog cost $b(D-x)^+$ for unmet demand. Its expected cost is $\gamma(x)$ . The decentralized system incurs one such cost at each location; the pooled system orders once for total demand. The published InventoryControl_newsboy definition supplies this Gaussian expected cost, with the same orientation of holding and backlog penalties as Su's equations (29) and (31). Su, 2008, p. 584

For an expected profit function $\pi$ on a decision set $S$ , the logit choice density is proportional to $e^{\pi(x)/\beta}$ on $S$ , where $\beta>0$ is a common bounded-rationality parameter. Larger $\beta$ spreads choices more widely; smaller positive $\beta$ concentrates them near high-profit choices. For normal demand, the decision domain is all of $\mathbb R$ . With $p=h+b$ and $c=h$ , expected profit differs from minus expected cost by a constant independent of the order. The same logit law is therefore obtained from utility $-\gamma(x)$ . The random behavioral order is denoted $X_i^b$ at location $i$ and $X_T^b$ for the pool. Su, 2008, pp. 571–572, 584

Formalization targets

Strict pooling reduction

The goal is Proposition 7. Under positive holding and backlog costs, one common positive $\beta$ , at least two locations, positive individual standard deviations, and

\sigma_T\leq\sum_{i=1}^{n}\sigma_i, \qquad \sigma_T\geq\sigma_i\quad\text{for every }i,

the claim is

\mathbb E\bigl[\gamma_T(X_T^b)\bigr] <\sum_{i=1}^{n}\mathbb E\bigl[\gamma_i(X_i^b)\bigr].

The first standard-deviation inequality is automatic for the sum of jointly normal demands. The second excludes a total demand whose standard deviation is smaller than an individual location's. The result still includes perfect positive correlation, where the first inequality is an equality. Su, 2008, Proposition 7, p. 585

Supporting statements

Five milestones record the source's route to that comparison: invariance of the choice distribution under an order-preserving affine change of quantity (Lemma 1), invariance under an additive shift in utility (Lemma 2), standardization of the Gaussian newsvendor objective (equation (63)), the optimum of the canonical standard-normal newsvendor and the nonpositivity of its profit, and the comparison of its expected values at different positive scales. The milestone text preserves the wording of the printed article; the precise Lean conditions and corrections are stated with the items. Su, 2008, pp. 572, 587–588

Significance

The strict inequality separates two mechanisms of pooling. Demand aggregation can reduce variability, while a single pooled order also avoids accumulating the costs of several noisy decisions. Proposition 7 shows that the latter mechanism can make the cost reduction strict even when perfect correlation removes the usual variance benefit. It provides a condition that can be checked from individual and total standard deviations, rather than requiring an explicit covariance matrix in the final comparison. Su, 2008, pp. 584–585

The result is proved in the paper; the remaining task is a machine-checked formalization of its definitions and argument. The Gaussian expected-cost object is already published on Prove2Me, while the continuous logit law and this behavioral pooling theorem are new to this mission. The invariance statements and canonical profit comparison are reusable wherever a continuous logit rule acts on a transformed one-dimensional objective.

Difficulty

The usual pooling comparison evaluates cost at an optimal order. Here each system draws its order from a different continuous probability law, and the cost to compare is averaged over those choices. Comparing $\sigma_T$ with $\sum_i\sigma_i$ alone does not compare the logit distributions; in particular, it gives equality under perfect positive correlation while the target is strict. A formal development must also show that the normalizing integrals and the resulting cost expectations are genuine finite integrals for every set of parameters covered by the theorem.

Formalization scope

The Lean model uses Mathlib's real Gaussian law with variance $\sigma^2$ and the published InventoryControl_newsboy.newsboyCost for equations (29) and (31). It records the choice density, CDF, expectation, canonical profit, and behavioral expected cost as separate definitions. The behavioral density uses $e^{-\gamma/\beta}$ on $\mathbb R$ ; the utility shift from profit is covered by Lemma 2. The theorem specifies normal marginals and a normal total with mean $\sum_i\mu_i$ and standard deviation $\sigma_T$ . Every jointly normal demand vector in the paper yields these laws, and the final comparison uses no further feature of its joint distribution.

The conditions $h>0$ , $b>0$ , and $\beta>0$ are standing readings needed for the continuous choice law on the unbounded domain. Proposition 7 additionally states $n\geq2$ and $\sigma_i>0$ : for one location the alleged strict comparison becomes equality, while zero variance makes the paper's continuous density on a point support undefined. Lemma 1 requires positive affine scale because a negative scale reverses CDF order, and its two invariance lemmas require a finite positive normalizer. Equation (66) is read with $\min(Z,z)$ , as dictated by the surrounding formulas; the printed display drops the word “min.” These corrections and the cost-based choice convention are recorded item by item in the moderation notes.

No optimizer is supplied as a free variable, and no zero normalizer is allowed to turn a logit expectation into a trivial zero. Useful solver contributions include proofs that the cost-based logit normalizer and expected cost are integrable, Gaussian change-of-variables lemmas, and the strict scale comparison. These analytic facts can serve other continuous-choice models.

Selected references

Xuanming Su, Bounded Rationality in Newsvendor Models, Manufacturing & Service Operations Management 10(4):566–589, 2008. DOI: 10.1287/msom.1070.0200.

9 thms3 active usersReviewed

Bandit Algorithms Stochastic Systems·Captain: mikedeng1

On the Gittins Index for Multiarmed Bandits 2: A Policy Falls Short of the Gittins Policy by at Most Its Expected Discounted Gap Between the Greatest Gittins Index and That of the Bandit It PlaysResearch Paper

Motivation

The multiarmed bandit problem asks how to allocate a single resource, one play at a time, among several alternative projects whose states evolve only when they are worked on. It models the scheduling of jobs on a single machine, the design of sequential clinical trials and many problems of research planning. Gittins and Jones showed that it is optimal to play, at each time, a project of greatest Gittins index, a number computed from that project alone (Gittins and Jones 1974; Gittins 1979).

In practice the Gittins index policy is often replaced by a heuristic: indices are computed approximately, or a policy is constrained by operational rules. A practitioner then needs to know how much value is lost. R. Weber's paper On the Gittins index for multiarmed bandits (Ann. Appl. Probab. 1992) gives a short proof of the index theorem through prevailing charges, and in its Section 5 derives from it two suboptimality bounds. This mission formalizes the second of them, Theorem 3, which bounds the loss of an arbitrary policy using Gittins indices only.

Timeline. Gittins and Jones (1974) and Gittins (1979) prove optimality of the index policy by an interchange argument; Whittle (1980) gives a proof by retirement options; Glazebrook (1982) bounds the suboptimality of policies in terms of Gittins indices, the bound Weber calls "usually weaker than (6)"; Glazebrook (1990) gives the prevailing-charge bound that is Weber's Theorem 2; Weber (1992) proves the index theorem by prevailing charges and states Theorems 2–4.

Setting

There are $k$ bandit processes. Bandit $i$ has a state $x_i(t)$ in a state space $S$ ; at each epoch $t = 0, 1, 2, \dots$ the gambler plays one bandit $j(t)$ , receives a reward with mean $r(x_{j(t)}(t))$ , the state of bandit $j(t)$ moves according to a Markov transition kernel $P$ , and the states of all other bandits are unchanged. Rewards are nonnegative and uniformly bounded, and $0 < \beta < 1$ is a discount factor. A policy $\pi$ chooses $j(t)$ , possibly at random, as a function of everything observed so far. Its value from the initial state vector $x$ is the expected total-discounted reward

V_\pi(x) = E_\pi\Big[\sum_{t=0}^\infty \beta^t r\big(x_{j(t)}(t)\big) \,\Big|\, x(0) = x\Big]. \tag{1}

The fair charge $\gamma(y)$ of a state $y$ is the largest ratio of expected discounted reward to expected discounted time that a stopping time $\tau \ge 1$ of a single bandit started at $y$ can achieve,

\gamma(y) = \sup_{\tau \ge 1} \frac{E\big[\sum_{t=0}^{\tau-1}\beta^t r(x(t)) \mid x(0)=y\big]}{E\big[\sum_{t=0}^{\tau-1}\beta^t \mid x(0)=y\big]},

and Weber's Gittins index is $G(y) = \gamma(y)/(1-\beta)$ . A Gittins index policy $\pi^*$ plays, at every epoch, a bandit with the greatest index, ties broken arbitrarily. Theorem 1 of the paper, already formalized on Prove2Me as BanditAlgorithm.gittins_index_theorem, states that every Gittins index policy maximizes $V_\pi(x)$ .

The model, the fair charge and the Gittins index policy are the published GittinsIndex definitions of Shuze Chen, and the history truncation used to write round expectations is from Harry_Xu's GittinsTerminalPotential.

Formalization targets

Goal: Theorem 3

For a Gittins index policy $\pi^*$ , every policy $\pi$ and every initial state vector $x$ ,

V_{\pi^*}(x) - V_\pi(x) \le E_\pi\left[\sum_{t=0}^\infty \beta^t\Big(\max_i G_i\big(x_i(t)\big) - G_{j(t)}\big(x_{j(t)}(t)\big)\Big) \,\middle|\, x(0)=x\right]. \tag{7}

The right-hand side is computed along the trajectory of $\pi$ alone: in each epoch it charges the gap between the greatest index and the index of the bandit $\pi$ actually plays.

Milestones

The proof compares, for each $t$ , two policies built from $\pi$ : $\pi^*(t)$ , identical to $\pi$ before time $t$ and a Gittins index policy from $t$ on, and $\pi(t)$ , identical to $\pi$ up to and including time $t$ , which then continues playing $j(t)$ until its fair charge drops below its value at time $t$ and is a Gittins index policy thereafter.

Switching to Gittins later never hurts. If $\sigma'$ is identical to $\sigma$ through time $t$ and a Gittins index policy from $t+1$ on, then $V_\sigma(x) \le V_{\sigma'}(x)$ ; in particular $V_{\pi(t)}(x) \le V_{\pi^*(t+1)}(x)$ .
Equation (8).

V_{\pi^*(t)}(x) - V_{\pi(t)}(x) \le \beta^t E_\pi\left[\frac{\max_i \gamma_i(x_i(t)) - \gamma_{j(t)}(x_{j(t)}(t))}{1-\beta} \,\middle|\, x(0)=x\right].

Significance

The result. Theorem 3 turns any per-epoch guarantee about the index of the bandit played into a guarantee on value. If a policy always plays a bandit whose Gittins index is within $\varepsilon$ of the greatest, it loses at most $\varepsilon/(1-\beta)$ ; this is the form in which index heuristics, approximate index computations and constrained index policies are analysed. The open Prove2Me goal AllocationIndices.eps_index_policy_near_optimal (Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices, Theorem 4.18, after Glazebrook 1982) is a bound of this kind for $\varepsilon$ -index policies and follows from (7); it is a separate item and is not part of this mission. Unlike Theorem 2 of the same paper, the bound (7) involves only Gittins indices, not prevailing charges or rewards.

Formalizing it. Theorem 3 is proved in the paper; no machine-checked proof exists. The mission produces a formal statement of the bound on top of the published Markov bandit model and Theorem 1, together with the two intermediate statements of Weber's proof, which have uses of their own: optimality of switching to the index policy after any finite prefix of play is the dynamic-programming form of the index theorem.

Difficulty

The informal proof is half a page, and its key sentence is that the difference of the charges paid by $\pi^*(t)$ and $\pi(t)$ at any later time is never more than the gap at time $t$ . Making it rigorous requires the value-to-go of a history-dependent randomized policy after a fixed time, the fact that both policies from time $t$ on are fair games in which expected discounted reward equals expected discounted charge, and a pathwise comparison of two interleavings of charge sequences. The naive reading, that $\pi(t)$ loses only the single epoch $t$ , is wrong: playing $j(t)$ at time $t$ commits the policy to a whole run of $j(t)$ , and the bound accounts for the entire run through the factor $1/(1-\beta)$ . Telescoping (8) over $t$ also needs $V_{\pi^*(t)}(x) \to V_\pi(x)$ as $t \to \infty$ , which rests on bounded rewards and $\beta < 1$ .

Formalization scope

The Lean development uses the published BanditAlgorithm model, in which all bandits share one state space $S$ (a standard Borel space), one kernel $P$ and one reward $r$ ; Weber's bandits with different state spaces are encoded by taking the disjoint union. Time is 0-indexed in both. The committed readings of the paper's phrases are:

" $\pi^*$ is the optimal (Gittins) policy" is any policy satisfying IsGittinsIndexPolicy; it is not assumed to be built from $\pi$ .
$R_j(x_j(t))$ is represented by its conditional mean $r(x_j(t))$ , and " $E_\pi[\sum_t \beta^t \cdots]$ " by the series of per-epoch expectations $\sum_t \beta^t E_\pi[\cdots]$ , the published value convention.
The index in (7) is $G = \gamma/(1-\beta)$ (weberIndex), and (8) is written with $\gamma$ (gittinsIndex) divided by $1-\beta$ , as on the page.
$\pi^*(t)$ and $\pi(t)$ are predicates on a policy (IsSwitchToGittinsAt, IsRunThenGittinsAt), and (8) is stated for every pair of policies satisfying them. "Identical to $\pi$ for times less than $t$ " is rounds $n < t$ ; "plays $j(t)$ at time $t$ " and "identical through time $t$ " are rounds $n \le t$ . "Drops below" is strict.
The standing assumptions of Section 1 (nonnegative, uniformly bounded rewards and $0<\beta<1$ ) are hypotheses of every theorem, as are measurability of $r$ and of $y \mapsto \gamma(y)$ , which the paper takes for granted.

Using the fair charge $\gamma$ in place of $G$ in (7) would make the bound false by the factor $1-\beta$ ; dropping the measurability of $\gamma$ would let the expectation degenerate to $0$ and make the bound claim that every policy is optimal. Neither is the statement posed here, and a constant-index or one-armed instance, where both sides vanish, only checks that the hypotheses are satisfiable.

Theorem 1 is referenced, not posed. Theorem 2 (the prevailing-charge bound) and Theorem 4 (submodularity of the optimal value in the set of bandits) are missions 1 and 3 of this series; this mission does not depend on them. Weber's definition of an index consistent policy (p. 1028) is not formalized here: the proof of (8) needs the fair-game property in the form of Remark 2 (continue while the fair charge exceeds the prevailing charge), which differs from the definition's "initial value" after an interruption. Contributions welcome: a measurable greatest-index selection, value-to-go decompositions for history-dependent policies, and the fair-game identity for index-consistent play are reusable beyond this mission.

Selected references

R. Weber, On the Gittins index for multiarmed bandits, The Annals of Applied Probability 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
K. D. Glazebrook, Procedures for the evaluation of strategies for resource allocation in a stochastic environment, Journal of Applied Probability 27, 215–220, 1990.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19, 716–722, 1982.
J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms3 active usersReviewed

Completed

Bandit Algorithms Dynamic Programming Probability·Captain: mikedeng1

A Short Proof of the Gittins Index Theorem: For Finite-State Semi-Markov Bandits, Every Priority Policy Ordering States by the Index Algorithm's Indices Is OptimalResearch Paper

Motivation

The multi-armed bandit problem with discounted rewards asks how to allocate effort among $n$ independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an $n$ -dimensional dynamic program into $n$ one-dimensional computations.

Several proofs followed, each with its own model and its own definition of the index:

Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
Weber (1992): the "prevailing charge" proof.
Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.

Setting

There are $n\ge1$ bandit processes. Bandit $i$ has a finite nonempty state space $\mathcal X_i$ , and $\mathcal X=\mathcal X_1\cup\cdots\cup\mathcal X_n$ is their disjoint union. When bandit $i$ at state $x\in\mathcal X_i$ is played, a random reward $R(x)$ is received, the bandit is busy for a random time $T(x)\ge0$ , and it then moves to a random state $Y(x)\in\mathcal X_i$ ; the other bandits do not move. The joint law of $(T(x),R(x),Y(x))$ depends only on $x$ , and different plays are independent.

A policy is a map $\pi:\mathcal X_1\times\cdots\times\mathcal X_n\to\{1,\dots,n\}$ : at time zero and at every play completion time it chooses the bandit to play from the current states. With $t_i$ the start time and $R_i$ the reward of the $i$ -th play and a discount rate $\beta>0$ , the expected discounted reward from the initial joint state $z$ is

J_\pi(z)=\mathbb E\Big[\sum_{i=1}^{\infty}R_i e^{-\beta t_i}\Big].

A policy is optimal if it maximizes $J_\pi(z)$ for every initial state $z$ . A priority rule is a policy for which some ordering of $\mathcal X$ makes it always play the bandit whose current state is ordered highest.

The reward rate of a state is

r(x)=\frac{\mathbb E[R(x)]}{\mathbb E\big[\int_0^{T(x)}e^{-\beta t}\,dt\big]}. \tag{2.1}

Reducing bandit $i^*$ by removing a state $s^*$ merges every play that ends in $s^*$ with the following run of plays at $s^*$ into one composite play, whose reward rate is $\hat r(x)$ of (2.3). The index algorithm repeatedly picks a state $s^*$ of maximal current rate, sets its index $\gamma(s^*)$ to that rate, and reduces its bandit by removing $s^*$ (or removes the bandit if $s^*$ was its last state).

Formalization targets

Goal: Theorem 2.2

Let $\gamma$ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies

\gamma(y)<\gamma(x)\ \Longrightarrow\ y \text{ is ordered below } x

is optimal. Ties in $\gamma$ may be ordered either way, and the run may break ties in its own choices arbitrarily.

Milestones, in the order the proof uses them

(2.2), the interchange inequality $\mathbb E\big[(1-e^{-\beta\tau})\int_0^{T(s^*)}r(s^*)e^{-\beta t}dt\big]\ge\mathbb E\big[(1-e^{-\beta T(s^*)})\int_0^{\tau}\bar r(t)e^{-\beta t}dt\big]$ when $\bar r\le r(s^*)$ .
Lemma 2.1: if $r(s^*)=\max_{x}r(x)$ , some optimal policy always plays bandit $i^*$ when it is at $s^*$ .
Reduction step: optimizing within the policies giving $s^*$ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
Theorem 2.1: some priority rule is optimal.
Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
Index monotonicity: along a run, $\gamma(s^*)\ge\gamma(q^*)$ for consecutive picks $s^*,q^*$ .
Picked-before characterization: $x$ can be picked before $y$ (in a run with the same indices) if and only if $\gamma(x)\ge\gamma(y)$ .

Significance

The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the $c\mu$ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.

The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.

Difficulty

Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.

Formalization scope

Bandits are indexed by Fin n ( $0,\dots,n-1$ ), with $n\ge1$ and each state type finite and nonempty. $\mathcal X$ is the sigma type Σ i, X i, disjoint by construction.
The law of $(T(x),R(x),Y(x))$ is a probability measure on $\mathbb R\times\mathbb R\times\mathcal X_i$ with $T\ge0$ almost surely and $R$ integrable. The model also assumes $\mathbb P(T(x)>0)>0$ , which the page leaves implicit: it makes the denominator of (2.1) nonzero.
$J_\pi$ is computed from the moments $\mathbb E[R(x)]$ and $D(x,y)=\mathbb E[e^{-\beta T(x)};Y(x)=y]$ : it is the limit of the expected discounted reward of the first $k$ plays, given by the first-step recursion. No path space is constructed. The row sums of $D$ are below $1$ , so the limit exists; it never mentions rates, indices or reductions.
Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of $\mathcal X$ is an injective ranking into $\mathbb N$ .
The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
The index is that of any run of the index algorithm, with arbitrary tie choices.

A formalization in which the value of a policy is defined through rates or indices, or in which $\gamma$ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.

Needed infrastructure: the convergence of the $k$ -play values and the first-step (Bellman) equation for $J_\pi$ ; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.

Selected references

J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
P. Whittle, Multi-armed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42 (1980), 143–149. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4) (1992), 1024–1033. https://doi.org/10.1214/aoap/1177005588

11 thms3 active usersReviewed

Dynamic Programming Probability·Captain: mikedeng1

Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes IV: Critical-Level Ordering at Nondecreasing Myopic Levels ȳₘ Is OptimalResearch Paper

Motivation

A firm with one product may face several customer classes in each selling interval. When stock is scarce, it must decide which outstanding demands to satisfy and how much inventory to carry into later intervals. When new stock can be bought at several dates, the rationing choice also changes the value of future purchasing opportunities. Topkis studied these linked decisions in a nonstationary model with class-dependent shortage penalties and a finite number of ordering periods. His Theorem 4 identifies conditions under which a policy computed from each period's myopic cost is optimal in the full multiperiod problem Topkis 1968.

The result belongs to a line of work on critical-level policies: choose a stock target and order up to it if current stock is lower. Here the target can be computed one period at a time despite the possibility of future purchases and the separate question of how to ration stock among demand classes. The paper attributes a related myopic policy result to Veinott and explains that its own setting allows a more general rationing policy than the special zero-rationing-level case discussed there Topkis 1968, pp. 175–176. This mission formalizes Topkis's multiperiod statement, including its ordering and rationing conclusions.

Setting

There are $N$ ordering periods, numbered $1$ through $N$ . Period $m$ has a unit purchase cost $c_m$ . It contains $k_m$ selling intervals, numbered backward: interval $k_m$ is first and interval $1$ is last. Within an interval, a random nonnegative demand vector has one component for each of $n$ customer classes. The vectors in distinct intervals and periods are independent and each class has a finite mean. At the start of an interval the demand is observed. A decision then selects how much of each class's outstanding demand to leave unsatisfied. The remaining physical stock incurs a holding cost, and each unsatisfied unit incurs a class-specific penalty. Unsatisfied demand is either carried entirely to the next interval or lost entirely, according to the interval. Penalties are nonnegative and rise with class index, so class $n$ has the highest shortage penalty Topkis 1968, pp. 162–163, 174.

Let $w$ be net stock before ordering at the start of period $m$ : physical stock minus outstanding backlogs. The order must clear the backlog, so the post-order stock $z$ satisfies $z\ge w^+=\max(w,0)$ . After period $N$ , a further unit can be purchased for $c_{N+1}\ge0$ , while unused stock can be salvaged for revenue $v\le c_{N+1}$ . The terminal cost is $C_{N+1}(w)=(c_{N+1}-v)w^+$ . Working backward, $C_m(w)$ is the optimal continuation cost, including the period- $m$ ordering decision. The actual period cost $\widetilde g^m(z)$ includes the later continuation value $C_{m+1}$ , and equation (19) reads

C_m(w)=\inf_{z\ge w^+}\widetilde g^m(z).

The single-period cost $g^m(z)$ uses the same demand, holding costs and rationing choices in period $m$ , but replaces the later continuation value by the linear terminal charge $-c_{m+1}y$ . A myopic level $\bar y_m$ is any minimum of $g^m$ on $[0,\infty)$ ; it is $+\infty$ if no such minimum exists. Thus the level need not be the smallest minimum when several stock levels tie Topkis 1968, pp. 174–175.

Formalization targets

Theorem 4: myopic ordering and rationing

Suppose $v=c_{N+1}$ and the selected myopic levels are nondecreasing from period $m$ onward:

\bar y_m\le\bar y_{m+1}\le\cdots\le\bar y_N.

Then $\bar y_m<+\infty$ , and ordering to $w\vee\bar y_m$ minimizes $\widetilde g^m$ over all feasible post-order levels $z\ge w^+$ . If $m<N$ and the stock at the start of period $m$ is at most $\bar y_{m+1}$ , the optimal rationing policy during that period is the optimal policy for its single-period problem, calculated with terminal costs $v_1\equiv0$ and $v_2(y)=-c_{m+1}y$ Topkis 1968, Theorem 4.

The milestones are the paper's regularity claim for $C_m$ and $\widetilde g^m$ , existence of an actual optimal order-up-to level, finiteness of $\bar y_N$ , the shape of $C_m$ around an optimal level, and the comparison in equation (20). Together these specify the route from the general dynamic program to the myopic target.

Significance

Theorem 4 gives a checkable sufficient condition for replacing a multiperiod ordering computation with a sequence of single-period cost minimizations. It also identifies when the rationing decisions can be obtained from the same single-period model. The stock bound in its rationing clause matters: outside that range, future costs may alter which class demands should be filled now. The result therefore describes both the simplification and its operational domain Topkis 1968, pp. 175–176.

Topkis proved the theorem in 1968; the task here is to produce machine-checked definitions and proofs of that known result. The definitions of feasible rationing, backward value functions, myopic costs and order-up-to levels will also support comparisons with other finite-horizon inventory models. The §1 model is duplicated locally while the four missions for this paper are drafted in parallel, then intended for consolidation into a shared interface.

Difficulty

Convexity alone gives an order-up-to form for the actual cost $\widetilde g^m$ , but it does not identify its minimizing level with a minimum of the simpler cost $g^m$ . The continuation value $C_{m+1}$ depends on all later ordering and rationing decisions. When some unsatisfied demand is lost, the end-of-period net stock can depend on the within-period rationing choice as well. The core issue is therefore to control the difference between the actual and myopic objectives in the stock range relevant to period $m$ Topkis 1968, pp. 174–176. A statement restricted to a preselected rationing rule would miss the theorem's claim about optimality among all feasible decisions.

Formalization scope

Classes are indexed by Fin n; the largest index is the highest penalty class. Intervals and ordering periods use natural numbers with explicit bounds, and intervals retain the paper's backward numbering. Stock, penalties and costs are real. A period's demand vector has a probability law on real vectors supported on the nonnegative orthant, with every coordinate integrable. The §1 dynamic program uses real infima for feasible rationing choices and Bochner integrals for demand expectations. The multiperiod value $C_m$ uses the nonnegative post-order domain $z\ge w^+$ in (19). Its defining infimum is intended to be finite under the paper's assumptions; the regularity and attainment milestones expose the facts that rule out Lean's default value for an unbounded infimum. These functions are used only at $1\le m\le N+1$ , with period costs at $1\le m\le N$ .

The multiperiod standing assumptions require $n>0$ , $N>0$ , and at least one interval per period, matching the paper’s positive counts.

Holding costs and the appropriate terminal costs satisfy the convexity and continuity assumptions of §1. Within each period, backlog multipliers equal $0$ or $1$ . The terminal procurement cost is nonnegative and salvage revenue does not exceed it. Assumption (D′) is encoded as an eventually positive lower bound on the extended-real right derivative of $c_mw+\sum_{i=m}^N\sum_t h_{t,i}(w)-vw$ . The §1 terminal functions used in the period assumptions are the linear functions required by the single-period comparison; their regularity adds no independent restriction. Independence across intervals and periods is built into successive expectations. The goal separately assumes $v=c_{N+1}$ and monotonicity of the selected myopic levels only from $m$ through $N$ .

The formal target compares the actual and single-period sets of optimal rationing decisions at every interval and at every nonnegative state with stock at most $\bar y_{m+1}$ . The stock bound and the full feasible set prevent the claim from becoming a result about a handpicked policy. Contributions to the backward recursion, convexity and attainment facts, and the comparison of these two decision sets are all part of this mission.

Selected references

Donald M. Topkis, Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes, Management Science 15(3), 160–176, 1968. DOI: 10.1287/mnsc.15.3.160.

9 thms3 active usersReviewed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XI: The Random Assignment Problem — Fluctuations of the Optimal Cost of Order (log N)²/(√N log log N)Textbook

Motivation

The assignment problem asks for a one-to-one matching of $N$ agents to $N$ tasks that minimizes the total cost. It is one of the basic problems of combinatorial optimization and is solved in polynomial time by the Hungarian method. Its random version, in which the $N^2$ costs are independent random variables, is a standard model for the typical behavior of optimization problems on random inputs, and it has been studied in probability, operations research and statistical physics.

Timeline:

Walkup (1979) showed that the expected optimal cost $E(L_N)$ of the random assignment problem with independent uniform $[0,1]$ costs stays bounded as $N \to \infty$ (doi:10.1137/0208036).
Karp (1987) proved $E(L_N) \le 2$ .
Talagrand (1995), in the article this mission formalizes, bounded the fluctuations of $L_N$ around its median by $K(\log N)^2/(\sqrt N \log\log N)$ , as a showcase of his concentration inequality for product measures (doi:10.1007/BF02699376).
Aldous (2001) proved the limit $E(L_N) \to \pi^2/6$ , the value predicted by Mézard and Parisi (doi:10.1002/rsa.1015).

This mission is Chapter 10 of Talagrand's article.

Setting

Fix $N$ and two sets $I$ and $J$ of cardinal $N$ . An assignment is a one-to-one map $\tau$ from $I$ onto $J$ . Given a cost matrix $a = (a_{i,j})_{i \in I, j \in J}$ , the cost of $\tau$ is $\sum_{i \in I} a_{i,\tau(i)}$ . In the random problem the costs are $X_{i,j}$ , independent and uniformly distributed on $[0,1]$ , and the optimal cost is the random variable

L_N = \min\Big\{ \sum_{i \in I} X_{i,\tau(i)} \;;\; \tau \text{ assignment} \Big\}.

A median of $L_N$ is any real $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$ .

The argument uses digraphs. A digraph is a subset $D \subseteq I \times J$ , and for $S \subseteq I$ the set of neighbors is $D(S) = \{ j \in J ;\ \exists i \in S,\ (i,j) \in D \}$ . For $\alpha \ge 2$ , $D$ is $\alpha$ -expanding if for every $S \subseteq I$

\operatorname{card} S \le \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge \min\big(\alpha \operatorname{card} S, \tfrac N2\big), \qquad \operatorname{card} S \ge \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge N - \tfrac 1\alpha (N - \operatorname{card} S).

For $u > 0$ the threshold digraph is $D_u = \{(i,j) ;\ X_{i,j} \le 2uN^{-1}\log N\}$ : it keeps only the cheap edges.

Formalization targets

Goal: Theorem 10.5

There is a universal constant $K$ such that for $N \ge 3$ , every median $M$ of $L_N$ and every $t \ge 0$ ,

t \le \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t (\log N)^2}{\sqrt N \log\log N}\Big) \le 2 e^{-t^2},

t \ge \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t^3 \log N}{\sqrt N \log t^2}\Big) \le 2 e^{-t^2}.

The constant $K$ is left unspecified, as in the paper.

Milestones, in attack order

Lemma 10.1 (deterministic): in an $\alpha$ -expanding digraph with $\alpha^m \ge N/2$ , every $i \in I$ lies on a cycle $i = i_1, \dots, i_{n+1} = i$ of distinct points, $n \le 2m$ , with $(i_\ell, \tau(i_{\ell+1})) \in D$ .
Corollary 10.2 (deterministic in the costs): if $D_u$ is $\alpha$ -expanding and $\alpha^m \ge N/2$ , every optimal assignment satisfies $X_{i,\tau(i)} \le 4muN^{-1}\log N$ .
Lemma 10.4: for independent events of probability $p$ , fewer than $\delta p N$ occur with probability at most $\exp(-Np/K(\delta))$ .
Proposition 10.3: for a universal $K$ and $u > K$ with $u \log N \le N$ , $D_u$ is $u\log N$ -expanding with probability at least $1 - N^{-u/K}$ .

Significance

The expected value of $L_N$ is of the same order as a single cost, yet $L_N$ is a function of $N^2$ independent variables. A generic bounded-difference bound in all $N^2$ coordinates gives no useful concentration at this scale. Theorem 10.5 shows that the fluctuations are at most of order $(\log N)^2/(\sqrt N \log\log N)$ , and by the remark after the theorem, so is the standard deviation of $L_N$ . The chapter is a worked example of how a concentration inequality in product spaces is combined with a combinatorial localization argument, the reduction to small costs, and that pattern recurs in the study of random combinatorial optimization problems.

Status: the theorem and its lemmas are proved in the paper. As far as a search of the platform shows, none of them has a machine-checked proof. The two posed statements of Theorem 4.1.1 on the platform (finite-alphabet form) are the concentration inequality the proof calls on; formalizing this chapter adds the combinatorics of expanding digraphs, the random-graph estimate Proposition 10.3 and the final assembly.

Difficulty

The naive approach applies a concentration inequality directly to $L_N$ as a function of the $N^2$ costs, each of which can change $L_N$ by up to $1$ . That loses all control, because the variance proxy grows with the number of coordinates. The central step is to show that, with high probability, an optimal assignment only uses costs of order $N^{-1}(\log N)^2$ . This requires the cycle structure of Lemma 10.1, and it requires showing that the sparse random digraph $D_u$ has expansion uniformly over all subsets $S$ of $I$ , whose number is exponential in $N$ . Proposition 10.3 has to beat that union bound, and its proof covers only one of the two expansion conditions in detail; the condition (10.2) for large sets is "left to the reader". The final step combines the truncation with Theorem 4.1.1 and a careful choice of parameters for the two ranges of $t$ .

Formalization scope

The Lean development lives in the namespace TalagrandConc.Assignment and commits to the following conventions:

$I = J =$ Fin N, assignments are Equiv.Perm (Fin N), and $L_N$ is optCost, a Finset.inf' over all permutations (no junk value).
The probability space is the cost matrices Fin N × Fin N → ℝ with costLaw N, the product of Lebesgue measure restricted to $[0,1]$ . The coordinates are the $X_{i,j}$ .
Cardinalities of subsets are Set.ncard on the finite type Fin N. $\alpha$ -expansion includes $\alpha \ge 2$ as part of the definition.
Probabilities are in ℝ≥0∞, and $1 - N^{-u/K}$ is truncated subtraction there.
Universal constants are existentially quantified before every object they are uniform over. $K(\delta)$ in Lemma 10.4 is chosen after $\delta$ and before everything else.
Implicit side conditions of the paper are stated: $m \ge 1$ in Lemma 10.1 and Corollary 10.2, $n \ge 1$ for the cycle, $N \ge 1$ in Proposition 10.3, $t \ge 0$ in Theorem 10.5.

A cycle of length $n = 0$ would satisfy Lemma 10.1 vacuously. The formal statement therefore requires $n \ge 1$ , which rules out that trivializing reading. Similarly, Theorem 10.5 fixes one constant $K$ for all $N$ ; a $K$ depending on $N$ would make the bound empty.

Infrastructure: the product of uniform laws on a finite index set, iterated expansion arguments for bipartite digraphs, a lower-tail Chernoff bound for independent events, and the union bound over subsets are reusable beyond this mission. Theorem 4.1.1 of the paper is posed elsewhere on the platform and is not restated here. The bound (8.1.1) used in Step 2 of the proof belongs to another chapter of the series. Contributions of proofs of any milestone, or of intermediate displayed estimates such as (10.5), (10.6) and (10.9), are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. doi:10.1007/BF02699376
D. W. Walkup, On the expected value of a random assignment problem, SIAM J. Comput. 8 (1979), 440–442. doi:10.1137/0208036
R. M. Karp, An upper bound on the expected cost of an optimal assignment, in Discrete Algorithms and Complexity, Academic Press (1987), 1–4.
J. M. Steele, Probability Theory and Combinatorial Optimization, SIAM (1997). doi:10.1137/1.9781611970029
D. J. Aldous, The ζ(2) limit in the random assignment problem, Random Structures Algorithms 18 (2001), 381–418. doi:10.1002/rsa.1015

7 thms3 active usersReviewed

Completed

Complexity Theory Linear Optimization Optimization·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 2: The Adaptive-Step Algorithm in N∞(β) or N∞⁻(β) with γ ≤ 2(1 − β) Attains Precision t in O(nt) IterationsResearch Paper

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$ . Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$ , $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$ , $m\ge0$ , $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider

\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$ , $s>0$ , $Ax=b$ , and $A^Ty+s=c$ for some $y$ . For such a pair the duality gap is $x^Ts$ , and the duality measure is $\mu=x^Ts/n$ . Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$ .

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$ , $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$ . For $\beta\in(0,1)$ the wide neighbourhoods are

\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$ .

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$ ,

Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}

and the step is $x(\theta)=x+\theta d_x$ , $s(\theta)=s+\theta d_s$ . The scaled quantities $p=X^{-1/2}S^{1/2}d_x$ , $q=X^{1/2}S^{-1/2}d_s$ , $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$ . The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$ .

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$ . While $(x^k)^Ts^k>2^{-t}$ , it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$ , and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$ .

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$ , and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$ . Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .

The paper states " $O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$ .
Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$ , $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$ , $\|Pq\|_\infty\le\|r\|^2/4$ .
Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$ ; in $\mathcal N_\infty(\beta)$ , $\|r\|_\infty^2\le(1+\beta)\mu$ .
Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$ , and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$ .
Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$ ).
(15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$ .

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$ , $\mathcal N_\infty^-$ , of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$ , which comes from $Ad_x=0$ and $d_s=-A^Td_y$ . Those relations hold only for a solution of the full system (2), not for the first equation alone.
Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
"The largest $\bar\theta$ " is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$ , but the formal run must say what $\bar\theta$ is.
Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$ , real powers of $2$ , and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$ , and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$ .

Committed conventions and repairs:

The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
"The largest $\bar\theta$ " is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$ . When no maximum exists (always the case for $n=1$ , where $Pq=0$ ), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$ .
A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$ . Its behaviour after the stopping test is unconstrained.
In $\theta_2$ and $\theta_2^-$ , a zero norm makes the quotient $+\infty$ and the minimum $1$ . Since Lean's real division by zero is $0$ , this case is defined explicitly.
The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$ . At $n=1$ it can fail (e.g. $\beta=1/2$ , $\gamma=0.9$ ), and Algorithm 2 makes no iterations there.
The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

11 thms3 active usersReviewed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs: A Variable-Rate Queue Has an Average Cost Optimal Stationary Policy Whenever λ < max aβResearch Paper

Motivation

Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).

Timeline:

1962–1970. Derman and Ross obtain average cost optimal stationary policies from the vanishing discount approach when the relative values $h_\alpha$ are bounded.
1986. Sennott treats the queue with variable service rates under bounded costs and gives a first discrete-time Tauberian argument (Operations Research 34, 1986a; 1986b).
1989. This paper: Assumptions 1–3, the Theorem, the Markov chain test of Propositions 4–5, and applications to a packet system and to the queue with variable service rates (Proposition 8).

Setting

A Markov decision chain has states $i=0,1,2,\dots$ ; in state $i$ a finite nonempty set $A_i$ of actions; a cost $0\le C(i,a)<\infty$ ; and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may depend on the whole history and may randomize; a stationary policy $f$ chooses $f(i)\in A_i$ in state $i$ . For $0<\alpha<1$ , $V_{\theta,\alpha}(i)$ is the expected total $\alpha$ -discounted cost from $i$ and $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , possibly infinite. The average cost of $\theta$ is

g_\theta(i)=\limsup_{N\to\infty}\frac1N\,E_\theta\Big[\sum_{t=0}^{N-1}C(X_t,a_t)\,\Big|\,X_0=i\Big].

A stationary policy $f$ is average cost optimal if there is a finite constant $g$ with $g=g_f(i)\le g_\theta(i)$ for every policy $\theta$ and every state $i$ .

The queue with variable service rates (Example 2). Time is slotted; $p_i$ is the probability of $i$ arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables $a$ and serves at rate $a\beta\in(0,1)$ , so that the customer in service leaves during the slot with probability $a\beta$ ; there is no decision in state $0$ . From state $i\ge1$ the next state is $i-1+k$ with probability $a\beta p_k+(1-a\beta)p_{k-1}$ ( $p_{-1}=0$ ), and from $0$ it is $j$ with probability $p_j$ . The cost structure: $B(a)>0$ ; $Q$ a polynomial of degree $n\ge0$ , nonnegative and increasing on $i\ge0$ ; $C(0)=Q(0)$ and $C(i,a)=Q(i)+B(a)$ for $i\ge1$ . The arrival moments are $\lambda^{(k)}=\sum_i i^kp_i$ and $\lambda=\lambda^{(1)}$ .

Formalization targets

Goal: Proposition 8

If $\lambda^{(n+1)}<\infty$ , then

\lambda<\max_a(a\beta)\ \Longrightarrow\ \text{there is an average cost optimal stationary policy},

and

\lambda<\min_a(a\beta)\ \Longrightarrow\ g+h(i)=\min_a\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\quad i\ge0,

with $g$ the optimal average cost, $g=\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)$ , and $h$ bounded below.

Milestones

Propositions 1–3 (p. 627): $V_\alpha$ solves the discount optimality equation, is its minimal nonnegative solution, and is the limit of value iteration (already proved on the platform, referenced).
The Lemma (p. 628): discount optimal stationary policies along $\alpha_n\to1$ have a stationary limit point.
Lemmas A1 and A2 (p. 632): the comparison between solutions of the optimality inequality and average costs, and $\limsup_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)\le g_\theta(i)$ .
The Theorem (p. 628): under Assumptions 1–3, any limit point $f$ from the Lemma is average cost optimal, with the optimality inequalities (5); under Assumption 3*, the optimality equation (6).
Propositions 4, 5 and the Corollary (pp. 629–630): the Markov chain criteria that yield Assumptions 1, 3 and 3* from one well-behaved stationary policy.
Two steps of the proof of Proposition 8 (p. 631): $V_\alpha(i)$ is increasing in $i$ (hence Assumption 2), and the drift of $r(i)=Ai^{n+1}$ is a polynomial of degree at most $n$ with leading coefficient $A(n+1)(\lambda-a\beta)$ , display (14).

Significance

Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.

All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.

Difficulty

The obvious route takes a limit of $h_\alpha=V_\alpha-V_\alpha(0)$ along a sequence $\alpha_n\to1$ and passes to the limit in the discount optimality equation. With unbounded costs and unbounded $h_\alpha$ the sum $\sum_jP_{ij}(a)h_\alpha(j)$ is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of $V_\alpha$ and a Lyapunov drift computation whose leading term, $A(n+1)(\lambda-a\beta)i^n$ , has to dominate a cost polynomial of the same degree.

Formalization scope

The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:

costs, discounted values and average costs lie in $[0,\infty]$ ; $V_\alpha$ may be infinite unless Assumption 1 is assumed;
$h_\alpha$ is a real number, used only together with Assumption 1;
the constants $N$ and $M_i$ of Assumptions 2–3 are explicit and chosen before $i$ and $\alpha$ ; Assumption 3* uses the same $M$ ;
"average cost optimal" always carries a finite constant $g\ge0$ and compares with all policies, not only stationary ones;
sums $\sum_jP_{ij}(a)h(j)$ against a real function are extended reals (positive part minus negative part);
"ergodic" means positive recurrent (no aperiodicity);
in the queue, every decision is formally available in state $0$ with identical cost $Q(0)$ and identical transitions, which represents "no decision in state 0"; $\lambda<\max_a(a\beta)$ is "for some $a$ " and $\lambda<\min_a(a\beta)$ "for every $a$ ".

The second half of the goal is not "there exist $g$ and $h$ satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties $g$ to the optimal average cost and $\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha$ and requires $h$ bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals $p_0=3/4$ , $p_1=1/4$ , one rate $a\beta=1/2$ , $Q(i)=i+1$ , $B=1$ ), so the goal is not vacuous.

A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on $\prod_iA_i$ , first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

L. I. Sennott, Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs, Operations Research 37(4):626–633, 1989. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970.
A. G. Pakes, Some Conditions for Ergodicity and Recurrence of Markov Chains, Operations Research 17(6):1058–1061, 1969. https://doi.org/10.1287/opre.17.6.1058
A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey, SIAM J. Control Optim. 31(2):282–344, 1993. https://doi.org/10.1137/0331018

22 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Numerical Analysis+1·Captain: mikedeng1

Régularisation d'inéquations variationnelles par approximations successives II: The Proximal Regularization of a Convex Minimization Problem Is a Minimizing SequenceResearch Paper

Motivation

The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point $x^n$ it solves the original problem with a quadratic penalty $\|x-x^n\|^2$ added, and takes the solution as $x^{n+1}$ . The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).

The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.

Timeline.

1970, Martinet: the regularization (13) for convex minimization over a closed convex set in a Hilbert space; Théorème 3 (weak cluster points are minimizers, the sequence is minimizing), stated without proof.
1976, Rockafellar (SIAM J. Control Optim. 14): the proximal point algorithm for maximal monotone operators, with inexact steps and weak convergence of the whole sequence when a zero exists.
1991, Güler (SIAM J. Control Optim. 29): the rate $f(x^n)-\inf f = O(1/n)$ for convex minimization, and an example in which the iterates converge weakly but not strongly.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $C\subseteq H$ be a nonempty, closed, convex set, and let $f:H\to\mathbb R$ be a convex, lower semicontinuous function such that, for every $a\in\mathbb R$ , the sublevel set $\{x\in C \mid f(x)\le a\}$ is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is

(12)\qquad \min\,\{\,f(x)\mid x\in C\,\},

and its solution set (solSet f C) is the set of $\bar x\in C$ with $f(\bar x)\le f(x)$ for all $x\in C$ .

The regularization algorithm (13) starts from $x^0\in C$ and, given $x^n$ , takes

(13)\qquad x^{n+1}\in C\ \text{ the minimizer of } \ f(x)+\|x-x^n\|^2\ \text{ over } x\in C .

Lean encodes one step as IsProxStep f C xn y ( $y\in C$ and $f(y)+\|y-x^n\|^2\le f(x)+\|x-x^n\|^2$ for all $x\in C$ ) and a run as IsProxSeq f C x.

A point $\tilde x$ is a weak cluster point of $(x^n)$ (IsWeakClusterPt) if every neighbourhood of $\tilde x$ in the weak topology of $H$ contains $x^n$ for infinitely many $n$ . A sequence is minimizing if $f(x^n)\to\inf_{x\in C} f(x)$ .

Formalization targets

Existence for (12) and well-posedness of (13)

\exists\,\bar x\in C\ \ \forall x\in C:\ f(\bar x)\le f(x), \qquad \forall x^n\in C\ \ \exists!\,y\in C:\ y \text{ minimizes } f(x)+\|x-x^n\|^2 \text{ over } C .

These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").

Goal: Théorème 3

For every sequence generated by (13),

\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in \operatorname{sol}(12), \qquad \lim_{n\to\infty} f(x^n)=\inf_{x\in C} f(x)\in\mathbb R .

The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.

Stronger: Remarque 1

If in addition $f$ is uniformly convex, i.e. $f(ax+by)\le af(x)+bf(y)-ab\,\varphi(\|x-y\|)$ for $a,b\ge0$ , $a+b=1$ , with $\varphi(t)>0$ for $t>0$ , then (12) has a unique solution $\bar x$ and $\|x^n-\bar x\|\to0$ .

Significance

The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of $f$ , and no bound on $f$ beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.

Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.

Difficulty

Each iterate $x^{n+1}$ is defined only implicitly, as the minimizer of a problem that changes with $n$ . Monotonicity of $f(x^n)$ follows at once from comparing $x^{n+1}$ with $x^n$ . Monotonicity alone gives convergence of $f(x^n)$ to some limit, but not to $\inf_C f$ . Closing that gap needs information about the minimizers of (12) and their distance to the iterates.

The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: $f$ is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from $C$ , which may be unbounded.

Formalization scope

All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:

$H$ is a real complete inner product space (InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.
$C\neq\emptyset$ is a standing hypothesis. The paper leaves it implicit, but its existence claim for (12) is false for $C=\emptyset$ .
$f$ is real-valued, convex and lower semicontinuous on all of $H$ , as printed. The constraint $x\in C$ stays explicit in (12) and (13). It is not absorbed into an extended-valued indicator.
The penalty in (13) has weight $1$ , as printed, not $\tfrac12$ .
The algorithm is a relation on sequences: IsProxSeq accepts any sequence with $x^0\in C$ satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.
"Minimisante" is stated as: some real $m$ is the greatest lower bound of $f(C)$ and $f(x^n)\to m$ . This avoids the junk value sInf takes on sets unbounded below. As a side effect, the theorem asserts that $f$ is bounded below on $C$ .
Weak cluster points are cluster points in WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.
Remarque 1 uses Mathlib's UniformConvexOn Set.univ φ f with $\varphi(t)>0$ for $t>0$ . It keeps every hypothesis of §4.1.

The goal does not assume that (12) has a solution, that $f$ is bounded below on $C$ , or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.

Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system $(A^*A+2I)x^{n+1}=A^*b+2x^n$ corresponds to $f=\tfrac12\|Ax-b\|^2$ . For the printed $f=\|Ax-b\|^2$ , (13) gives $(A^*A+I)x^{n+1}=A^*b+x^n$ . The variational inequality case (§II) is the companion mission I of this series.

Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for $x\mapsto f(x)+\|x-x^n\|^2$ , are welcome.

Selected references

B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3), 154–158, 1970. https://doi.org/10.1051/m2an/197004R301541
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2), 403–419, 1991. https://doi.org/10.1137/0329022
J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 293–318, 1992. https://doi.org/10.1007/BF01581204
J. L. Lions and G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20, 493–519, 1967. https://doi.org/10.1002/cpa.3160200302

6 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Quality Control under Markovian Deterioration 3: Sufficient Conditions for a Three-Region Optimal Policy and for an Optimal Policy That Never InspectsResearch Paper

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$ . The discount factor is $\beta\in(0,1)$ . Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$ . Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$ . The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$ . Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$ . The three current-plus-continuation costs are

\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$ . A stationary rule is $\beta$ -optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$ . If

\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$ , inspects for $P_1\le P<P_2$ , and revises for $P\ge P_2$ . The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$ . If revision is optimal somewhere, the conclusion includes $P_2\le1$ . This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$ . Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$ . It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$ , exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$ . The last quotient in Corollary 3.6 divides by $\pi$ , so that second inequality is stated under $\pi>0$ ; the first inequality, and the main theorem, cover $\pi=0$ . If $\pi=1$ , then $\Delta=0$ . Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

8 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Quality Control under Markovian Deterioration 2: Never Inspecting or Revising Is Optimal Exactly When R ≥ C/(1 − β(1 − π))Research Paper

Motivation

A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.

The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.

Setting

There are two underlying states: good and bad. The current state is hidden, and $P\in[0,1]$ is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and $C$ in the bad state, so its expected immediate cost is $CP$ . A good process becomes bad with probability $\pi$ in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to $T(P)=P+\pi-\pi P$ . These are the conventions of the paper's Section 3 Ross 1971, p. 590.

The other actions are inspection, at cost $I$ , and revision, at cost $R$ . Inspection reveals the current state: the next belief is $1$ when the state was bad and $\pi$ when it was good. Revision returns the process to the good state before its next transition, so the next belief is $\pi$ . The standing parameter conditions are $0<\beta<1$ , $0\le\pi\le1$ , and $0<C<I<R$ ; $\beta$ is the discount factor. The paper explicitly assumes $C<I<R$ and a discount factor in $(0,1)$ . Positive $C$ states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.

For a future-cost function $W$ , the three Bellman alternatives at belief $P$ are $CP+\beta W(TP)$ , $I+\beta P W(1)+\beta(1-P)W(\pi)$ , and $R+\beta W(\pi)$ . Their minimum defines one step of finite-horizon value iteration, beginning with $V^0=0$ . The limit $V_\beta(P)$ is the optimal discounted cost. Write $R^0$ for the rule that always produces without inspection, and define its cost from the actual discounted series $\psi(P)=\sum_{n=0}^{\infty}\beta^n C T^nP$ Ross 1971, equations (3)–(5).

Formalization targets

The first target establishes that value iteration converges on $[0,1]$ , gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of $R^0$ :

T^nP=1-(1-P)(1-\pi)^n,\qquad \psi(P)=\frac{C}{1-\beta}-\frac{C(1-P)}{1-\beta(1-\pi)}.

The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for $P_1,P_2\in[0,1]$ ,

|V_\beta(P_1)-V_\beta(P_2)|\le \frac{C|P_1-P_2|}{1-\beta(1-\pi)}.

The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold

R\ge\frac{C}{1-\beta(1-\pi)}.

Below that threshold, revision is the unique minimizing action for beliefs sufficiently near $1$ from the left Ross 1971, pp. 591–592.

Significance

The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.

Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.

Difficulty

The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near $P=1$ requires control of the value as the belief varies; pointwise action comparison at $P=1$ does not itself establish an interval Ross 1971, pp. 591–592.

Formalization scope

The Lean model uses real parameters and a real belief restricted to $[0,1]$ . It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from $V^0=0$ , so $V^1=\min\{CP,I,R\}$ matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.

The discounted-optimality claim for $R^0$ means $\psi(P)=V_\beta(P)$ for every $P\in[0,1]$ . The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near $1$ ” means a one-sided neighborhood within $[0,1]$ . The second inequality in Corollary 3.6 is stated only when $\pi>0$ , because division by $\pi=0$ has a default value in Lean. The first inequality and Theorem 3.4 retain the $\pi=0$ case.

The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of $R^0$ are computed from the model data.

Selected references

Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587.

8 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 2: Enumerating Long Assignments and Rounding the LP Gives a (1 + ε)-Approximation for MakespanResearch Paper

Motivation

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines $m$ is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy $1+\varepsilon$ .

Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed $m$ , but its space requirement grows like $(nm/\varepsilon)^m$ . The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in $m$ , and in $\log(1/\varepsilon)$ . This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).

Timeline:

1976. Horowitz and Sahni, a fully polynomial approximation scheme for a fixed number of unrelated machines, with exponential space in $m$ .
1985. Potts, a 2-approximation for unrelated machines whose running time is $m^{m-1}$ times a polynomial, based on LP rounding with enumeration.
1987. Lenstra, Shmoys and Tardos, the Rounding Theorem, a polynomial 2-approximation for arbitrary $m$ , and, for fixed $m$ , the scheme formalized here (FOCS 1987; journal version in Mathematical Programming 46, 1990).

Setting

There are $m$ machines and $n$ jobs. If job $j$ is scheduled on machine $i$ it takes $p_{ij}$ time units, a positive integer; $P=(p_{ij})$ is the processing-time matrix. A schedule $\sigma$ assigns every job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$ , the makespan is the largest load, and $\mathrm{OPT}$ is the smallest makespan over all schedules.

Fix an integer deadline $d\ge0$ and an accuracy $\varepsilon>0$ . Assigning job $j$ to machine $i$ is long if $p_{ij}>\varepsilon d$ and short otherwise. A schedule of long assignments $L$ is a partial assignment of jobs to machines using only long assignments; its long load on machine $i$ is $t_i$ , and $L$ is admissible if $t_i\le d$ for every $i$ .

For a threshold $t$ and deadlines $d_1,\dots,d_m$ , the linear program (LP) of the Rounding Theorem has a variable $x_{ij}\ge0$ for every pair with $p_{ij}\le t$ , the constraints $\sum_i x_{ij}=1$ for each job, and $\sum_j p_{ij}x_{ij}\le d_i$ for each machine. The residual LP of $(d,L)$ is (LP) for the jobs left unassigned by $L$ , with $d_i=d-t_i$ and $t=\varepsilon d$ .

The procedure $A_\varepsilon$ , on input $d$ , tries every admissible $L$ ; if the residual LP is feasible it takes a vertex $\tilde x$ , rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with $L$ . It answers 'no' if no residual LP is feasible. A $\rho$ -relaxed decision procedure answers 'no' only when no schedule has makespan at most $d$ , and otherwise returns a schedule of makespan at most $\rho d$ . The binary search of Lemma 1 runs such a procedure on deadlines between $\lceil t/m\rceil$ and $t$ , where $t$ is the makespan of the greedy schedule, and returns the best schedule found.

Formalization targets

Goal: Theorem 3

For every $m\ge1$ , every positive integer matrix $P$ , every $\varepsilon>0$ , every LP solver $V$ , the procedure $A_\varepsilon$ run with $V$ exists, and the binary search driven by any such procedure returns a schedule $\sigma$ with

\mathrm{makespan}(\sigma)\le(1+\varepsilon)\,\mathrm{OPT}.

Milestones (§3, p. 6)

Every machine in an admissible $L$ carries fewer than $1/\varepsilon$ long assignments, and for $n,m\ge1$

\#\{L\text{ admissible}\}<(n+1)^{m/\varepsilon}.

If some schedule has makespan at most $d$ , its long part is admissible and its short part is a feasible solution of the residual LP.
If the short assignments take at most $d-t_i+\varepsilon d$ on machine $i$ , the combined schedule has load at most $(1+\varepsilon)d$ on every machine.
$A_\varepsilon$ exists for every LP solver and is a $(1+\varepsilon)$ -relaxed decision procedure.

Significance

Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in $\log(1/\varepsilon)$ . It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.

The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold $t=\varepsilon d$ ).

Difficulty

The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than $t$ . The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent $m/\varepsilon$ and a strict inequality.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.
A vertex of an LP is a point of Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to $0$ , which leaves the vertices unchanged.
The LP solver is a parameter (a vertex selector) and $A_\varepsilon$ is a predicate on procedures: each answer must extend an admissible schedule of long assignments, round the selected vertex within its support, and satisfy the (IP) load bound. The guarantee is proved for every such procedure. The output is thereby tied to what the algorithm computes, so the bound is not witnessed by an optimal schedule.
The binary search is a definition: greedy start, $l=\lceil t/m\rceil$ (the paper's $t/m$ rounded up because makespans are integers), $d=\lfloor(u+l)/2\rfloor$ , best stored schedule as output.
Not formalized: that $m$ is fixed, the polynomial running time, and the space bound polynomial in $m$ , $\log(1/\varepsilon)$ and the input size. The guarantee is stated for every $m\ge1$ . The count $(n+1)^{m/\varepsilon}$ of milestone 1, on which the running-time claim rests, is formalized, with the real power Real.rpow.
The constants are exact: $1+\varepsilon$ , $(n+1)^{m/\varepsilon}$ , $d-t_i+\varepsilon d$ . Milestone 1 needs $n\ge1$ and $m\ge1$ for strictness.
Theorem 1 (the Rounding Theorem) and Lemma 1 are milestones of mission 1 of this series and are not restated here.

Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.

Selected references

J.K. Lenstra, D.B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source; Theorem 3, p. 6). Journal version: Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951
C.N. Potts, Analysis of a linear programming heuristic for scheduling unrelated parallel machines, Discrete Applied Mathematics 10 (1985) 155–164. https://doi.org/10.1016/0166-218X(85)90009-5
D.S. Hochbaum, D.B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34 (1987) 144–162. https://doi.org/10.1145/7531.7535

10 thms3 active usersReviewed

Completed

Linear algebra Optimization·Captain: mikedeng1

Strongly Regular Generalized Equations IV: Strong Second-Order Sufficiency and Linearly Independent Binding Gradients Make the KKT Generalized Equation Strongly RegularResearch Paper

Motivation

A nonlinear program is rarely solved once. Its data are estimated, rounded, or varied on purpose in a parametric study, and an algorithm such as sequential quadratic programming replaces it at every iteration by a nearby linearised problem. Both uses need the same fact: near a solution, the Karush–Kuhn–Tucker (KKT) system should have exactly one solution for every small perturbation, and that solution should move Lipschitz-continuously with the perturbation. For problems with equality constraints only, or with strict complementary slackness, the classical implicit-function theorem gives this, as in Fiacco's sensitivity analysis (Fiacco 1976, reference [4] of the paper). Without strict complementarity the KKT system is not a smooth equation, and the classical theorem does not apply.

S. M. Robinson's paper Strongly regular generalized equations, Math. Oper. Res. 5 (1980) 43–62 introduced strong regularity to handle exactly this case. §2 of the paper proves an implicit-function theorem for generalized equations, §3 characterises strong regularity of linear generalized equations through a Schur complement, and §4, the subject of this mission, applies both to nonlinear programming. Its Theorem 4.1 identifies the conditions under which the KKT system is strongly regular. These conditions (strong second-order sufficiency and linearly independent binding gradients) became standard hypotheses in the stability theory of nonlinear programs and in the local convergence analysis of Newton-type methods.

Setting

Let $\Omega\subseteq\mathbb R^n$ be open and let $\theta:\Omega\to\mathbb R$ , $g:\Omega\to\mathbb R^p$ , $h:\Omega\to\mathbb R^q$ be Fréchet differentiable. The program is

\text{minimize } \theta(x)\quad\text{subject to}\quad g(x)\le0,\ h(x)=0.\qquad(4.1)

The Lagrangian is $\mathcal L(x,u,v)=\theta(x)+\langle u,g(x)\rangle+\langle v,h(x)\rangle$ , and $\mathcal L'$ is its gradient in $x$ .

For a set $C$ and a point $z$ , the normal-cone operator $\partial\psi_C(z)$ is the set of vectors $y$ with $\langle y,c-z\rangle\le0$ for all $c\in C$ when $z\in C$ , and the empty set when $z\notin C$ . The KKT conditions of (4.1) are the generalized equation

0\in F(x,u,v)+\partial\psi_{\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q}(x,u,v),\qquad F(x,u,v)=\big(\mathcal L'(x,u,v),\,-g(x),\,-h(x)\big).\qquad(4.3)

Its middle block says $g(x)\le0$ , $u\ge0$ and $\langle u,g(x)\rangle=0$ .

A generalized equation $0\in F(z)+\partial\psi_C(z)$ is strongly regular at a solution $z_0$ (DEFINITION, p. 45) if its linearisation $T(z)=F(z_0)+F'(z_0)(z-z_0)+\partial\psi_C(z)$ satisfies the following. There are neighbourhoods $U$ of $0$ and $V$ of $z_0$ and a constant $\lambda$ such that, for every $y\in U$ , the inclusion $y\in T(z)$ has exactly one solution $z=s(y)$ in $V$ , and $s$ is $\lambda$ -Lipschitz on $U$ .

At a solution $(x_0,u_0,v_0)$ the inequality constraints split into three groups:

$g^+$ , with $g_i(x_0)=0$ and $u_{0,i}>0$ ;
$g^0$ , the weakly active ones, with $g_i(x_0)=0=u_{0,i}$ ;
$g^-$ , with $g_i(x_0)<0$ .

Write $\mathcal L''=\mathcal L''(x_0,u_0,v_0)$ for the Hessian of the Lagrangian in $x$ , $H=h'(x_0)$ , $G^+=g^{+\prime}(x_0)$ and $G^0=g^{0\prime}(x_0)$ . A square matrix is a P-matrix if all its principal minors are positive.

Formalization targets

Goal: Theorem 4.1 (p. 56)

Assume $\theta,g,h$ are twice differentiable at $x_0$ and $(x_0,u_0,v_0)$ solves (4.3). Assume also:

(a′) strong second-order sufficiency: $\langle y,\mathcal L''y\rangle>0$ for all $y\ne0$ with $G^+y=0$ and $Hy=0$ ;
(b) linear independence: the matrix $\begin{bmatrix}G^+\\G^0\\H\end{bmatrix}$ has full row rank.

Then

\text{(4.3) is strongly regular at }(x_0,u_0,v_0).

The Lipschitz constant is not fixed; the goal asserts that one exists.

Milestones

The matrix $K=\begin{bmatrix}\mathcal L''&H^T&G^{+T}\\-H&0&0\\-G^+&0&0\end{bmatrix}$ of (4.5) is nonsingular.
The equations (4.8) define $V,A,B$ uniquely, and the Schur complement $S=[G^0\ 0\ 0]\,K^{-1}\,[G^0\ 0\ 0]^T$ of (4.6) satisfies $S=G^0V=V^T\mathcal L''V$ , so $S$ is symmetric.
A symmetric matrix is a P-matrix if and only if it is positive definite.
$S$ is positive definite.
The §4 criterion (p. 55): (4.3) is strongly regular at $(x_0,u_0,v_0)$ if and only if $K$ is nonsingular and $S$ is a P-matrix.

A further item formalizes the example (4.9)–(4.10) on pp. 56–57: a linear generalized equation in $\mathbb R^4$ whose unique solution satisfies the ordinary second-order sufficient condition and (b), yet is not strongly regular.

Significance

Strong regularity is the hypothesis of Robinson's implicit-function theorem (Theorem 2.1 of the paper). Theorem 4.1 therefore yields, for a parametrised nonlinear program, a locally unique and Lipschitz-continuous KKT point together with its multipliers, without strict complementary slackness. The same property underlies the local quadratic convergence of Josephy–Newton and SQP methods, and the criterion of milestone 5 is the form in which it is usually checked. The example of (4.10) shows that the ordinary second-order sufficient condition is not enough; the weakly active constraints have to be dropped from the cone on which $\mathcal L''$ must be positive.

All statements are proved in the paper. None of them, nor the notion of strong regularity, has a machine-checked proof on this platform. The matrix milestones (1–4) are self-contained linear algebra and can be proved independently. Milestone 3 for arbitrary symmetric matrices is a variant of Sylvester's criterion, which Mathlib does not currently state. Milestone 5 rests on §3 and the appendix of the paper (the Schur-complement criterion and the reduction of a linear generalized equation over a polyhedral set), which are the subjects of the companion missions II and III of this series.

Difficulty

The obvious argument would apply the classical implicit-function theorem to the active KKT equations. It fails because of the weakly active constraints. Near $(x_0,u_0,v_0)$ a constraint with $g_i(x_0)=0=u_{0,i}$ can become active or inactive under arbitrarily small perturbations, so the solution map is piecewise smooth, not smooth. Uniqueness has to hold across all the pieces simultaneously, which is a combinatorial condition: the P-matrix property of a Schur complement, not the nonsingularity of a single Jacobian. Example (4.10) shows that the natural guess (nonsingularity of every piece, guaranteed by ordinary second-order sufficiency) is insufficient: three distinct KKT points can coalesce at the origin.

The analytic part is also not routine. Strong regularity concerns the linearised problem with an arbitrary small perturbation on the right-hand side, including perturbations of the complementarity block. The criterion needs the reduction of §3 and the appendix, which localises the polyhedral set $\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q$ around the solution.

Formalization scope

Spaces. Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n). The triple $(x,u,v)$ lives in EuclideanSpace ℝ (Fin n ⊕ (Fin p ⊕ Fin q)), the Euclidean $\mathbb R^{n+p+q}$ , so the normal cone uses the standard inner product. A product type, which carries the sup norm and no inner product, is deliberately not used.
Normal cone. The operator includes the clause $z\in C$ , so it is empty off $C$ .
Strong regularity. It is stated on the linearisation data, with a real Lipschitz constant $\lambda$ , and requires existence, uniqueness in $V$ and the Lipschitz bound. Strong regularity at a point bundles a Fréchet derivative of $F$ there.
Twice differentiable at $x_0$ . This is encoded as $\theta$ , $g_i$ , $h_j$ differentiable on the open set $\Omega$ (the standing assumption of (4.1)), together with differentiability at $x_0$ of their gradients. It is not $C^2$ on $\Omega$ , and symmetry of $\mathcal L''$ is not assumed; it follows.
Matrix conventions. Positive definite means $\langle w,Mw\rangle>0$ for $w\ne0$ , without symmetry. P-matrix quantifies over all nonempty principal index sets. The Schur complement is used only together with nonsingularity of (4.5), because Mathlib's inverse of a singular matrix is $0$ .
What must not be formalized. Replacing (a′) by the ordinary second-order sufficient condition, or restricting (b) to $G^+$ and $H$ , gives a false or a different theorem. The milestones state exactly which constraints enter each condition: (a′) uses $G^+$ and $H$ , and (b) uses $G^+$ , $G^0$ and $H$ . A formalization that drops the weakly active constraints from (b), or assumes strict complementarity, trivializes the goal to the classical implicit-function theorem.
Infrastructure. A complete development needs the normal cone of a product of orthants, block-matrix inversion and Schur-complement identities, Sylvester-type criteria for symmetric matrices, and the reduction of a linear generalized equation over a polyhedral set to its reduced form. The linear-algebra milestones are reusable beyond this mission. Proofs of any milestone, and of the general P-matrix/positive-definite equivalence, are welcome.

Selected references

S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1) (1980) 43–62. https://doi.org/10.1287/moor.5.1.43
A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968 (reference [3] of the paper; second-order sufficient condition, Chapter 2).
A. V. Fiacco, Sensitivity analysis for nonlinear programming using penalty methods, Mathematical Programming 10 (1976) 287–311 (reference [4] of the paper). https://doi.org/10.1007/BF01580379
R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8 (1974) 189–211 (reference [1] of the paper). https://doi.org/10.1016/0024-3795(74)90055-4
A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014 (modern account of strong regularity). https://doi.org/10.1007/978-1-4939-1037-3

9 thms3 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 3: Shifting and Scaling the Processing Times Changes Neither the Optimal Sequence nor the Branch-and-Bound PathResearch Paper

Motivation

Branch and bound was introduced for integer programming by Land and Doig (1960) and for the travelling salesman problem by Little, Murty, Sweeney and Karel (1963). Ignall and Schrage (1965) were among the first to apply it to machine scheduling. They give lower bounds for two permutation flow-shop problems: the makespan on three machines, and the mean completion time on two. Their Appendix then asks how the method depends on the units and the origin of the data. Its THEOREM says that changing the location and the scale of all processing times changes neither the optimal sequence nor the path the branch-and-bound procedure takes.

The statement matters for computational experiments of the kind the paper reports. Run times and node counts measured on one jobset carry over to every jobset obtained from it by a positive affine change of the processing times, so a test family need only vary the shape of the data, not its location and scale. It is also a correctness property of the procedure: a branch-and-bound method whose behaviour depended on the time unit would be suspect.

Setting

There are $n$ jobs, and every job visits the machines in the same order: $A$ , then $B$ (two-machine problem), or $A$ , $B$ , then $C$ (three-machine problem). Job $i$ has nonnegative processing times $a_i, b_i$ (and $c_i$ ). Following Johnson (1954), both problems are restricted to permutation schedules. A full sequence $\sigma$ lists the jobs in the order in which every machine processes them, and each operation starts as early as possible. The makespan of $\sigma$ is the time machine $C$ finishes its last job. The completion time $d_i$ of job $i$ is the time machine $B$ finishes it, and the two-machine objective is $\sum_i d_i$ , which is $n$ times the mean completion time.

A node $J_r$ is a partial sequence of $r$ distinct jobs, and $\bar J_r$ is the set of the $n-r$ jobs it has not scheduled. For three machines, $\mathrm{TIMEA}, \mathrm{TIMEB}, \mathrm{TIMEC}(J_r)$ are the times the machines finish $J_r$ , and the lower bound (p. 401) is

LB(J_r)=\max\Big[\mathrm{TIMEA}+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}+\sum_{\bar J_r}c_i\Big].

For two machines, $\hat T_r$ and $\hat S_r$ are the minima over orderings of $\bar J_r$ of two explicit sums $T_r$ , $S_r$ (pp. 405–406), and the lower bound is $LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r)$ .

The branch-and-bound procedure (p. 402) keeps a list of nodes ranked by $LB$ , starting from the root alone. At each step it removes the first node and inserts each of its children $J_r\,j$ ranked into the list. On ties a new node goes before an old one (p. 403). It stops when the first node has scheduled $n-1$ jobs, which fixes the whole sequence. The list after $k$ steps is $\mathrm{run}_{LB}(k)$ .

Problems $P'$ (data $a'_i,b'_i,c'_i$ ) and $\tilde P$ are related by a change of location and scale when

\tilde a_i = H(a'_i+G),\qquad \tilde b_i=H(b'_i+G),\qquad \tilde c_i = H(c'_i+G),\qquad H,G>0.

Formalization targets

Goal: the Appendix THEOREM (p. 411)

For both the three-machine makespan problem and the two-machine sum-of-completion-times problem:

\sigma \text{ is optimal for } \tilde P \iff \sigma \text{ is optimal for } P', \qquad \mathrm{run}_{LB_{\tilde P}}(k)=\mathrm{run}_{LB_{P'}}(k)\ \text{ for all } k .

Milestones, in the order of the paper's proof

Adding $G$ to every processing time raises the completion time of the $r$ -th job on machine $M$ by $G(r+M-1)$ .
On two machines, $\sum_i d_i$ rises by $\tfrac12 Gn(n+3)$ for every sequence.
On two machines, $\hat T_r$ and $\hat S_r$ rise by $G[r(n-r)+\tfrac12(n-r)(n-r+1)+(n-r)]$ , $\sum_{J_r}d_i$ by $\tfrac12Gr(r+3)$ , and $LB(J_r)$ by $\tfrac12Gn(n+3)$ , for $1\le r\le n-1$ .
On three machines, every makespan and every $LB(J_r)$ with $1\le r\le n-1$ rises by $G(n+2)$ .
Multiplying all processing times by $H>0$ multiplies all these quantities by $H$ .
If $LB'=\varphi\circ LB$ on the nodes with $1\le r\le n-1$ , for a strictly increasing $\varphi$ , the two runs coincide at every step.

Significance

The THEOREM makes the method's behaviour a function of the shape of the data alone, not of its location or scale. This justifies normalizing test data, comparing running times across jobsets that differ by a change of units, and reporting results for one representative of each class. The proof also isolates a general principle: a deterministic best-first search depends on its bound only through the order the bound induces on the nodes it compares. Milestone 6 states that principle for the procedure of p. 402 with an arbitrary bound, so it applies to any other bound plugged into the same procedure.

As far as is known, no machine-checked version of this result or of the two lower bounds exists. The formalization needs the paper's procedure, with its tie rule, as an explicit deterministic function, and both lower bounds as functions of a node. The mission produces both, along with exact shift identities for every quantity the procedure uses.

Difficulty

The obvious argument is "adding $G$ adds a constant to everything", and it is not literally true. The constant depends on the position of a job and on the machine, so the identities must be computed term by term: maxima over machine-availability times commute with the shift only because both arguments move by the same amount, and that fails at the first job if processing times may be negative. The paper's own accounting contains a slip, the missing factor $G$ in $\tfrac12 r(r+3)$ . Its claim that "all lower bounds" of the three-machine problem rise by $G(n+2)$ is false at the root, where $\mathrm{TIMEB}=0$ does not move. The run equality therefore has to use the fact that the root is never compared with another node. The minima $\hat T_r$ , $\hat S_r$ range over all orderings of $\bar J_r$ , so their shift requires every ordering to move by the same amount. Finally, "the same path" has to be shown for the procedure's insertion with ties, step by step.

Formalization scope

Jobs are Fin n, numbered from $0$ . Processing times are real, and the shift statements and the goal assume them nonnegative, the paper's standing convention for durations. With negative times the goal is false (a three-job counterexample is recorded in the goal's statement). Scaling needs no sign condition.
The schedules of full sequences are Johnson's published as-soon-as-possible schedules (JohnsonFlowShop.ThreeStage.asapDone, JohnsonFlowShop.TwoStage.asapC2). Node attributes are computed by the same recursion on lists.
The two-machine objective is $\sum_i d_i$ instead of the mean; the two have the same minimizers.
$\hat T_r$ and $\hat S_r$ are minima over all orderings of $\bar J_r$ , not values at a sorted order.
Terminal nodes have depth $n-1$ . The procedure inserts children one at a time in increasing job index, each before every node of equal bound. Dominance discarding is not part of it.
Explicit readings. "The same sequence is optimal for both problems" means the sets of optimal sequences are equal, stated as an iff for every $\sigma$ . "Will follow the same path" means $\mathrm{run}(k)$ is equal for both problems at every $k$ . The paper's "all lower bounds" in the three-machine shift is restricted to nodes with $1\le r\le n-1$ . The hypotheses $H>0$ and $G>0$ are kept as stated.
Trivializations ruled out. A goal asserting only that some common optimal sequence exists, or only that the optimal values are related, would be weaker than the THEOREM. The goal states the iff and the equality of runs, with the procedure fixed independently of the data except through the bound.
The procedure, the node attributes and the lower bounds are also drafted in missions 1 and 2 of this series. Milestone 6 is reusable for any bound used with the same procedure. Proofs of any milestone are welcome. Generalizations, such as arbitrary real $G$ in the shift identities, are welcome as separate items.

Credit: Johnson (1954) for the reduction to permutation schedules and the published schedule definitions. No platform item treats flow-shop lower bounds or branch and bound over sequences. The nearest is the branch-and-bound mission BiconvexProg.BranchBound (Al-Khayyal and Falk), an unrelated algorithm for biconvex programs.

Selected references

E. Ignall, 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
A. H. Land, A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 972–989, 1963. https://doi.org/10.1287/opre.11.6.972

15 thms3 active usersReviewed

Convex Optimization Markov Chain Stochastic Systems·Captain: mikedeng1

An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand: Adaptive(α, β) Has Per-Period Regret O(N(L)^(−1/3)) at α = β = 1/2Research Paper

Motivation

Periodic-review inventory systems with lost sales and a positive replenishment lead time are a basic model of retail and spare-parts operations: demand that cannot be met from stock is lost, and an order placed today arrives $\tau$ periods later. Even with a known demand distribution the optimal policy depends on the whole vector of outstanding orders and is intractable for long lead times, so practice and theory fall back on base-stock (order-up-to) policies, which are asymptotically optimal as the lost-sales penalty grows relative to the holding cost (Huh, Janakiraman, Muckstadt and Rusmevichientong, Management Science 2009).

Computing the best base-stock level still requires the demand distribution. In many settings the distribution is unknown and, worse, demand is censored: the manager records sales, $\min\{D_t, I_t\}$ , and never sees the demand lost to a stockout. The paper behind this mission, Huh, Janakiraman, Muckstadt and Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand (working paper of February 8, 2007; published in Mathematics of Operations Research 2009, DOI 10.1287/moor.1080.0367), gives an algorithm that learns the optimal base-stock level from sales data alone and bounds its regret against the best base-stock policy. It extended the zero-lead-time adaptive newsvendor analyses (e.g. Huh and Rusmevichientong, Math. Oper. Res. 2009) to positive lead times, where the inventory process is a Markov chain on $\mathbb R^\tau$ .

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative, continuous random variable $D$ with $E[D] > 0$ and distribution function $F$ . The inventory vector in period $t$ is

X_t = (Q_{t-1}, \dots, Q_{t-\tau+1}, I_t) \in \mathbb R^\tau_+,

the $\tau - 1$ outstanding orders and the on-hand inventory $I_t$ ; its inventory position is $X_t \cdot \mathbf 1^\tau$ . Under the order-up-to- $S$ policy the manager orders $Q_t = [S - X_t\cdot\mathbf 1^\tau]^+$ , demand $D_t$ is realized, and

I_{t+1} = [I_t - D_t]^+ + Q_{t-\tau+1}.

A period with on-hand inventory $y$ costs, in expectation, $C(y) = h\,E[y - D]^+ + b\,E[D - y]^+$ , with holding cost $h$ and lost-sales penalty $b$ . The long-run average cost of level $S$ is

C(I_\infty(S)) = \lim_{T\to\infty} \frac1T \sum_{t=1}^T E[C(I_t(S))],

and $S^*$ denotes a level minimizing it over $S \ge 0$ . Write $\gamma(S) = \mathcal P[D \le S/(\tau+1)]$ .

The algorithm $\textsc{Adaptive}(\alpha,\beta)$ runs in cycles $k = 1, 2, \dots$ of length $T_k = \lceil k^\beta\rceil$ ; $N(L) = \sum_{k\le L} T_k$ . Cycle $k$ uses a fixed level $S_k$ . From sales data it computes a sample-path derivative $I'$ by a recursion over the last $\tau$ periods, forms a gradient estimate $H_k \in \{h, -b, 0\}$ from the last period of the cycle, and sets $S_{k+1} = P_{[\underline M, \overline M]}(S_k - \epsilon_k H_k)$ with $\epsilon_k = (\overline M - \underline M)/(\max\{b,h\}k^\alpha)$ . The inventory is carried over between cycles. The regret after $L$ cycles is

\Lambda(L) = E\Big[\sum_{k=1}^L\sum_{j=1}^{T_k} C(I_{(k,j)})\Big] - C(I_\infty(S^*))\,N(L).

Formalization targets

Goal: Theorem 10, corrected

Under Assumption 1 ( $0 \le \underline M \le S^* \le \overline M$ and $\gamma(\underline M) > 0$ ) and infinite support of $D$ , for $\alpha,\beta \in (0,1)$ and $L \ge 1$ , with $N = N(L)$ and $\nu = \max\{1 - \gamma(\underline M)^{2\tau}, F(\overline M), 1/e\}$ ,

\frac{\Lambda(L)}{N} \le (b+h)\Big[(\overline M - \underline M)\Big(\frac{4}{N^{\frac{1-\alpha}{1+\beta}}} + \frac{4/(1-\alpha)}{N^{\frac{\alpha}{1+\beta}}} + \frac{C_3}{N^{\frac1{1+\beta}}}\Big) + \overline M\,\frac{24\tau/\ln(1/\nu)}{N^{\frac{\beta}{1+\beta}}}\Big],

with $C_3 = 12(4\tau)^{1/\beta}\Gamma(1/\beta)(1/\beta)/(\ln(1/\nu))^{1/\beta}$ . At $\alpha = \beta = 1/2$ this is $O(N^{-1/3})$ .

Milestones

Lemma 5 (tail of $D_1 + \dots + D_t$ ), Lemma 6 (the inventory position falls to $S$ ), Theorem 7 (existence, independence of the start, convexity and differentiability of $C(I_\infty(S))$ , and existence of $S^*$ with $\gamma(S^*) > 0$ ), Theorem 11 (projected stochastic gradient descent with biased gradients), Lemmas 12 and 13 (sums over cycles of length $\lceil k^\beta\rceil$ ), Lemma 14 (the regret $\Lambda_1$ from $S_k \ne S^*$ ) and Lemma 15 (the transient regret $\Lambda_2$ ).

Significance

The theorem gives a nonparametric, sales-only policy whose average cost approaches that of the best base-stock policy at an explicit polynomial rate, uniformly over demand distributions satisfying Assumption 1. Its ingredients are reusable: an explicit geometric ergodicity rate for the lost-sales base-stock chain, convexity of the long-run base-stock cost in $S$ , and a regret bound for projected gradient descent whose gradients are biased by Markov dependence.

The result is published; to our knowledge none of it has been machine-checked. The mission formalizes the regret bound, which requires Markov-chain ergodicity on a continuous state space, long-run averages, and stochastic approximation with biased gradients. It also repairs the printed constants: Theorem 10 and Lemma 15 are false as printed (see Formalization scope), and the formal statements make the dependence on $\overline M$ explicit.

Difficulty

The obvious route treats the cycle's last-period derivative as an unbiased gradient of $C(I_\infty(S_k))$ and applies standard online convex optimization. That fails: the estimate is computed from a Markov chain started at whatever state the previous cycle left, so it is biased, and the bias decays only as the chain mixes. Controlling the bias requires an explicit mixing rate for a chain on $\mathbb R^\tau_+ \times \{0,1\}^\tau$ whose state includes the derivative process, uniformly over the levels in $[\underline M, \overline M]$ and over starting positions above $S$ . The ergodicity argument uses a coalescing demand pattern, which exists only when $\gamma(S) > 0$ ; without that condition the chain need not be ergodic. A second obstacle is that the objective $C(I_\infty(S))$ is defined as a long-run average, so its convexity and differentiability in $S$ must be established before any gradient argument applies.

Formalization scope

Everything is stated in Lean 4 with Mathlib. The inventory vector is a pair (pipeline Fin (τ-1) → ℝ, newest order first; on-hand ℝ). Lean periods are $0$ -based (Lean period $t$ is the paper's $t+1$ ); cycles are numbered from $1$ . Demand is a sequence on a probability space that is i.i.d., nonnegative, integrable, with $E[D] > 0$ and an atomless law; infinite support is $F(x) < 1$ for all $x$ ; $\tau \ge 1$ , $h, b > 0$ . The long-run cost is a limsup of Cesàro averages from the empty start (Theorem 7 shows it is a limit from every start), and $S^*$ is any minimizer over $[0,\infty)$ . The algorithm is a deterministic function of the demand path; the sample derivative is the recursion the algorithm computes, not a derivative. Integrability of every expectation follows from boundedness of the inventory and is not assumed.

Corrections, all disclosed in the items: Theorem 10 carries $\overline M$ instead of $\overline M - \underline M$ on the $C_4$ term, because the printed bound fails for $\underline M = \overline M = S^*$ , $X_{(1,1)} = 0$ , $L = 1$ , where the right side is $0$ and $\Lambda(1) = C(0) - C(I_\infty(S^*)) > 0$ . Lemma 15 carries $\overline M$ and $12\tau + 1$ . Lemma 14 keeps its printed constant; its proof appears to use the ergodicity theorem one period early. Theorem 11 is stated on an interval with the bias taken conditionally on the history. Lemmas 5 and 6 are stated for infinite support only.

A goal that bounds the regret by $\Lambda_1$ alone (costs at the steady state of $S_k$ ), or that lets the levels be any sequence in $[\underline M, \overline M]$ , is not the theorem: the regret here uses the realized inventory of the algorithm. Lean's conventions $x/0 = 0$ and $\ln$ of a nonpositive number cannot trivialize the bound, because infinite support and $\gamma(\underline M) > 0$ give $\nu \in [1/e, 1)$ . The source is the authors' working paper of February 8, 2007, whose printed page numbers equal the PDF's.

Not yet stated: Theorem 3 and Lemma 4 (ergodicity rate), Theorem 8 and Lemma 9 (bias bounds), Theorem 1 (sample derivatives). They need the joint chain $(X_t, X'_t)$ and are welcome as contributions, as are the general pieces: geometric ergodicity via coalescence, and the biased projected-gradient bound.

Selected references

W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand, working paper, 2007; Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0367
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
W. T. Huh, P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0355
G. Janakiraman, R. O. Roundy, Lost-Sales Problems with Stochastic Lead Times: Convexity Results for Base-Stock Policies, Operations Research 2004. https://doi.org/10.1287/opre.1040.0130

12 thms3 active usersReviewed

Machine Learning Optimization Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 1: AIM's Average Expected Cost Is Within O(1/√T) of the Newsvendor Cost, Perishable and Non-PerishableResearch Paper

Motivation

A retailer who restocks a product every period must choose an order-up-to level without knowing the demand distribution, and in most retail settings it observes only sales, the minimum of demand and stock. Demand above the stock is lost and never recorded. This is censored demand: the data needed to estimate the distribution are truncated exactly at the decision. Classical inventory theory assumes the distribution is known, and then the optimal policy in the stationary case is to order up to the newsvendor quantity in every period.

Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) give a nonparametric policy that learns from censored sales alone, the Adaptive Inventory Management (AIM) algorithm, and prove that its average expected cost approaches the newsvendor cost at rate $1/\sqrt T$ . The perishable case reduces to online convex optimization in the sense of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). The non-perishable case is new: leftover stock constrains the next decision, and the paper controls this constraint through a single-server queue.

Setting

Demands $D_1, D_2, \dots \ge 0$ are independent and identically distributed with an unknown law of finite mean; $D$ denotes a generic demand and $F$ its distribution function. A holding cost $h > 0$ is paid per unit left over and a penalty $b > 0$ per unit of lost demand. The newsvendor cost of a level $y \ge 0$ is

Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ ,

and the newsvendor quantity is $y^{NV} = \inf\{y \ge 0 \mid F(y) \ge b/(b+h)\}$ .

In period $t$ the manager holds $x_t \ge 0$ units ( $x_1 = 0$ ), raises the stock to $y_t \ge x_t$ , and observes $\min\{D_t, y_t\}$ . Excess inventory is either perishable ( $x_{t+1} = 0$ ) or non-perishable ( $x_{t+1} = [y_t - D_t]^+$ ).

Assumption 1 gives the manager a bound $\bar y \ge y^{NV}$ , and in the non-perishable case a bound $\rho$ with $0 < \rho < E[D_1]$ . AIM keeps a target $\hat y_t$ and an implemented level $y_t$ : $y_1 = \hat y_1 \in [0, \bar y]$ , and for $t \ge 1$

\hat y_{t+1} = P_{[0,\bar y]}\big(\hat y_t - \epsilon_t H_t(\hat y_t)\big), \qquad y_{t+1} = \max\{\hat y_{t+1}, x_{t+1}\},

with the projection $P_{[0,\bar y]}(z) = \max\{\min\{z,\bar y\},0\}$ , steps $\epsilon_t = \gamma\bar y/(\max\{b,h\}\sqrt t)$ for a scale $\gamma > 0$ , and the censored gradient estimate $H_t(\hat y_t) = h$ if $D_t < \hat y_t$ and $-b$ if $D_t \ge \hat y_t$ . The manager can compute $H_t$ from the observed sales.

For $\theta > 0$ the waiting times $W_1(\theta) = 0$ , $W_{t+1}(\theta) = [W_t(\theta) + \theta - D_t]^+$ describe a GI/D/1 queue with inter-arrival times $D_t$ and service time $\theta$ . Its busy periods $J_i(\theta)$ are the stretches between successive returns to $0$ . The auxiliary queue $Z_1(\theta) = 0$ , $Z_{t+1}(\theta) = [Z_t(\theta) + \theta/\sqrt t - D_t]^+$ has shrinking service times.

Formalization targets

Goal: Theorem 2

For every $T \ge 1$ , in the perishable case

E\Big[\frac1T\sum_{t=1}^T Q(y_t)\Big] - Q(y^{NV}) \le \Big(\gamma + \frac1\gamma\Big)\frac{\bar y\max\{b,h\}}{\sqrt T},

and in the non-perishable case, if $E[D_1^6] < \infty$ and $\gamma \le \rho\max\{b,h\}/(h\bar y)$ , there is a constant $C$ , independent of $T$ , with

E\Big[\frac1T\sum_{t=1}^T Q(y_t)\Big] - Q(y^{NV}) \le \frac{C}{\sqrt T}.

The non-perishable bullet asserts only the existence of $C$ , because the paper's explicit formula (9) depends on Proposition 4 (i), which is false as printed.

Milestones

§2.4: $Q$ is convex with left derivative $h P\{D<y\} - bP\{D\ge y\}$ , and $E[H_t \mid \hat y_t]$ equals it.
Lemma 3: projected stochastic subgradient descent with steps $\gamma\operatorname{diam}(S)/(\bar B\sqrt t)$ has average error at most $(\gamma + 1/\gamma)\operatorname{diam}(S)\bar B/\sqrt T$ .
§2.4: $Q(y) - Q(\hat y) \le h(y - \hat y)$ for $0 \le \hat y \le y$ .
Theorem 6: if $\gamma \le \rho\max\{b,h\}/(h\bar y)$ , then $y_t - \hat y_t \le Z_t(\rho)$ .
Lemma 13: $E|J_{i(\theta,t)}(\theta)| \le E[|J_1(\theta)|^2]$ .
Lemma 5: $E[\sum_{t=1}^T Z_t(\theta)] \le 2\theta E[|J_1(\theta)|^2]\sqrt T$ .
Lemma 12: $E[(\sum_{i\le n} X_i)^6] \le 21 n^3 E X_1^6$ for i.i.d. mean-zero $X_i$ (and the fourth-moment analogue).
Proposition 4 (i), corrected: $E[|J_1(\theta)|^2] \le 1 + \tfrac{21\pi^2}{2}E[(D_1 - ED_1)^6]/(ED_1 - \theta)^6$ for $0 < \theta < E[D_1]$ .

Significance

Theorem 2 shows that a manager who never observes lost sales can still reach the cost of a manager who knows the distribution, at a dimension-free rate, under only a sixth-moment condition in the non-perishable case. The example of §2.5 of the paper shows that the rate $1/\sqrt T$ cannot be improved in general for AIM. Theorem 6, the coupling of the excess inventory $y_t - \hat y_t$ with a queue, is the step that handles decisions constrained by past decisions, and the same paper reuses it when $\rho$ is unknown (§3.2).

The results are proved in the paper, and none of them is formalized as far as is known. This mission formalizes them and also corrects them: Proposition 4 (i) fails for deterministic demand, its explicit constant has to be replaced, and Eq. (2) labels a right derivative as a left one. Lemma 3 for decreasing steps and Lemma 12 are standard tools that are not in Mathlib.

Difficulty

The perishable case is a stochastic subgradient method, but its estimates are conditionally unbiased only given the current iterate, and $Q$ is merely convex, not differentiable, so the textbook smooth argument does not apply directly. In the non-perishable case the implemented levels $y_t$ are not the gradient iterates, and $y_t - \hat y_t$ is not small along a path: carried-over stock can keep $y_t$ above the target for many periods. A bound on $E[y_t - \hat y_t]$ for each $t$ does not follow from a bound on one period. The queue $Z_t(\rho)$ dominates the whole excess process, but it is non-stationary. Its sum has to be compared with the stationary queue $W_t(\rho)$ , whose busy period covering a fixed time is length-biased, so second moments of busy periods enter.

Formalization scope

All declarations are in the namespace AIMInventory.Known. The demand law and the i.i.d. path measure are the published CappedBaseStock.DemandLaw and demandPathLaw, whose law has finite and strictly positive mean. $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. The optimality of $y^{NV}$ is the already posed LostSalesOrderUpTo.Asymptotic.newsvendor_optimal and is included as a reference.

Conventions:

The demand path is zero-based ( $D_t$ is d (t - 1)), and all paper indices $t \ge 1$ are kept.
The AIM run, $W$ , $Z$ , the renewal epochs and the busy periods are functions of the demand path, defined by recursion exactly as printed.
The queue indexing is $W_1 = Z_1 = 0$ and $\tau_0 = 1$ (the paper's $W_0$ , $Z_0$ need an undefined $D_0$ and $\theta/\sqrt 0$ ). Period $1$ lies in no busy period, so Lemma 13 is stated for $t \ge 2$ .
Busy-period lengths are ℕ∞-valued. Every expectation that can be infinite is a lower Lebesgue integral in $[0,\infty]$ . The expectations in Theorem 2 have bounded integrands.
Readings of loose phrases:
- "for some $\gamma > 0$ " means for every $\gamma > 0$ ;
- "any value in $[0,\bar y]$ " means for every $\hat y_1 \in [0, \bar y]$ ;
- "with probability one" in Theorem 6 means for every demand path;
- "There is a constant $C$ " means $\exists C,\ \forall T \ge 1$ .
The implicit positivity of $h$ , $b$ , $\bar y$ (they appear in denominators) is added as hypotheses.
Lemma 3 is stated on $\mathbb R^n$ for every comparator $u \in S$ , with $E[H(z)\mid z]$ read as conditioning on the σ-algebra of the current iterate.
Proposition 4 (ii) and the explicit constant (9) are not stated.

The mission does not accept a formalization that sums over arbitrary sequences with $y_t \ge \hat y_t$ instead of the AIM run, uses an uncensored gradient, or lets a non-integrable expectation default to $0$ .

Contributions toward a stochastic subgradient method with anytime steps, moment bounds for i.i.d. sums, and busy periods of Lindley's recursion are reusable beyond this mission.

Selected references

W. T. Huh, P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
A. Flaxman, A. T. Kalai, H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
E. Hazan, A. Agarwal, S. Kale, Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8

15 thms3 active usersReviewed

Machine Learning Optimization Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 3: For Any Step Scale γ, Non-Perishable AIM's Excess Cost Λ₂(T) Is Bounded by a Hitting Time and a Busy PeriodResearch Paper

Motivation

A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate $O(1/\sqrt T)$ , with no parametric assumption on demand.

In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale $\gamma$ to satisfy $\gamma\le\rho\max\{b,h\}/(h\bar y)$ , where $\rho$ is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale $\gamma>0$ , at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.

Setting

Demands $D_1,D_2,\dots$ are independent, nonnegative, identically distributed, with finite positive mean $E[D_1]$ and otherwise unknown law. The holding cost is $h>0$ per unit left over and the penalty is $b>0$ per unit of unmet demand. The newsvendor cost of stocking up to $y\ge0$ is

Q(y)=h\,E[y-D_1]^+ + b\,E[D_1-y]^+ ,

and the newsvendor quantity is $y^{NV}=\inf\{y\ge0: P(D_1\le y)\ge b/(b+h)\}$ . The manager knows an upper bound $\bar y\ge y^{NV}$ .

AIM, non-perishable case. Fix $\gamma>0$ and a starting target $\hat y_1\in[0,\bar y]$ . Put $y_1=\hat y_1$ , $x_1=0$ . In period $t\ge1$ the step is $\epsilon_t=\gamma\bar y/(\max\{b,h\}\sqrt t)$ , the observed slope is $H_t=h$ if $D_t<\hat y_t$ and $H_t=-b$ otherwise, and

\hat y_{t+1}=\max\{\min\{\hat y_t-\epsilon_tH_t,\bar y\},0\},\qquad x_{t+1}=[y_t-D_t]^+,\qquad y_{t+1}=\max\{\hat y_{t+1},x_{t+1}\}.

The target $\hat y_t$ follows the gradient step. The implemented level $y_t$ can exceed it because stock that has already been bought cannot be returned. The excess-cost term is

\Lambda_2(T)=E\Big[\frac1T\sum_{t=1}^T\big(Q(y_t)-Q(\hat y_t)\big)\Big].

Auxiliary processes. Let $m=h\gamma\bar y/\max\{b,h\}$ . For a real $\theta$ :

$W_1(\theta)=0$ , $W_{t+1}(\theta)=[W_t(\theta)+\theta-D_t]^+$ is a queue with constant inflow. Its first busy period has length $|J_1(\theta)|=\inf\{t>1:W_t(\theta)=0\}-1$ .
$Z_1(\theta)=0$ , $Z_{t+1}(\theta)=[Z_t(\theta)+\theta/\sqrt t-D_t]^+$ is a queue with decreasing inflow.
$K(\theta,z)=\min\{t\ge0: z+\sum_{s=1}^t(\theta-D_s)\le0\}$ is the hitting time of $(-\infty,0]$ by the random walk started at $z$ .

For $0<\rho'<m$ , the proof uses $\tilde T=\lceil(m/\rho')^2\rceil$ and $\tilde K=\min\{t>\tilde T:Z_t(m)=0\}$ .

Formalization targets

Goal: Theorem 8 (p. 13)

For every $T\ge1$ and every $\rho'$ with $0<\rho'<\min\{m,E[D_1]\}$ ,

\Lambda_2(T)\le\frac{\max\{b,h\}\,\bar y}{T}\Big\{\big\lceil(m/\rho')^2\big\rceil+E\Big[K\Big(\rho',\frac{2\sqrt2\,m^2}{\rho'}\Big)\Big]\Big\}+\frac{2hm\,E\big[|J_1(\rho')|^2\big]}{\sqrt T}.

The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.

Milestones

Coupling (proof of Theorem 8, p. 13). For every demand path and every $t\ge1$ , $y_t-\hat y_t\le Z_t(m)$ .
Restart bound (p. 14). For $0<\rho'<m$ , $E[\tilde K]\le\lceil(m/\rho')^2\rceil+E[K(\rho',2\sqrt2m^2/\rho')]$ .
Claim (14) (p. 14, proved in Appendix E). For $0<\rho'<\min\{m,E[D_1]\}$ , $\frac hT E\big[\sum_{t=\tilde K+1}^T Z_t(m)\big]\le 2hm\,E[|J_1(\rho')|^2]/\sqrt T$ .
Lemma 9, corrected (p. 13). If $\theta<E[D_1]$ , $E[D_1^4]<\infty$ and $z>0$ , then $E[K(\theta,z)]\le1+\frac{2z}{E[D_1]-\theta}+\frac{8\pi^2E[(D_1-E[D_1])^4]}{(E[D_1]-\theta)^4}$ .

Significance

The result. The cost of AIM relative to the newsvendor benchmark splits as $\Lambda_1(T)+\Lambda_2(T)$ . Stochastic subgradient descent controls $\Lambda_1(T)$ for every $\gamma$ , so Theorem 8 is the remaining step in showing that AIM converges at rate $O(1/\sqrt T)$ without any knowledge of a lower bound on mean demand. The first term of the bound is $O(1/T)$ whenever $E[K]$ is finite, and Lemma 9 gives that under a finite fourth moment. The second term is $O(1/\sqrt T)$ whenever $E[|J_1|^2]$ is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than $\bar y$ , that the non-perishable analysis needed.

Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.

Difficulty

The argument behind Theorem 2 dominates $y_t-\hat y_t$ by a queue whose inflow $\rho/\sqrt t$ is below the mean demand. For large $\gamma$ the inflow $m/\sqrt t$ exceeds $E[D_1]$ in early periods, so the queue $Z(m)$ is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on $E[\sum_t Z_t(m)]$ through busy periods of $W(m)$ fails, because $W(m)$ may never empty when $m\ge E[D_1]$ . The proof therefore separates a random initial stretch, which ends at the first time after $\tilde T$ that $Z(m)$ empties, from the remainder. The two parts are bounded by different processes. The random index $\tilde K$ sits inside the sums, so the expectations have to be handled with that dependence.

Formalization scope

Demand uses the published definition CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.
The demand path is zero-based: the paper's $D_t$ is d (t-1). AIM is a deterministic recursion on the path, and $\hat y_t,y_t,x_t$ depend on $D_1,\dots,D_{t-1}$ only. Levels are real numbers, and $Q$ is evaluated at nonnegative levels.
The conventions are $Z_1=W_1=0$ and $\tau_0=1$ . The paper's own indexing ( $Z_0=0$ in (7)) is undefined at $t=0$ , and these are the conventions its proofs use.
$K$ , $|J_1|$ and $\tilde K$ take values in $[0,\infty]$ , and $E[K]$ , $E[|J_1|^2]$ , $E[\tilde K]$ are Lebesgue integrals in $[0,\infty]$ . Theorem 8 and Claim (14) are stated in $[0,\infty]$ . A divergent expectation therefore makes a bound trivially true. It can never make a bound false or vacuous through a junk value $0$ . $\Lambda_2(T)$ is a real expectation of a bounded integrand.
Explicit readings of loose phrases: "for any choice of the parameter $\gamma$ " means every $\gamma>0$ . "Set $y_1=\hat y_1$ to any value in $[0,\bar y]$ " means the statements hold for every such start. "With probability one" in the coupling is stated pathwise. $0<\rho'$ is added (the bound divides by $\rho'$ ), as are $h,b,\bar y>0$ . In Claim (14) the random lower limit $\tilde K$ is read inside the expectation, as in (13) and Appendix E.
Lemma 9 is false as printed: for $D\equiv1$ , $\theta=0$ , $z=1/4$ one has $K=1$ while the printed bound is $1/2$ . The mission states it with an additive $1$ , which is what the printed proof gives once the integers below $2z/(E[D_1]-\theta)$ are counted correctly.
Ruled out: stating the goal about an arbitrary sequence of levels instead of the AIM recursion, taking $E[K]$ or $E[|J_1|^2]$ as real Bochner integrals (which are $0$ when the expectation diverges and would make the bound false), and dropping the newsvendor bound $y^{NV}\le\bar y$ from the goal.
Welcome contributions: a reusable Lindley-recursion (see Asmussen 2003, Ch. III) and busy-period library (the inspection-paradox bound $E|J_{i(\theta,s)}(\theta)|\le E|J_1(\theta)|^2$ , Lemma 13 of the paper), fourth-moment Markov bounds for sums of i.i.d. centred variables, and shift invariance of the i.i.d. path measure.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1):103–123, 2009. https://doi.org/10.1287/moor.1080.0355
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Optimization·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 2: For g = 0 ≤ f, the Tour ψ′ Minimizes the Largest Changeover CostResearch Paper

Motivation

A machine whose condition is described by one real number — the temperature of a furnace, the setting of a cutting knife — must process $N$ jobs in some order. Job $i$ must be started in state $A_i$ and leaves the machine in state $B_i$ ; moving the state between jobs costs money. Ordering the jobs so that the machine returns to its starting job after the last one is a traveling salesman problem whose distance matrix has a special structure. P. C. Gilmore and R. E. Gomory showed in 1964 (Oper. Res. 12(5), 655–679) that this special traveling salesman problem can be solved exactly with $O(N^2)$ operations, one of the first nontrivial polynomially solvable cases of the problem.

The same paper also treats a second objective: instead of the total changeover cost, minimize the largest single changeover cost of the cycle. This is the bottleneck traveling salesman problem, relevant whenever the binding constraint is the worst transition (a maximal temperature swing, a longest retooling) rather than the total. Without the tour constraint it is the bottleneck assignment problem solved by O. Gross (RAND, 1959). Gilmore and Gomory solve the bottleneck tour problem for the cost matrix of their model when only increases of the state cost anything. This mission formalizes that solution.

Timeline: Gross (1959) solves the bottleneck assignment problem; Gilmore and Gomory (1964) solve the sum and bottleneck traveling salesman problems for one state-variable costs; Gilmore, Lawler and Shmoys survey the well-solved special cases of the traveling salesman problem in The Traveling Salesman Problem (Wiley, 1985), where this case is a standard entry.

Setting

There are $N = n+1$ jobs. Job $i$ has a starting state $A_i\in\mathbb R$ and a final state $B_i\in\mathbb R$ , and the jobs are numbered so that $B_1\le B_2\le\dots\le B_N$ . Given two cost densities $f, g:\mathbb R\to\mathbb R$ , the cost of having job $j$ follow job $i$ is

c_{ij} = \int_{B_i}^{A_j} f(x)\,dx \ \text{ if } A_j\ge B_i,\qquad c_{ij} = \int_{A_j}^{B_i} g(x)\,dx \ \text{ if } B_i > A_j .

A permutation $\psi$ of the jobs means "job $\psi(i)$ follows job $i$ ". It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if $\psi$ is a single cycle. The bottleneck cost of $\psi$ is

m(\psi) = \max_{1\le i\le N} c_{i\psi(i)} .

The bottleneck case of the paper is $g = 0$ and $f\ge 0$ : lowering the state is free, raising it costs $\int f$ .

A permutation $\varphi$ ranks the $A$ 's if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . An interchange $\alpha_{ij}$ is the transposition of $i$ and $j$ ; $\psi\alpha_{ij}$ means "first apply $\alpha_{ij}$ , then $\psi$ ". The graph $G_\varphi$ has the jobs as nodes and an undirected arc $R_{i\varphi(i)}$ for each $i$ ; $R_{q,q+1}$ is the arc joining consecutive nodes $q$ and $q+1$ . A spanning tree of $G_\varphi$ is a set $T$ of arcs $R_{q,q+1}$ such that $G_\varphi\cup T$ is connected and no proper subset of $T$ connects $G_\varphi$ . In the bottleneck case the arc $R_{q,q+1}$ is given the cost $c_{q\varphi(q+1)}$ , and a minimum spanning tree minimizes the sum of these costs. If its arcs are $R_{j_1,j_1+1},\dots,R_{j_m,j_m+1}$ with $j_1<\dots<j_m$ , the paper's candidate tour is

\psi' = \varphi\,\alpha_{j_1 j_1+1}\,\alpha_{j_2 j_2+1}\cdots\alpha_{j_m j_m+1}.

Formalization targets

Goal: $\psi'$ solves the bottleneck traveling salesman problem

For $B$ sorted, $f\ge0$ locally integrable, $g=0$ , $\varphi$ ranking the $A$ 's and $T$ a minimum spanning tree as above,

\psi' \text{ is a tour}\quad\text{and}\quad m(\psi')\le m(\psi)\ \text{ for every tour } \psi .

The goal fixes no numerical constant. It asserts both that the construction produces a tour and that the tour is optimal, so it is a statement about the paper's algorithm, not only about the optimal value.

Milestones

Lemma 8 (p. 668): for a fixed $q$ , the number of $i$ with $i\le q<\varphi^{-1}\psi(i)$ equals the number of $j$ with $\varphi^{-1}\psi(j)\le q<j$ .
Lemma 7 (p. 668): for a tour $\psi$ , the graph $G_\psi^*$ — $G_\varphi$ plus the arcs $R_{q,q+1}$ selected by these two conditions — is connected.
Eq. (30) (p. 670): if $R_{q,q+1}$ is an arc of $G_\psi^*$ not in $G_\varphi$ , then $m(\psi)\ge c_{q\varphi(q+1)}$ .
$\varphi$ minimizes $m$ (p. 671): $m(\varphi)\le m(\psi)$ for every permutation $\psi$ .
The value of $m(\psi')$ (p. 671): $m(\psi')$ equals some $c_{j\varphi(j)}$ or the cost $c_{q\varphi(q+1)}$ of an arc of $T$ .
Theorem 6, corrected (p. 671): for a directed graph with nested out-neighbourhoods $\Gamma_1\subseteq\dots\subseteq\Gamma_N=\{1,\dots,N\}$ and $\varphi$ listing them as initial segments, a Hamiltonian circuit exists iff $\varphi(q)\in\Gamma_q$ for all $q$ and the graph $G'_\varphi$ is connected.

Significance

The result gives an exact solution of a bottleneck traveling salesman problem by one minimum spanning tree computation and a fixed sequence of transpositions. Since general bottleneck traveling salesman problems are NP-hard, cases with an exact algorithm are the reference points against which heuristics and approximation results are compared. Theorem 6, an application, characterizes Hamiltonicity for directed graphs whose out-neighbourhoods form a chain, a class on which the general Hamiltonian circuit problem becomes a connectivity test.

The result is proved in the paper; the mission formalizes the proof. To our knowledge none of it has a machine-checked proof. The formalization adds two things to the paper. First, the statements are made explicit: the order in which interchanges are applied, the reading of "spanning tree", the integrability of $f$ . Second, Theorem 6 as printed is false (see below), and the mission states and asks for a proof of the corrected version. Machine-checked statements of $G_\psi^*$ and Lemmas 7–8 are also the shared core of the companion mission on the minimal sum tour.

Difficulty

The obvious argument — every tour must "cross" each gap between consecutive components of $G_\varphi$ , so it pays at least the cheapest crossing — fails because the cost of a crossing is not intrinsic to the gap: a tour may cross between components using arcs that are not of the form $R_{q,q+1}$ , and $m$ looks at one arc at a time, not at a sum. The connection between an arbitrary tour and the spanning trees of $G_\varphi$ goes through the auxiliary graph $G_\psi^*$ and a counting argument (Lemma 8), and the sum-minimizing tree must be shown to be bottleneck-optimal as well. For the upper bound, the transpositions in $\psi'$ cascade along runs of consecutive tree arcs, so $\psi'(i)$ need not be $\varphi(i)$ or $\varphi(i+1)$ ; only the maximum $m(\psi')$ has that form, and showing it needs the monotonicity of $c_{ij}$ in $A_j$ and $B_i$ , which holds because $f\ge0$ and $g=0$ .

Formalization scope

Jobs are Fin (n + 1) (0-based; the paper's job $i$ is index $i-1$ ). $A, B : \text{Fin}(n+1)\to\mathbb R$ with Monotone B. The cost keeps the general two-density form (1); the bottleneck hypotheses are $f\ge0$ everywhere, $g$ identically $0$ , and $f$ locally integrable, so that every interval integral is genuine. Permutations are Equiv.Perm, and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j. $m$ is a Finset.sup' over all jobs, including those that $\psi'$ leaves unchanged. The arc $R_{q,q+1}$ is indexed by q : Fin n.

Explicit readings of the paper's phrases:

"tour": $\psi(s)\ne s$ for every nonempty proper subset $s$ (the empty set is always fixed);
"a minimal set of additional arcs that connect": a connecting set of arcs $R_{q,q+1}$ none of whose proper subsets connects;
"minimum spanning tree … with these new costs": minimum sum of $c_{q\varphi(q+1)}$ over all such trees, not a bottleneck tree;
" $j_1,\dots,j_m$ in increasing order": the interchanges are applied to $\varphi$ in increasing index, lowest first;
" $\psi'$ minimizes $m(\psi')$ ": $\psi'$ is a tour and $m(\psi')\le m(\psi)$ for every tour $\psi$ ;
Theorem 6: the condition $\varphi(q)\in\Gamma_q$ for all $q$ is added, without which sufficiency fails (for $N=3$ , $\Gamma_1=\Gamma_2=\{3\}$ , $\Gamma_3=\{1,2,3\}$ , $\varphi=(3,1,2)$ , $G'_\varphi$ is connected but no Hamiltonian circuit exists); the existence of $\varphi$ is a hypothesis, not a claim.

Not formalized: the remark that the results hold for $f=0$ , $g\ge0$ ; the remark that $\psi'=\psi^*$ when $B_i\ge A_{\varphi(i)}$ ; the $O(N^2)$ operation count.

Trivializing formalizations are ruled out: with a Bochner integral and no integrability hypothesis every cost could collapse to $0$ and every claim would hold; dropping the tour conjunct of the goal would let $\varphi$ itself be "optimal"; and a maximum that ignored the unchanged arcs $c_{j\varphi(j)}$ would make the goal false.

The traveling salesman items already on the platform (metric and symmetric models with tours as visiting orders, e.g. MetricTSP, TSPHeuristics.Shared.TSPModel) describe a different model and are not used. A complete development needs permutation cycle structure (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, and interval integrals of nonnegative functions; the lemmas on $G_\psi^*$ and Lemma 8 are reusable for the sum objective. Proofs of any milestone are welcome independently.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5) (1964), 655–679. https://doi.org/10.1287/opre.12.5.655
O. Gross, The bottleneck assignment problem, RAND Corporation P-1630, 1959. https://www.rand.org/pubs/papers/P1630.html
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in E. L. Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, 1985, 87–143. ISBN 978-0-471-90413-7

9 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Contact Interactions on a Lattice II: If λₖ/μ < k/(2d − 1), the Expected Size of a Contact Process Is Integrable in TimeResearch Paper

Motivation

The contact process is the basic model of an infection spreading on a graph: infected sites recover at a constant rate, and healthy sites are infected at a rate that depends on how many of their neighbours are infected. T. E. Harris introduced it in Contact Interactions on a Lattice (Ann. Probab. 2, 1974, doi:10.1214/aop/1176996493), and it became one of the central examples of the theory of interacting particle systems (Liggett, Interacting Particle Systems, 1985, Ch. VI; Liggett, Stochastic Interacting Systems, 1999, Part I). Its questions are those of epidemiology and population dynamics on a spatial grid: does a finite infection die out, and how large does it get on the way?

Harris's paper gives the first rigorous subcritical bounds. Section 7 treats two quantities for a process started from a finite set: the probability $p_\infty(\xi)$ of surviving forever, and the expected size $m_t(\xi)$ at time $t$ . This mission formalizes the second, Theorem 7.6: under an explicit condition on the rates, the expected size is integrable in time. The companion mission (Contact Interactions on a Lattice I) formalizes Theorem 7.1, extinction under the same condition.

A short timeline. Harris (1974) defined the process, proved monotonicity, subadditivity and submodularity by coupling, and gave the bounds of §7 and a survival result for large rates (§9). Holley and Liggett (Ann. Probab. 3, 1975) developed duality for such systems. Holley and Liggett's paper also proves, for a discrete-time branching process with interference, the analogue $P_F(A_n\ne\varnothing)\le E_F|A_n|\le\lambda^n|F|$ of the size bounds studied here; it is a different process, related but not reused.

Setting

Fix $d \ge 1$ and the lattice $Z_d$ of integer points $x = (x^1, \dots, x^d)$ . Sites $x, y$ are neighbours, $x \sim y$ , if $\sum_i |x^i - y^i| = 1$ ; $N_x$ is the set of the $2d$ neighbours of $x$ . A configuration is a finite set $\xi \subset Z_d$ (the set $\Xi_0$ ); $|\xi|$ is its number of points, $\xi(N_x)$ is the number of neighbours of $x$ in $\xi$ , and $x \sim \xi$ means $x \notin \xi$ and $x$ has a neighbour in $\xi$ .

The parameters are a death rate $\mu \ge 0$ and birth rates $\lambda_0 = 0, \lambda_1, \dots, \lambda_{2d} \ge 0$ . The contact process is the continuous-time Markov chain on finite configurations that, from $\xi$ , removes a point $x \in \xi$ at rate $\mu$ and adds a site $x \sim \xi$ at rate $\lambda_{\xi(N_x)}$ . Its total jump rate is

q_\xi = \mu|\xi| + \sum_{x \sim \xi} \lambda_{\xi(N_x)} .

The empty configuration is absorbing. $P_t(\xi, \eta)$ is its transition function, $r(\xi,\eta) = q_{\xi\eta}/q_\xi$ the transition matrix of its jump chain, and

m_t(\xi) = \mathscr E_\xi\, |\xi_t| = \sum_{\eta} P_t(\xi, \eta)\, |\eta|

the expected size at time $t$ . In the Lean development these are trans μ lam t ξ η, jump μ lam ξ η and meanSize μ lam t ξ, where lam k is $\lambda_k$ .

Formalization targets

Goal: Theorem 7.6 (p. 982)

If $\mu > 0$ and

\frac{\lambda_k}{\mu} < \frac{k}{2d-1}, \qquad k = 1, \dots, 2d,

then for every finite $\xi$ ,

\int_0^\infty m_t(\xi)\, dt < \infty .

Milestones

In the paper's proof order:

Lemma 4.7: $m_t(\xi) \le |\xi|\, e^{(2d\Lambda - \mu)t}$ with $\Lambda = \max_i \lambda_i$ .
Lemma 5.8, its $m_t$ half: $\lambda_k \le \min_{j \ge k} \lambda'_j$ implies $m_t \le m'_t$ .
The change of time scale: multiplying all rates by $c$ replaces $m_t$ by $m_{ct}$ .
Remark 5.5, three times. $m_t$ is increasing in $\xi$ when $\lambda_k \uparrow$ ; it is subadditive when also $\lambda_k / k \downarrow$ ; and it is submodular when $\lambda$ is concave and non-decreasing.
The first-jump equation (7.7) for a pair of neighbours, with $K = 2 + (4d-2)\lambda$ .
The bound after (7.11): $M_2(T) - M_1(T) \le 1/(1 - (2d-1)\lambda)$ .
Lemma 7.5: if $\int_0^\infty m_t(\{x\})\,dt = \infty$ , then $\int_0^\infty (m_t(\xi) - m_t(\{x\}))\,dt = \infty$ for $|\xi| \ge 2$ .

After the goal come two consequences: Lemma 4.11, $m_{t+h}(\xi) \ge e^{-\mu h} m_t(\xi)$ , and Remark 7.12, $m_t(\xi) \to 0$ .

Significance

The theorem says that the total expected infection time, summed over all sites, is finite. That is stronger than extinction (Theorem 7.1), and it quantifies how fast the process dies out on average. With Lemma 4.11 it gives $m_t(\xi) \to 0$ . Bounds on the expected size are the standard route to subcritical estimates for spatial epidemics and branching systems with interference. The milestones are also the paper's general tools. Monotonicity, subadditivity and submodularity of $m_t$ , comparison of rate sequences, and time scaling hold for every contact process and are reusable beyond this mission.

The theorem has been known since 1974, and the formalization of the contact process is new work: the platform has no machine-checked development of an interacting particle system on $Z_d$ , nor of a continuous-time chain with unbounded rates. The mission produces a formal model of the contact process from a finite set, a Lean proof of the subcritical bound, and the coupling inequalities (stated here for $m_t$ ) that any further work on the process will need.

Difficulty

The obvious argument fails. One would bound the growth rate of $|\xi_t|$ by its worst case: a site is born at rate at most $\lambda_k$ for each of at most $2d|\xi|$ boundary sites. This gives only Lemma 4.7, an exponential bound whose exponent $2d\Lambda - \mu$ is positive in most of the regime of the theorem. The factor $2d - 1$ instead of $2d$ comes from correlations: a newly born site always has an occupied neighbour, so it adds at most $2d - 1$ new boundary sites. Capturing this needs the comparison between a single site and a pair of neighbours in (7.7)–(7.11), together with submodularity, which is a coupling statement about the whole process. Lemma 7.5 then has to turn a bound on the difference $M_2 - M_1$ into a bound on $M_1$ , and the paper omits its proof.

In the formal setting the chain has unbounded rates (since $q_\xi$ grows with $|\xi|$ ), so its transition function is not a matrix exponential. Uniformization does not apply either, and every statement goes through the minimal solution of the backward equations.

Formalization scope

The chain model. The process is the countable-state chain on finite configurations that the paper itself uses from §4 on. Theorems 4.1 and 4.3 show that the infinite-volume process started in $\Xi_0$ is this chain. No process on infinite configurations and no probability space is constructed, and $P_\xi$ , $\mathscr E_\xi$ enter only through $P_t$ .
The transition function. $P_t$ is the minimal transition function of the rates (4.4)–(4.5), $P_t = \sup_n P^{(n)}_t$ , where $P^{(n)}_t$ is defined by Feller's backward recursion over at most $n$ jumps.
Finite initial sets. Statements the paper makes for all $\xi \in \Xi$ (Lemmas 4.11 and 5.8, Remark 5.5) are drafted for finite $\xi$ .
Values. $P_t$ , $p_t$ and $m_t$ take values in $[0, \infty]$ . Integrals of $m_t$ are Lebesgue integrals of $[0,\infty]$ -valued functions.
Lattice. Sites are Fin d → ℤ with the $\ell^1$ adjacency of the paper.
Standing hypotheses. Every statement carries $d \ge 1$ , $\mu \ge 0$ , $\lambda_0 = 0$ and $\lambda_k \ge 0$ for $k \le 2d$ . Conditions on $\lambda$ range over $k \le 2d$ only, since $\lambda_k$ for $k > 2d$ never enters the model. The goal adds $\mu > 0$ , which the paper's ratio $\lambda_k/\mu$ presupposes.

Several trivializing formalizations are excluded:

$m_t$ is not a real tsum, which would be $0$ when the series diverges;
the integral is not a real Bochner integral, which would be $0$ for a non-integrable function;
the rate condition does not range over all $k \in \mathbb N$ ;
$\mu > 0$ is not left implicit: in Lean $\lambda_k / 0 = 0$ , and at $\mu = 0$ the conclusion is false;
the goal is not stated for singletons only.

A complete development needs the backward equation and non-explosion for $P_t$ (Theorem 4.3, formalized in the companion mission), Fubini–Tonelli for $\sum$ and $\int$ in $[0,\infty]$ , and couplings of contact processes. The couplings are the paper's auxiliary multi-type processes (§§5–6), or an equivalent argument on the generator. Contributions are welcome at every level. The coupling lemmas and the backward and forward equations for minimal chains are the parts most reusable beyond this mission.

Selected references

T. E. Harris, Contact interactions on a lattice, Ann. Probab. 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
R. Holley, T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
T. M. Liggett, Interacting Particle Systems, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Trans. Amer. Math. Soc. 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

13 thms3 active usersReviewed

Operations Research

Missions

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 2: τᵏ Stays Bounded Below If (LP) Has an Optimum, and Otherwise κᵏ Stays Bounded Below and τᵏ/θᵏ Is BoundedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 63)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Semidefinite Programming 2: If Every Step Lowers the Potential φ by δ > 0, Then After k ≥ (ν√n log(1/ε) + ψ(x⁽⁰⁾, Z⁽⁰⁾))/δ Steps the Duality Gap Is at Most ε Times Its Initial ValueResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Potential Games 3: A Finite Game Has the Finite Improvement Property If and Only If It Has a Generalized Ordinal PotentialResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 2.5

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

Motivation

Setting

Formalization targets

Theorem 5.2: WMC total loss

Supporting numbered results

Significance

Difficulty

Formalization scope

Selected references

Potential Games 2: Every Finite Potential Game Is Isomorphic to a Congestion GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 165)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Implicit Renewal Theory and Tails of Solutions of Random Equations 2: Kesten's Theorem for R = Q + MR — Unique Stationary Law, Power Tails with Explicit C±, and C₊ + C₋ > 0 iff Q ≢ (1 − M)cResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Setting

Formalization targets

Strict pooling reduction

Supporting statements

Significance

Difficulty

Formalization scope

Selected references