Missions · Prove2Me

Completed

Algorithmic Game Theory Dynamic Programming Linear Optimization+2·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems VIII: Single-Controller Stochastic Games — a Dual Pair of Linear Programs Gives the Value and Stationary Optimal PoliciesTextbook

Motivation

A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).

Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).

Timeline.

1953: Shapley proves existence of the value and of stationary optimal policies for the discounted game.
1977–1978: Parthasarathy and Raghavan study games in which one player controls the transitions and identify an order-field property for the value and optimal decision rules (cited in Kallenberg 1983, pp. 192, 196).
1983: Kallenberg presents the dual pair (6.2.1)/(6.2.2), with the controlling player's policy read off the dual and the opponent's from the primal, and a constructive existence proof (Remark 6.2.2).

Setting

The state space is $E = \{1,\dots,N\}$ with $N>0$ . In state $i$ player I chooses an action $a$ from a finite nonempty set $A(i)$ and player II an action $b$ from a finite nonempty set $B(i)$ . Player I then receives $r_{iab}$ from player II, and the next state is $j$ with probability $p_{iabj} \ge 0$ , where $\sum_j p_{iabj} \le 1$ .

A history at time $t$ is $(i_1,a_1,b_1,\dots,i_{t-1},a_{t-1},b_{t-1},i_t)$ . A policy $R_1$ of player I chooses, at each time and history, a probability distribution on $A(i_t)$ ; policies $R_2$ of player II are defined likewise. A policy is stationary, written $\pi^\infty$ or $\rho^\infty$ , if the distribution depends only on the current state. With $v_i^t(R_1,R_2)$ the expected reward in period $t$ from initial state $i$ , the total reward is $v_i(R_1,R_2) = \sum_{t\ge1} v_i^t(R_1,R_2)$ .

A pair $(R_1^*,R_2^*)$ is optimal if, componentwise,

v(R_1,R_2^*) \le v(R_1^*,R_2^*) \le v(R_1^*,R_2) \qquad\text{for all policies } R_1,R_2, \tag{6.1.1}

and then $\mathrm{val(TMG)} := v(R_1^*,R_2^*)$ is the value of the game.

Assumption 6.2.1 (contraction). There are $\mu \gg 0$ and $\alpha\in[0,1)$ with $\sum_j p_{iabj}\mu_j \le \alpha\mu_i$ for all $i$ , $a\in A(i)$ , $b\in B(i)$ . The discounted game is the case $\mu = e$ .

Assumption 6.2.2 (single controller). $p_{iabj}$ does not depend on $b$ ; it is written $p_{iaj}$ .

For a stationary $\rho$ write $r_{ia}(\rho) = \sum_b r_{iab}\rho_{ib}$ and $p_{iaj}(\rho)=\sum_b p_{iabj}\rho_{ib}$ . A vector $y$ is TMG-superharmonic if some stationary $\rho^\infty$ of player II satisfies $y_i \ge r_{ia}(\rho) + \sum_j p_{iaj}(\rho) y_j$ for all $a\in A(i)$ , $i\in E$ . For weights $\beta_j>0$ the two linear programs are

\min\Big\{\textstyle\sum_j\beta_jy_j \ \Big|\ \sum_j(\delta_{ij}-p_{iaj})y_j-\sum_b r_{iab}\rho_{ib}\ge0;\ \sum_b\rho_{ib}=1;\ \rho_{ib}\ge0\Big\} \tag{6.2.1}

\max\Big\{\textstyle\sum_iz_i \ \Big|\ \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=\beta_j;\ -\sum_a r_{iab}x_{ia}+z_i\le0;\ x_{ia}\ge0\Big\} \tag{6.2.2}

Formalization targets

Goal: Theorem 6.2.3

Under Assumptions 6.2.1 and 6.2.2, let $(y^*,\rho^*)$ and $(x^*,z^*)$ be optimal solutions of (6.2.1) and (6.2.2), and $\pi^*_{ia} := x^*_{ia}/\sum_a x^*_{ia}$ . Then

v(R_1,(\rho^*)^\infty) \le v((\pi^*)^\infty,(\rho^*)^\infty) = y^* \le v((\pi^*)^\infty,R_2)\qquad\text{for all policies } R_1,R_2 .

The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.

Milestones

Theorem 6.2.1 (Shapley): under Assumption 6.2.1 both players have stationary optimal policies.
Theorem 6.2.2: under Assumption 6.2.1, $\mathrm{val(TMG)}$ is the smallest TMG-superharmonic vector.
Theorem 6.2.4 (i): for a stationary $\pi^\infty$ of player I, $x_{ia}(\pi) = [\beta^T(I-P(\pi))^{-1}]_i\pi_{ia}$ and $z_i(\pi) = \min_{b} r_{ib}(\pi)\sum_a x_{ia}(\pi)$ give a feasible point of (6.2.2) with $\sum_i z_i(\pi) = \min_\rho \sum_j\beta_j v_j(\pi^\infty,\rho^\infty)$ .
Theorem 6.2.4 (ii): every feasible $(x,z)$ of (6.2.2) has $x = x(\pi)$ and $z\le z(\pi)$ for $\pi_{ia} = x_{ia}/\sum_a x_{ia}$ .

Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.

Significance

The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.

Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.

Difficulty

There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.

Formalization scope

Model. $E$ is Fin N with $N>0$ . Actions live in finite types α, β, and $A(i)$ , $B(i)$ are nonempty Finsets. Rows are substochastic.
Policies. A history in $H_{n+1}$ is a record of $n+1$ states and $n$ actions of each player. A policy is a family of distributions indexed by time and history, supported on the current action set. Stationary policies are the image of state-dependent decision rules.
Probabilities and reward. History probabilities are explicit finite products, with no measure theory. The total reward is the tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.
Linear programs. Their variables are functions on all actions that vanish off $A(i)$ (resp. $B(i)$ ). Optimality means feasible and attaining the min/max over the feasible set. The common $p_{iaj}$ is $p_{iab_0j}$ for a fixed $b_0\in B(i)$ , and Assumption 6.2.2 makes the choice irrelevant. $\beta_j>0$ is a hypothesis, as on p. 194.
The minimum in Theorem 6.2.4 (i) is over stationary policies of player II and is stated with attainment.

Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.

Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 6. https://ir.cwi.nl/pub/13008
L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
T. Parthasarathy and T. E. S. Raghavan, Finite algorithms for stochastic games, International Conference on Dynamic Programming, Vancouver, 1977; cited in Kallenberg 1983, p. 232. https://ir.cwi.nl/pub/13008
T. Parthasarathy and T. E. S. Raghavan, An order field property for stochastic games when one player controls the transition probabilities, Game Theory Conference, Cornell, 1978; cited in Kallenberg 1983, p. 233. https://ir.cwi.nl/pub/13008

7 thms2 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems II: An Extreme Optimal Solution of the Dual Linear Program Yields a Pure Stationary Policy Optimal among Transient PoliciesTextbook

Why optimize only transient policies?

A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.

The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.

The finite model and its policies

Let $E=\{1,\ldots,N\}$ be a nonempty finite state set. Each state $i$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is selected, the system earns the real reward $r_{ia}$ and then moves to $j$ with probability $p_{iaj}\ge0$ . The row sum $\sum_jp_{iaj}$ is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.

A policy $R$ selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action $f(i)\in A(i)$ in each state. These four classes are denoted $C$ , $C_M$ , $C_S$ , and $C_D$ . The first decision occurs at time $t=1$ in the book.

Write $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ for the chance of being in state $j$ and choosing action $a$ at time $t$ , given initial state $i$ . A policy is transient if the expected number of visits to each state is finite from every initial state:

\sum_{t=1}^{\infty}\mathbb P_R(X_t=j\mid X_1=i)<\infty\qquad(i,j\in E).

For such a policy, its expected total reward $v_i(R)$ is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is $w_i=\sup\{v_i(R):R\text{ transient}\}$ , which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.

Formalization targets

Fix positive weights $\beta_j>0$ . The linear program (3.3.7) maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative state-action arrays satisfying the flow equations

\sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}=\beta_j\qquad(j\in E).

Its feasible set is $P$ . A transient stationary rule $\pi$ has an occupation vector $x(\pi)$ , where $x_{ia}$ is the $\beta$ -weighted expected number of visits to state-action pair $(i,a)$ . Theorem 3.3.3 identifies transient stationary rules bijectively with $P$ and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: $\overline{K(D)}\subset K(S)=K(M)=K=P$ , where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.

The goal is Theorem 3.3.5, p. 57. If $x^*$ is an extreme optimal solution of that program and $f_*(i)$ is the action with $x^*_{i f_*(i)}>0$ , then the pure stationary policy $f_*^\infty$ is transient and

v_i(R)\le v_i(f_*^\infty) \qquad\text{for every transient policy }R\text{ and every }i\in E.

A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that $w$ is finite; the existence of an extreme LP optimum is its stated premise.

What the result gives

An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by $\beta$ to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.

The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.

Where the difficulty lies

Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.

The LP flow constraints are equalities and $\beta$ is strictly positive. The goal does not normalize $\beta$ to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse $(I-P(\pi))^{-1}$ only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares $f_*^\infty$ only with stationary (or Markov) policies, or that identifies the classes $C$ , $C_M$ , $C_S$ , $C_D$ , would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, §§2.2 and 3.3, pp. 19–23 and 49–60. Publisher repository.

9 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Outline of an Algorithm for Integer Solutions to Linear Programs: The Fractional Cut (3) Cuts Off the Simplex Solution but Keeps Every Nonnegative Integer Solution and the Integer Maximum of wResearch Paper

Motivation

Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.

The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.

Setting

A tableau is a finite array of real numbers $a'_{i,j}$ . Row $0$ represents the objective variable $w$ ; rows $1,\ldots,m$ represent $x'_1,\ldots,x'_m$ . Column $0$ holds constants; columns $1,\ldots,n$ multiply the negatives of the variables $t'_1,\ldots,t'_n$ . A solution of (2) is a pair $(x',t')$ satisfying

x'_i=a'_{i,0}+\sum_{j=1}^{n}a'_{i,j}(-t'_j),\qquad 0\le i\le m.

The original integer program requires $w=x'_0$ , every $x'_i$ , and every $t'_j$ to be nonnegative integers. The simplex solution of this tableau has $t'=0$ and $x'_i=a'_{i,0}$ . It is a real tableau solution, whether or not any of its coordinates are integers.

Choose a row $i_0$ whose constant $a'_{i_0,0}$ is not an integer. For each coefficient let $n'_{i_0,j}=\lfloor a'_{i_0,j}\rfloor$ be the greatest integer at most that coefficient, and let $f'_{i_0,j}=a'_{i_0,j}-n'_{i_0,j}$ be its fractional part. Equation (3) defines a new variable

s_1=-f'_{i_0,0}-\sum_{j=1}^{n}f'_{i_0,j}(-t'_j).

The augmented system (2)* adds this equation to the tableau. Feasibility now also requires $s_1\ge0$ ; an integer solution additionally requires $s_1\in\mathbb Z$ . For example, the one row relation $x'=\tfrac12-\tfrac12t'$ admits the integer solution $(x',t')=(0,1)$ , and its cut value is $s_1=0$ . At the simplex point $t'=0$ , the same cut value is $-\tfrac12$ .

Formalization targets

Fractional cut and integer optimum

The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing $\mathcal I_2$ and $\mathcal I_{2^*}$ for the two sets of nonnegative integer solutions, the correspondence is

(x',t')\in\mathcal I_2\quad\Longleftrightarrow\quad (x',t',s_1(x',t'))\in\mathcal I_{2^*}.

Every member of $\mathcal I_{2^*}$ has the displayed cut value for $s_1$ , and the projection that drops $s_1$ leaves $w$ unchanged. Consequently a real $W$ is the greatest attained $w$ value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.

Supporting claims

The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving $s_1$ integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.

Significance

The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.

This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.

Difficulty

The cut value is visibly at least $-f'_{i_0,0}$ when the nonbasic variables are nonnegative, but that inequality alone does not give $s_1\ge0$ : the right side is negative for the chosen row. The key additional statement is that the real expression for $s_1$ is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.

Formalization scope

Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases $m=0$ and $n=0$ ; row $0$ is $w$ , column $0$ is the constant column, and Lean's Fin n index $j$ denotes the paper's $t'_{j+1}$ . The selected row can be row $0$ in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and $w$ is integral in the stated problem. Every variable, including $w$ and the added $s_1$ , is required to be nonnegative and integral in an integer solution.

The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained $w$ values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving $w$ , and equivalence of greatest attained $w$ values, respectively.

The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the $m+n+2$ equation bound and deletion of re-entering $s$ variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.

Selected references

Ralph E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the American Mathematical Society 64(5), 1958, 275–278. DOI: 10.1090/S0002-9904-1958-10224-4.
George B. Dantzig, R. Fulkerson, and S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 1954, 393–410. DOI: 10.1287/opre.2.4.393.

7 thms2 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems I: Five Equivalent Characterizations of a Transient Markov Decision Problem, among Them Contraction and a Finite Linear ProgramTextbook

Motivation

Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.

The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.

Setting

Let $E$ be a finite nonempty state space of size $N$ . For every state $i$ , let $A(i)$ be a nonempty finite set of actions. Choosing $a\in A(i)$ gives the transition number $p_{iaj}\ge0$ to state $j$ , with $\sum_jp_{iaj}\le1$ . The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.

A policy $R$ specifies, at each epoch $t\ge1$ , a probability distribution on $A(i_t)$ after the full history $(i_1,a_1,\ldots,a_{t-1},i_t)$ . It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy $f^\infty$ chooses a single admissible action $f(i)$ in state $i$ at every epoch. Write $P_R(X_t=j\mid X_1=i)$ for the probability of state $j$ at epoch $t$ from initial state $i$ . The policy is transient when $\sum_{t\ge1}P_R(X_t=j\mid X_1=i)<\infty$ for every pair $i,j$ . Kallenberg, pp. 20–23.

The finite-horizon survival recursion starts from $y_i^0=1$ and sets $y_i^t=\max_{a\in A(i)}\sum_jp_{iaj}y_j^{t-1}$ for $t\ge1$ . A model is contracting if there is a strictly positive vector $\mu$ and a scalar $0\le c<1$ for which $\sum_jp_{iaj}\mu_j\le c\mu_i$ for every admissible $(i,a)$ . These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.

Formalization targets

Five equivalent conditions

For any fixed $\beta_j>0$ , Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; $\max_i y_i^N<1$ ; contraction; and existence of a finite solution of

\max\left\{\sum_{i\in E}\sum_{a\in A(i)}x_{ia}:\ \sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}\le\beta_j\ (j\in E),\quad x_{ia}\ge0\right\}.

“Finite solution” means an attained finite optimum. The $\beta_j$ are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count $N$ is the exponent in $y^N$ , and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.

Supporting targets

The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:

Theorem 2.5.1 (Derman–Strauch) and its Corollary 2.5.1: for a fixed initial distribution, a memoryless policy reproduces the state-action probabilities $P_R(X_t=j,Y_t=a\mid X_1=i)$ of any policy or of any countable mixture of policies.
Lemma 3.2.1: under Assumption 3.2.1, $\lim_{\alpha\uparrow1}v_i^\alpha(R)=v_i(R)$ in $[-\infty,+\infty]$ .
Theorem 3.2.1: under Assumption 3.2.1 there is a pure stationary policy $f^\infty$ with $v(f^\infty)=v$ , where $v_i=\sup_Rv_i(R)$ .
Theorem 3.2.2: if $v$ is p-summable, then $v_i=\max_{a\in A(i)}\{r_{ia}+\sum_jp_{iaj}v_j\}$ .
Theorem 3.2.3: if some policy is transient, some pure stationary policy is transient.
Lemma 3.2.2: $y_i^t=\sup_R\sum_jP_R(X_{t+1}=j\mid X_1=i)$ , attained by the policy $(f_t,f_{t-1},\dots,f_1,f_1,\dots)$ built from maximizers of the recursion.

Assumption 3.2.1 says that every policy's expected total reward $v_i(R)=\lim_T\sum_{t\le T}v^t_i(R)$ exists in $[-\infty,+\infty]$ ; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.

Significance

The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only $N$ recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.

The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.

Difficulty

Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, $y_i^N<1$ is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use $\le\beta_j$ , and finite value includes attainment. Kallenberg, pp. 41–45.

Formalization scope

States are Fin N with $N>0$ , and actions form one finite ambient type with a nonempty admissible subset $A(i)$ at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch $t=1$ is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.

The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums $\sum_jp_{iaj}x_j$ of extended reals are only asserted for p-summable $x$ , where no $+\infty$ and $-\infty$ meet with positive coefficients; the convention $0\cdot(\pm\infty)=0$ is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight $\mu$ and requires $0\le c<1$ ; it does not normalize $\mu$ to the all-ones vector. The $N$ -step test uses the cardinality of the original state space.

All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
C. Derman and R. E. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699618
A. F. Veinott Jr., Discrete dynamic programming with sensitive discount optimality criteria, Annals of Mathematical Statistics 40 (1969), 1635–1660. https://doi.org/10.1214/aoms/1177697379
E. V. Denardo and U. G. Rothblum, Optimal stopping, exponential utility, and linear programming, Mathematical Programming 16 (1979), 228–244. https://doi.org/10.1007/BF01582110
A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25 (1979), 352–362. https://doi.org/10.1287/mnsc.25.4.352

12 thms2 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems III: Contracting Dynamic Programming — Pure, Stationary, Markov and General Policies Span One State-Action Frequency PolytopeTextbook

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$ . Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$ . A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$ . A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$ , $C_M$ , $C_S$ , and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$ , with $\beta_i\ge0$ and $\sum_i\beta_i=1$ , write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$ , $K(M)$ , $K(S)$ , and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

\sum_{a\in A(j)}x_{ja} -\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}=\beta_j \qquad(j\in E).

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$ , and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

\overline{K(D)}=K(S)=K(M)=K=P.

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$ , different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$ . The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository copy.

6 thms2 active usersReviewed

Algorithmic Game Theory Complexity Theory Linear Optimization+1·Captain: mikedeng1

The Polynomial Hierarchy and a Simple Model for Competitive Analysis: Every Optimum of the (p+1)-Level Linear Game J'(F) Is Binary, with x(F) = 1 iff the Σ_p Sentence (3.3) HoldsResearch Paper

Why multi-level programs are hard

Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.

R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a $(p+1)$ -level linear program with fixed criteria can encode the truth of a $\Sigma_p$ quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the $\Sigma_p$ -hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case $p=1$ .

Setting

A multi-level program has real variables $x=(x^1,\dots,x^p)$ , a feasible set $S_0$ (a polyhedron $\{x: \sum_i A^ix^i\ge b\}$ in the linear case), and players $p,p-1,\dots,1$ who move in that order; player $i$ controls $x^i$ and minimises a fixed linear criterion $c^ix$ . The solution sets are defined from the last mover upwards: $S_1$ is the set of $x\in S_0$ at which player 1's criterion is minimal given the choices of all earlier movers, and in general $S_{j}$ keeps the points of $S_{j-1}$ minimising $c^jx$ among the points of $S_{j-1}$ that agree with $x$ on $x^{j+1},\dots,x^p$ . The value is $c^px$ on $S_p$ , when $S_p\neq\emptyset$ . The sets $S_j$ can be empty even when $S_0$ is a nonempty polytope: the paper's four-level Example has $S_4=\emptyset$ because $S_3$ is not closed.

A propositional formula $F$ over blocks of atoms $X_1,\dots,X_p$ (block $X_k$ has $n_k$ atoms) is encoded by the linear system $L_F$ : one variable $x(G)\in[0,1]$ per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for $\vee$ , $\wedge$ , $\neg$ . The quantifier of block $X_k$ is $Q_k=\exists$ when $p-k$ is even, so

(\exists X_p)(\forall X_{p-1})\cdots(Q_1X_1)\,[F(X_1,\dots,X_p)=1] \qquad (3.3)

is a $\Sigma_p$ sentence.

The game $J'(F)$ adds a bookkeeper, player $0$ , who moves last. Player $k\ge1$ controls the atoms of $X_k$ , and player $1$ also controls auxiliary variables $y$ ; the bookkeeper controls the $x(G)$ , a variable $u$ fixed to $1$ , and auxiliary variables $z$ . Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions $Z_k=1-x(F)+2\sum_jP(x_{kj})$ (or $x(F)+\dots$ for universal $Q_k$ ) and $Z_1=(1-x(F))+fr(1-x(F))+10L\sum_j fr(x_{1j})+\dots$ , where $L$ is the length of $F$ , $fr(x)=\min\{x,1-x\}$ , and $P(x)=1$ at $x\in\{0,1\}$ , $2$ otherwise.

Formalization targets

Goal: Theorem 4.5 ( $p\ge2$ )

Let $S$ be the set of optimal solutions $S_{p+1}$ of $J'(F)$ . Then $S\neq\emptyset$ ; at every optimum all atom variables and all $x(G)$ are binary; and

x(F)=1 \iff (3.3)\ \text{holds},\qquad \text{value}(J'(F)) = 2n_p+1-x(F).

Moreover, when (3.3) holds, $v\in\mathbb R^{n_p}$ is player $p$ 's block in some optimum iff $v$ is binary and the $\Pi_{p-1}$ sentence (4.17) holds at the truth valuation of $v$ .

Milestones

In attack order: Lemma 3.1 (correctness of $L_F$ on binary inputs); Lemma 4.1 (robustness of $L_F$ near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities $z=|2y-x|$ and $z=fr(x)$ in $S_1$ ; (4.2) and (4.3) (player 1's and player $k$ 's responses on the gadgets); Lemma 4.4 (the induction on $k$ with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value $0$ iff $(\exists X_1)F$ ), the §2 Example, and Proposition 3.2 (the pure binary game $J(F)$ ).

Significance

The theorem shows that deciding the value of a $(p+1)$ -level linear program with fixed criteria is at least as hard as deciding $\Sigma_p$ sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once $p\ge2$ , and even recognising an optimal move is $\Pi_{p-1}$ -hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.

The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the $\wedge$ , $\neg$ cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable $z$ has no upper bound).

Difficulty

The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game $J(F)$ (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight $10L$ , and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.

Formalization scope

Players are indexed from $0$ ; player $i$ optimises at level $i+1$ . In $J'(F)$ the players are $0,\dots,p$ as in the paper; in the §2 Example and in $J(F)$ the paper's player $i$ is index $i-1$ . Blocks are 0-based: block k : Fin p is the paper's $X_{k+1}$ , owned by player $k+1$ in $J'(F)$ .
solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires $S_N\neq\emptyset$ ; the value $+\infty$ is not modelled.
Formulas use $\neg,\wedge,\vee$ (the paper rewrites $\to$ as $\neg G_1\vee G_2$ ); the length counts atoms and connectives. Data are real; the paper's rationality assumption plays no role in the statements.
The bookkeeper controls the $x(G)$ and has criterion " $+z$ on (4.1) gadgets, $-z$ on (4.6) gadgets, and $+x(G)$ for each non-atomic subformula," as stated on p. 155. The (4.1) variable $z$ has no upper bound. The constant $1$ of (4.4)/(4.7) is the variable $u$ with $u=1$ .
"Binary value, zero iff $F\in B_p$ " is stated exactly: the value is $2n_p+1-x(F)$ , and $x(F)=1$ iff (3.3). "All optimal solutions are binary" covers the atom variables and the $x(G)$ , not the gadget variable $z$ , which equals $2$ at $y=1$ , $\xi=0$ .
The goal is not trivialisable: its first conjunct asserts that the optimal set is nonempty, which fails for general multi-level programs (the §2 Example), so the remaining conjuncts are not vacuous.

A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.

Selected references

R. G. Jeroslow, The polynomial hierarchy and a simple model for competitive analysis, Mathematical Programming 32 (1985) 146–164. https://doi.org/10.1007/BF01586088
W. Candler and R. Townsley, A linear two-level programming problem, Computers & Operations Research 9 (1982) 59–76. https://doi.org/10.1016/0305-0548(82)90006-5
J. F. Bard and J. E. Falk, An explicit solution to the multi-level programming problem, Computers & Operations Research 9 (1982) 77–100. https://doi.org/10.1016/0305-0548(82)90007-7
L. J. Stockmeyer, The polynomial-time hierarchy, Theoretical Computer Science 3 (1976) 1–22. https://doi.org/10.1016/0304-3975(76)90061-X

13 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Shock Models and Wear Processes III: The First Passage Time of a Nondecreasing Markov Wear Process Above a Fixed Level Has an IHRA DistributionResearch Paper

Motivation

Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?

Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process $\{Z(t), t \ge 0\}$ and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.

A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space. "Decreasing" means non-increasing throughout.

A survival function $\bar F$ is IHRA if $t \mapsto [\bar F(t)]^{1/t}$ is decreasing on $t > 0$ (p. 631). For an exponential life, $[\bar F(t)]^{1/t}$ is constant. IHRA says the average failure rate over $[0, t]$ never decreases.

Dependent damages. Let $X_1, X_2, \dots$ be nonnegative random variables, the damages caused by successive shocks, and let $Z_0 = 0$ and $Z_k = X_1 + \dots + X_k$ . The paper's conditions (p. 636) are:

(4.3) the conditional law of $X_k$ given $X_1, \dots, X_{k-1}$ depends only on $Z_{k-1}$ ;
(4.4) $P\{X_k \le u \mid Z_{k-1} = z\}$ is decreasing in $z \ge 0$ (accumulated damage lowers resistance);
(4.5) $P\{X_k \le u \mid Z_{k-1} = z\} \ge P\{X_{k+1} \le u \mid Z_k = z\}$ for $z \ge 0$ (later shocks are more severe).

Wear process. $Z(t)$ is the wear accumulated in $[0, t]$ . The conditions (pp. 640–641) are:

(4.8) $Z(0) = 0$ and $Z(t + \Delta) - Z(t) \ge 0$ for all $t, \Delta \ge 0$ , with probability one;
(4.9) $\{Z(t), t \ge 0\}$ is a Markov process;
(4.10) $P\{Z(t + \Delta) - Z(t) \le u \mid Z(t) = z\}$ is decreasing in both $z$ and $t$ in the region $t \ge 0$ , $z \ge 0$ , $\Delta \ge 0$ .

The first passage time above a level $x$ is $T_x = \inf\{t : Z(t) > x\}$ . Its survival function is $\bar H_x(t) = P\{T_x > t\}$ , and $F_t(x) = P\{Z(t) \le x\}$ is the distribution function of the wear at time $t$ .

Formalization targets

Goal: Theorem 4.10 (p. 641)

If $\{Z(t), t \ge 0\}$ satisfies (4.8), (4.9) and (4.10), then for every level $x$

t \longmapsto \big[\bar H_x(t)\big]^{1/t} \text{ is decreasing on } t > 0,

that is, $T_x$ has an IHRA distribution.

Milestones

Lemma 4.1b (p. 637): under (4.3)–(4.5), $[P\{X_1 + \dots + X_k \le x\}]^{1/k}$ is decreasing in $k = 1, 2, \dots$ .
Proof of Theorem 4.10, first claim (a): for $\Delta > 0$ , the grid increments $X_i = Z(i\Delta) - Z((i-1)\Delta)$ satisfy (4.3)–(4.5).
Proof of Theorem 4.10, first claim (b): $[F_{k\Delta}(x)]^{1/(k\Delta)}$ is decreasing in $k = 1, 2, \dots$ .
Proof of Theorem 4.10, second claim: $[F_s(x)]^{1/s} \ge [F_t(x)]^{1/t}$ whenever $0 < s \le t$ .
Proof of Theorem 4.10, third claim: $\bar H_x(t) = \lim_{\varepsilon \downarrow 0} F_{t+\varepsilon}(x)$ , under (4.8) alone.

An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate $\lambda > 0$ with damages satisfying (4.3)–(4.5) give an IHRA life $\bar H(t) = \sum_k e^{-\lambda t} (\lambda t)^k / k! \cdot P\{Z_k \le x\}$ .

Significance

The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities $\bar P_k$ with $\bar P_k^{1/k}$ decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.

Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.

Difficulty

The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of $X_{k+1}$ given $(X_1, \dots, X_k)$ . Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of $Z_k$ . The extension from rational to arbitrary ratios $s/t$ uses the monotonicity of paths. The identification of $\bar H_x(t)$ as a right limit of $F_{t+\varepsilon}(x)$ needs the pathwise reading of (4.8). The natural first idea, approximating $Z$ by a compound Poisson process, would add hypotheses the theorem does not have.

Formalization scope

All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:

Probability space. A measure pr with IsProbabilityMeasure. Time is $\mathbb R_{\ge 0}$ ; $Z : \mathbb R_{\ge0} \to \Omega \to \mathbb R$ with every $Z(t)$ measurable.
(4.8) is read pathwise. Almost every path has $Z(0) = 0$ and is nondecreasing. The paper's "for all $t, \Delta \ge 0$ with probability one" is ambiguous in quantifier order; this reading is the one used by the proof's equivalence " $T_x > t$ iff $Z(t+\varepsilon) \le x$ for some $\varepsilon > 0$ ".
(4.9) is the Markov property for the natural filtration $\sigma(Z(r), r \le s)$ : $P(Z(t) \in B \mid \mathcal F_s) = P(Z(t) \in B \mid Z(s))$ a.s. for $s \le t$ and Borel $B$ .
Conditional probabilities are explicit versions. $P\{X_{k+1} \le u \mid Z_k = z\}$ and $P\{Z(t+\Delta) - Z(t) \le u \mid Z(t) = z\}$ are the values on $(-\infty, u]$ of Markov kernels $\kappa$ that agree almost everywhere with Mathlib's condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions $z \ge 0$ , $t \ge 0$ . "Is decreasing in $z$ " is read as "has a version decreasing in $z$ ".
Nonnegativity of damages is almost sure.
Index base. Lean's X i is the paper's $X_{i+1}$ , and the kernel κ k describes $X_{k+1}$ given $Z_k$ .
First passage time $T_x$ takes values in $[0, \infty]$ and may be infinite with positive probability; it is not assumed finite. $\bar H_x(t) = 1$ for $t < 0$ . The level $x$ ranges over all reals.
Powers $[\,\cdot\,]^{1/t}$ , $[\,\cdot\,]^{1/k}$ , $[\,\cdot\,]^{1/(k\Delta)}$ are real powers with real exponents.

Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of $Z(t)$ are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process $Z(t) = t$ satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).

Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.

Selected references

J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, Ann. Probability 1(4) (1973) 627–649. https://doi.org/10.1214/aop/1176996891
Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-out for Components and Systems, Ann. Math. Statist. 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
R. C. Morey, Stochastic Wear Processes, Technical Report ORC 65-16, Operations Research Center, University of California, Berkeley, 1965 (cited on p. 640 of Esary, Marshall and Proschan).
R. E. Barlow and F. Proschan, Statistical Theory of Reliability and Life Testing, Holt, Rinehart and Winston, 1975.

7 thms2 active usersReviewed

Dynamic Programming Linear Optimization Markov Chain+1·Captain: mikedeng1

Linear Programming and Markov Decision Chains 3: The Representative of a Pure Stationary Policy Is an Extreme Point of the Dual LPResearch Paper

Linear programs for average-reward Markov decision chains

A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.

In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.

Timeline:

1960: Manne; de Ghellinck; d'Epenoux. The linear program for unichain average-reward problems, with pure policies at the vertices.
1962: Blackwell. The limit matrix $P^*$ and deviation matrix $D$ of a finite stochastic matrix, and their identities (Ann. Math. Statist. 33).
1968–1970: Denardo and Fox; Denardo. Multichain problems by a sequence of linear programs.
1979: Hordijk and Kallenberg. A single dual pair for the multichain case; representatives of stationary policies; Theorem 10.

Setting

The state space $E$ is finite. Each state $i$ has a finite nonempty set $A(i)$ of actions; action $a$ in state $i$ earns $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$ , $\sum_j p_{iaj}=1$ . Fix weights $\beta_j>0$ with $\sum_j\beta_j=1$ .

The dual linear program has one pair of variables $x_{ia},y_{ia}$ for each state $i$ and each admissible action $a\in A(i)$ . Its feasible set consists of the $(x,y)$ with

\textstyle\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\qquad(j\in E),\qquad x,y\ge 0 .

A pure stationary policy $f^\infty$ uses the action $f(i)\in A(i)$ whenever the chain is in state $i$ . Its transition matrix is $P(f)=(p_{if(i)j})$ . For a stochastic matrix $P$ , the limit matrix $P^*=\lim_n\frac1n\sum_{k=1}^nP^{k-1}$ exists, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$ . A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set $T$ collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write $E_1,\dots,E_m$ for the ergodic sets of $P(f)$ .

The representative of $f^\infty$ is

x_{ia}(f)=[\beta^TP^*(f)]_i\,\delta_{af(i)},\qquad y_{ia}(f)=[\beta^TD(f)+\gamma^TP^*(f)]_i\,\delta_{af(i)},

with $\gamma_l=0$ for $l\in T$ and, for $l\in E_j$ , $\gamma_l=\max_{i\in E_j}\big(-\sum_k\beta_kd_{ki}\big)\big/\sum_{k\in E_j}p^*_{ki}$ . The paper defines the same formulas for randomized stationary policies $\pi$ , with $\pi_{ia}$ in place of $\delta_{af(i)}$ .

Formalization targets

Goal: Theorem 10 (p. 361)

(x(f),y(f))\ \text{is an extreme point of the feasible set of the dual linear program}

for every finite Markov decision chain, every positive probability vector $\beta$ and every pure stationary policy $f^\infty$ . The statement contains feasibility of the representative.

Milestones

§3.3, pp. 359–360: the representative $(x(\pi),y(\pi))$ of any stationary policy is feasible.
Proof of Theorem 10, p. 362: for a stochastic $P$ , every solution of $x^T(I-P)=0$ , $x^T+y^T(I-P)=\beta^T$ (system (7)) satisfies $x^T=\beta^TP^*$ and $y^T=\beta^TD+y^TP^*$ .
Proof of Theorem 10, p. 362: such a solution has $y_i=(\beta^TD)_i$ for $i\in T$ .
Proof of Theorem 10, p. 362: on each ergodic set $E_k$ of $P(f)$ there is a state $i(k)$ with $y_{i(k)f(i(k))}(f)=0$ .
Proof of Theorem 10, p. 362 (Chung, p. 33): a row vector $z$ with $z_i=\sum_{l\in E_k}z_lp_{li}$ on an ergodic set $E_k$ that vanishes at one state of $E_k$ vanishes on all of $E_k$ .

Significance

Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.

The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of $\gamma$ : the paper prints the denominator of $\gamma_l$ as $\sum_k p^*_{ki}$ , a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, $0\to1\to1$ : $y_1=-\beta_0/2$ ). The denominator $\sum_{k\in E_j}p^*_{ki}$ is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.

Difficulty

Feasibility is a calculation with the identities $PP^*=P^*P=P^*P^*=P^*$ and $(I-P)D=I-P^*$ . Extremality is the substance. Restricted to the pairs $(i,f(i))$ , the constraints become the square system (7) in the state variables, and system (7) determines $x$ and the transient part of $y$ , but on each ergodic set it determines $y$ only up to adding a multiple of the stationary distribution of that class: the matrix $I-P$ is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of $\gamma$ matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of $P^*$ , uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets $A(i)$ (nonempty), transition probabilities nonnegative with unit row sums. $P^*$ and $D$ are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.
The dual variables are functions on the subtype of admissible state–action pairs, so non-admissible actions have no coordinates. The feasible set is a subset of $(\mathrm{Pair}\to\mathbb R)\times(\mathrm{Pair}\to\mathbb R)$ and "extreme point" is Mathlib's Set.extremePoints ℝ. Membership in it includes feasibility.
Row vectors act by vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent $l$ is the set of states accessible from $l$ . The maximum in $\gamma$ is a Finset.sup' over that finite nonempty set.
$\gamma$ uses the corrected denominator $\sum_{k\in E_j}p^*_{ki}$ . A formalization with $\gamma=0$ , or one in which the non-admissible coordinates of the program are free, is a different and false or trivial statement and is ruled out.
Stationary randomized rules are nonnegative weights on $A(i)$ summing to one; the pure rule of $f$ is the indicator of $f(i)$ .
Useful contributions: the class decomposition of a finite stochastic matrix (closed classes, $p^*_{ki}=0$ for transient $i$ , positivity of $p^*_{ii}$ on recurrent states), uniqueness of invariant vectors on a closed communicating class, and proofs of Blackwell's Lemma 1(a), 1(d). All of these are reusable beyond this mission.

Selected references

A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
E. V. Denardo and B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259

9 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

The Relation between Customer and Time Averages in Queues: H = λG on Every Sample Path When 0 < λ < ∞, G < ∞ and Each f_n Vanishes Outside [t_n, t_n + s_n] with s_n/n → 0Research Paper

Motivation

Little's law $L = \lambda W$ says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average $H$ and a customer average $G$ , of the form $H = \lambda G$ .

Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the $L = \lambda W$ theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.

Timeline.

1961: Little proves $L = \lambda W$ under stationarity assumptions (Little 1961).
1971: Brumelle proves $H = \lambda G$ under conditions (v.a), (v.b) on the tails of the $f_n$ (J. Appl. Prob. 8, 508–520).
1972: Stidham gives a new proof of $L = \lambda W$ , including the lemma relating $N(t)/t$ and $t_n/n$ (Stidham 1972).
1974: Stidham proves $L = \lambda W$ on each sample path, assuming each sojourn is one uninterrupted interval (Stidham 1974).
1980: Heyman and Stidham prove $H = \lambda G$ on every sample path under the support condition below, and give the counterexample. The paper notes that its Theorem 1 is weaker than the sample-path version of Brumelle's theorem, with hypotheses stated directly on the sample path.

Setting

Fix one sample path. Customers $n = 1, 2, \ldots$ arrive at epochs $0 \le t_1 \le t_2 \le \cdots$ ; ties are allowed. The arrival count $N(t)$ is the number of $n$ with $t_n \le t$ , and the arrival rate is $\lambda = \lim_{t\to\infty} N(t)/t$ when the limit exists.

Customer $n$ carries a real-valued function $f_n$ on $[0,\infty)$ . Its total is $g_n = \int_0^\infty f_n(t)\,dt$ , and the rate is $h(t) = \sum_{n=1}^\infty f_n(t)$ . The customer average and time average are

G = \lim_{N\to\infty} \frac1N \sum_{n=1}^N g_n, \qquad H = \lim_{T\to\infty} \frac1T \int_0^T h(t)\,dt .

When $f_n$ is the indicator of $[t_n, t_n + W_n)$ , $g_n = W_n$ is the sojourn time and $h(t)$ is the number in system, so $H = \lambda G$ is $L = \lambda W$ .

The ASSUMPTION of the paper is that for each $n$ there is $s_n \in [0,\infty)$ with

(i) $f_n(t) = 0$ for $t \notin [t_n, t_n + s_n]$ ;
(ii) $s_n / n \to 0$ .

For signed $f_n$ write $f_n^+ = \max[0, f_n]$ , $f_n^- = \max[0, -f_n]$ , and let $g_n^\pm$ , $h^\pm$ , $G^\pm$ , $H^\pm$ be the corresponding totals, rates and averages.

Formalization targets

Goal: Theorem 2 (p. 986)

Assume (i), (ii) and (v) $\int_0^\infty |f_n(t)|\,dt < \infty$ for every $n$ . If $\lambda$ , $G^+$ and $G^-$ exist with $0 < \lambda < \infty$ and $G^\pm < \infty$ , then $G$ exists, equals $G^+ - G^-$ , $H$ exists, and

H = \lambda G. \tag{1}

Milestones

(2): for $0 < \lambda < \infty$ , $N(t)/t \to \lambda$ if and only if $t_n / n \to \lambda^{-1}$ .
(3): for $f_n \ge 0$ , $V(T) \le \int_0^T h(t)\,dt \le U(T)$ , where $U(T)$ sums $g_n$ over arrived customers and $V(T)$ over customers with $t_n + s_n \le T$ .
(4): $\lambda G = \lim_{t\to\infty} U(t)/t$ .
$s_n / t_n \to 0$ , and $\lim U(t)/t = \lim V(t)/t$ .
Theorem 1 (p. 985): for $f_n \ge 0$ under (i)–(iv), $H = \lambda G$ .
The identity $\int_0^T h^+ - \int_0^T h^- = \int_0^T h$ and (6): $G = G^+ - G^-$ , $H = H^+ - H^-$ .

Companion results

The §3 counterexample: $t_n = n$ , indicator $f_n$ with $g_n = 1$ , so $\lambda = G = 1$ , but $H = \log 2$ ; its support span $s_n = n$ satisfies (i) and fails (ii).
Corollary 3 (p. 988): if $\lambda(\omega) = \lambda$ is constant, the ensemble averages satisfy $\int H\,dP = \lambda \int G\,dP$ .
$G = W < \infty$ implies $W_n / n \to 0$ (p. 986), the step by which Theorem 1 contains $L = \lambda W$ .

Significance

The result. $H = \lambda G$ converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different $f_n$ it yields $L = \lambda W$ , the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn $L = \lambda W$ theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite $\lambda$ , $G$ alone do not suffice.

Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case $L = \lambda W$ (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average $\log 2$ , and the ensemble corollary.

Difficulty

The obvious argument, exchanging the time integral of $h$ with the sum over customers, gives $\int_0^T h = \sum_n \int_0^T f_n$ , but a customer that has arrived by $T$ may contribute only part of its total $g_n$ by $T$ . The sandwich $V(T) \le \int_0^T h \le U(T)$ only bounds this loss; the hard step is showing that $U(t)/t$ and $V(t)/t$ have the same limit, which needs $s_n / t_n \to 0$ to compare $V$ at time $t$ with $U$ at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.

For signed $f_n$ the sandwich is not available directly, and the proof splits $f_n$ into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every $[0,T]$ .

Formalization scope

All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.

Conventions:

Customers are indexed from $0$ in Lean; index $n$ is the paper's customer $n+1$ , so $s_n/n \to 0$ is written $s_n/(n+1) \to 0$ .
Arrival epochs are Monotone with $t_0 \ge 0$ ; ties are allowed.
$f_n : \mathbb R \to \mathbb R$ , but only values on $[0,\infty)$ enter: (i) is required only for $t \ge 0$ , $g_n$ integrates over $[0,\infty)$ , and time averages integrate over $[0,T]$ .
(iv) and (v) are stated as integrability of $f_n$ on $[0,\infty)$ ; the page prints (iv) as " $\le \infty$ ", a misprint for " $< \infty$ ".
$N(t)$ is the cardinality of $\{n : t_n \le t\}$ ; $h$ , $U$ , $V$ are infinite sums over all customers.
" $H$ exists" includes integrability of $h$ on every $[0,T]$ .
The page prints (6) as " $G = G^+ - G^+$ "; the stated identity is $G = G^+ - G^-$ , as the proof shows.

Added hypotheses: milestones (3), the $h^\pm$ identity and (6) assume $t_n \to \infty$ , which the paper derives from (2); Corollary 3 assumes $G(\omega)$ is integrable, which its definition of the ensemble average presupposes.

A formalization in which $h$ sums only over arrived customers, or in which a non-integrable $h$ or $f_n$ has integral $0$ , would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.

Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums $\sum_{m=\lceil (k+1)/2\rceil}^{k} 1/m \to \log 2$ . The counting-function lemma (2) and the squeeze for $U$ and $V$ are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

D. P. Heyman and S. Stidham, Jr., The relation between customer and time averages in queues, Operations Research 28(4):983–994, 1980. https://doi.org/10.1287/opre.28.4.983
J. D. C. Little, A proof for the queuing formula: L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
S. Stidham, Jr., L = λW: a discounted analogue and a new proof, Operations Research 20(6):1115–1126, 1972. https://doi.org/10.1287/opre.20.6.1115
S. Stidham, Jr., A last word on L = λW, Operations Research 22(2):417–421, 1974. https://doi.org/10.1287/opre.22.2.417
S. L. Brumelle, On the relation between customer and time averages in queues, Journal of Applied Probability 8:508–520, 1971.

11 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

On Approximate Solutions of Systems of Linear Inequalities: If Ax ≦ b Is Consistent, Every x Has a Solution x₀ with Fₙ(x − x₀) ≦ c·Fₘ((Ax − b)⁺)Research Paper

Motivation

Iterative methods for a system of linear inequalities $Ax\le b$ stop at a vector $\bar x$ that only almost satisfies the system: the violation $(A\bar x-b)^+$ is small but not zero. A user then needs to know that $\bar x$ is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from $\bar x$ to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.

The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.

Timeline.

1952: S. Agmon (The relaxation method for linear inequalities, NAML Report 52-27, NBS; later Canad. J. Math. 6, 1954, doi:10.4153/CJM-1954-037-2) proves the two geometric lemmas on which Hoffman's proof rests, and a bound in the Euclidean/max norm setting.
1952: A. J. Hoffman proves the bound for arbitrary positive homogeneous size functions $F_n$ , $F_m$ , and gives explicit constants in the max and sum norms by way of matrix games.
Later work (Robinson 1973; Güler, Hoffman and Rothblum 1995; Peña, Vera and Zuluaga 2021) extends the bound to perturbed systems, characterises the sharp constant, and studies its computation.

Setting

Let $A=(a_{ij})$ be a real $m\times n$ matrix with rows $A_1,\dots,A_m$ and let $b\in\mathbb R^m$ . The system (1) is $A_i\cdot x\le b_i$ for $i=1,\dots,m$ , briefly $Ax\le b$ ; its solution set is $\Omega=\{x : Ax\le b\}$ , and the system is consistent if $\Omega\ne\emptyset$ . The $i$ th half space is $\{x : A_i\cdot x\le b_i\}$ .

For a real number $a$ , $a^+=a$ if $a\ge0$ and $a^+=0$ otherwise; for a vector, $y^+$ is taken coordinatewise. So $(Ax-b)^+$ records by how much $x$ violates each inequality.

Hoffman measures sizes with a positive homogeneous function $F_k$ on $\mathbb R^k$ : a continuous real function with (i) $F_k(x)\ge0$ and $F_k(x)=0$ only for $x=0$ , and (ii) $F_k(\alpha x)=\alpha F_k(x)$ for $\alpha\ge0$ . Norms are examples, but $F_k$ need not be symmetric, subadditive or convex.

For a set $S$ of rows, $M$ is the $m\times n$ matrix obtained from $A$ by replacing the rows outside $S$ by $0$ , and $\bar y$ keeps the coordinates of $y\in\mathbb R^m$ in $S$ and zeroes the others. "Nearest" always refers to Euclidean distance. The set $E$ consists of the points $x$ outside the cone $\{z : Mz\le0\}$ whose nearest point in that cone is the origin; $K'$ is the cone spanned by the rows of $M$ with the origin removed.

Section 3 uses three norms: $|x|$ (largest absolute coordinate), $\|x\|$ (sum of absolute coordinates) and the Euclidean norm. With $g_{ij}=A_i\cdot A_j$ , $a_S$ is the largest absolute coordinate of a row in $S$ , and $v_S=\min_\lambda\max_{i\in S}\sum_{j\in S}g_{ij}\lambda_j$ over probability vectors $\lambda$ on $S$ , the value of the matrix game $(g_{ij})_{i,j\in S}$ .

Formalization targets

Goal: Hoffman's theorem (Section 2, p. 263)

If $Ax\le b$ is consistent and $F_n$ , $F_m$ are positive homogeneous, there is $c>0$ such that for every $x$ some solution $x_0$ satisfies

F_n(x-x_0)\le c\,F_m\bigl((Ax-b)^+\bigr).

The constant is existential and fixed before $x$ ; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.

Milestones: the proof's lemmas (pp. 263–264)

Lemma 2: if $y$ is the point of $\Omega$ nearest to $x\notin\Omega$ , then $x$ lies outside the intersection $\Omega_S$ of the half spaces active at $y$ , and $y$ is also the point of $\Omega_S$ nearest to $x$ .
Lemma 3: for every set $S$ of rows there is $d_S>0$ with $F_m((Mx)^+)\ge d_S F_n(x)$ for all $x\in E$ .
Lemma 1: there is $e>0$ with $F_m(\bar y)\le e\,F_m(y)$ for all $y$ and all $S$ .
Lemma 4: $K'=E$ .

Milestones: explicit constants (pp. 264–265)

\text{(9)}\quad |x-x_0|\le\frac{a}{v}\,|(Ax-b)^+|\quad\text{if all }A_i\cdot A_j>0,\ v=\min_{i,j}A_i\cdot A_j,\ a=\max_{i,j}|a_{ij}|;

\text{(10)}\quad |x-x_0|\le\frac{a}{w}\,\|(Ax-b)^+\|\quad\text{if } w=\min_i\Bigl(g_{ii}+\sum_{j:\,g_{ij}<0}g_{ij}\Bigr)>0;

\text{(8)}\quad |x-x_0|\le c\,|(Ax-b)^+|,\qquad c=\max_{v_S>0}\frac{a_S}{v_S}.

Each is stated as in the theorem: for every $x$ there is a solution $x_0$ with the bound.

Significance

The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives $(Ax-b)^+$ to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of $A$ through a matrix game.

Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.

Difficulty

For a single $x$ , a bound is trivial: take $x_0$ the nearest solution and choose $c$ accordingly. The whole content is that one $c$ works for all $x$ , including $x$ far from $\Omega$ and $x$ approaching $\Omega$ along every direction. A compactness argument on $\{x : F_n(x)=1\}$ alone fails, because the ratio $F_n(x-x_0)/F_m((Ax-b)^+)$ is not a continuous function of $x$ on a compact set: the nearest solution and the set of active constraints jump as $x$ moves. Lemma 3 needs a positive lower bound on a set $E$ that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since $F_n$ , $F_m$ are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set $S$ can arise in Lemma 2 with $v_S=0$ (e.g. $x_1\le0$ , $-x_1\le0$ in $\mathbb R^2$ with $x=(1,0)$ ), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.

Formalization scope

Vectors are Fin k → ℝ, $A$ is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and $y^+$ is posPartVec y = fun i => max (y i) 0.
$F_n$ , $F_m$ are arbitrary functions satisfying IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at $0$ , positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.
"Nearest" is Euclidean and written with the dot product: $y$ is nearest to $x$ in $\Omega$ if $(x-y)\cdot(x-y)\le(x-z)\cdot(x-z)$ for all $z\in\Omega$ . (Mathlib's dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".
A "subset $S$ of the half spaces" is a Finset (Fin m) of row indices; $M$ keeps all $m$ rows, with zero rows outside $S$ .
In (8)–(10), $|x|$ is ⨆ i, |x i| and $\|x\|$ is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. $v_S$ is defined directly by (7) as a min over the simplex of a max, for nonempty $S$ , so no minimax theorem is needed. In (8), $c$ is the maximum over nonempty $S$ with $v_S>0$ and is $0$ when there is none (only when $A=0$ ). In $w$ , the page's summation range " $j=1,\dots,n$ " is read as ranging over the $m$ rows, since $g$ is indexed by rows.
Consistency is a hypothesis of the goal and of (8)–(10).

The quantifier order $\exists c>0,\ \forall x,\ \exists x_0$ is part of the statement: a version with $c$ chosen after $x$ is trivially true and is not this theorem; likewise $e$ precedes $y$ and $S$ in Lemma 1 and $d_S$ precedes $x$ in Lemma 3.

Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.

Selected references

A. J. Hoffman, On Approximate Solutions of Systems of Linear Inequalities, J. Res. Nat. Bur. Standards 49(4) (1952), 263–265. https://doi.org/10.6028/jres.049.027
S. Agmon, The Relaxation Method for Linear Inequalities, Canad. J. Math. 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
S. M. Robinson, Bounds for error in the solution set of a perturbed linear program, Linear Algebra Appl. 6 (1973), 69–81. https://doi.org/10.1016/0024-3795(73)90007-4
O. Güler, A. J. Hoffman, U. G. Rothblum, Approximations to solutions to systems of linear inequalities, SIAM J. Matrix Anal. Appl. 16(2) (1995), 688–696. https://doi.org/10.1137/S0895479892237744
J. Peña, J. C. Vera, L. F. Zuluaga, New characterizations of Hoffman constants for systems of linear constraints, Math. Program. 187 (2021), 79–109. https://doi.org/10.1007/s10107-020-01473-6

10 thms2 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Approximation Schemes for the Restricted Shortest Path Problem: The Rounding Algorithm Outputs a T-Path of Length at Most (1 + ε)·OPTResearch Paper

Motivation

The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.

Timeline.

1966–1985. Practical exact methods and pseudopolynomial dynamic programs (Joksch 1966; Lawler 1976; Handler and Zang 1980; Aneja, Aggarwal and Nair 1983; Henig 1985).
1987. Warburton gives the first fully polynomial approximation scheme (FPAS) for this problem on acyclic graphs, based on rounding and scaling (Warburton, Oper. Res. 35, 1987).
1992. Hassin gives two faster FPASs: a rounding-and-scaling scheme driven by an approximate decision test (§3–§4), and a strongly polynomial scheme (§5–§6) (Hassin, Math. Oper. Res. 17, 1992).
2001. Lorenz and Raz give a simpler and faster scheme built on the same test-and-search pattern (Lorenz–Raz, Oper. Res. Lett. 28, 2001).

Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.

Setting

A directed graph has vertex set $\{1,\dots,n\}$ , $n\ge 2$ , and edge set $E$ . Following the paper, the vertices are numbered so that every edge $(i,j)\in E$ has $i<j$ ; in particular the graph is acyclic. Each edge carries a positive integer length $c_{ij}$ and a positive integer transition time $t_{ij}$ . A path $p=(v_0,\dots,v_m)$ has length $c(p)=\sum_r c_{v_{r-1}v_r}$ and transition time $t(p)=\sum_r t_{v_{r-1}v_r}$ . For a nonnegative integer $T$ , a $T$ -path is a path from $1$ to $n$ with $t(p)\le T$ , and $\mathrm{OPT}$ is the length of a shortest $T$ -path.

Fix $0<\varepsilon<1$ . For a real $V$ , the rounded lengths are

\tilde c^V_{ij}=\Big\lfloor \frac{c_{ij}(n-1)}{V\varepsilon}\Big\rfloor .

Procedure TEST(V) deletes the edges with $c_{ij}>V$ and answers NO if, for some integer $c<(n-1)/\varepsilon$ , some $1$ – $n$ path in the remaining graph has transition time at most $T$ and rounded length at most $c$ ; otherwise it answers YES.

The Rounding Algorithm keeps bounds $(LB,UB)$ on OPT. Starting from initial bounds $(LB_0,UB_0)$ , Step 1 repeats while $UB>2LB$ : with $V=(LB\cdot UB)^{1/2}$ it sets $LB\leftarrow V$ if TEST(V) = YES and $UB\leftarrow V(1+\varepsilon)$ if TEST(V) = NO. Step 2 outputs a $T$ -path that is shortest for the rounded lengths $\tilde c^{LB}_{ij}=\lfloor c_{ij}(n-1)/(\varepsilon LB)\rfloor$ . The bounds after $k$ passes are written $(LB_k,UB_k)$ .

Formalization targets

Goal: the approximation guarantee of the Rounding Algorithm

If $LB_0>0$ is a lower bound on the length of every $T$ -path, $N$ is a stage at which $UB_N\le 2LB_N$ , and $p$ is a Step 2 output at $LB_N$ , then

c(p)\le (1+\varepsilon)\,c(q)\qquad\text{for every }T\text{-path }q,

that is, $c(p)\le(1+\varepsilon)\,\mathrm{OPT}$ . The initial upper bound $UB_0$ is arbitrary.

Milestones (§3–§4)

Rounding error (§3, p. 38): with $\delta=V\varepsilon/(n-1)$ , $0\le c_{ij}-\delta\tilde c^V_{ij}\le\delta$ for every edge, and $0\le c(p)-\delta\tilde c^V(p)\le V\varepsilon$ for every path.
TEST(V) = NO (§3, p. 38): some $T$ -path has length $<V(1+\varepsilon)$ , so $\mathrm{OPT}<V(1+\varepsilon)$ .
TEST(V) = YES (§3, p. 38): every $T$ -path has length $\ge V$ , so $\mathrm{OPT}\ge V$ .
Bound update (§4, p. 39): along the run, $LB_k>0$ and $LB_k$ is a lower bound on every $T$ -path; if some $T$ -path has length at most $UB_0$ , some $T$ -path has length at most $UB_k$ .
Scaled-optimum error (§4, p. 39): a Step 2 output $p$ at any $LB>0$ satisfies $c(p)\le c(q)+\varepsilon LB$ for every $T$ -path $q$ .

Companion statements

Termination when $(1+\varepsilon)^2<2$ : some stage $N$ has $UB_N\le 2LB_N$ ; and an explicit instance with $\varepsilon=9/10$ on which Step 1 never stops.
Initial bounds (Step 0, p. 39): every $1$ – $n$ path has length between $1$ and the sum of the $n-1$ longest edge-lengths.
Algorithms A and B (§2, pp. 37–38): their recursions compute $f_j(t)$ and $g_j(c)$ , with $\mathrm{OPT}=f_n(T)=\min\{c\mid g_n(c)\le T\}$ .

Significance

The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a $(1+\varepsilon)$ -approximate $T$ -path is computed in time polynomial in the input size and $1/\varepsilon$ . The two ingredients, an approximate decision test that answers "OPT $\ge V$ " or "OPT $<V(1+\varepsilon)$ ", and a geometric search on the ratio $UB/LB$ , are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.

The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when $\varepsilon>\sqrt2-1$ , and proves termination under $(1+\varepsilon)^2<2$ .

Difficulty

The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most $V\varepsilon$ only because a $1$ – $n$ path has at most $n-1$ edges, which follows from the numbering $i<j$ and must be derived for list-encoded paths. The YES case must cover $T$ -paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that $(LB\cdot UB)^{1/2}$ is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for $LB_0$ .

Formalization scope

Representation. Vertices are natural numbers; an instance is a structure with $n$ , a finite edge set of pairs, and length and time functions, with a well-formedness predicate: $n\ge 2$ , every edge $(i,j)$ has $1\le i<j\le n$ , and lengths and times are positive. The requirement $n\ge2$ is not printed: a $1$ – $n$ path and the divisions by $n-1$ presuppose it. Paths are nonempty vertex lists.
Arithmetic. $n-1$ is taken in the reals; $\lfloor\cdot\rfloor$ is the natural-number floor of a nonnegative real; $(LB\cdot UB)^{1/2}$ is the real square root. Bounds and $\varepsilon$ are reals, $T$ is a natural number.
OPT. OPT is never a number in the formal statements, because it is $\infty$ when no $T$ -path exists. "OPT $\ge V$ " is a bound on every $T$ -path, "OPT $<V(1+\varepsilon)$ " is the existence of a $T$ -path, and the goal compares the output with every $T$ -path. Algorithms A and B use values in $\mathbb N\cup\{\infty\}$ .
TEST(V) is defined by the answer the procedure reaches, not through Algorithm B's printed recursion, whose initial condition $g_j(0)=\infty$ is wrong for rounded lengths $0$ ; for $n\ge2$ and $\varepsilon<1$ the answers agree.
The run is the iterate of one pass of Step 1; a stopped state is a fixed point. Step 2 outputs any $T$ -path optimal for the rounded lengths, without pruning edges, as printed.
Added hypothesis. The termination statement assumes $(1+\varepsilon)^2<2$ , which the page does not state; without it the printed loop can run forever, and an explicit instance is included.
Not a trivialization. The goal assumes nothing about TEST's correctness, the rounding error or the lower-bound invariant along the run, and the termination companion shows that its stopping hypothesis is reachable.
Out of scope. The second, strongly polynomial scheme of §5–§6 is not included, because as printed its Partitioning Algorithm can report infeasibility on a feasible instance and formalizing it would require a corrected algorithm that is not the author's. All running-time claims, stated as $O(\cdot)$ bounds under an informal operation count, are also excluded, as are the $V'$ variant of the test points and the scheduling application of §7.
Reusable parts. The list-based path layer with two additive weights, and the correctness of the pseudopolynomial recursions of Algorithms A and B, are independent of the approximation scheme. Contributions of proofs for any milestone or companion are welcome.

Selected references

R. Hassin, Approximation schemes for the restricted shortest path problem, Mathematics of Operations Research 17(1):36–42, 1992. https://doi.org/10.1287/moor.17.1.36
A. Warburton, Approximation of Pareto optima in multiple-objective, shortest-path problems, Operations Research 35(1):70–79, 1987. https://doi.org/10.1287/opre.35.1.70
D. H. Lorenz and D. Raz, A simple efficient approximation scheme for the restricted shortest path problem, Operations Research Letters 28(5):213–219, 2001. https://doi.org/10.1016/S0167-6377(01)00069-4
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

7 thms2 active usersReviewed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

The Ellipsoid Method and Its Consequences in Combinatorial Optimization: With a Weak Separation Oracle, the Rounded Ellipsoid Method Is ε-Optimal After N = 4n²⌈log(2R²‖c‖/(rε))⌉ StepsResearch Paper

Motivation

The ellipsoid method decides questions about a convex set $K \subseteq \mathbb{R}^n$ by maintaining an ellipsoid that contains the relevant part of $K$ and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of $K$ : it only needs, for a query point $y$ , either a confirmation that $y$ is (nearly) in $K$ or a hyperplane (nearly) separating $y$ from $K$ . From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.

The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number $N$ of ellipsoid steps produces an $\varepsilon$ -optimal point.

Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.

Setting

All norms are Euclidean: $\|v\| = \sqrt{v^{\mathsf T}v}$ , and for a symmetric matrix $\|A\|$ is the largest absolute eigenvalue. $S(a_0,\rho)$ is the closed Euclidean ball of radius $\rho$ about $a_0$ , and $S(K,\delta)$ the set of points within distance $\delta$ of $K$ .

A convex body $(K, a_0, r, R)$ consists of a compact convex $K\subseteq\mathbb{R}^n$ , $n\ge 2$ , and $0<r\le R$ with

S(a_0,r)\subseteq K\subseteq S(a_0,R).

A weak separation oracle with precision $\delta>0$ answers a query $y$ either with " $y\in S(K,\delta)$ ", or with a vector $d$ , $\|d\|\ge 1$ , such that $d^{\mathsf T}x\le d^{\mathsf T}y+\delta$ for all $x\in K$ .

Given an objective $c$ and an accuracy $\varepsilon>0$ (with $\varepsilon<r$ and $\|c\|\ge 1$ ), set

N = 4n^2\left\lceil \log\frac{2R^2\|c\|}{r\varepsilon}\right\rceil,\qquad \delta = \frac{R^2\,4^{-N}}{300n},\qquad p = 5N .

Start from $x_0=a_0$ , $A_0=R^2I$ . At step $k$ query the oracle at $x_k$ . If it answers "feasible", $k$ is a feasible index and $a=c$ ; otherwise $a=-d$ . Put $b_k = A_ka/\sqrt{a^{\mathsf T}A_ka}$ and

x_k^* = x_k+\frac{1}{n+1}b_k,\qquad A_k^* = \frac{2n^2+3}{2n^2}\Bigl(A_k-\frac{2}{n+1}b_kb_k^{\mathsf T}\Bigr),

and obtain $x_{k+1}$ , $A_{k+1}$ by rounding $x_k^*$ , $A_k^*$ to $p$ binary digits, keeping $A_{k+1}$ symmetric. The ellipsoids are $E_k=\{x : (x-x_k)^{\mathsf T}A_k^{-1}(x-x_k)\le 1\}$ , and $K_k$ is the set of points of $K$ whose objective value is at least that of every feasible centre found before step $k$ .

In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is $K_k$ , and $E_k$ is the published LinearOptimization.ellipsoid (x k) (A k).

Formalization targets

Goal: Theorem (2.4)

If $j<N$ is a feasible index whose centre is best among the feasible centres, $c^{\mathsf T}x_j=\max\{c^{\mathsf T}x_k : k<N \text{ feasible}\}$ , then

c^{\mathsf T}x_j \ \ge\ \max_{x\in K} c^{\mathsf T}x - \varepsilon .

The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.

Milestones, in attack order

(13): the explicit inverse $(A_k^*)^{-1}=\frac{2n^2}{2n^2+3}\bigl(A_k^{-1}+\frac{2}{n-1}\frac{aa^{\mathsf T}}{a^{\mathsf T}A_ka}\bigr)$ , and $A_k^*\succ 0$ .
Lemma (2.1): $A_0,\dots,A_N$ are positive definite, $\|x_k\|\le\|a_0\|+R2^k$ , $\|A_k\|\le R^22^k$ , $\|A_k^{-1}\|\le R^{-2}4^k$ .
Lemma (2.2): $\mu(E_{k+1}) < e^{-1/(5n)}\mu(E_k)$ .
Lemma (2.3): $K_k\subseteq E_k$ for $k=0,\dots,N$ .
(32): $\mu(K_N)\le\mu(E_N)\le e^{-N/(4n)}\mu(E_0)=e^{-N/(4n)}R^nV_n$ .
(34): the piece above the level $t$ of the cone with base the $r$ -disc through $x_0$ orthogonal to $c$ and apex $y\in K$ has volume $\frac{V_{n-1}r^{n-1}(\zeta-c^{\mathsf T}x_0)}{n\|c\|}\bigl(\frac{\zeta-t}{\zeta-c^{\mathsf T}x_0}\bigr)^n$ , which bounds $\mu(\{z\in K: c^{\mathsf T}z\ge t\})$ from below.

Significance

Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in $n$ , $\log R$ , $\log(1/r)$ , $\log\|c\|$ and $\log(1/\varepsilon)$ . This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.

The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor $(2n^2+3)/(2n^2)$ , or rounding.

Difficulty

For the exact update with factor $n^2/(n^2-1)$ and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by $\delta$ , so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from $A_k^*$ by up to $n2^{-p}$ in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound $R^24^{-k}$ is what controls it. The containment $K_{k+1}\subseteq E_{k+1}$ must absorb both errors, and it is the inflation factor $(2n^2+3)/(2n^2)$ , chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate $e^{-N/(4n)}$ in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.

Formalization scope

$\mathbb{R}^n$ is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds $\|A_k\|\le R^22^k$ , $\|A_k^{-1}\|\le R^{-2}4^k$ are stated as quadratic-form (eigenvalue) bounds. $N$ uses the natural logarithm and the integer ceiling.

The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within $2^{-p}$ entrywise; and data are real rather than rational.

The page's standing assumptions $\varepsilon<r$ , $\|c\|\ge1$ , $n\ge2$ (p. 173) are hypotheses. Two hypotheses are added, because the page's $N$ , $\delta$ and $p$ are absolute numbers and the claims fail at extreme scales:

$R\ge 1$ (Lemmas (2.1)–(2.3), (32), Theorem (2.4)): for $R=r=2^{-1000}$ , $\varepsilon=r/2$ , $n=2$ , rounding can make $A_1=0$ .
$\varepsilon\le1$ (Lemma (2.3), (32), Theorem (2.4)): for $R=r=10^{13}$ , $\varepsilon=0.99r$ , $n=2$ , $\delta>2r$ , and a valid oracle can cut away all of $K$ .

Neither is needed in (13) or (34).

A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the $A_k$ is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is $0$ , assuming it would hide the lemma's content.

Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.

Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.

Selected references

M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1(2) (1981) 169–197. https://doi.org/10.1007/bf02579273
P. Gács, L. Lovász, Khachiyan's algorithm for linear programming, Mathematical Programming Study 14 (1981) 61–68. https://doi.org/10.1007/BFb0120921
L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20 (1979) 191–194 (English translation of the original article).
R. G. Bland, D. Goldfarb, M. J. Todd, The ellipsoid method: a survey, Operations Research 29(6) (1981) 1039–1091. https://doi.org/10.1287/opre.29.6.1039
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Ch. 8. Book record.
S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8 (2015). https://arxiv.org/abs/1405.4980

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Reflected Brownian Motion on an Orthant: The Skorokhod Construction Yields an Adapted, Almost Surely Unique, Time-Homogeneous Markov ProcessResearch Paper

Motivation

Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a $K$ -station network the scaled queue-length vector lives in the nonnegative orthant $\mathbb R^K_+$ ; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general $K$ -station open networks lead exactly to the class of processes studied here.

Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.

Setting

Fix a positive integer $K$ . Vectors in $\mathbb R^K$ are row vectors, indexed by $j=1,\dots,K$ . Let $A$ be a $K\times K$ covariance matrix (symmetric, nonnegative definite), $b\in\mathbb R^K$ a drift vector, and $Q=(q_{ij})$ a nonnegative $K\times K$ matrix with zeros on the diagonal and spectral radius strictly less than one. $S=\mathbb R^K_+$ is the nonnegative orthant.

Let $C$ be the space of continuous paths $x:[0,\infty)\to\mathbb R^K$ with the topology of uniform convergence on compact intervals, and $C_S$ the paths with $x(0)\in S$ . For $x\in C_S$ , the Skorokhod problem asks for $y,z\in C$ with, for every $j$ ,

z_j(t)=x_j(t)+y_j(t)-\sum_{i=1}^K q_{ij}\,y_i(t),\qquad z_j(t)\ge 0,\qquad t\ge0, \tag{5–6}

$y_j$ nondecreasing with $y_j(0)=0$ (7), and $y_j$ increasing only at times $t$ where $z_j(t)=0$ (8). In matrix form, $z=x+y(I-Q)$ . Theorem 1 of the paper shows there is exactly one such pair, written $y=\psi(x)$ , $z=\phi(x)$ .

The process is obtained by feeding a Brownian path into this map. On a probability space $(\Omega,\mathcal F,P)$ let $X$ be a $K$ -dimensional Brownian motion with covariance matrix $A$ , drift $b$ and $X(0)\in S$ almost surely, with $X(0)$ independent of the increments of $X$ . Let $\mathcal F_t=\mathcal F(X(s);0\le s\le t)$ . Set $Y=\psi(X)$ and $Z=\phi(X)$ where $X\in C_S$ , and $Y=Z=0$ on the exceptional null set. $Z$ is reflected Brownian motion on $S$ with reflection matrix $I-Q$ .

Formalization targets

Goal: Corollary 1

There is a family $(\kappa_t)$ of Markov transition kernels on $\mathbb R^K$ , depending only on $(Q,A,b)$ , such that for every such $X$ , $Y$ , $Z$ :

\text{(a)}\quad Y(t),\ Z(t)\ \text{are } \mathcal F_t\text{-measurable},\ t\ge0;

\text{(b)}\quad (Y,Z)\ \text{satisfies (1)–(4) a.s., and any pair satisfying (1)–(4) a.s. equals } (Y,Z) \text{ a.s.};

\text{(c)}\quad P\big[Z(s+t)\in B \mid \mathcal F_s\big]=\kappa_t\big(Z(s),B\big)\ \text{a.s.},\qquad s,t\ge0,\ B \text{ Borel}.

Here (1)–(4) are (5)–(8) for the paths of $X$ , $Y$ , $Z$ . The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.

Milestones

The milestones follow the proof of Theorem 1 on pp. 304–305:

a positive diagonal $\Lambda$ with $\|\Lambda^{-1}Q\Lambda\|<1$ (Veinott scaling);
(5)–(8) are invariant under $(Q,x,y,z)\mapsto(\Lambda^{-1}Q\Lambda,x\Lambda,y\Lambda,z\Lambda)$ ;
the key observation that (5)–(8) are equivalent to $y\in C_0$ , the fixed-point equation $y=\pi(y)$ with $\pi(y)(t)=\sup_{0\le s\le t}[y(s)Q-x(s)]^+$ , and $z=x+y(I-Q)$ ;
the contraction $\|\pi(y)-\pi(y')\|\le\alpha\|y-y'\|$ on $[0,T]$ ;
convergence of the Picard iterates $y^{n+1}=\pi(y^n)$ , $y^0\equiv0$ ;
the Lipschitz bound $\|\psi(x)-\psi(x')\|\le\|x-x'\|/(1-\alpha)$ ;
Theorem 1 itself: existence and uniqueness, non-anticipation (9), continuity (10);
the regeneration property (11): with $x^*(t)=z(T)+x(T+t)-x(T)$ , $y^*(t)=y(T+t)-y(T)$ , $z^*(t)=z(T+t)$ , one has $y^*=\psi(x^*)$ , $z^*=\phi(x^*)$ .

Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.

Significance

Corollary 1 is what makes $Z$ a usable stochastic process: adaptedness and almost-sure uniqueness say $Z$ is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which $Z$ appears as the limit. The pathwise map $\phi$ and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.

The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.

Difficulty

The pathwise part is a contraction argument, but the contraction is not in the original norm: the map $y\mapsto yQ$ need not be a contraction for any standard norm when only the spectral radius of $Q$ is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of $Q$ enters.

For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post- $s$ increments of $X$ from $\mathcal F_s$ , and a kernel that is jointly measurable and independent of the initial law. Conditioning on $\mathcal F_s$ alone, without identifying the future as a fixed functional of $Z(s)$ and an independent Brownian motion, does not give a kernel that is the same for all $s$ .

Formalization scope

$\mathbb R^K$ is Fin K → ℝ (paper index $j$ = Lean index $j-1$ ), with $K\ge1$ ; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times $t\ge0$ are constrained.
Spectral radius $<1$ is rendered as $Q^m\to0$ , the rendering of Reiman84.QueueLength.lemma_1. $A$ is PosSemidef.
(5)–(8) are the published Reiman84.QueueLength.IsReflectionPair; (8) reads " $y_j$ is constant on every interval $[s,t]\subseteq[0,\infty)$ on which $z_j>0$ ". $C_S$ is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from $0$ with drift and covariance is IsDriftedBM.
The norm on $C[0,T]$ is $\sup_{0\le t\le T}\|y(t)\|_\infty$ . The suprema in $\pi$ and in the norm are real suprema, honest only for continuous paths, and every statement using them assumes continuity.
The paper's $\|P\|$ is printed as the maximal row sum. Under the row-vector convention the contraction, Picard and Lipschitz steps need the maximal column sum; with the printed reading the contraction inequality is false (a nilpotent $3\times3$ counterexample is recorded in those items). Veinott scaling is stated as printed; applying it to $Q^\top$ gives the column version.
The Brownian motion is $X=X_0+\xi$ with $\xi$ a drifted Brownian motion from $0$ and $X_0\ge0$ a.s. independent of the whole process $\xi$ . $\mathcal F_t$ is the uncompleted σ-algebra generated by $X(s)$ , $0\le s\le t$ .
$Y$ and $Z$ enter Corollary 1 as hypotheses: a solution of (5)–(8) on $\{X\in C_S\}$ , zero elsewhere. That such processes exist is the existence part of Theorem 1, the referenced open item.
The kernel family is quantified before the probability space, so it cannot depend on $s$ , on $\Omega$ or on the law of $X(0)$ . A version of (c) with a kernel depending on these, with the completed or full σ-algebra in place of $\mathcal F_s$ , or with one-dimensional marginals only, is a different and weaker statement and is ruled out.

Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius $<1$ , and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on $C_S$ , and general lemmas on measurability of continuous path functionals.

Selected references

J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9(2), 302–308, 1981. https://doi.org/10.1214/aop/1176994471
M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3), 441–458, 1984. https://doi.org/10.1287/moor.9.3.441
A. F. Veinott, Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Annals of Mathematical Statistics 40(5), 1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
A. V. Skorokhod, Stochastic Equations for Diffusion Processes in a Bounded Region, Theory of Probability and Its Applications 6(3), 264–274, 1961. https://doi.org/10.1137/1106035
D. W. Stroock and S. R. S. Varadhan, Diffusion Processes with Boundary Conditions, Communications on Pure and Applied Mathematics 24, 147–225, 1971. https://doi.org/10.1002/cpa.3160240206

12 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 1: The Bregman Proximal Point Algorithm Converges to a Zero of a Maximal Monotone OperatorResearch Paper

Motivation

The proximal point algorithm is a way to find a zero of a set-valued monotone operator by repeatedly solving a regularized version of that operator equation. Its classical regularizer is quadratic, so the distance from one iterate to the next is Euclidean. In convex optimization, that geometry can be poorly matched to the domain: the natural iterates may be constrained to a positive orthant, a simplex, or an open set with a meaningful boundary. Eckstein's 1993 paper studies what happens when a Bregman function supplies the regularization instead. The convergence question matters because the later multiplier methods in the same paper are instances of this general iteration. Eckstein (1993) develops the general result before applying it to convex programs.

The result considered here is Theorem 1 of that paper. It concerns an existing infinite run: it states what such a run does, while Theorems 4 and 5 address conditions under which a run can be generated. This separation keeps the convergence assertion precise. The result is known mathematically; the mission asks for a Lean proof of its stated generality, including its alternative when the operator has no zero.

Setting

Work in a finite-dimensional real inner-product space $H$ , representing the paper's $\mathbb R^n$ . A monotone operator $T:H\to 2^H$ associates a set $T(x)$ of vectors with each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ for every $u\in T(x)$ and $v\in T(y)$ , and maximal monotone when its graph has no proper monotone extension. Its domain is $\operatorname{dom}T=\{x:T(x)\ne\varnothing\}$ ; a zero is a point $z$ with $0\in T(z)$ .

Let $S\subseteq H$ be open and $h$ a real function on $\overline S$ . At $y\in S$ , define the Bregman distance

D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle,\qquad x\in\overline S.

It need not be symmetric and is generally not a metric. Definition 1 requires $h$ to be continuously differentiable on $S$ , strictly convex and continuous on $\overline S$ , and to satisfy boundedness of both kinds of partial $D_h$ sublevel sets. Two sequential conditions connect convergence in $H$ to convergence of Bregman distances, including sequences approaching the boundary of $S$ . These six requirements together define a Bregman function with zone $S$ .

A Bregman proximal-point run uses positive parameters $c_k$ and a sequence $x^k\in S$ satisfying

\frac{\nabla h(x^k)-\nabla h(x^{k+1})}{c_k}\in T(x^{k+1}),\qquad k=0,1,\ldots.

This is the inclusion form (4) of the paper's recursion (3). It permits set-valued $T$ and does not assert that a next iterate exists for arbitrary starting data. The model also uses the paper's standing domain condition $\operatorname{dom}T\subseteq\overline S$ .

Formalization targets

The main target is Theorem 1. Assume that the positive parameters have a common positive lower bound and that one of the following conditions holds: (C1) $\overline{\operatorname{dom}T}\subseteq S$ , or (C2) $T=\partial f$ for a proper lower semicontinuous convex extended-valued function $f$ . Then

\begin{aligned} T^{-1}(0)\ne\varnothing &\quad\Longrightarrow\quad x^k\longrightarrow z\text{ for some }z\in T^{-1}(0),\\ T^{-1}(0)=\varnothing\text{ and (C1)} &\quad\Longrightarrow\quad \{x^k:k\ge0\}\text{ is unbounded}. \end{aligned}

The second line retains the paper's extra (C1) requirement. The standing inclusion $\operatorname{dom}T\subseteq\overline S$ has a different direction and role. The milestone list follows Lemma 1 and the three labelled steps of Theorem 1's convergence proof: the resolvent inequality, boundedness of the run when a zero exists, identification of every limit point as a zero, and convergence of the full run. The no-zero alternative remains in the goal because restating that conjunct as a separate milestone would add no independent target.

Significance

Theorem 1 says that the nonlinear iteration cannot remain bounded without approaching a zero under (C1), and that when a zero exists the whole sequence converges under either (C1) or (C2). This is stronger than saying only that accumulation points solve the operator equation. It supplies a common convergence result for the paper's later proximal minimization and multiplier algorithms, where the operator is often a subdifferential and the geometry comes from a nonquadratic $h$ . Eckstein (1993) gives those applications after the general theorem.

A formalization would add a reusable interface for Bregman functions with open zones, including their boundary behavior, and for proximal-point runs of set-valued maximal monotone operators. The published platform definitions of monotone operators and extended-valued convex analysis are reused. The new proof work is the Bregman resolvent estimate and the convergence alternative at Theorem 1's level of generality. No machine-checked proof of this specific theorem is claimed here.

Difficulty

The usual Euclidean proximal-point theorem does not apply directly after changing coordinates by $y=\nabla h(x)$ : the transformed operator need not remain monotone, as the paper observes after Theorem 1. A proof must account for the nonsymmetric $D_h$ , the possible boundary of $S$ , and two distinct ways to identify a limit point as a zero. Under (C1), the point lies where the gradient is continuous; under (C2), the argument uses the subdifferential structure instead. The no-zero case has its own difficulty because boundedness would have to contradict maximal monotonicity without first assuming that a zero exists. The proof cites a closed-graph result for maximal monotone operators and a zero-existence fact for operators with bounded domain; those external facts are groundwork for solvers, not invented milestones.

Formalization scope

Lean uses a finite-dimensional real inner-product space rather than a coordinate-fixed $\mathbb R^n$ . The total function $h:H\to\mathbb R$ is constrained only on $\overline S$ ; its gradient is evaluated only on the open zone $S$ . The Bregman distance is used on $\overline S\times S$ . Definition 1's condition (vi) explicitly places its first sequence in $\overline S$ , the natural domain stated immediately after the definition. The run explicitly keeps every $x^k$ in $S$ and encodes recursion (3) using the equivalent inclusion (4). A positive lower bound on $c_k$ is expressed by one $\varepsilon>0$ with $c_k\ge\varepsilon$ for every $k$ .

The operator $T$ is a published set-valued operator object, with its published notions of monotonicity, maximality, domain, and zeros. The proper and convex extended-valued function in (C2) uses the published epigraph and subgradient definitions, with EReal able to express $+\infty$ . Subdifferentials are built from those definitions. A limit point means a limit along a strictly increasing subsequence, and unboundedness means that the full set of iterates is not bounded. The proof step on p. 207 prints $T^{-1}(0)\subseteq S$ ; the formal Step 1 uses the standing condition $T^{-1}(0)\subseteq\overline S$ , which is sufficient for the Bregman distance and also covers (C2).

The run relation cannot be satisfied by an arbitrary constant sequence: its inclusion must hold at every step, and a zero-free operator under (C1) triggers the unbounded conclusion. Nor does the theorem replace convergence by existence of one convergent subsequence. Reusable contributions include properties of the Bregman resolvent and maximal-monotone graph limits. Theorem 5's separate existence and minimization claims are outside this mission's core.

Selected references

Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI: 10.1287/moor.18.1.202.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

How Many Parts to Make at Once: The Cost per Unit (CX + S)/240M + S/X + C Is Minimized Exactly at the Lot Size X = √(240MS/C)Research Paper

Motivation

Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.

Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.

Setting

A part is used at a regular rate of $M$ units per month (the movement). Each unit costs $C$ dollars (the unit cost), and each order costs $S$ dollars to set up. Parts are made in lots of $X$ units, the lot size. Under regular movement a lot of $X$ is delivered when the stock reaches nothing and is then used up at rate $M$ , so the stock at time $t \ge 0$ (months, from a delivery) is the sawtooth

\operatorname{stock}(t) = X\bigl(1 - \{Mt/X\}\bigr),

with $\{u\}$ the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.

Harris prices a unit in three parts:

the interest charge per piece: the average stock is $X/2$ , its value including set-up is $\tfrac12(CX+S)$ , ten per cent of this is the annual charge, and dividing by the $12M$ units used a year gives $\frac{1}{240M}(CX+S)$ ;
the set-up cost per piece $S/X$ ;
the unit cost $C$ .

The cost per unit is therefore

Y(X) = \frac{1}{240M}(CX + S) + \frac{S}{X} + C,

and the economic lot size is $X^* = \sqrt{240MS/C}$ . In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.

Formalization targets

Goal: the square-root formula

For $M, C, S > 0$ ,

X^* > 0, \qquad Y(X^*) \le Y(X) \text{ for all } X > 0, \qquad Y(X) = Y(X^*),\ X > 0 \implies X = X^* .

This is Harris's claim that the value of $X$ giving the minimum value to $Y$ "reduces to the square root of (240MS divided by C)": $X^*$ is admissible, attains the minimum, and is the only lot size that does.

Milestones: the derivation of $Y$

The long-run average of the sawtooth stock is $X/2$ : $\lim_{T\to\infty}\frac1T\int_0^T \operatorname{stock}(t)\,dt = X/2$ .
The interest charge per piece, built in the paper's steps, equals $\frac{1}{240M}(CX+S)$ , and $Y$ is the sum of the three per-piece costs.

These justify the objective $Y$ , not its minimization; the paper gives no argument for the minimization.

Companion statements

$X^* = K\sqrt M$ with $K = \sqrt{240S/C}$ (p. 948).
The fourfold law: $X^*(M') = 2X^*(M) \iff M' = 4M$ (p. 950).
A lot too small by $d$ costs more than one too large by $d$ : $Y(X^*+d) < Y(X^*-d)$ for $0 < d < X^*$ (p. 949, general form of an observation made on an example).
At the optimum, $S/X^* = CX^*/(240M)$ (p. 948).
The paper's three worked lot sizes 2,190, 6,850 and 48.5, each to its last printed digit (pp. 948–949).

Significance

The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.

Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ( $S/2$ in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is $X/2$ becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.

Difficulty

The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with $\frac{1}{240M}$ meaning $1/(240\cdot M)$ , and the claim includes uniqueness, not only that $X^*$ is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over $[0, T]$ with $T$ not a whole number of cycles, which is where the integration and limit bookkeeping lies.

Formalization scope

All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses $M, C, S > 0$ are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over $X > 0$ . Time is measured in months, and the interest rate is fixed at ten per cent, so the constant $240 = 12 \cdot 2 \cdot 10$ appears as printed; the formula is not generalized to an arbitrary rate.

A trivializing formalization is ruled out: $Y$ is defined as the printed display, not rewritten around $X^*$ ; the average stock is an integral of the stock level, never defined as $X/2$ ; and the goal does not quantify over all real $X$ , where Lean's convention $S/0 = 0$ would make $X = 0$ a spurious minimizer.

The manufacturing interval $T$ and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.

Selected references

F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2):135–136, 152, 1913; reprinted in Operations Research 38(6):947–950, 1990. https://doi.org/10.1287/opre.38.6.947
D. Erlenkotter, Ford Whitman Harris and the economic order quantity model, Operations Research 38(6):937–946, 1990. https://doi.org/10.1287/opre.38.6.937
R. H. Wilson, A scientific routine for stock control, Harvard Business Review 13:116–128, 1934.
Y.-S. Zheng, On properties of stochastic inventory systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87

4 thms2 active usersReviewed

Operations Research Optimization Probability+1·Captain: mikedeng1

Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach 3: Robust Optimal Values and Solution Sets over f-Divergence Balls Are ConsistentResearch Paper

Motivation

Stochastic optimization asks for a decision $x$ in a set $\mathcal X\subset\mathbb R^d$ that minimises an expected loss $E_{P_0}[\ell(x;\xi)]$ when the distribution $P_0$ of the data $\xi$ is known only through a sample $\xi_1,\dots,\xi_n$ . The classical estimator, sample average approximation, replaces $P_0$ by the empirical distribution $\widehat P_n$ . Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to $\widehat P_n$ . Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an $f$ -divergence ball of radius $\rho/n$ and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.

A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).

Setting

Let $\xi_1,\xi_2,\dots$ be i.i.d. random elements of a separable metric space $\Xi$ with law $P_0$ , and let $\widehat P_n$ be the empirical distribution of $\xi_1,\dots,\xi_n$ . Let $\ell:\mathbb R^d\times\Xi\to\mathbb R$ be lower semicontinuous on $\mathcal X\times\Xi$ , with $\ell(x;\cdot)$ measurable for $x\in\mathcal X$ , and let $\mathcal X\subset\mathbb R^d$ be a nonempty closed feasible set, as in the paper's opening setup (p. 1).

The divergence generator $f:[0,\infty)\to\mathbb R\cup\{+\infty\}$ is convex with $f(1)=0$ ; Assumption A asks moreover that $f$ be three times differentiable near $1$ with $f'(1)=0$ and $f''(1)=2$ . For a distribution $P\ll\widehat P_n$ with weights $p_i$ on the sample points, $D_f(P\|\widehat P_n)=\frac1n\sum_i f(np_i)$ . The robust objective and the population objective are

\widehat F_n(x)=\sup_{P\ll\widehat P_n}\Big\{E_P[\ell(x;\xi)] : D_f(P\|\widehat P_n)\le\frac{\rho}{n}\Big\},\qquad F(x)=E_{P_0}[\ell(x;\xi)],

with radius parameter $\rho\ge0$ . Their solution sets are $S^\star_{\widehat P_n}=\operatorname{argmin}_{x\in\mathcal X}\widehat F_n(x)$ and $S^\star_{P_0}=\operatorname{argmin}_{x\in\mathcal X}F(x)$ (display (23)). The inclusion distance from a set $A$ to a set $B$ is $d_\subset(A,B)=\sup_{x\in A}\operatorname{dist}(x,B)$ (display (6)).

Assumption E asks for a measurable envelope $Z\ge0$ with $|\ell(x;\xi)|\le Z(\xi)$ for all $x\in\mathcal X$ and $E_{P_0}[Z^{1+\epsilon}]<\infty$ for some $\epsilon>0$ . A class $\mathcal H$ of functions on $\Xi$ is Glivenko–Cantelli (Definition 2) if $\sup_{h\in\mathcal H}|E_{\widehat P_n}[h]-E_{P_0}[h]|\to0$ almost surely.

Formalization targets

Goal: Corollary 1 (p. 17)

Let Assumptions A and E hold, let $\mathcal X$ be nonempty and compact, and let $\ell(\cdot;\xi)$ be continuous on $\mathcal X$ for every $\xi$ . Then, in outer probability,

\inf_{x\in\mathcal X}\widehat F_n(x)-\inf_{x\in\mathcal X}F(x)\xrightarrow{P^*}0 \qquad\text{and}\qquad d_\subset\big(S^\star_{\widehat P_n},S^\star_{P_0}\big)\xrightarrow{P^*}0 .

Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.

Milestones

Lemma 13 (p. 34): the likelihood-ratio vectors of the ball satisfy $\|np-\mathbb 1\|_2\le\sqrt{\rho C_f}$ uniformly in $n$ , and the bound is of the right order ( $\ge\sqrt{\rho c_f}$ for some $n,p$ ).
(47) (App. E.1, p. 46): $|E_P[\ell]-E_{P_0}[\ell]|\le E_{\widehat P_n}[|L-1|^p]^{1/p}E_{\widehat P_n}[|\ell|^q]^{1/q}+|E_{\widehat P_n}[\ell]-E_{P_0}[\ell]|$ with $q=\min\{2,1+\epsilon\}$ , $p=\max\{2,1+1/\epsilon\}$ .
The display after (47) (p. 46): $E_{\widehat P_n}[|L-1|^p]^{1/p}\le n^{-1/p}\sqrt{\rho C_f}$ .
Theorem 7 (p. 16): if $\{\ell(x;\cdot):x\in\mathcal X\}$ is Glivenko–Cantelli, then

\sup_{x\in\mathcal X}\sup_{P\ll\widehat P_n}\Big\{|E_P[\ell(x;\xi)]-E_{P_0}[\ell(x;\xi)]| : D_f(P\|\widehat P_n)\le\tfrac{\rho}{n}\Big\}\xrightarrow{\text{a.s.}^*}0.

Example 5 (p. 16, from van der Vaart, Asymptotic Statistics, Example 19.8): a class of losses continuous on a compact $\mathcal X$ for almost every $\xi$ , with an integrable envelope, is Glivenko–Cantelli.

Significance

The result. Corollary 1 shows that robustness against a $\rho/n$ -divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over $\mathcal X$ , which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.

Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.

Difficulty

The obvious argument writes $E_P[\ell]-E_{P_0}[\ell]$ as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term $\frac1n\sum_i(np_i-1)\ell(x;\xi_i)$ is the obstacle: the weights $np_i$ are not bounded uniformly in $n$ for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair $(p,q)$ and the uniform $\ell_2$ control of Lemma 13 are what make $1+\epsilon$ moments enough.

For the solution sets, uniform convergence of $\widehat F_n$ to $F$ does not by itself place the minimisers of $\widehat F_n$ near those of $F$ ; compactness of $\mathcal X$ and continuity of $F$ are needed to separate $F$ on the complement of an $\epsilon$ -enlargement of $S^\star_{P_0}$ from its minimum. Measurability is a further obstacle: suprema over uncountable $\mathcal X$ and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.

Formalization scope

Samples are ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; $P_0$ is the law of ξ 0, and $\widehat P_n$ uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each $x\in\mathcal X$ .
$f$ is ℝ → EReal satisfying the published IsPhiDivergenceFunction (never $-\infty$ , finite on $(0,\infty)$ , $f(1)=0$ , convex on $[0,\infty)$ ) plus the smoothness of Assumption A, stated on $t\mapsto(f\,t).\mathrm{toReal}$ on an open interval around $1$ .
A distribution $P\ll\widehat P_n$ in the ball is a weight vector in the published probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. $\{p\ge0:\sum p_i=1,\ \sum_i f(np_i)\le\rho\}$ . Every supremum "over $P$ with $D_f(P\|\widehat P_n)\le\rho/n$ " is read over $P\ll\widehat P_n$ , as in (4a).
Suprema of absolute deviations (Definition 2, Theorem 7) are taken in $[0,\infty]$ , and $d_\subset$ is $[0,\infty]$ -valued; an unbounded family therefore cannot satisfy them through a junk real supremum of $0$ . Almost-sure statements use Mathlib's ∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is $\mu\{\omega:\delta<|X_n(\omega)|\}\to0$ for every $\delta>0$ with Mathlib's outer measure and no measurability hypothesis.
Readings recorded in the items: in (47) the middle term is $E_{\widehat P_n}[|L-1|\,|\ell|]$ (the page omits the absolute value on $\ell$ ); in the display after (47), $\sqrt{\rho/\gamma_f}$ is $\sqrt{\rho C_f}$ with $C_f$ from Lemma 13; in Lemma 13 the constants may depend on $\rho$ as well as $f$ , as in its proof.
A trivializing formalization would take the suprema in $\mathbb R$ (where an unbounded set has supremum $0$ ), or allow the argmin sets to be empty by construction; neither is possible here, and nonemptiness of the solution sets is not assumed.
Contributions welcome: a Glivenko–Cantelli library for parametric classes (Example 5), the deterministic inequalities (47) and Lemma 13, and the argmin-consistency argument of Corollary 1.

Selected references

J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; Math. Oper. Res. 46(3), 2021. https://arxiv.org/abs/1610.03425 , https://doi.org/10.1287/moor.2020.1085
A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 1998 (Example 19.8). https://doi.org/10.1017/CBO9780511802256
A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2
A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

16 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Bounds on Multiprocessing Timing Anomalies 1: Changing the List, Relaxing the Order, Shortening the Tasks and Using n′ Processors Multiplies the Finishing Time by at Most 1 + (n − 1)/n′Research Paper

Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$ . A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$ . Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$ . Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$ . The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$ . The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$ .

The same task set is run a second time, with processing times $\mu'$ , order $\prec'$ , list $L'$ , processor count $n'$ , and finishing time $\omega'$ . The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$ . Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$ , positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

\frac{\omega'}{\omega}\le 1+\frac{n-1}{n'}.

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$ . The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$ , the factor is $2-1/n$ ; when the first run has one processor, it is $1$ . The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$ . The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

7 thms2 active usersReviewed

Analysis Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 1: The Square Function and the Martingale Have Equivalent L^p Norms for 1 < p < ∞Research Paper

Why the square function of a martingale matters

A martingale $f = (f_1, f_2, \dots)$ is a sum $f_n = d_1 + \cdots + d_n$ of increments that are uncorrelated with the past. For sums of independent random variables, sizes are compared through the sum of squares of the summands; for martingales the corresponding object is the square function

S(f) = \Bigl(\sum_{k=1}^\infty d_k^2\Bigr)^{1/2}.

Comparing the size of $f$ with the size of $S(f)$ is one of the basic tools of probability and of harmonic analysis: it underlies Khintchine-type inequalities, the $L^p$ theory of martingale transforms, the Littlewood–Paley theory of dyadic and Fourier series, and the Burkholder–Davis–Gundy inequalities used throughout stochastic calculus.

Timeline. Paley (1932) proved $L^p$ bounds for the square function of Walsh–Paley series, the dyadic model case. Marcinkiewicz and Zygmund (1937–38) proved the analogous inequalities for sums of independent mean-zero random variables. Burkholder (1966, Ann. Math. Statist. 37) proved them for general martingales, $1 < p < \infty$ , together with the weak-type $(1,1)$ bound for $S(f)$ . Burkholder and Gundy (1970) extended the comparison to functions $\Phi$ of moderate growth by distribution function ("good- $\lambda$ ") inequalities, and Davis (1970) settled $p = 1$ for $f^* = \sup_n |f_n|$ . The 1973 Wald lectures formalized here re-derive the $1 < p < \infty$ inequality from one elementary stopping-time identity (Lemma 2.1), with explicit constants.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ sub- $\sigma$ -fields of $\mathcal A$ . A martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ is a sequence of integrable random variables $f_n$ , with $f_n$ $\mathcal A_n$ -measurable and $E(f_{n+1} \mid \mathcal A_n) = f_n$ ; a submartingale has $\ge$ in place of $=$ .

With the convention $f_0 = 0$ , the difference sequence is $d_k = f_k - f_{k-1}$ (so $d_1 = f_1$ ). Write

$S_n(f) = (\sum_{k=1}^n d_k^2)^{1/2}$ and $S(f) = \sup_n S_n(f) \in [0, \infty]$ ;
$f_n^* = \max_{1\le k\le n} |f_k|$ and $f^* = \sup_n |f_n|$ ;
$\|Y\|_p = (E|Y|^p)^{1/p}$ for a random variable $Y$ , and $\|f\|_p = \sup_{n\ge1} \|f_n\|_p$ for the process. The process is $L^p$ -bounded when $\|f\|_p < \infty$ .

For $\lambda > 0$ the exit time $\mu = \inf\{n \ge 1 : |f_n| > \lambda\}$ (with $\inf\emptyset = \infty$ ) is a stopping time; $f_\mu$ , $f_{\mu-1}$ , $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty = \lim_n f_n$ and $S_\infty(f) = S(f)$ .

In Lean these are dseq, sqFnN, sqFn, maxFnN, lpNormE, pNorm, exitTime, valAt and sqFnAt in the namespace BurkholderDFI.SquareFnLp.

Formalization targets

Goal: Theorem 3.2

For each $1 < p < \infty$ there are positive constants $c_p, C_p$ , depending only on $p$ , such that every martingale satisfies

c_p \|S(f)\|_p \le \|f\|_p \le C_p \|S(f)\|_p .

The goal asserts only existence of the constants, so that it does not depend on the particular numbers the paper's proof produces.

Milestones

In attack order:

Doob's maximal inequality (1.1): $\lambda P(f_n^* > \lambda) \le \int_{\{f_n^*>\lambda\}} |f_n| \le \|f\|_1$ .
Doob's facts (§1): an $L^1$ -bounded martingale or nonnegative submartingale converges a.e., and $\|f_\mu\|_1 \le \|f\|_1$ for every stopping time $\mu$ .
The classical extrapolation (1.2)–(1.3): $\lambda P(Y > \beta\lambda) \le \alpha\int_{\{Y>\lambda\}} X$ for all $\lambda > 0$ implies $\|Y\|_p \le \alpha\beta^p q \|X\|_p$ .
Lemma 2.1: $\|S_{\mu-1}(f)\|_2^2 + \|f_{\mu-1}\|_2^2 \le 2E f_\mu f_{\mu-1} \le 2\lambda\|f\|_1$ , with equality on the left for martingales.
Theorem 3.1: $\lambda P(S(f) > \lambda) \le 3\|f\|_1$ .
Lemma 3.1, (3.4) and (3.5): for nonnegative submartingales, $\|S_n(f)\|_p \le 9p^{1/2}q\|f_n\|_p$ .
(3.7): for martingales, $\|S_n(f)\|_p \le 18 p^{1/2} q \|f_n\|_p$ .
The duality bound: $\|f_n\|_p \le 18 q^{1/2} p \|S_n(f)\|_p$ .

Here $q$ is the conjugate exponent, $p^{-1} + q^{-1} = 1$ .

Significance

The result. Theorem 3.2 says that a martingale is bounded in $L^p$ exactly when its square function lies in $L^p$ , with comparable norms. It reduces questions about $f$ , whose increments interact, to questions about $\sum d_k^2$ , a sum of nonnegative terms. Immediate consequences include the $L^p$ boundedness of martingale transforms $\sum v_k d_k$ with $|v_k| \le 1$ (unconditionality of martingale differences in $L^p$ ), Marcinkiewicz–Zygmund and Khintchine inequalities, and, by passing through dyadic martingales, Littlewood–Paley inequalities. Theorem 3.1 is the endpoint estimate: at $p = 1$ the strong inequality fails, and weak type $(1,1)$ is what survives.

The formalization. The theorem is classical and proved; the remaining work is to machine-check it. Mathlib at the pinned revision contains no square function inequality for martingales (no occurrence of Burkholder's inequality or of a martingale square function in Mathlib/Probability); it has Doob's maximal inequality for nonnegative submartingales, optional stopping, and a.e. convergence of $L^1$ -bounded submartingales. The mission would add the stopping-time identity of Lemma 2.1, the weak-type bound with constant 3, the explicit $L^p$ constants $18 p^{1/2} q$ and $18 q^{1/2} p$ , and the general extrapolation lemma (1.3), each reusable on its own.

Difficulty

The obvious route, expanding $E S_n(f)^2 = E f_n^2$ by orthogonality, works only at $p = 2$ . For $p \ne 2$ no such identity exists, and interpolation from $p = 2$ needs an endpoint estimate that is itself the hard part: $S(f)$ is not bounded on $L^1$ . The paper obtains the endpoint from Lemma 2.1, whose content is an exact computation at the random time $\mu$ ; turning it into rigorous Lean requires handling evaluation at $\mu = \infty$ (where the a.e. limit $f_\infty$ enters), passage to the limit $n \to \infty$ in stopped identities with only $L^1$ control, and integrability of the products $f_\mu f_{\mu-1}$ . The upper bound is not a formal consequence of the lower one at the same exponent: it requires passing to the conjugate exponent $q$ .

Formalization scope

Processes are f : ℕ → Ω → ℝ; martingales and submartingales are Mathlib's Martingale f ℱ P / Submartingale f ℱ P for a filtration ℱ : Filtration ℕ _ with ℱ k $= \mathcal A_k$ . The paper's $f_0 = 0$ is built into every definition, which never reads Lean's f 0. Mathlib additionally relates f 0 to $f_1$ ; this is no restriction, since any martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ extends by $f_0 := E(f_1 \mid \mathcal A_0)$ .
"Nonnegative submartingale" means $f_n \ge 0$ almost everywhere for $n \ge 1$ .
$S(f)$ , $f^*$ , $\|\cdot\|_p$ and $\|f\|_p$ take values in $[0, \infty]$ . Neither $\|f\|_p$ nor $\|S(f)\|_p$ is assumed finite in Theorem 3.2, which therefore also asserts that one is infinite exactly when the other is. In Theorem 3.1, $\|f\|_1 = \infty$ makes the bound trivial, matching the paper's "we may assume that $f$ is $L^1$ -bounded".
The constants of Theorem 3.2 are quantified before the probability space, the filtration and the martingale. A formalization in which $c_p, C_p$ may depend on $f$ (for instance $C_p = \|f\|_p / \|S(f)\|_p$ ) would be trivially true and is excluded by this quantifier order; so is assuming finiteness of either side.
The a.e. limit $f_\infty$ is a parameter of Lemma 2.1 together with the hypothesis that $f_n \to f_\infty$ a.e.; Doob's §1 facts assert that such a limit exists.
Probability spaces live in Type (universe 0).
The asymptotic remark after Theorem 3.2 ( $c_p^{-1} = O(p^{1/2}q)$ , $C_p = O(q^{1/2}p)$ ) is not formalized; the explicit constants it summarizes are milestones 7 and 8.

Infrastructure that a complete development needs and that is reusable beyond this mission: evaluation of a process at an $\mathbb N \cup \{\infty\}$ -valued stopping time, the layer-cake formula $\|Y\|_p^p = \int_0^\infty p\lambda^{p-1} P(Y > \lambda)\, d\lambda$ for $[0,\infty]$ -valued $Y$ , and conditional-expectation martingales $E(g \mid \mathcal A_k)$ with their difference sequences. Proofs of any milestone, in any order, are welcome.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141
D. L. Burkholder and R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394573
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771313
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.
R. E. A. C. Paley, A remarkable series of orthogonal functions (I), Proc. London Math. Soc. (2) 34 (1932), 241–264. https://doi.org/10.1112/plms/s2-34.1.241

11 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Bounds on Multiprocessing Timing Anomalies 2: Scheduling the k Longest Independent Tasks Optimally First Gives ω(k)/ω₀ ≤ 1 + (1 − 1/n)/(1 + ⌊k/n⌋)Research Paper

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$ , the rule is ordinary list scheduling and has ratio at most $2-1/n$ . With $k=n$ , the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$ . Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$ , and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$ . Task $j$ takes a strictly positive time $\mu_j$ . A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$ . For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$ , let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$ ; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$ .

Formalization targets

Theorem 3

For $0\le k\le r$ , when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

\frac{\omega(k)}{\omega_0} \le 1+\frac{1-1/n}{1+\lfloor k/n\rfloor}.

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$ . The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$ , the case in which completing all tasks takes no longer than completing the first $k$ , and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$ , so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$ . Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$ . Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$ , and is defined as zero when none remains; statements using it require $k<r$ . Division is by $n>0$ and by $\omega_0>0$ . Lean's natural-number quotient represents $\lfloor k/n\rfloor$ ; real subtraction is used for coefficients such as $n-1$ . Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

8 thms2 active usersReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management 2: Frequent Re-solving Loses at Most O(√T) Against the Deterministic LP, Uniformly in the CapacitiesResearch Paper

Motivation

Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).

The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses $O(\sqrt{T})$ against that bound over a horizon of length $T$ . A natural improvement is to re-solve the LP as capacity is consumed.

Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):

1997: Gallego and van Ryzin: static policies built from the DLP lose $\Theta(\sqrt{T})$ .
2002: Cooper gives an example in which re-solving the DLP makes booking-limit control worse.
2008: Reiman and Wang re-solve exactly once, at an endogenous random time, with probabilistic allocation, and obtain $o(\sqrt{T})$ loss.
2012: Jasin and Kumar prove that re-solving after every unit of time with probabilistic allocation (the policy FR below) loses $O(1)$ , provided the DLP solution is nondegenerate. Wu et al. (2015) obtain $O(1)$ for one resource, with a constant that blows up as the solution approaches degeneracy.
2018: Bumpensanti and Wang (arXiv:1802.06192) show that FR can lose $\Omega(\sqrt{T})$ against the hindsight optimum on a degenerate instance, propose a modified policy with $O(1)$ loss in all cases, and prove that FR never loses more than $O(\sqrt{T})$ against the DLP. This mission formalizes the last of these results.

Setting

There are $n$ customer classes $j \in [n]$ and $m$ resources $l \in [m]$ . Over the horizon $[0, T]$ , class- $j$ customers arrive according to independent Poisson processes with rates $\lambda_j > 0$ . Accepting a class- $j$ customer earns $r_j \ge 0$ and consumes $a_{lj} \ge 0$ units of each resource $l$ ; $A = (a_{lj})$ is the bill-of-materials matrix and $A_j$ its $j$ -th column. The initial capacity vector is $C \ge 0$ . A customer can be accepted only if $A_j \le C'$ componentwise, where $C'$ is the capacity remaining at its arrival.

For a capacity-per-unit-time vector $b \ge 0$ , let

v(b) = \max\Big\{ \sum_{j=1}^n r_j x_j \ :\ \sum_{j=1}^n A_j x_j \le b,\ 0 \le x_j \le \lambda_j \Big\}.

The DLP value is $v^{\mathrm{DLP}}(T, C) = T\, v(C/T)$ .

The Frequent Re-solving policy (FR) divides the horizon into $T$ unit periods $[t, t+1)$ . At the start of period $t$ , with remaining capacity $C(t)$ , it sets $b(t) = C(t)/(T - t)$ , computes an optimal solution $x(t)$ of the LP with right-hand side $b(t)$ , and during the period accepts each class- $j$ arrival with probability $x_j(t)/\lambda_j$ , subject to the capacity check. Its expected revenue is $v^{\mathrm{FR}}(T, C)$ . The LP may have several optimal solutions; the results hold for every rule choosing among them.

Formalization targets

Goal: Proposition 3

There is a constant $M$ , depending only on $\lambda$ , $r$ and $A$ , such that for every integer $T \ge 1$ , every capacity $C \ge 0$ and every choice of optimal LP solutions,

v^{\mathrm{DLP}}(T, C) - v^{\mathrm{FR}}(T, C) \le M \sqrt{T}.

The content is the uniformity: $M$ does not depend on $C$ , so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.

Milestones, in the order the proof uses them

Eq. (32), p. 35. The capacity check costs FR at most $\sum_j r_j(\log T + 1) + \sum_j r_j \lambda_j$ relative to the LP revenue it targets:

v^{\mathrm{FR}} \ge \mathbb{E}\Big[\sum_{t=0}^{T-1} \sum_{j=1}^n r_j x_j(t)\Big] - \sum_{j=1}^n r_j (\log T + 1) - \sum_{j=1}^n r_j \lambda_j .

Eq. (33), p. 35. LP sensitivity in the right-hand side: $v(b) - v(b') \le \sum_l r^l_{\max} (b_l - b'_l)^+$ with $r^l_{\max} = \max_j r_j \mathbb{I}(a_{lj} > 0)/a_{lj}$ .
Lemma 8, p. 43 (corrected). $\mathbb{E}[(b_l - b_l(t))^+] \le K_l \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}}$ with $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$ .
p. 36. $\sum_{t=0}^{T-1} \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}} \le 2\sqrt{T} + \sqrt{2}$ .
p. 36, explicit bound.

v^{\mathrm{DLP}} - v^{\mathrm{FR}} \le \sum_{l=1}^m r^l_{\max} K_l (2\sqrt{T} + \sqrt{2}) + n\, r_{\max} (\log T + 1) + n\, r_{\max} \lambda_{\max} .

Significance

The result. Because $v^{\mathrm{DLP}}$ bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most $O(\sqrt{T})$ against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the $\Omega(\sqrt{T})$ lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order $\sqrt{T}$ is exact for FR. The nondegeneracy assumption of the earlier $O(1)$ analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from $(\lambda, r, A)$ .

Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.

Difficulty

The obvious argument compares FR with the DLP period by period: the LP that FR solves at time $t$ differs from the original only in its right-hand side, so the loss should be controlled by how far $b(t)$ drifts below $b = C/T$ . Two things break a naive version of this. First, $b(t)$ is a ratio whose denominator $T - t$ shrinks to $1$ , so fluctuations late in the horizon are amplified; a crude bound on the drift at each $t$ sums to more than $\sqrt{T}$ . Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions $x(i)$ depend on the whole past, so the consumption in different periods is not independent.

Uniformity in $C$ is the whole point. Arguments that rely on a margin between $C/T$ and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.

Formalization scope

The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.

LP value. $v(b)$ is the published piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for $b \ge 0$ ).
Optimal solutions. The " $\arg\max$ " of Algorithm 2 is an arbitrary optimal-solution selector sel; every theorem quantifies over all selectors, with constants chosen before the selector.
Randomness. Within a period the acceptance probabilities are fixed, so the period's arrivals are represented exactly as a Poisson number of customers in arrival order, with i.i.d. classes of law $\lambda_j / \sum_i \lambda_i$ and independent Bernoulli acceptance coins. Expectations are series over this law (windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of $C(t)$ are a forward recursion (frStateExp).
Horizon. $T$ is a positive integer; capacities are real vectors.
Standing assumptions of p. 7, left implicit there and hypotheses here: $\lambda_j > 0$ , $r_j \ge 0$ , $a_{lj} \ge 0$ , $C \ge 0$ .
$O(\cdot)$ . " $= O(\sqrt{T})$ " is $\exists M,\ \forall\, \mathrm{sel}, T \ge 1, C \ge 0$ . The paper's threshold $T_1$ is dropped, which is equivalent because $0 \le v^{\mathrm{FR}}$ and $v^{\mathrm{DLP}} \le T\sum_j r_j\lambda_j$ .
Corrected slip, Lemma 8. The printed $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j^2}$ is false: the proof replaces the conditional variance $x_j(i) \le \lambda_j$ of a Poisson increment by $\lambda_j^2$ . With one class, one resource, $a = 1$ , $\lambda = 0.01$ , $C = \lambda T$ , $T = 1000$ and $t = 2$ , an exact computation gives $\mathbb{E}[(b - b(2))^+] \approx 1.96 \cdot 10^{-5}$ , above the printed bound $1.42 \cdot 10^{-5}$ . The mission uses $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$ in Lemma 8 and in the explicit bound.
Index slip. The paper's sums $\sum_{l=1}^L$ run over its $m$ resources and are read as $l \in [m]$ .

A trivializing formalization is ruled out. The constant $M$ is chosen before $C$ . FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.

Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.

Selected references

Y. Bumpensanti, H. Wang, A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv:1802.06192v3, 2018 (the source of this mission; later in Management Science 66(7), 2020). https://arxiv.org/abs/1802.06192
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997.
W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4), 720–727, 2002.
M. I. Reiman, Q. Wang, An Asymptotically Optimal Policy for a Quantity-Based Network Revenue Management Problem, Mathematics of Operations Research 33(2), 257–282, 2008.
S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2), 313–345, 2012.
K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004.

Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Scheduling Deteriorating Jobs on a Single Processor II: If E(X_j)/α_j and α_j/[c_j(1+α_j)] Both Increase in j, the Order 1, …, N Minimizes the Weighted Expected Completion Time (Proposition 2)Research Paper

Why deteriorating jobs need a scheduling rule

On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.

The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.

Jobs, schedules, and cost

There are $N$ jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule $\pi$ is a permutation of the jobs: $\pi(k)$ is the job processed in position $k$ . The paper labels positions and jobs from $1$ to $N$ ; the Lean development labels them from $0$ to $N-1$ . The identity schedule $\pi_0$ processes jobs in label order.

For job $i$ , $X_i$ is its random initial processing requirement, $\alpha_i$ its deterministic growth rate, and $c_i$ its waiting cost rate. If the job starts at time $t$ , its actual processing time is $Y_i(t)=X_i+\alpha_i t$ . Deterioration stops once processing starts. Write $S_k(\pi)$ for the time at which the first $k$ scheduled jobs have all finished. The model sets $S_0(\pi)=0$ and

S_{k+1}(\pi)=S_k(\pi)+X_{\pi(k+1)}+\alpha_{\pi(k+1)}S_k(\pi)

in the paper's one-based position notation. Thus the completion time of the job in position $k$ is $S_k(\pi)$ . Its cost is its own rate $c_{\pi(k)}$ times that completion time, giving

C(\pi)=\sum_{k=1}^{N}c_{\pi(k)}S_k(\pi).

All of these are random quantities until an expectation is taken. Equation (2) of the paper writes $S_k$ as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into $C(\pi_0)$ . Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in $C$ from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.

Formalization targets

The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,

\frac{E(X_1)}{\alpha_1}<\cdots<\frac{E(X_N)}{\alpha_N}, \qquad \frac{\alpha_1}{c_1(1+\alpha_1)} <\cdots< \frac{\alpha_N}{c_N(1+\alpha_N)},

then, for every permutation $\sigma$ ,

E[C(\pi_0)]\le E[C(\sigma)].

The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.

The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.

What the result establishes

The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only $E(X_i)/\alpha_i$ , enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.

The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.

Where the argument is difficult

Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.

The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.

Formalization scope

Jobs are $\mathrm{Fin}\,N$ , and a policy is an equivalence permutation with $\pi(k)$ equal to the job in position $k$ . Completion time is defined by the processing rule $Y_i(t)=X_i+\alpha_i t$ , not by the closed form (2). At positions beyond the $N$ jobs it stays constant, and theorems about the closed form restrict $k$ to $0\le k\le N$ . The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.

The proposition uses a probability space and the Bochner integral of the real-valued cost. Every $X_i$ is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.

The two strict orderings are over the labels of jobs in $\pi_0$ , not positions of an arbitrary schedule. The conclusion compares $\pi_0$ with every permutation, not only with schedules obtained by one adjacent swap. The $N=0$ and $N=1$ cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.

Selected references

Browne, Sid, and Uri Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 495–498 (1990). DOI: 10.1287/opre.38.3.495.

6 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Statistics·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VI: The Group-Lasso Block Update Is Zero iff ‖Aᵢᵀv‖₂ ≤ λ/ρ, Otherwise Ridge with ν‖xᵢ‖₂ = λ/ρTextbook

Why distributed model fitting

Fitting a statistical model usually means solving a convex problem of the form

\text{minimize}\quad l(Ax-b)+r(x),

where $A\in\mathbb R^{m\times n}$ holds one training example per row and one feature per column, $b\in\mathbb R^m$ is the response, $l$ is a convex loss and $r$ a convex regularizer. Least squares, the lasso, logistic regression and the support vector machine are all of this form. When either dimension is very large, or the data are stored on many machines, the problem has to be solved by processors that each see only a block of $A$ .

Chapter 8 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) shows how ADMM does this in two ways: by splitting $A$ by rows (splitting across examples, §8.2), which turns the problem into a global consensus problem, and by splitting it by columns (splitting across features, §8.3), which turns it into a sharing problem. In both cases the method is only practical because the individual updates have closed forms or reduce to small standard problems. This mission formalizes those closed forms, culminating in the update for the group lasso.

Setting

Vectors are in $\mathbb R^n$ with the Euclidean norm $\|\cdot\|_2$ ; $\|x\|_1=\sum_j|x_j|$ . Throughout, $\rho>0$ is the ADMM penalty parameter and $\lambda>0$ a regularization weight.

Splitting across examples. Partition $A$ and $b$ by rows into $N$ blocks $A_i\in\mathbb R^{m_i\times n}$ , $b_i\in\mathbb R^{m_i}$ . With scaled dual variables $u_i$ and averages $\bar x=\frac1N\sum_ix_i$ , $\bar u=\frac1N\sum_iu_i$ , the consensus ADMM iteration is

x_i^{k+1}=\operatorname*{argmin}_{x_i}\Bigl(l_i(A_ix_i-b_i)+\tfrac{\rho}{2}\|x_i-z^k+u_i^k\|_2^2\Bigr),\quad z^{k+1}=\operatorname*{argmin}_{z}\Bigl(r(z)+\tfrac{N\rho}{2}\|z-\bar x^{k+1}-\bar u^k\|_2^2\Bigr),

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z^{k+1}$ . For the lasso, $l(w)=\frac12\|w\|_2^2$ and $r=\lambda\|\cdot\|_1$ .

Splitting across features. Partition $x=(x_1,\dots,x_N)$ with $x_i\in\mathbb R^{n_i}$ and $A=[A_1\cdots A_N]$ with $A_i\in\mathbb R^{m\times n_i}$ , so $Ax=\sum_iA_ix_i$ . Introducing $z_i=A_ix_i$ gives a sharing problem; its ADMM $z$ -update minimizes $l(\sum_iz_i-b)+\sum_i\frac\rho2\|A_ix_i-z_i+u_i\|_2^2$ . Writing $\overline{Ax}=\frac1N\sum_iA_ix_i$ and $\bar z$ for the average of the $z_i$ , this reduces to a single problem in $\bar z\in\mathbb R^m$ , all dual variables coincide, and each block update minimizes

\tfrac{\rho}{2}\|A_ix_i-v\|_2^2+r_i(x_i)

for a vector $v\in\mathbb R^m$ assembled from the previous iterate. For the group lasso, $r_i(x_i)=\lambda\|x_i\|_2$ (not squared).

Soft thresholding is $S_\kappa(a)=a-\kappa$ for $a>\kappa$ , $0$ for $|a|\le\kappa$ , $a+\kappa$ for $a<-\kappa$ .

Formalization targets

Goal: the group-lasso block update (§8.3.2, pp. 69–70)

Let $h(x)=\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_2$ on $\mathbb R^{n_i}$ and $x(\nu)=(A_i^TA_i+\nu I)^{-1}A_i^Tv$ . Then

0\in\operatorname*{argmin}h\iff\|A_i^Tv\|_2\le\lambda/\rho,

and then $0$ is the only minimizer; if $\|A_i^Tv\|_2>\lambda/\rho$ , there is exactly one $\nu>0$ with $\nu\|x(\nu)\|_2=\lambda/\rho$ , the point $x(\nu)$ minimizes $h$ , and every minimizer is of this form.

Milestones

Ridge $x_i$ -update (§8.2.1, p. 65): $x_i^{k+1}=(A_i^TA_i+\rho I)^{-1}(A_i^Tb_i+\rho(z^k-u_i^k))$ , the unique minimizer.
Soft-thresholding $z$ -update (§8.2.1, p. 65): $z^{k+1}=S_{\lambda/(\rho N)}(\bar x^{k+1}+\bar u^k)$ componentwise.
Reduction to $\bar z$ and equal duals (§8.3, p. 68): minimizers of the $N$ -block $z$ -update are exactly the vectors $z_i=\bar z+A_ix_i+u_i-\overline{Ax}-\bar u$ with $\bar z$ solving the $\bar z$ -update, and then $u_i^{k+1}=\overline{Ax}^{k+1}+\bar u^k-\bar z^{k+1}$ for every $i$ .
Feature-split lasso $\bar z$ -update (§8.3.1, p. 69): $\bar z^{k+1}=(b+\rho\overline{Ax}^{k+1}+\rho u^k)/(N+\rho)$ .
Lasso zero test, corrected (§8.3.1, p. 69): $0$ minimizes $\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_1$ iff $\|A_i^Tv\|_\infty\le\lambda/\rho$ .
Eigendecomposition identity (§8.3.2, p. 70): if $A_i^TA_i=Q\,\mathbf{diag}(\mu)Q^T$ with $Q$ orthogonal, then $\|x(\nu)\|_2=\|\mathbf{diag}(\mu+\nu\mathbf 1)^{-1}Q^TA_i^Tv\|_2$ for $\nu>0$ .
SVM $\bar z$ -update (§8.3.4, pp. 70–71): the minimizer of $\mathbf 1^T(N\bar z+\mathbf 1)_++\frac\rho2\|\bar z-\overline{Ax}-u\|_2^2$ is a shifted soft thresholding of $v=\overline{Ax}+u$ .

Significance

The goal result says that a group-lasso block either switches off entirely, which is how group sparsity arises, or solves a ridge regression whose ridge parameter is the unique root of a scalar monotone equation; this is what makes the distributed group lasso implementable with one cached factorization per block and a bisection. The milestones are the remaining closed forms that turn the two distributed schemes of Chapter 8 into concrete algorithms, and the reduction of milestone 3 is the structural fact that lets feature splitting carry a single dual variable.

The book derives these facts in running text and states them without proof. None of them is formalized on Prove2Me, and the book's printed zero test for the lasso (p. 69) uses the wrong norm; a machine-checked collection of the correct updates removes that kind of error from the record and gives later ADMM missions a verified library of update formulas.

Difficulty

Each statement is a characterization of all minimizers of a nonsmooth convex function, not a check that a formula satisfies a stationarity equation. For the goal, the nonsmooth term $\lambda\|x\|_2$ has a kink at $0$ , $h$ need not be strictly convex when $A_i$ has a nontrivial kernel, and the existence and uniqueness of the parameter $\nu$ is part of the claim rather than an assumption: the obvious move of assuming a suitable $\nu$ and checking the formula proves nothing about the case split or about uniqueness, and the singular case of $A_i^TA_i$ is exactly where naive arguments break. Milestone 3 must handle an arbitrary convex loss $l$ , with no closed form at all.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n); matrices are Matrix (Fin m) (Fin n) ℝ acting through Matrix.toEuclideanLin; blocks are indexed by Fin N (0-based); the regularization weight $\lambda$ is lam; the eigenvalue vector the book also calls $\lambda$ (p. 70) is μ. " $x$ minimizes $F$ " is Mathlib's IsMinOn F Set.univ x. Iteration superscripts are dropped: each statement is about one update with the previous iterate given. Explicit choices:

$\rho>0$ , $\lambda>0$ and $N\ge1$ are hypotheses wherever the book uses them.
Closed forms are stated as "minimizer $\iff$ formula", which contains existence and uniqueness; the book's "the solution" in §8.3.2 is stated as existence and uniqueness of $\nu$ plus a characterization of every minimizer, with no invertibility hypothesis on $A_i^TA_i$ .
$(A_i^TA_i+\nu I)^{-1}$ is Mathlib's matrix inverse, used only for $\nu>0$ , where it is the true inverse.
The loss in milestone 3 is real valued and convex, as in (8.1).
The lasso zero test is stated with $\|\cdot\|_\infty$ ; the book prints $\|\cdot\|_2$ , which is false for the $\ell_1$ term.
The SVM $\bar z$ -update uses the coefficient $\rho/2$ printed on p. 70, which matches the printed thresholds $N/\rho$ .
The book's "assuming $A_i$ is tall" (p. 70) is not imposed; the identity holds without it.

A statement that only checks that $x(\nu)$ satisfies the optimality equation, or that assumes the parameter $\nu$ exists, does not capture the goal; the goal asserts existence and uniqueness of $\nu$ and describes every minimizer of $h$ .

Contributions welcome: subgradient calculus for $\|\cdot\|_2$ and $\|\cdot\|_1$ in EuclideanSpace, first-order optimality for convex quadratics plus a convex nonsmooth term, and the monotonicity of $\nu\mapsto\nu\|(M+\nu I)^{-1}c\|_2$ for positive semidefinite $M$ ; these are reusable for every proximal and ADMM update.

Selected references

S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1):1–122, 2011. https://doi.org/10.1561/2200000016
M. Yuan, Y. Lin, Model selection and estimation in regression with grouped variables, Journal of the Royal Statistical Society B 68(1):49–67, 2006. https://doi.org/10.1111/j.1467-9868.2005.00532.x
R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

10 thms2 active usersReviewed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

An Additive Algorithm for Solving Linear Programs with Zero-One Variables: In Finitely Many Iterations the Additive Algorithm Yields an Optimal Solution or Proves InfeasibilityResearch Paper

Motivation

Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)

The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)

Setting

Let $N$ be a finite set of binary coordinates and $M$ a finite set of constraints. The data are a real matrix $A=(a_{ij})_{i\in M,j\in N}$ , a real vector $b=(b_i)_{i\in M}$ , and nonnegative objective coefficients $c_j\ge0$ . A binary assignment is represented by the set $J\subseteq N$ of coordinates assigned one; all other coordinates are zero. Its slack and cost are

y_i(J)=b_i-\sum_{j\in J}a_{ij},\qquad z(J)=\sum_{j\in J}c_j.

The assignment is feasible when $y_i(J)\ge0$ for every $i\in M$ . It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem $P$ and solutions (1)–(8). The coefficients of $A$ and $b$ may have either sign; $N$ and $M$ may be empty. Balas (1965), pp. 519, 523

The algorithm generates assignments $J_0,J_1,\ldots,J_s$ , starting at $J_0=\varnothing$ . Among the generated feasible assignments, their least cost is the ceiling $z^{*(s)}$ ; if there are none, $z^{*(s)}=+\infty$ . Each generated assignment has an improving set $N_p$ formed when it first appears. Later steps cancel candidate indices and keep records $C_k^s$ of which values attached to an earlier assignment have been cancelled by the time $J_s$ is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528

Formalization targets

The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion $J_t\supset J_s$ below the current ceiling adds no index in $C^s$ ; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533

The mission's goal is Convergence Theorem 2:

\text{every run from }J_0=\varnothing\text{ stops after finitely many steps, with either an optimal feasible assignment or a valid infeasibility verdict.}

The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, $z^{*(s)}=+\infty$ means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for $P$ . These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a

Significance

The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533

The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)

Difficulty

It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533

Formalization scope

Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem $P$ adds the paper's standing assumption $c_j\ge0$ . There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol $\subset$ means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525

The ceiling is represented in WithTop ℝ, with $\top$ for $+\infty$ . The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set $N_p$ remains fixed after generation; the step-5 scan uses $N_k^s=N_k-(C_k^s\cup D_k^s)$ with the stored snapshot $C_k^s$ , as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: $u^k$ is abandoned when the algorithm is instructed to stop, or to check some $N_p^s$ with $p<k\le s$ , including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads $C_p^{s+1}$ either as the cancellations accumulated so far during iteration $s+1$ or as the cancellation records at the transition that obtains $u^{s+1}$ . Balas (1965), pp. 525–533

The paper prints $z^{*(k)}$ in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, $z^{*(s)}$ ; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to $P$ , the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533

Selected references

Egon Balas, An Additive Algorithm for Solving Linear Programs with Zero-One Variables, Operations Research 13(4), 517–546, 1965. DOI: 10.1287/opre.13.4.517

10 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

Convex Programming in Hilbert Space: Gradient Projection x_{k+1} = P(x_k − ρ_k∇f(x_k)) with σ ≤ ρ_k ≤ 2ρ₀ − σ Stays in the Level Set, and for Convex f Drives f(x_k) to inf_C fResearch Paper

Motivation

Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than $\mathbb R^n$ .

A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).

Timeline.

1959: Cheney and Goldstein study proximity maps (metric projections) onto convex sets and a fixed-point construction for the distance between two convex sets (Cheney–Goldstein 1959, cited by the note as [1]).
1964: Goldstein, this note: the gradient projection method in Hilbert space with steps in $[\sigma, 2\rho_0 - \sigma]$ .
1966: Levitin and Polyak give the same method and convergence rates for constrained minimization.
1987: Calamai and Moré extend the analysis to Armijo-type step rules and identification of the active constraints in $\mathbb R^n$ (Calamai–Moré 1987).

Setting

Let $H$ be a real Hilbert space with inner product $[x, y]$ and norm $\|x\|$ . Let $C \subseteq H$ be closed and convex, and let $P : H \to H$ be the projection onto $C$ : $P(x)$ is the point of $C$ closest to $x$ . In Lean, IsProjection C P says that $P(x) \in C$ and $\|x - P(x)\| \le \|x - y\|$ for all $y \in C$ .

Let $f : H \to \mathbb R$ , $x_0 \in C$ , and let

S = \{x \in C : f(x) \le f(x_0)\}

be the level set (levelSet f C x0). Let $\hat S$ be an open set containing the convex hull of $S$ . Write $f'(x, h)$ for the Fréchet derivative of $f$ at $x$ applied to $h$ , $\nabla f(x)$ for the gradient (so $f'(x, h) = [\nabla f(x), h]$ ), and

f''(x, h, h) = \frac{d}{dt}\Big|_{t=0} f'(x + th, h)

for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some $\rho_0 > 0$ , at every $x \in \hat S$ and for every $h \in H$ , these derivatives exist and

|f''(x, h, h)| \le \frac{\|h\|^2}{\rho_0}.

Choose $0 < \sigma \le \rho_0$ and step sizes $\sigma \le \rho_k \le 2\rho_0 - \sigma$ . The method is

x_{k+1} = P\big(x_k - \rho_k \nabla f(x_k)\big), \qquad k \ge 0.

A point $z \in C$ is stationary if $P(z - \rho \nabla f(z)) = z$ for every $\rho > 0$ .

Formalization targets

Goal: the THEOREM, parts (i)–(v)

Assume $f$ is bounded below and continuous on $C$ . There is $L \in \mathbb R$ such that

(i) $x_k \in S$ for all $k$ , $x_{k+1} - x_k \to 0$ , and $f(x_k)$ decreases to $L$ ;
(ii) if $S$ is compact, every cluster point $z$ of $(x_k)$ near which $\nabla f$ is continuous is stationary, and a unique cluster point is the limit of $(x_k)$ ;
(iii) if $S$ is convex and $f''(x, h, h) \ge \mu \|h\|^2$ on $S$ for some $\mu \ge 0$ , then

L = \inf\{f(x) : x \in C\};

(iv) under (iii) with $S$ bounded, every weak cluster point of $(x_k)$ minimizes $f$ on $C$ ;
(v) under (iii) with $\mu > 0$ and $\nabla f$ bounded on $S$ , there is $z \in S$ with $f(z) = L$ , $x_k \to z$ in norm, and $z$ is the unique minimizer of $f$ on $C$ .

The goal is the whole theorem, because its five parts share one limit $L$ and one standing setting.

Milestones

The projection inequality $[x - y, P(x) - y] \ge \|P(x) - y\|^2$ for $y \in C$ ; the Lipschitz property of $P$ ; the characterization of stationarity for convex $f$ at a differentiability point; the one-step Taylor estimate; the step lemma (for $\sigma \le \rho \le 2\rho_0 - \sigma$ the new point stays in $S$ and the decrease is at least $\|x_{k+1} - x_k\|^2 \sigma / 4\rho_0^2$ ); parts (i) and (ii); the strong-convexity bound $f(x) \ge f(y) + [\nabla f(y), x - y] + \frac12\mu\|x - y\|^2$ on $S$ ; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of $f$ on $C$ .

Significance

The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.

Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.

Difficulty

The obvious argument for (i) applies a quadratic upper bound for $f$ along the segment from $x_k$ to $x_{k+1}$ . That bound is only available where the curvature hypothesis holds, on $\hat S$ , and nothing guarantees in advance that $x_{k+1}$ , or the segment, lies in $\hat S$ . Ruling this out requires control of $f$ up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.

Formalization scope

$H$ is a real Hilbert space: [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product $[x, y]$ is ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f.
$P$ is any map with IsProjection C P; there is no chosen projection and no junk value.
$f''(x, h, h)$ is the derivative at $t = 0$ of $t \mapsto f'(x + th, h)$ . The hypothesis on $\hat S$ (SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.
The run starts at $x_0$ , and $0 < \sigma \le \rho_0$ makes the step window nonempty.
" $L = \inf$ " is IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.
Added hypothesis: $f$ is continuous on $C$ . Part (i) as printed is false without it: on $H = C = \mathbb R$ with $P = \mathrm{id}$ , $f(x) = (x - 2)^2$ for $x < 1$ and $f(x) = 100$ for $x \ge 1$ , $x_0 = 0$ , $\hat S = (-1, 1)$ , $\rho_0 = 1/2$ , $\sigma = 1/4$ , $\rho_k = 1/2$ , the first step lands at $x_1 = 2$ with $f(x_1) = 100 > f(x_0)$ .
Moved clause. The last clause of (ii), " $z$ minimizes $f$ on $C$ ", is false for nonconvex $f$ (a unique cluster point can be a stationary point that is not a minimizer). The goal omits it, and a companion item states it under convexity of $f$ on $C$ .
The goal assumes nothing about the step decrease, the step size $\hat\rho$ of the proof, or the iterates beyond the run's definition. A formalization that adds such facts as hypotheses, or that proves only one of the five parts, does not count as closing the goal.

Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).

Selected references

A. A. Goldstein, Convex programming in Hilbert space, Bull. Amer. Math. Soc. 70 (1964), 709–710. https://doi.org/10.1090/s0002-9904-1964-11178-2
E. W. Cheney and A. A. Goldstein, Proximity maps for convex sets, Proc. Amer. Math. Soc. 10 (1959), 448–450.
A. V. Balakrishnan, An operator theoretic formulation of a class of control problems and a steepest descent method of solution, J. SIAM Control Ser. A 1 (1963), 109–127.
E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Comput. Math. Math. Phys. 6(5) (1966), 1–50.
P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), 93–116. https://doi.org/10.1007/BF02592073

14 thms2 active usersReviewed

Control Theory Probability Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 1: A Backward Equation Driven by a Bounded-Variation Integrator Has a Unique Adapted Solution in L¹(μ) Under Integrability AloneResearch Paper

Motivation

Backward stochastic differential equations (BSDEs) prescribe a process by its terminal value rather than its initial value: the unknown $V$ must be adapted to the information flow, yet must reach a given random variable $Y$ at the horizon $T$ . They arise in mathematical finance (pricing and hedging, where $Y$ is a contingent claim), in stochastic control (adjoint equations of the stochastic maximum principle) and in economics, where the stochastic differential utility of Duffie and Epstein (1992) defines the utility of a consumption stream as the solution of a backward equation.

Timeline:

1990. Pardoux and Peng prove existence and uniqueness of adapted solutions for Lipschitz BSDEs driven by a Brownian motion, with square-integrable data (doi:10.1016/0167-6911(90)90082-6).
1992. Duffie and Epstein introduce stochastic differential utility and state a conjecture on the well-posedness of the defining backward equation under $L^p$ integrability (doi:10.2307/2951600).
1993. Antonelli treats the backward equation with a general bounded-variation integrator $A$ in place of $dt$ , under integrability alone, and answers the Duffie–Epstein question for $p=1$ (doi:10.1214/aoap/1177005363). This mission formalizes that result, §2 of the paper.

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{0\le t\le T},P)$ be a complete filtered probability space satisfying the usual hypotheses: the filtration is right-continuous and $\mathcal F_0$ contains every $P$ -null set. Let $A$ be an adapted process with right-continuous paths of bounded variation, $A_0=0$ , whose total variation process $|A|_t$ satisfies $|A|_T\le\beta$ for a constant $\beta>0$ . Integrals $\int_s^t h_r\,dA_r$ are pathwise Lebesgue–Stieltjes integrals over $(s,t]$ .

The Doléans–Dade measure $\mu$ of $|A|$ is the finite measure on $[0,T]\times\Omega$ with

\int X\,d\mu=E\Big(\int_0^T X_s\,|dA_s|\Big),

and $L^1(\mu)$ is the space of jointly measurable processes $V$ with $\|V\|_{L^1(\mu)}=E\big(\int_0^T|V_t|\,|dA_t|\big)<+\infty$ .

The data are a driver $g_s(\omega,u)$ , jointly measurable, and a terminal value $Y$ , subject to hypotheses 1–4:

$|g_s(u)-g_s(v)|\le k|u-v|$ for some $k>0$ , all $u,v$ and all $s\in[0,T]$ ;
$g_s(\cdot,u)$ is $\mathcal F_s$ -measurable;
$E\big(\int_0^T|g_s(0)|\,|dA_s|\big)<+\infty$ ;
$Y\in L^1(P)$ is $\mathcal F_T$ -measurable.

The backward equation is the fixed-point problem for

G(V)_t=E\Big(\int_t^T g_s(V_s)\,dA_s+Y\ \Big|\ \mathcal F_t\Big).\tag{2.1}

When $A_t=t$ this is the Duffie–Epstein equation $V_t=E\big(\int_t^T g_s(V_s)\,ds+Y\mid\mathcal F_t\big)$ .

Formalization targets

Goal: Theorem 2.4

Under hypotheses 1–4 there is a progressively measurable process $V\in L^1(\mu)$ with càdlàg paths such that

E\Big(\int_0^T|G(V)_t-V_t|\,|dA_t|\Big)=0,

$V$ is a semimartingale through the decomposition

V_t=E\Big(\int_0^T g_s(V_s)\,dA_s+Y\ \Big|\ \mathcal F_t\Big)-\int_0^t g_s(V_s)\,dA_s,\tag{2.9}

and any two solutions in $L^1(\mu)$ agree $\mu$ -almost everywhere.

Milestones

In the order of the paper's argument:

Remark 2.2, (2.6): $E\big(H\int_{[0,\infty)}a(s)\,dC_s\big)=E\big(\int_{[0,\infty)}H_s\,a(s)\,dC_s\big)$ for an adapted increasing càdlàg $C$ and a càdlàg version $H_t$ of $E(H\mid\mathcal F_t)$ , for $H$ positive or in $L^1$ .
Lemma 2.3: $G$ maps $L^1(\mu)$ into $L^1(\mu)$ .
The relation $\sum_{i=0}^n(-1)^iA_t^{((n-i)-)}A_t^{(i)}=0$ between the iterated integrals $A^{(n)}=((A\cdot A)\cdots)\cdot A$ and $A^{(n-)}=((A_-\cdot A)_-\cdots)\cdot A$ .
(2.7): $|G^{(n)}(U)_t-G^{(n)}(V)_t|\le k^nE\big(\int_t^T(A_{s-}-A_t)^{[n-1]}|U_s-V_s|\,dA_s\mid\mathcal F_t\big)$ .
(2.8): $E\int_0^T|G^{(n)}(U)_t-G^{(n)}(V)_t|\,dA_t\le k^nE\int_0^TA^{(n-)}_{t-}|U_t-V_t|\,dA_t$ .
$A^{(n-)}_t\le A_t^n/n!$ .
The iterate bound $\|G^{(n)}(U)-G^{(n)}(V)\|_{L^1(\mu)}\le k^n(\beta^n/n!)\|U-V\|_{L^1(\mu)}$ .

Milestones 3–7 live inside the proof, after its reduction to nondecreasing $A$ .

Significance

The result. Theorem 2.4 gives well-posedness of a backward equation with no square-integrability and no Brownian structure: the filtration is arbitrary (subject to the usual hypotheses), the integrator may jump, and only first moments are required. In the case $A_t=t$ it settles the $p=1$ case of the Duffie–Epstein conjecture, so stochastic differential utility is well defined for integrable consumption data. The same fixed-point scheme, with the Doléans measure of a dominating process, is the basis of the coupled backward–forward result of §3 of the paper (a separate mission of this series).

Formalizing it. The theorem is proved in the literature but, as far as is known, has no machine-checked proof; Mathlib has conditional expectations, filtrations, martingales and Stieltjes measures, but no càdlàg process theory, no optional projection and no Doléans measure. A complete development produces these pieces. Its milestones also make precise points the paper leaves implicit: G is defined only up to versions, and the iterate bound is printed with $G$ in place of $G^{(n)}$ .

Difficulty

The obvious approach is to show that $G$ itself is a contraction on $L^1(\mu)$ . It is not in general: the one-step bound is $k\beta$ , and nothing makes $k\beta<1$ . The argument must instead control the $n$ -th iterate. This needs exchanging a conditional expectation with a Stieltjes integral against a random measure, which is the optional projection identity (2.6). It also needs iterated integrals against an integrator with jumps, where the continuous-case identity $A^{(n)}=A^n/n!$ fails and only the inequality $A^{(n-)}\le A^n/n!$ survives. A second difficulty is measure-theoretic: $G(V)_t$ is defined only almost surely for each fixed $t$ , and the $L^1(\mu)$ norm sees the whole path. A version must be chosen with càdlàg paths before the equation even makes sense in $L^1(\mu)$ .

Formalization scope

Time is $\mathbb R_{\ge0}$ with a horizon $T>0$ ; only $[0,T]$ matters. Integrals $\int_s^t$ are over $(s,t]$ .
The integrator is a structure BVIntegrator carrying $A$ with its Jordan decomposition $A=A^+-A^-$ as data, tied to Mathlib's eVariationOn so that $A^++A^-=|A|$ . $|dA|=dA^++dA^-$ are Stieltjes measures of the paths.
$L^1(\mu)$ norms are lower integrals in $[0,\infty]$ ; membership is joint measurability plus a finite norm.
$G(V)$ is never a Lean function. Statements quantify over versions: jointly measurable processes $W$ , càdlàg on $[0,T]$ , with $W_t=E(\xi_t\mid\mathcal F_t)$ a.s. for each $t$ , where every $\xi_t=\int_t^Tg_s(V_s)\,dA_s+Y$ is required to be integrable. Picard iterates are chains of such versions.
Explicit choices relative to the page: the usual hypotheses and right-continuous integrators (Protter's conventions, p. 778); integrability of every conditional-expectation argument; càdlàg versions; $A$ nondecreasing in milestones 3–7, as in the proof; in (2.6), $C_0\ge0$ with $C_{0-}=0$ , an $[0,\infty]$ -valued version of $E(H\mid\mathcal F_t)$ in the positive case, and in the $L^1$ case finiteness of $E(|H|\int a\,dC)$ ; "semimartingale" expressed by the decomposition (2.9), with the martingale property stated for $M_{\min(t,T)}$ ; $G^{(n)}$ in place of the printed $G$ in the iterate bound.
A formalization that lets $G(V)$ be a conditional expectation of a non-integrable argument (Mathlib returns $0$ ), or that states only existence or only uniqueness, is trivial and is ruled out: both halves are in the goal, and every version carries the integrability of its argument.
Reusable infrastructure: optional projection for increasing integrators, càdlàg versions of martingales, iterated Stieltjes integrals and their factorial bounds. Contributions to any of these are welcome, as are proofs of the special case $A_t=t$ .

Selected references

F. Antonelli, Backward-forward stochastic differential equations, Ann. Appl. Probab. 3(3) (1993) 777–793. doi:10.1214/aoap/1177005363
D. Duffie and L. G. Epstein, Stochastic differential utility, Econometrica 60(2) (1992) 353–394. doi:10.2307/2951600
E. Pardoux and S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1) (1990) 55–61. doi:10.1016/0167-6911(90)90082-6
C. Dellacherie and P.-A. Meyer, Probabilities and Potential B, North-Holland, 1982 (Theorem VI.57).
P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. doi:10.1007/978-3-662-02619-9

10 thms2 active usersReviewed

All missions

Linear Programming and Finite Markovian Control Problems VIII: Single-Controller Stochastic Games — a Dual Pair of Linear Programs Gives the Value and Stationary Optimal PoliciesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Finite Markovian Control Problems II: An Extreme Optimal Solution of the Dual Linear Program Yields a Pure Stationary Policy Optimal among Transient PoliciesTextbook

Why optimize only transient policies?

The finite model and its policies

Formalization targets

What the result gives

Where the difficulty lies

Formalization scope

Selected references

Outline of an Algorithm for Integer Solutions to Linear Programs: The Fractional Cut (3) Cuts Off the Simplex Solution but Keeps Every Nonnegative Integer Solution and the Integer Maximum of wResearch Paper

Motivation

Setting

Formalization targets

Fractional cut and integer optimum

Supporting claims

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Finite Markovian Control Problems I: Five Equivalent Characterizations of a Transient Markov Decision Problem, among Them Contraction and a Finite Linear ProgramTextbook

Motivation

Setting

Formalization targets

Five equivalent conditions

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Finite Markovian Control Problems III: Contracting Dynamic Programming — Pure, Stationary, Markov and General Policies Span One State-Action Frequency PolytopeTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The Polynomial Hierarchy and a Simple Model for Competitive Analysis: Every Optimum of the (p+1)-Level Linear Game J'(F) Is Binary, with x(F) = 1 iff the Σ_p Sentence (3.3) HoldsResearch Paper

Why multi-level programs are hard

Setting

Formalization targets

Goal: Theorem 4.5 (p≥2p\ge2p≥2)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Shock Models and Wear Processes III: The First Passage Time of a Nondecreasing Markov Wear Process Above a Fixed Level Has an IHRA DistributionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.10 (p. 641)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Markov Decision Chains 3: The Representative of a Pure Stationary Policy Is an Extreme Point of the Dual LPResearch Paper

Linear programs for average-reward Markov decision chains

Setting

Formalization targets

Goal: Theorem 10 (p. 361)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Relation between Customer and Time Averages in Queues: H = λG on Every Sample Path When 0 < λ < ∞, G < ∞ and Each f_n Vanishes Outside [t_n, t_n + s_n] with s_n/n → 0Research Paper

Motivation

Setting

Goal: Theorem 4.5 ( $p\ge2$ )

Milestones: the derivation of $Y$