The OR Formalization Drive

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 5 (p. 29)

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

y^*(n, s_n) - 1

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

Milestones

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

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

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

Significance

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

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

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

A formal development makes each of these precise.

Difficulty

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

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

Formalization scope

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

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

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

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

Conventions and pinnings:

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

Corrections to the book:

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

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

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

Selected references

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

8 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains III: Palm's Theorem for (s–1, s) PoliciesTextbook

Motivation

Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level $s$ . Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.

Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.

Setting

A single item is stocked at one location. Customer orders arrive at epochs $T_0 < T_1 < \cdots$ of a Poisson process with rate $\lambda > 0$ , started empty at time $0$ : the interarrival times $A_k$ are independent and exponential with rate $\lambda$ , and $T_k = A_0 + \cdots + A_k$ . The $k$ -th order triggers a resupply order with resupply time $L_k \ge 0$ . The resupply times are independent and identically distributed, independent of the arrival process, with a density $g$ , distribution function $G(u) = P[L \le u]$ and finite mean

\bar\tau = E[L] = \int_0^\infty [1 - G(u)]\,du .

With backorders allowed, the number of units in resupply at time $t$ is

X(t) = \#\{k : T_k \le t < T_k + L_k\},

and $N(t) = \#\{k : T_k \le t\}$ counts the orders placed in $[0,t]$ . On-hand stock and backorders at time $t$ are $(s - X(t))^+$ and $(X(t) - s)^+$ .

In the compound Poisson version the $k$ -th order asks for $X_k \ge 1$ units, the sizes are i.i.d. with $u_j = P[X_k = j]$ , independent of arrivals and resupply times, and all units of one order share its resupply time $L_k$ . The units in resupply are $Y(t) = \sum_{k : T_k \le t < T_k + L_k} X_k$ . Writing $u^{(y)}_n$ for the probability that $y$ orders ask for $n$ units in total, the compound Poisson probabilities with parameter $\mu$ are

p(n \mid \mu) = \sum_{y=0}^{n} \frac{\mu^y e^{-\mu}}{y!}\,u^{(y)}_n .

In the lost-sales version an order that finds no stock on hand is lost, so at most $s$ units are ever in resupply.

Formalization targets

Goal: Palm's theorem (Theorem 6, p. 39)

For every $x \ge 0$ ,

\lim_{t\to\infty} P[X(t) = x] = e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^x}{x!}.

The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.

The proof's milestones (pp. 38–41)

Eq. (3.5): $P[N(t) = n] = e^{-\lambda t}(\lambda t)^n/n!$ .
Eq. (3.3): given $N(t) = n$ , the epochs $(T_0, \dots, T_{n-1})$ have density $n!/t^n$ on $0 < t_1 < \cdots < t_n < t$ .
Eq. (3.7): given $N(t) = n$ , $X(t)$ is binomial with parameters $n$ and $p = \frac1t\int_0^t[1-G(u)]\,du$ .
Eq. (3.8): for every $t > 0$ , $X(t)$ is Poisson with mean $\lambda\int_0^t[1-G(u)]\,du$ .
Eq. (3.10): $\int_0^t[1-G(u)]\,du \to \bar\tau$ .

Extensions in Section 3.1

Theorem 7 (pp. 43–44): with compound Poisson demand, $\lim_{t\to\infty}P[Y(t) = n] = p(n \mid \lambda\bar\tau)$ .
Theorem 8 (p. 44): in the lost-sales system with exponential resupply times of rate $\beta$ , the probability vectors solving the balance equations are exactly the truncated Poisson law $\pi_x \propto (\lambda/\beta)^x/x!$ , $0 \le x \le s$ .
Theorem 9 (pp. 46–47): for a due-date delay $T \ge 0$ , the units in resupply that have been there for at least $T$ satisfy $\lim_{t\to\infty}P[Y_T(t) = n] = p(n \mid \lambda\bar\tau\alpha)$ with $\alpha = \frac1{\bar\tau}\int_T^\infty[1-G(t)]\,dt$ .

Significance

The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, $\bar\tau$ . This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level $s$ are $\sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$ , the fill rate is $P[X \le s - 1]$ , and both can be optimized over $s$ with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.

Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.

Difficulty

The algebra of the proof (summing the binomial against the Poisson law of $N(t)$ ) is short. The work is in the probabilistic step the book treats in a sentence: that, given $N(t) = n$ , the $n$ orders behave like independent uniform epochs, each of which independently is still in resupply at time $t$ with the same probability $p$ . This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing $P[X(t) = x]$ by conditioning on individual epochs does not go through without that exchangeability step. The limit $t \to \infty$ is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.

Formalization scope

The model is a structure on a probability space $(\Omega, P)$ : exponential interarrival times with rate $\lambda > 0$ , nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from $0$ , so the book's $X_1, \dots, X_n$ are $T_0, \dots, T_{n-1}$ . Counts are cardinalities of sets of order indices, with value $0$ on the probability-zero event where infinitely many orders fall in a bounded interval.

Commitments and pinnings:

"Steady state probability" (Theorems 6, 7, 9) is $\lim_{t\to\infty}P[\cdot(t) = x]$ for the system empty at time $0$ , which is what the proofs compute via (3.8)–(3.11).
Independence of resupply times from arrivals is not written in Theorem 6 but is used on p. 40; it is part of the model.
The stock level $s$ does not enter the backorder model; it matters only in Theorem 8.
Theorem 8 is stated algebraically: a vector on $\{0, \dots, s\}$ solves the balance equations (3.26), (3.25) for $0 < j < s$ and (3.32), and sums to one, if and only if it is the truncated Poisson law. The book obtains these equations by letting $t \to \infty$ in the forward equations under the unproved assumption $P_j'(t) \to 0$ . The book writes (3.25) "for $0 \le j \le s$ ", which at $j = s$ contradicts its own (3.32); the boundary equation (3.32) is used. The sentence on p. 46 extending Theorem 8 to arbitrary resupply densities is asserted without proof and is not stated.
Theorem 7 identifies the limit law by its probabilities (3.22)–(3.23); its mean $\lambda\bar\tau\bar u$ is a property of that law. Theorem 9 is stated for compound demand as the book states it, although the book's proof covers only the Poisson case.

A model in which $X(t)$ is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here $X(t)$ is computed from the primitive arrival and resupply times, whose joint law is fully specified.

Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 3. https://doi.org/10.1007/b138879
C. Palm, "Analysis of the Erlang traffic formula for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
G. J. Feeney and C. C. Sherbrooke, "The (s–1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
C. C. Sherbrooke, "METRIC: A multi-echelon technique for recoverable item control", Operations Research 16(1), 1968, 122–141. https://doi.org/10.1287/opre.16.1.122
S. M. Ross, Stochastic Processes, 2nd ed., Wiley, 1996, Section 2.3 (conditional distribution of arrival times) and Section 2.4 (the M/G/∞ queue).

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains V: Marginal Allocation and Risk PoolingTextbook

Motivation

Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?

Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.

Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.

Setting

Allocation data (Section 7.4). There is a set $M = \{1, \dots, \bar M\}$ of locations and an augmented set $M_0 = \{0\} \cup M$ . Each location $m \in M_0$ has integer gridpoints $0 = r^m_0 < r^m_1 < \dots < r^m_{n(m)}$ . For $m \in M$ , the value $c^m_n$ of a convex function is given at each gridpoint. The slopes (7.19) are $\hat c^m_n = (c^m_{n+1} - c^m_n)/(r^m_{n+1} - r^m_n)$ for $n < n(m)$ , and $\hat c^m_{n(m)}$ repeats the last one. The piecewise linear approximation $\tilde C_m$ of (7.20)–(7.21) interpolates the values $c^m_n$ at the gridpoints and continues with slope $\hat c^m_{n(m)}$ beyond the last one. A convex function $f$ on $\mathbb R_+$ is also given.

The allocation optimization (7.22) asks, for each $n \in N_0 = \{0, \dots, n(0)\}$ , for

c^0_n = f(r^0_n) + \min\Bigl\{ \sum_{m \in M} \tilde C_m(r_m) : r_m \ge 0 \text{ integer},\ \sum_{m \in M} r_m = r^0_n \Bigr\}.

Algorithm AllocOpt (Definition 4) keeps a current gridpoint index $n^*(m)$ and allocation $r^*(m)$ per location. For each increment $r^0_n - r^0_{n-1}$ of the target, it repeatedly gives units to a location $m^*$ whose current slope $\hat c^{m^*}_{n^*(m^*)}$ is minimal, up to that location's next gridpoint, and records the accumulated cost.

Pooling system (Section 7.2.1). One depot supplies $m$ warehouses. The demand $d_{jt}$ at warehouse $j$ in period $t$ is normal with mean $\mu_j$ and variance $\sigma_j^2$ , independent across periods and warehouses. The supplier-to-depot lead time is $D$ periods, the depot-to-warehouse lead time $A$ periods, and holding and backorder costs $h, b$ are equal at all warehouses. Positions $I_j$ are in balance when $\Phi((I_j - A\mu_j)/(\sqrt A\,\sigma_j))$ is the same for all $j$ . For system inventory position $s$ , with $Y_0$ the system demand over $D$ periods and $Y_j$ the demand at $j$ over the next $A + 1$ periods, the balanced allocation gives each warehouse a share proportional to $\sigma_j$ , and $z_j$ is its end-of-period net inventory.

Formalization targets

Goal: Proposition 2 (correctness)

For every tie-breaking rule in its arg min steps, AllocOpt returns values $c^0_n$ that satisfy (7.22) for every $n \in N_0$ : some feasible integer allocation attains $c^0_n - f(r^0_n)$ , and no feasible integer allocation does better.

Milestones

Slope monotonicity (p. 178): $\hat c^m_n \ge \hat c^m_{n-1}$ for $0 < n \le n(m)$ .
Convexity of $\tilde C_m$ on $[0, \infty)$ (proof of Proposition 2, p. 179).
Remark 2 (p. 179): with the inner loop run only while the current slope is $\le 0$ , AllocOpt solves (7.22) with $\sum_m r_m \le r^0_n$ .
Lemma 3 (p. 152): if the positions are in balance and

\sum_{j} d_{j,t-1} \ge \max_{i} \Bigl\{ \sum_{j \ne i} d_{j,t+D-1} + d_{i,t+D-1}\Bigl(1 - \frac{\sum_j \sigma_j}{\sigma_i}\Bigr)\Bigr\},

then a nonnegative allocation of the arriving $\sum_j d_{j,t-1}$ units restores balance. 5. Net inventory law (pp. 156–157): $z_j$ is normal with mean $(s - (D + A + 1)\sum_i \mu_i)\,\sigma_j / \sum_i \sigma_i$ and variance $(A + 1)\sigma_j^2 + (\sigma_j / \sum_i \sigma_i)^2 D \sum_i \sigma_i^2$ . 6. Critical fractile (pp. 157–158): $s$ minimizes $\sum_j E[h (z_j)^+ + b (z_j)^-]$ if and only if $\Phi(z) = b/(b+h)$ , where

z = \frac{s - (D + A + 1)\sum_i \mu_i}{\bigl[(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2\bigr]^{1/2}}.

Significance

The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time $n \log n$ in the number of locations. Because AllocOpt produces the whole vector $(c^0_n)_{n \in N_0}$ in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term $(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2$ is what the book compares with the single-warehouse and the decentralized systems.

On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.

Difficulty

The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets $r^0_{n-1} \to r^0_n$ without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before $u$ reaches zero, and that point is optimal only because the slopes are nondecreasing.

For the pooling results, the balanced allocation mixes the depot-lead-time demand $Y_0$ of all warehouses with the local demand $Y_j$ , and the Gaussian law of $z_j$ rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in $s$ , not only a first-order condition.

Formalization scope

Indices and types. Locations of $M$ are Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: $\bar M \ge 1$ , $n(m) \ge 1$ for $m \in M$ (a slope (7.19) needs two gridpoints), gridpoints starting at $0$ and strictly increasing at every location of $M_0$ , each $c^m_n$ the value of a function convex on $[0, \infty)$ , and $f$ convex on $[0, \infty)$ .
The minimum in (7.22) is stated as attainment plus a lower bound over the finite, nonempty set of feasible integer allocations, never as an unconstrained infimum.
Ties. The book's arg min fixes no tie-breaking rule. Results are stated for every selection rule that returns a minimizing location.
Termination. AllocOpt is a total Lean function. The inner loop is given more passes than it can use, so it always exits through its own condition.
Not stated. The operation count of Proposition 2, $O((1 + \log_2 \bar M)\sum_{m \in M_0} n(m))$ , and Proposition 1 and Remark 1 (p. 177) are operation counts with no machine model and are left out.
Corrections. The first expected-cost display on p. 157 has $+\,b\int_{-\infty}^0 z\,dF_{z_j}(z)$ , which is negative. The formalization uses $b\,E[(z_j)^-]$ , as in the book's next display.
Pinnings. Lemma 3 is deterministic: the demands are arbitrary reals, and "in balance following the allocation" means that some $x_j \ge 0$ with $\sum_j x_j = \sum_j d_{j,t-1}$ exists. The critical-fractile milestone is the characterization "minimizer if and only if $\Phi(z) = b/(b+h)$ " of the book's "can be found by setting".
Trivialization ruled out. The allocation problem (7.22) is defined independently of the algorithm, as a minimum over explicit integer allocations, and the $\tilde C_m$ are built from the data by (7.19)–(7.21). Neither (7.22) nor the $\tilde C_m$ are defined as, or required to agree with, what AllocOpt returns.
Welcome contributions. Lemmas on the invariants of AllocOpt, in particular that after each outer step the allocation $r^*$ is feasible for $r^0_n$ with cost $z$ and all slopes to the left of $n^*(m)$ are at most those to the right. Also Gaussian sum lemmas over finite index sets and a general newsvendor first-order characterization.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005. DOI 10.1007/b138879
G. D. Eppen and L. Schrage, "Centralized ordering policies in a multi-warehouse system with lead times and random demand", in L. B. Schwarz (ed.), Multi-Level Production/Inventory Control Systems: Theory and Practice, Studies in the Management Sciences, North-Holland, Amsterdam, 1981, pp. 51–67.
G. D. Eppen, "Effects of centralization on expected costs in a multi-location newsboy problem", Management Science 25(5), 1979, 498–501. DOI 10.1287/mnsc.25.5.498
B. Fox, "Discrete optimization via marginal analysis", Management Science 13(3), 1966, 210–216. DOI 10.1287/mnsc.13.3.210
T. Ibaraki and N. Katoh, Resource Allocation Problems: Algorithmic Approaches, MIT Press, 1988.

10 thms3 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VI: The Shortfall Distribution of Capacity-Limited SystemsTextbook

Motivation

Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.

The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.

Setting

A single item is produced in periods $n = 1, 2, \dots$ of an infinite horizon; at most $c$ units can be produced per period. The demand of period $n$ is $D_n$ ; the demands are nonnegative, independent and identically distributed, with generic demand $D$ and $E[D] < c$ (the standing assumption of Section 8.1.1).

Under the modified $(s-1, s)$ policy with target level $s$ , the facility observes $D_n$ and produces $\min\{c, s - I_{n-1} + D_n\}$ units, where $I_n$ is the end-of-period net inventory and $I_0 = s$ . The shortfall $V_n = s - I_n$ satisfies $V_0 = 0$ and

V_n = \left[V_{n-1} + D_n - c\right]^+ . \tag{8.1}

With the random walk $S_n = \sum_{k=1}^{n} (D_k - c)$ ( $S_0 = 0$ ), the stationary shortfall is

V = \sup_{n \ge 0} S_n .

A law on $\mathbb R$ is lattice if it is concentrated on a progression $a + d\mathbb Z$ with $d > 0$ .

In the discrete case ( $c$ and $D$ integer valued) $(V_n)$ is a Markov chain on $\{0, 1, 2, \dots\}$ with transition probabilities $p_{ij}$ (p. 185). In the repair model of Section 8.3.1, reparable units of item $i$ arrive at rate $\lambda_i$ , $\lambda = \sum_i \lambda_i$ , a single exponential server repairs at rate $\mu > \lambda$ , $N$ is the number of units in repair and $N_i$ the number of item- $i$ units, and $\eta_i = \lambda_i/(\mu - \lambda + \lambda_i)$ .

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Assume $E[e^{\alpha D}] < \infty$ for all $\alpha < \delta$ , with $\delta > 0$ ; $P[D > c] > 0$ ; the law of $D$ is non-lattice; and $E[e^{-\alpha(c-D)}] = 1$ has a root in $(0, \delta)$ . Then there are $\beta > 0$ and $\alpha > 0$ with

\frac{P\{V > v\}}{\beta e^{-\alpha v}} \to 1 \quad (v \to \infty), \qquad \alpha \text{ the unique positive root of } E\left[e^{-\alpha(c - D)}\right] = 1 .

The constant $\beta$ is left unspecified, as in the book.

Milestones, in attack order

Eq. (8.1): under the modified policy, $s - I_n = V_n$ for every $n$ , independently of $s$ .
Section 8.1.1: $V < \infty$ almost surely, $P\{V_n > v\} \to P\{V > v\}$ for every $v$ , and the law of $V$ is stationary for (8.1).
Eq. (8.2): for $v > 0$ , $P\{V_n > v\} = P\{D_n > v + c\} + E_D[1(d \le v + c)\, P\{V_{n-1} > v + c - d\}]$ .
Theorem 11, second sentence: $E[e^{-\alpha(c-D)}] = 1$ has at most one positive root.
Section 8.1.2: with integer demand, $(V_n)$ is a Markov chain with transition probabilities $p_{ij}$ .
Section 8.1.2: $\pi_i = \lim_n P\{V_n = i\}$ exists and solves $\pi\mathcal P = \pi$ , $\sum_i \pi_i = 1$ , $\pi_i \ge 0$ .
Section 8.3.1: if $N$ is geometric with parameter $\lambda/\mu$ and $N_i$ given $N = j$ is binomial $(j, \lambda_i/\lambda)$ , then $P[N_i = j] = (1 - \eta_i)\eta_i^j$ .
Section 8.3.1: $\sum_{j > s} p_i(j) = \eta_i^{s+1}$ , and the smallest cost-minimising stock level is the smallest $s$ with $\eta_i^{s+1} \le h_i/(h_i + b)$ .

Significance

The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate $\alpha$ depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of $N_i$ reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.

The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.

Difficulty

The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root $\alpha$ turns $P\{V > v\}$ into an expectation under a law with positive drift, but it only yields the upper bound $P\{V > v\} \le e^{-\alpha v}$ (Lundberg's inequality); it does not show that $e^{\alpha v}P\{V > v\}$ converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of $V_n$ with that of $\max_{k \le n} S_k$ , plus the strong law of large numbers to show $V < \infty$ from $E[D] < c$ .

Formalization scope

Model. Demands are real, nonnegative, measurable, i.i.d. (iIndepFun plus IdentDistrib with $D_1$ ), integrable, with $E[D] < c$ ; these are fields of ShortfallModel. Periods are numbered from $1$ as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with $\mathbb N$ -valued demand and capacity.
Stationary shortfall. The book's "stationary distribution ... Let $V$ represent this random variable" is pinned to $V = \sup_{n \ge 0} S_n$ , taken in $[0, \infty]$ and converted to a real number; milestone 2 proves that it is the limit law of $V_n$ from $V_0 = 0$ and a stationary law of (8.1). The discrete $\pi_i$ is pinned to $\lim_n P\{V_n = i\}$ .
Corrections to Theorem 11. The printed theorem is false. For integer demand $P\{V > v\}$ is a step function, and no $\beta e^{-\alpha v}$ is asymptotic to it. If $E[e^{\alpha D}]$ is finite only for $\alpha < \delta$ , the equation $E[e^{-\alpha(c-D)}] = 1$ may have no root in $(0,\delta)$ . The goal therefore adds two labelled hypotheses: a non-lattice demand law, and a root in $(0, \delta)$ . The mass-exponential demand of Section 8.1.3 (an atom at $0$ plus a density) is non-lattice. The approximation $\beta \approx e^{-2(.583)(c-E(D))/\sigma}$ is not stated.
Repair model. The M/M/1 queue is not built. The geometric law of $N$ (asserted on p. 202) and the binomial split of $N$ (quoted from Chapter 3) enter milestone 7 as hypotheses, exactly as the page's proof uses them. The stability condition $\lambda < \mu$ , not written on the page, is a hypothesis. "The optimal $s_i$ " is read as the smallest minimiser of the cost.
Ruled out. Stating Theorem 11 with $\alpha$ or $\beta$ allowed to depend on $v$ , with $\beta = 0$ (the ratio would be a division by zero, which Lean evaluates to $0$ ), or for a $V$ postulated to have an exponential tail proves nothing. Here $\beta, \alpha$ are quantified before $v$ , both are asserted positive, and $V$ is constructed from the demands.
Not formalized. The mass-exponential approximations (8.3)–(8.4), the Roundy–Muckstadt refinement, the fill-rate formula $\eta(s)$ (a definition, whose steady-state identity needs uniform integrability the book does not discuss), the random-capacity chain on p. 186, and the monotonicity of $s_i$ in $\mu$ .
Reusable infrastructure. Welcome: the Lindley recursion and its reversal identity, the Loynes existence theorem, Lundberg's inequality, and a non-lattice renewal theorem. All of these are needed well beyond this mission, in queueing (GI/G/1 waiting times) and ruin theory.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 8. https://doi.org/10.1007/b138879
P. Glasserman, Bounds and asymptotics for planning critical safety stocks, Operations Research 45(2), 244–257, 1997. https://doi.org/10.1287/opre.45.2.244
P. Glasserman and S. Tayur, Sensitivity analysis for base-stock levels in multiechelon production-inventory systems, Management Science 41(2), 263–281, 1995 (the book's reference [97]). https://doi.org/10.1287/mnsc.41.2.263
R. O. Roundy and J. A. Muckstadt, Heuristic computation of periodic-review base stock inventory policies, Management Science 46(1), 104–109, 2000. https://doi.org/10.1287/mnsc.46.1.104.15131
D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Chapter XII.
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Chapter XIII. https://doi.org/10.1007/b97236

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VIII: Bounds on Optimal Stock AllocationsTextbook

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$ , and $J$ is the finite set of bases. For each base $j$ :

$T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$ ;
$T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$ , integers with $1 \le T^e_{ij} < T^r_{ij}$ ;
$\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$ . The latter is constant for $t \ge T^r_{ij}$ , since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
$X_{ijt}$ is the cumulative demand at base $j$ through period $t$ , a nonnegative integer random variable, nondecreasing in $t$ , with finite mean;
$h_{ij} > 0$ , $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$ , the expected cost of that period is

G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,

and stock left at the end of the horizon costs

Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$ , $t = 0, \dots, T_{i0}$ , with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$ , and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$ . The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$ , which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$ . Its largest optimal solution is written $\hat S_{ijt}$ .

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$ , for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$ ,

\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$ : its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$ .
Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$ .
The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$ .
Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$ .
Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$ , $\tilde S_{ijt} \le S^*_{ijt}$ . Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$ , also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$ , provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ .

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$ . Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$ , an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$ . This must be shown feasible, to change only $S_{ijk}$ , and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$ , and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$ , [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
$G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$ , and a tsum for $Q$ . The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$ .
"The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
"An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$ ; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$ 's series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$ ", the book's $\lceil F^{-1}\rceil$ / $\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso " $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ ". Separability is stated both for optimal plans and for optimal values.
Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$ . Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior I: Numerical Utility from the Axioms of Preference and MixtureTextbook

Motivation

Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields $u$ with probability $\alpha$ and $v$ with probability $1-\alpha$ is worth $\alpha\,\mathrm v(u) + (1-\alpha)\,\mathrm v(v)$ . Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).

The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.

Setting

A system of utilities (3.6.1) is an abstract set $U$ of entities $u, v, w, \dots$ , together with

a relation $u > v$ (" $u$ is preferable to $v$ "); write $u < v$ for $v > u$ ;
for every number $\alpha$ with $0 < \alpha < 1$ , an operation producing an element written $\alpha u + (1-\alpha) v$ of $U$ from $u, v \in U$ .

The axioms are:

(3:A) $>$ is a complete ordering: (3:A:a) for any $u, v$ exactly one of $u = v$ , $u > v$ , $u < v$ holds; (3:A:b) $u > v$ , $v > w$ imply $u > w$ .
(3:B) Ordering and combining: (3:B:a) $u < v$ implies $u < \alpha u + (1-\alpha)v$ ; (3:B:b) $u > v$ implies $u > \alpha u + (1-\alpha)v$ ; (3:B:c) $u < w < v$ implies $\alpha u + (1-\alpha)v < w$ for some $\alpha$ ; (3:B:d) $u > w > v$ implies $\alpha u + (1-\alpha)v > w$ for some $\alpha$ .
(3:C) Algebra of combining: (3:C:a) $\alpha u + (1-\alpha)v = (1-\alpha)v + \alpha u$ ; (3:C:b) $\alpha(\beta u + (1-\beta)v) + (1-\alpha)v = \gamma u + (1-\gamma)v$ with $\gamma = \alpha\beta$ .

All weights lie strictly between $0$ and $1$ , and $=$ is identity. The expression $\alpha u + (1-\alpha)v$ is notation for an abstract operation: $U$ carries no linear structure. The Appendix mostly writes the operation as $(1-\gamma)u + \gamma v$ , and writes $u \leqq v$ for " $u = v$ or $u < v$ ". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is $(1-\gamma)u + \gamma v$ .

A numerical utility (3.5.1) is a map $\mathrm v : U \to \mathbb R$ with

\text{(i)}\quad u > v \implies \mathrm v(u) > \mathrm v(v), \qquad \text{(ii)}\quad \mathrm v\big((1-\gamma)u + \gamma v\big) = (1-\gamma)\mathrm v(u) + \gamma\,\mathrm v(v) \quad (0<\gamma<1).

Formalization targets

Goal: (A:V) and (A:W), p. 627

For every system of utilities satisfying (3:A)–(3:C):

\exists\, \mathrm v : U \to \mathbb R \ \text{with (i), (ii)}, \qquad\text{and}\qquad \forall\, \mathrm v, \mathrm v' \text{ with (i), (ii)}:\ \exists\, \omega_0 > 0,\ \omega_1,\ \forall w,\ \ \mathrm v'(w) = \omega_0\,\mathrm v(w) + \omega_1 .

The constants $\omega_0, \omega_1$ are chosen before $w$ . No assumption on the size of $U$ is made.

Milestones

The milestones follow the Appendix's own chain:

(A:A) if $u < v$ and $\alpha < \beta$ then $(1-\alpha)u + \alpha v < (1-\beta)u + \beta v$ ;
(A:B), (A:C) for $u_0 < v_0$ , the map $\alpha \mapsto (1-\alpha)u_0 + \alpha v_0$ is a one-to-one, monotone map of $(0,1)$ onto the utility interval $u_0 < w < v_0$ ;
(A:E), (A:F) the interval function $f_{u_0,v_0}$ of (A:D) (value $0$ at $u_0$ , $1$ at $v_0$ , and the weight $\alpha$ in between) is monotone and linear toward each endpoint, and is characterized by these properties;
(A:R), (A:S) for fixed $u^* < v^*$ , the normalized mapping $h$ with $h(u^*) = 0$ , $h(v^*) = 1$ , monotone, and linear on combinations of $u < v$ , exists and is unique;
(A:T) $(1-\gamma)u + \gamma u = u$ always;
(A:U) $h$ is linear on all combinations, without the restriction $u < v$ .

Significance

The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.

The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.

Difficulty

The obvious argument treats $U$ as a convex set and $\alpha u + (1-\alpha)v$ as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence $(1-\gamma)u + \gamma u = u$ included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs $u > v$ and $u = v$ has to be recovered from the case $u < v$ .

Formalization scope

$U$ is an arbitrary type (Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype $(0,1)$ of $\mathbb R$ . mix α u v stands for $\alpha u + (1-\alpha)v$ . The operation is not defined at $\alpha = 0, 1$ (3.6.1, footnote 4) and is not extended there.
Axiom (3:A:a) is stated literally ("exactly one of the three relations"), so the order is a strict total order and indifference is identity (A.1.2). The weak-order generalization of §66 is not this theorem.
Numbers are real numbers. Monotony is strict, as in (3:1:a).
Standing hypotheses: every item assumes (3:A)–(3:C), bundled in UtilitySystem. The items from (A:E) on assume fixed $u_0 < v_0$ or $u^* < v^*$ as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every $U$ .
The interval function $f_{u_0,v_0}$ is a total Lean function; its value outside $u_0 \leqq w \leqq v_0$ is a placeholder that no statement uses.
A formalization in which $U$ is a convex subset of a vector space, or a space of probability measures, assumes more than the book and makes (A:T) free; it does not count. Neither does a weak monotony, under which constant maps satisfy (A:V) and (A:W) fails.

A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §3 and Appendix. https://doi.org/10.1515/9781400829460
I. N. Herstein, J. Milnor, An axiomatic approach to measurable utility, Econometrica 21 (1953), 291–297. https://doi.org/10.2307/1905540
J. Marschak, Rational behavior, uncertain prospects, and measurable utility, Econometrica 18 (1950), 111–141. https://doi.org/10.2307/1907264

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior II: Games with Perfect Information Are Strictly DeterminedTextbook

Motivation

Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).

Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).

Setting

A game tree $\Gamma$ is a finite rooted tree. Each leaf is a finished play $\pi$ and carries the payoff $\mathfrak F_1(\pi) \in \mathbb R$ to player 1; player 2 receives $-\mathfrak F_1(\pi)$ . Each internal node is a move $\mathfrak M$ of one of three kinds $k$ , with alternatives $\sigma = 1, \dots, \alpha$ leading to subtrees $\Gamma_\sigma$ :

$k = 0$ , a chance move, where alternative $\sigma$ occurs with probability $p(\sigma) \geqq 0$ , $\sum_\sigma p(\sigma) = 1$ ;
$k = 1$ , a personal move of player 1, with $\alpha \geqq 1$ ;
$k = 2$ , a personal move of player 2, with $\alpha \geqq 1$ .

A pure strategy $\tau_1$ of player 1 is a complete plan choosing an alternative at every node of kind 1; $\tau_2$ does the same at every node of kind 2. The normalized form $\mathcal H(\tau_1, \tau_2)$ is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,

v_1 = \operatorname{Max}_{\tau_1} \operatorname{Min}_{\tau_2} \mathcal H(\tau_1, \tau_2), \qquad v_2 = \operatorname{Min}_{\tau_2} \operatorname{Max}_{\tau_1} \mathcal H(\tau_1, \tau_2).

Always $v_1 \leqq v_2$ ; the game is strictly determined when $v_1 = v_2$ (14.4.2).

For a function $f(\sigma_1)$ of the alternatives of the first move $\mathfrak M_1$ , of kind $k_1$ , the operation $M^{k_1}_{\sigma_1}$ of (15:8) is $\sum_{\sigma_1} p_1(\sigma_1) f(\sigma_1)$ , $\operatorname{Max}_{\sigma_1} f(\sigma_1)$ or $\operatorname{Min}_{\sigma_1} f(\sigma_1)$ for $k_1 = 0, 1, 2$ . Applying these operations from the leaves back to the root gives the backward-induction value $v(\Gamma)$ .

Formalization targets

Goal: 15.6.1 with (15:12)

For every finite game tree $\Gamma$ ,

v_1 = v_2 = v = M^{k_1}_{\sigma_1} M^{k_2(\sigma_1)}_{\sigma_2} \cdots M^{k_\nu(\sigma_1, \dots, \sigma_{\nu-1})}_{\sigma_\nu} \mathfrak F_1(\pi(\sigma_1, \dots, \sigma_\nu)).

Both the equality $v_1 = v_2$ and the value formula are part of the goal.

Milestones

(13:E): for finite nonempty domains and $f$ ranging over all functions of $x$ , $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Min}_f \operatorname{Max}_x \psi(x, f(x))$ ; and (13:G): $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Max}_x \operatorname{Min}_u \psi(x, u)$ .
(15:2)–(15:7): $v_k = M^{k_1}_{\sigma_1} v_{\sigma_1/k}$ for $k = 1, 2$ , one milestone for each kind of first move, without assuming that any game is strictly determined.
(15:C:a): a game of length $0$ is strictly determined with value $w$ ; (15:C:b): if every $\Gamma_{\sigma_1}$ is strictly determined, so is $\Gamma$ .
(15:13), (15:D:a)–(15:D:c): for games without chance moves whose plays end in $1, 0, -1$ , the value is one of these three numbers, and it decides which player can force a win or whether both can force a tie.

Significance

The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.

Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.

Difficulty

The recursions (15:2)–(15:7) are not formal consequences of the definitions: $v_1$ and $v_2$ are extrema over whole plans of $\Gamma$ , while the right-hand sides are extrema over plans of the separate games $\Gamma_{\sigma_1}$ . At a personal move of player 1, $v_2 = \operatorname{Max}_{\sigma_1} v_{\sigma_1/2}$ requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over $\tau_1$ and the Min over $\tau_2$ as interchangeable without this step is circular.

A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of $\Gamma$ are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change $\mathcal H$ .

Formalization scope

A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from $0$ ). The conditions $p \geqq 0$ , $\sum p = 1$ and $\alpha \geqq 1$ at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; $\mathcal H$ is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.

Standing hypotheses and conventions taken from the book:

finite strategy sets and attained extrema (13.2.1, 14.1.1): finite trees with finitely many alternatives at every move;
perfect information, i.e. preliminarity equals anteriority (6.4.1, (15:B)): built into the tree model, which is the sequence of games (15:1);
zero-sum two-person (15.3.1): one payoff $\mathfrak F_1$ , player 2 receives $-\mathfrak F_1$ and minimizes $\mathcal H$ ;
chance probabilities nonnegative and summing to one (15.4.2, 10.1.1); $\alpha \geqq 1$ at every move;
(15:D) additionally assumes no chance moves and outcomes $1, 0, -1$ (15.7.1).

The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length $\nu$ for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.

Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make $v_1 = v_2$ trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.

Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of $\Gamma$ with the book's recursive description (15.4.2, 15.5.1).

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§6, 11, 13–15. https://doi.org/10.1515/9781400829460
E. Zermelo, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels, Proc. Fifth International Congress of Mathematicians, vol. II, 1913, pp. 501–504.
U. Schwalbe, P. Walker, Zermelo and the early history of game theory, Games and Economic Behavior 34 (2001), 123–137. https://doi.org/10.1006/game.2000.0794
H. W. Kuhn, Extensive games and the problem of information, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton, 1953, 193–216. https://doi.org/10.1515/9781400881970-012

14 thms3 active usersReviewed

Completed

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

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

A zero-sum two-person game in normalized form is a real matrix $\mathcal H(\tau_1, \tau_2)$ : player 1 chooses a row $\tau_1$ , player 2 simultaneously chooses a column $\tau_2$ , and player 2 pays player 1 the amount $\mathcal H(\tau_1, \tau_2)$ . Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.

Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:

1928. J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Math. Annalen 100, proves that every matrix game has a value in mixed strategies (the minimax theorem), by a topological argument. https://doi.org/10.1007/BF01448847
1937. von Neumann's growth-model paper gives a second proof via a fixed-point argument, later generalized by Kakutani (1941).
1938. J. Ville gives the first elementary proof, based on convexity.
1944. The Theory of Games presents Ville's route: a theorem of the alternative for matrices (§16) yields the minimax theorem (17:6), from which §17 derives the structure of the sets of good strategies.
1951. Gale, Kuhn and Tucker, and Dantzig, relate matrix games to linear-programming duality.

Setting

Player 1 has $\beta_1 \ge 1$ pure strategies $\tau_1$ , player 2 has $\beta_2 \ge 1$ pure strategies $\tau_2$ , and $\mathcal H$ is an arbitrary real $\beta_1 \times \beta_2$ matrix (14.1.1). A mixed strategy of player 1 is a probability vector $\xi$ in the simplex

S_{\beta_1} = \Big\{ \xi \in \mathbb R^{\beta_1} : \xi_{\tau_1} \ge 0,\ \sum_{\tau_1} \xi_{\tau_1} = 1 \Big\},

and similarly $\eta \in S_{\beta_2}$ for player 2. The pure strategy $\tau$ is the coordinate vector $\delta^{\tau}$ . The expected payoff is the bilinear form (17:2)

K(\xi, \eta) = \sum_{\tau_1=1}^{\beta_1} \sum_{\tau_2=1}^{\beta_2} \mathcal H(\tau_1, \tau_2)\, \xi_{\tau_1} \eta_{\tau_2}.

The good strategies of player 1 form the set $\bar A$ of those $\xi \in S_{\beta_1}$ at which $\operatorname{Min}_\eta K(\xi, \eta)$ assumes its maximum; those of player 2 form the set $\bar B$ of those $\eta \in S_{\beta_2}$ at which $\operatorname{Max}_\xi K(\xi, \eta)$ assumes its minimum ((17:B:a), (17:B:b)). A saddle point of $K$ is a pair with $K(\xi', \eta) \le K(\xi, \eta) \le K(\xi, \eta')$ for all $\xi', \eta'$ . With pure strategies alone one has $v_1 = \operatorname{Max}_{\tau_1}\operatorname{Min}_{\tau_2}\mathcal H$ and $v_2 = \operatorname{Min}_{\tau_2}\operatorname{Max}_{\tau_1}\mathcal H$ ; the game is specially strictly determined when $v_1 = v_2$ .

For a general real function $\phi(x, y)$ (§13) the same notions are $\operatorname{Max}_x \operatorname{Min}_y \phi$ , $\operatorname{Min}_y \operatorname{Max}_x \phi$ , saddle points, and the sets $A^\phi$ (maximizers of $\operatorname{Min}_y \phi$ ) and $B^\phi$ (minimizers of $\operatorname{Max}_x \phi$ ), always under the book's standing hypothesis that these maxima and minima exist.

Formalization targets

Goal: (17:D), good strategies characterized by their supports

For all $\xi \in S_{\beta_1}$ and $\eta \in S_{\beta_2}$ : $\xi \in \bar A$ and $\eta \in \bar B$ if and only if

\xi_{\tau_1} = 0 \text{ whenever } \sum_{\tau_2} \mathcal H(\tau_1, \tau_2)\eta_{\tau_2} < \max_{\tau_1'} \sum_{\tau_2} \mathcal H(\tau_1', \tau_2)\eta_{\tau_2},

\eta_{\tau_2} = 0 \text{ whenever } \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1} > \min_{\tau_2'} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2')\xi_{\tau_1}.

The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.

Milestones, in attack order

(13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$ .
(13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$ , the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$ .
(17:A) $\operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_{\tau_2} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1}$ , and dually for $\operatorname{Max}_\xi$ .
(16:C) For every matrix $a(i, j)$ exactly one of: some $x \in S_m$ with $\sum_j a(i,j)x_j \le 0$ for all $i$ ; some $w \in S_n$ with $\sum_i a(i,j)w_i > 0$ for all $j$ .
(16:F) The weak form with $\ge 0$ in place of $> 0$ .
(17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
(17:C:f) $\xi \in \bar A$ and $\eta \in \bar B$ iff $\xi, \eta$ is a saddle point of $K$ .

After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.

Significance

(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure $\bar A \times \bar B$ of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.

The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.

Difficulty

The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value $\operatorname{Max}_\xi \operatorname{Min}_\eta K$ equals $\operatorname{Min}_\eta \operatorname{Max}_\xi K$ , i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of $A^\phi \times B^\phi$ exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.

Formalization scope

Lean conventions, fixed throughout:

Pure strategies are Fin β₁, Fin β₂ (numbered from $0$ ), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and $S_\beta$ is Mathlib's stdSimplex ℝ (Fin β).
Nonempty strategy sets ( $\beta \ge 1$ , from "τ = 1, …, β" in 14.1.1): every theorem assumes 0 < β₁, 0 < β₂, or mixed strategies $\xi \in S_{\beta_1}$ , $\eta \in S_{\beta_2}$ , which force it. The theorems of the alternative assume $n, m \ge 1$ (a matrix with rows and columns).
Standing hypothesis of 13.2.1 ("we are restricting our considerations to such functions, for which Max and Min exist"): the §13 results (13:A*), (13:D*) are stated for an arbitrary $\phi : X \times Y \to \mathbb R$ under the predicate MaxMinAttained φ, which says that $\operatorname{Min}_y \phi(x, y)$ , $\operatorname{Max}_x \phi(x, y)$ , $\operatorname{Max}_x \operatorname{Min}_y \phi$ and $\operatorname{Min}_y \operatorname{Max}_x \phi$ are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as $\operatorname{Max}_x \operatorname{Min}_y \phi = \operatorname{Min}_y \operatorname{Max}_x \phi$ .
$\operatorname{Max}$ and $\operatorname{Min}$ are the real ⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of $K$ for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at $\tau_1$ " in the goal is written without any Max operator.
$\bar A$ , $\bar B$ are defined as maximizers and minimizers directly from $K$ , not through an assumed value $v'$ .

A trivializing formalization is ruled out: $\bar A$ and $\bar B$ are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.

Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§13, 16, 17. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
J. Ville, "Sur la théorie générale des jeux où intervient l'habileté des joueurs", in É. Borel, Traité du calcul des probabilités et de ses applications, IV.2, Gauthier-Villars, 1938, 105–113.
S. Kakutani, "A generalization of Brouwer's fixed point theorem", Duke Mathematical Journal 8 (1941), 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

11 thms4 active usersReviewed

Completed

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

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

Motivation

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

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

Setting

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

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

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

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

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

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

The two optimization problems are

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

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

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

Selected references

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

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior IV: The Characteristic Function of a Zero-Sum n-Person GameTextbook

Motivation

Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function $v(S)$ : the amount a group of players $S$ can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).

§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.

Setting

A zero-sum $n$ -person game in normalized form $\Gamma$ (11.2.3, 25.1.3) has players $k = 1, \dots, n$ . Player $k$ chooses a pure strategy $\tau_k \in \{1, \dots, \beta_k\}$ , $\beta_k \geqq 1$ , uninformed about the others' choices, and then receives the real amount $\mathcal H_k(\tau_1, \dots, \tau_n)$ , subject to (25:1)

\sum_{k=1}^n \mathcal H_k(\tau_1, \dots, \tau_n) \equiv 0 .

Let $I = \{1, \dots, n\}$ and, for $S \subseteq I$ , $-S = I \setminus S$ . The book defines $v(S)$ in 25.1.3 through a fictitious two-person game: all players of $S$ form one composite player $1'$ , all players of $-S$ another, $2'$ . The pure strategies of $1'$ are the aggregates $\tau^S$ (one choice $\tau_k$ for each $k \in S$ ), those of $2'$ are the aggregates $\tau^{-S}$ , and $1'$ receives (25:2)

\overline{\mathcal H}(\tau^S, \tau^{-S}) = \sum_{k \in S} \mathcal H_k(\tau_1, \dots, \tau_n).

A mixed strategy of $1'$ is a probability vector $\xi$ on the set of all aggregates $\tau^S$ , and one of $2'$ is a probability vector $\eta$ on the aggregates $\tau^{-S}$ . With $K(\xi, \eta) = \sum_{\tau^S, \tau^{-S}} \overline{\mathcal H}(\tau^S, \tau^{-S})\, \xi_{\tau^S} \eta_{\tau^{-S}}$ ,

v(S) = \operatorname{Max}_\xi \operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_\eta \operatorname{Max}_\xi K(\xi, \eta).

The coalition therefore randomizes jointly: $\xi$ is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and $I$ are coalitions too (footnote 2, p. 241).

The three conditions of 25.3.1 on a set function $v$ are

\text{(25:3:a)}\ v(\ominus) = 0, \qquad \text{(25:3:b)}\ v(-S) = -v(S), \qquad \text{(25:3:c)}\ v(S \cup T) \geqq v(S) + v(T) \ \text{ if } S \cap T = \ominus .

From 26.2 on, every set function satisfying them is called a characteristic function.

Two such functions are strategically equivalent (27.1) if $v'(S) = v(S) + \sum_{k \in S} \alpha^0_k$ for numbers $\alpha^0_k$ with $\sum_k \alpha^0_k = 0$ ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written $-\gamma$ , (27:5). A game is inessential if the reduced form of its characteristic function is $\equiv 0$ , and essential otherwise (27.3).

Formalization targets

Goal: the characterization of characteristic functions (26.2)

v \text{ satisfies (25:3:a)–(25:3:c)} \iff \exists\, \Gamma \text{ zero-sum } n\text{-person game with } v_\Gamma = v .

The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game $\Gamma$ realizing $v$ on every coalition simultaneously.

Milestones

25.3.1: every $v_\Gamma$ satisfies (25:3:a)–(25:3:c).
(25:A): the three conditions are equivalent to $v(S_1) + \dots + v(S_p) \leqq 0$ on decompositions of $I$ for $p = 1, 2, 3$ , with equality for $p = 1, 2$ .
26.1.1: every $v$ satisfying (25:3:a)–(25:3:c) is $v_\Gamma$ for some game $\Gamma$ .
(27:A): every characteristic function is strategically equivalent to exactly one reduced characteristic function, given by (27:2), (27:4).
(27:7): for reduced $\bar v$ and every $p$ -element $S$ , $-p\gamma \leqq \bar v(S) \leqq (n-p)\gamma$ , with equality in the stated boundary cases.
(27:B): inessential iff $\sum_j v((j)) = 0$ ; essential iff $\sum_j v((j)) < 0$ .
(27:C) and (27:D): inessential iff $v$ is additive, $v(S) \equiv \sum_{k \in S} \alpha^0_k$ , equivalently iff (25:3:c) always holds with equality.

Significance

The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on $v$ is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by $n$ and turns essentiality into a sign condition, which is used throughout the rest of the book.

These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ( $v(\emptyset) = 0$ only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an $n$ -person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.

Difficulty

The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition $S \cup T$ can guarantee as much as $S$ and $T$ separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since $v(-S)$ is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract $v$ one must produce one finite game whose characteristic function matches $v$ on all $2^n$ coalitions at once. Producing, for each $S$ separately, a game with the right value $v_\Gamma(S)$ is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.

Formalization scope

Players are Fin n (the book's $1, \dots, n$ are $0, \dots, n-1$ ), coalitions are Finset (Fin n), $-S$ is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate $\tau^S$ is a dependent function on the members of $S$ ; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's $\xi$ is a single distribution on aggregates, as in 25.1.3. The Max and Min in $v(S)$ are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on $n$ is imposed: the book's statements remain true for $n = 0$ and $n = 1$ , so dropping the implicit $n \geqq 1$ is a harmless strengthening.

Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of $\gamma$ ; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with $\frac1n$ as a real division that only matters for $n \geqq 1$ .

A trivializing reading of the goal, "for every $S$ there is a game with $v_\Gamma(S) = v(S)$ ", is excluded: the statement asks for one game $\Gamma$ with $v_\Gamma = v$ as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.

A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along $S$ and $-S$ , and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§25–27, pp. 238–254. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320 (the minimax theorem used for $v(S)$ ). https://doi.org/10.1007/BF01448847
M. Maschler, E. Solan and S. Zamir, Game Theory, Cambridge University Press, 2013, Ch. 16 (coalitional games with transferable utility). https://doi.org/10.1017/CBO9780511794216

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

16 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VII: Simple Games, Weighted Majorities and the Main Simple SolutionTextbook

Motivation

Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum $n$ -person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.

The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.

Setting

A zero-sum $n$ -person game with players $I = \{1, \dots, n\}$ is represented by its characteristic function $v$ , a real function on the subsets of $I$ with $v(\ominus) = 0$ , $v(-S) = -v(S)$ ( $-S$ the complement) and $v(S \cup T) \geqq v(S) + v(T)$ for disjoint $S, T$ . An imputation is a vector $\vec\alpha$ with $\alpha_i \geqq v((i))$ and $\sum_i \alpha_i = 0$ ; $\vec\alpha$ dominates $\vec\beta$ if some nonempty $S$ has $\sum_{i\in S}\alpha_i \leqq v(S)$ and $\alpha_i > \beta_i$ for $i \in S$ ; a solution is a set $V$ of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.

A coalition $S$ is flat if $v(S) = \sum_{k\in S} v((k))$ . The losing coalitions $L_\Gamma$ are the flat sets, and the winning coalitions $W_\Gamma$ are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. $W^m$ denotes the minimal winning coalitions, those of which no proper subset wins.

Weights $w_1, \dots, w_n$ define the winning system $W = \{S : \sum_{i\in S} w_i > \tfrac12 \sum_i w_i\}$ , and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game $[w_1,\dots,w_n]$ . The weights are homogeneous if the advantage $a_S = \sum_{i\in S} w_i - \sum_{i\in -S} w_i$ is the same for all $S$ in $W^m$ .

In §50 the game is taken in reduced form with $\gamma = 1$ , so $v((i)) = -1$ . For numbers $x_i \geqq 0$ and a coalition $S$ let $\vec\alpha^S$ give $-1$ to the players outside $S$ and $-1 + x_i$ to player $i$ in $S$ . When the $x_i$ satisfy $\sum_{i \in S} x_i = n$ for every $S \in W^m$ , the set $V$ of all $\vec\alpha^S$ , $S \in W^m$ , is a main simple solution.

Formalization targets

Goal: (50:K), p. 444

\text{Every homogeneous weighted majority game possesses a main simple solution,}

namely the set of $\vec\alpha^S$ , $S \in W^m$ , with $x_i = \frac{n}{b} w_i$ , $b = \frac12(\sum_i w_i + a)$ , $a$ the common advantage. Conversely, if $x_i \geqq 0$ solve $\sum_{i\in S} x_i = n$ on $W^m$ , then $w_i = x_i$ are homogeneous weights for the game if and only if

\sum_{i=1}^n x_i < 2n .

Milestones

(49:C) $L_\Gamma$ contains the empty set and all one-element sets.
(49:A) $W_\Gamma, L_\Gamma$ are mapped onto each other by complementation, $W_\Gamma$ is closed under supersets, and $L_\Gamma$ is closed under subsets.
(49:B) $W_\Gamma \cap L_\Gamma = \ominus$ if and only if the game is essential. If the game is inessential, every set is both winning and losing.
(49:F) The pairs $W, L$ of simple games are exactly those satisfying (48:A:a)–(48:A:d) and (49:C).
(50:A) The essential three-person game is simple: it is the direct majority game.
(50:B) Non-negative weights define a winning system with (49:W*) if and only if (50:B:a), (50:B:b) hold.
(50:D) $a_S > 0$ on $W$ , $a_S < 0$ on $L$ , and $a_S = 0$ never occurs.
(50:G) An imputation $\vec\beta$ is undominated by $V = \{\vec\alpha^S : S \in U\}$ if and only if $R(\vec\beta) \in U^+$ .
(50:J) The exact criterion (50:8*), (50:9*) for $V$ to be a solution.

Significance

The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.

All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.

Difficulty

The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether $V$ is a solution means classifying every imputation $\vec\beta$ by the set $R(\vec\beta)$ where it meets the shares $-1 + x_i$ .

The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of $U^+$ with $\sum_{i\in T} x_i < n$ by producing infinitely many undominated imputations against a finite $V$ . It also has to handle indifferent players with $x_i = 0$ , whose presence makes $R(\vec\beta)$ larger than the coalition that generated $\vec\beta$ . For the converse half of the goal, the obstacle is the strict inequality $a > 0$ : the equations (50:17) are linear and say nothing about it.

Formalization scope

Players are Fin n (the book's player $i$ is index $i - 1$ ), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every $v$ satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.

The standing hypotheses, stated in each theorem where the book has them in force:

(25:3:a)–(25:3:c) on $v$ in every theorem;
simplicity (essential + (49:1:b)) in (50:G), (50:J), (50:K);
the reduced form with $\gamma = 1$ , as $v((i)) = -1$ for all $i$ (50.4.1), in (50:G), (50:J), (50:K);
$U \subseteq W^m$ , (50:7) $x_i \geqq 0$ and (50:8) $\sum_{i\in S} x_i = n$ for $S \in U$ (50.5.1) in (50:G), (50:J);
(50:B) on the weights in (50:D) and in the first half of (50:K);
non-negative weights in (50:B). The book states (50:B) for arbitrary real weights, but its "only if" direction is false without $w_i \geqq 0$ : $[10, 10, 10, -\tfrac1{10}]$ is a counterexample. The corrected statement is recorded in the item.

The numbers $x_i$ are given for every player. Players in no minimal winning coalition, for whom the book defines no $x_i$ , do not affect any $\vec\alpha^S$ . In the converse of (50:K) the derived weights are $w_i = x_i$ for every player.

The goal is not the bare solvability of (50:17). A statement that only asserted " $x$ exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of $\vec\alpha^S$ is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set $V$ is built from $W^m$ only, never from all of $W$ .

Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting $W_\Gamma$ of a simple reduced game with the explicit formula (49:2), $v(S) = n - |S|$ on $W$ and $-|S|$ on $L$ .

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary ed., Princeton University Press, 2007 (reprint of the 3rd ed., 1953), Chapter X, §§48–50, pp. 420–444. https://doi.org/10.1515/9781400829460
L. S. Shapley, M. Shubik, "A method for evaluating the distribution of power in a committee system", American Political Science Review 48 (1954) 787–792. https://doi.org/10.2307/1951053

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VIII: Characteristic Functions of General n-Person GamesTextbook

Motivation

The theory of Theory of Games and Economic Behavior (von Neumann and Morgenstern, 1944; 3rd ed. 1953) rests on one object: the characteristic function $v(S)$ , the amount a coalition $S$ of players can secure for itself whatever the other players do. For zero-sum $n$ -person games, Chapter VI defines $v(S)$ and proves (25.3.1 and 26.1.1) that the set functions arising this way are exactly those with $v(\emptyset)=0$ , $v(-S)=-v(S)$ and superadditivity. Economic applications, however, are rarely zero-sum: exchange and production create value. Chapter XI extends the theory to general (non-zero-sum) games by adding a fictitious player who absorbs the total gain, and §57 answers the question that decides the scope of this extension: which set functions are characteristic functions of general games?

The answer, that these are exactly the superadditive set functions vanishing on the empty set, is the reason why the cooperative game theory that followed could take "a superadditive $v$ with $v(\emptyset)=0$ " as its primitive object, usually without any underlying strategic game.

Setting

A general $n$ -person game $\Gamma$ in normalized form has players $I=\{1,\dots,n\}$ . Player $k$ chooses $\tau_k\in\{1,\dots,\beta_k\}$ with $\beta_k\ge 1$ , without knowing the choices of the others, and receives the real amount $\mathcal H_k(\tau_1,\dots,\tau_n)$ . No condition is imposed on $\sum_k\mathcal H_k$ . The game is zero-sum if $\sum_{k=1}^n\mathcal H_k\equiv 0$ .

The zero-sum extension $\overline\Gamma$ (56.2.2) adds a fictitious player $n+1$ , who has no move and receives

\mathcal H_{n+1}(\tau_1,\dots,\tau_n)=-\sum_{k=1}^n\mathcal H_k(\tau_1,\dots,\tau_n).

Write $\overline I=\{1,\dots,n,n+1\}$ . For $S\subseteq\overline I$ , the coalition $S$ and its complement $\bot S=\overline I-S$ play a zero-sum two-person game. The pure strategies of $S$ are the tuples of choices of its real members. A mixed strategy $\xi$ of $S$ is a single probability distribution over these tuples, so the members of a coalition randomize jointly, and likewise $\eta$ for $\bot S$ . The payoff to $S$ is $\sum_{k\in S}\mathcal H_k$ . Then

v(S)=\max_\xi\min_\eta K(\xi,\eta),

where $K$ is the expected payoff to $S$ . The function $v$ on all $S\subseteq\overline I$ is the extended characteristic function; its restriction to $S\subseteq I$ is the restricted characteristic function (57.1). For a zero-sum game the restricted function is the characteristic function of Chapter VI.

Formalization targets

Goal: 57.3.4

For every $n$ and every set function $v$ on the subsets of $I$ ,

v \text{ is the restricted characteristic function of some general game} \iff v(\emptyset)=0 \text{ and } v(S\cup T)\ge v(S)+v(T) \text{ for } S\cap T=\emptyset,

and for every set function $v$ on the subsets of $\overline I$ ,

v \text{ is the extended characteristic function of some general game} \iff v(\emptyset)=0,\ v(\bot S)=-v(S),\ v \text{ superadditive}.

In each direction a single game realizes $v$ on every set simultaneously; $v(I)$ is not constrained.

Milestones

(57:1:a)–(57:1:c): necessity of the extended conditions.
(57:2:a), (57:2:c), (57:2:b): necessity of the restricted conditions, including $v(-S)\le v(I)-v(S)$ .
57.3.1: sufficiency of (57:2:a), (57:2:c).
57.3.3: sufficiency of (57:1:a)–(57:1:c).
(57:G): for such $v$ , $v(-S)=-v(S)$ for all $S$ holds iff $v(S)+v(-S)=v(I)$ for all $S$ and $v(I)=0$ .
(57:B): in a zero-sum game every one-element set of players is removable, meaning that some zero-sum game with the same characteristic function has payoffs that do not depend on that player's choice.
(57:C): the set of all players is removable iff the game is inessential, i.e. $v(S)=\sum_{k\in S}\alpha_k$ .

Significance

The characterization fixes the domain of Chapter XI: every statement about solutions of general games is, by 57.3.4, a statement about superadditive set functions with $v(\emptyset)=0$ , and conversely every such function is attained by a strategic game. That converse justifies studying cooperative games abstractly. (57:G) separates the zero-sum and constant-sum subclasses inside this domain. (57:B) and (57:C) quantify how much of a player's strategic role survives when his moves are removed, which is the book's justification for the fictitious player.

Status: all results are proved in the book (1944). To our knowledge none of them is machine-checked; the Prove2Me catalog has superadditive and convex cooperative games, but none tied to a strategic game, and no characteristic function built from a minimax value. The work here is formalizing the known proofs.

Difficulty

Necessity reduces to the zero-sum theory applied to $\overline\Gamma$ , but still requires the minimax theorem for the coalition's two-person game and a careful treatment of joint mixing when two disjoint coalitions merge. Sufficiency requires building one finite game whose coalition values equal an arbitrary superadditive $v$ exactly, for all $2^n$ coalitions at once. The obvious attempt, choosing payoffs coalition by coalition, fails because the payoffs are shared: a construction that gives $S$ the right value can change the value of every set that overlaps $S$ . The difficulty is to obtain the upper bound $v(S)\le v_0(S)$ for every $S$ simultaneously. For the extended function there is a further difficulty. The fictitious player has no move, so the values on sets containing $n+1$ are forced by the others, and they must be reconciled with (57:1:b).

For (57:B), the target game must reproduce an arbitrary zero-sum characteristic function while one prescribed player's choice has no effect on any payoff.

Formalization scope

Players are Fin n (book indices $1,\dots,n$ become $0,\dots,n-1$ ); sets of players are Finset (Fin n). The extended domain $\overline I$ is Fin (n + 1) with the fictitious player Fin.last n, and $\bot S$ is the complement in Fin (n + 1). A game (GeneralGame n) has $\beta_k\ge1$ strategies Fin (β k) per player and real payoffs; zero-sum is the predicate IsZeroSum. The fictitious player's single strategy is left out of the coalition's strategy tuples, which does not change the two-person game. Max and Min are ⨆/⨅ over Mathlib's stdSimplex on the coalition's strategy tuples (one joint distribution per coalition). Both simplices are nonempty and the payoff is bounded, so these are attained values and no junk value from an empty or unbounded supremum occurs.

Standing hypotheses and their instantiation:

finite strategy sets with $\beta_k\ge1$ (11.2.3, 56.2.2): a field of GeneralGame;
"always assuming (57:2:a), (57:2:c)" for (57:G) (p. 537): an explicit hypothesis;
"zero-sum $n$ -person game" in (57:A)–(57:C) (p. 533): the hypothesis Γ.IsZeroSum and the requirement that the replacement game $\Gamma'$ is zero-sum;
"no influence upon the course of the game" (57:A): all payoffs are independent of that player's variable, as in the proof of (57:C) on p. 534;
"inessential" (57:C): the additive form (57:13), which p. 534 calls "precisely the definition of inessentiality".

No normalization is imposed: $v(I)$ is arbitrary and nothing is reduced. Every statement is made for all $n\ge0$ ; the book's $n\ge1$ is not needed, so this is a strengthening.

A trivializing formalization is ruled out: the characteristic function is defined from the game through the coalition's minimax value, so it is never a free parameter, and the existence claims must produce one game for all coalitions at once.

Needed infrastructure: finite zero-sum two-person games with joint mixed strategies over dependent product types; the minimax theorem ((17:6), on the platform as AGT.zero_sum_minimax for matrices); and product decompositions of coalition strategy tuples. The coalition-value API is reusable for any mission built on characteristic functions (Chapters VI, IX–XI). Contributions of this API as separate lemmas are welcome.

Not stated: (57:E*), (57:F*) (given without proof on p. 535), the open question (57:D), and (57:H), because the notion of a "dummy" it uses (from 46.9 and 56.3) is not defined on these pages.

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§56–57, pp. 504–537. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior IX: Solutions for Acyclic RelationsTextbook

Motivation

The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set $D$ and an arbitrary relation $\mathcal S$ on $D$ , and ask which properties of $\mathcal S$ guarantee that exactly one solution exists.

The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc $x \to y$ whenever $x\mathcal S y$ ; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.

Timeline.

1944 (1st ed.; 3rd ed. 1953, reprinted 2007): von Neumann and Morgenstern define solutions for an arbitrary relation (§65), show that a finite set with an acyclic relation has exactly one solution (65:X), and that acyclicity is necessary for every subset to have a unique solution (65:Z).
1953: M. Richardson, Solutions of irreflexive relations, extends existence (not uniqueness) to finite relations without cycles of odd length.

Setting

Let $D$ be an arbitrary set and $\mathcal S$ an arbitrary relation on $D$ ; $x\mathcal S y$ is read " $x$ dominates $y$ ". A solution (in $D$ for $\mathcal S$ ) is a set $V \subseteq D$ with

\text{(65:1)}\qquad V = \{\, y \in D : x\mathcal S y \text{ holds for no } x \in V \,\}.

For $E \subseteq D$ , an element $x$ is a maximum of $E$ if $x \in E$ and no $y \in E$ has $y\mathcal S x$ ; the set of maxima is $E^m$ .

For $m \ge 1$ , condition $(A_m)$ says: never $x_1\mathcal S x_0, x_2\mathcal S x_1, \dots, x_m\mathcal S x_{m-1}$ with $x_0 = x_m$ and all $x_i \in D$ . The relation is acyclic if it satisfies every $(A_m)$ , $m = 1, 2, \dots$ ; in particular never $x\mathcal S x$ . It is strictly acyclic if there is no infinite sequence $x_0, x_1, x_2, \dots$ in $D$ with $x_{i+1}\mathcal S x_i$ for every $i$ . Property (65:K) says that every non-empty $E \subseteq D$ has $E^m \ne \ominus$ . A partial ordering (65:B) is a transitive relation for which at most one of $x = y$ , $x\mathcal S y$ , $y\mathcal S x$ holds.

For the main theorem the book constructs a candidate solution by induction (65.7.1): $A_1 = D$ ; $B_i = A_i^m$ ; $C_i$ is the set of elements of $A_i$ dominated by some element of $B_i$ ; $A_{i+1} = A_i - B_i - C_i$ . With $i_0$ the first index for which $A_{i_0} = \ominus$ ,

\text{(65:2)}\qquad V_0 = B_1 \cup \cdots \cup B_{i_0 - 1}.

In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning $x\mathcal S y$ ; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.

Formalization targets

Goal: (65:X)

If $D$ is finite and $\mathcal S$ is acyclic on $D$ , then

\exists!\, V:\ V \text{ is a solution in } D \text{ for } \mathcal S, \qquad\text{and}\qquad V \text{ is a solution} \iff V = V_0 .

Milestones, in attack order

(65:I) For a partial ordering, a finite $D$ satisfies (65:G): every non-maximal $y$ is dominated by some maximum.
(65:H) For a partial ordering of an arbitrary $D$ : $V$ is a solution $\iff$ (65:G) holds and $V = D^m$ .
(65:O:c) Strict acyclicity implies acyclicity; for finite $D$ the two are equivalent.
(65:P) (65:K) $\iff$ strict acyclicity, for arbitrary $D$ .
(65:S) For finite $D$ and acyclic $\mathcal S$ , some $A_i$ is empty.
(65:V) For finite $D$ and acyclic $\mathcal S$ , every solution equals $V_0$ .
(65:W) For finite $D$ and acyclic $\mathcal S$ , $V_0$ is a solution.
(65:Z) If every $E \subseteq D$ has a unique solution in $E$ for $\mathcal S$ , then $\mathcal S$ is acyclic on $D$ .

Significance

The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of $D$ , it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.

Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of $V_0$ , and the characterization of 65.8.2.

Difficulty

Most of the individual steps are short. The work is in making the book's finite induction precise. The sets $A_i$ are defined recursively and $V_0$ refers to the first empty stage $i_0$ . The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest $k$ with $y \notin A_k$ " and the disjoint decomposition (65:U) of $D$ into the $B_i$ and $C_i$ . A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the $V_0$ of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.

Formalization scope

Representation. An ambient type α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on $D$ (or its restriction to $E$ ). Finite and infinite sequences are functions ℕ → α.
Solutions. IsSolution D S V is the set equation (65:1) literally; it forces $V \subseteq D$ . Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.
Acyclicity. IsAcyclic D S requires $(A_m)$ for every $m \ge 1$ , all cycle elements in $D$ . The case $m = 0$ is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside $D$ , but the book's form is stated.
Construction. Stages are indexed from $0$ : stageA D S k is the book's $A_{k+1}$ . V0 D S is the union of all $B_i$ , which equals $B_1 \cup \cdots \cup B_{i_0 - 1}$ because every later $B_i$ is empty.
Standing hypotheses instantiated. (65:S), (65:V), (65:W) and the goal (65:X) carry the hypotheses of 65.7.1, " $D$ finite and $\mathcal S$ acyclic" (for finite $D$ equivalently strictly acyclic, i.e. (65:K)), as D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of $D$ . (65:O:c), (65:P) and (65:Z) are for arbitrary $D$ and $\mathcal S$ , as 65.6.2 and 65.8.2 state. The empty $D$ is allowed everywhere; there the unique solution is $\ominus$ .
Not stated. The infinite case of (65:X) and of (65:Y), which the book leaves open (65.7.1, 65.8.3, question (65:9)); the complete-ordering results (65:E), (65:F), which silently assume $D \neq \ominus$ ; the counting statement (65:8).
Needed infrastructure. Finite-set induction and pigeonhole on Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §65, pp. 587–602. https://doi.org/10.1515/9781400829460
M. Richardson, Solutions of irreflexive relations, Annals of Mathematics 58 (1953), 573–590. https://doi.org/10.2307/1969755

13 thms4 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems I: Finite Horizon Optimality and Approximating SequencesTextbook

Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each $i \in S$ a finite nonempty action set $A_i$ ; a finite cost $C(i,a) \ge 0$ ; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$ . A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$ , and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ : it may use the whole history and may randomize. Stationary policies $f$ ( $f(i) \in A_i$ ) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ( $\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$ . A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$ . For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$ , the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$ . Its value functions are $v^N_{\alpha,n}$ . In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$ . Assumption FH( $\alpha$ , $n$ ) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$ . A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$ .

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$ ,

\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$ .

Milestones

Proposition A.1.1: a probability average of $u$ is at least $\min u$ , with equality iff the distribution is concentrated on the minimizers.
Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$ , and the characterization of all optimal general policies.
Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$ .
Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$ , have limit points.
Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH( $\alpha$ , $n$ ), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$ . This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$ , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$ , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$ ; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$ , which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$ ; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$ ).

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

14 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems II: The Discount Optimality EquationTextbook

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$ . A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ ; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$ .

Fix a discount factor $\alpha \in (0,1)$ . For an initial state $i$ and a policy $\theta$ , the $n$ -horizon cost with terminal cost zero and the infinite horizon discounted cost are

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ , infima over all policies. All of these lie in $[0,\infty]$ . A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$ . The discount optimality equation is

W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}

With $W = V_\alpha$ , $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$ .

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$ ; and every stationary policy $f_\alpha$ with

C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ( $v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$ ); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$ ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$ ); then, beyond the goal, Corollary 4.1.5 ( $\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$ ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$ ), Proposition 4.3.1 ( $v_{\alpha,n} \uparrow V_\alpha$ , and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$ . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$ , where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
All values ( $v_{\theta,\alpha,n}$ , $V_{\theta,\alpha}$ , $v_{\alpha,n}$ , $V_\alpha$ , and the competing solutions $W$ ) are ℝ≥0∞-valued; $0 \cdot \infty = 0$ . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
$V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$ , and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems III: Approximating Sequences for the Discounted Cost CriterionTextbook

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC( $\alpha$ ), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$ . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; nonnegative finite costs $C(i,a)$ ; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$ . A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$ . A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$ . Fix a discount factor $\alpha\in(0,1)$ . The discounted cost of $\theta$ and the discounted value function are

V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),

both in $[0,\infty]$ , the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$ , probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$ . The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$ , $r\notin S_N$ , according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$ : $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$ .

Assumption DC( $\alpha$ ): for every $i\in S$ , $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$ .

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$ ) is discount optimal for $\Delta$ .

Milestones

Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
Proposition 4.7.1: bounded costs imply DC( $\alpha$ ).
Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$ -step transition probabilities.
Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$ .
Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC( $\alpha$ ) holds.
Corollary 4.7.5: the case of a single distinguished state $z$ , with the relative form of the optimality equation for $\Delta_N$ .
Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$ , then $V^N_\alpha\le V_\alpha$ on $S_N$ .

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$ -valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$ , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$ -valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$ . The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$ ; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$ , a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$ . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$ ) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC( $\alpha$ ) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$ .

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IV: Average Cost Optimal Stationary Policies Exist for Finite State SpacesTextbook

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , a finite nonempty action set $A_i$ in each state $i$ , nonnegative finite costs $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$ . A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$ .

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$ , define

the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$ , and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ ;
the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$ ;
the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ , its $\liminf$ version $J^*_\theta(i)$ , and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$ .

All infima range over all general policies, and every quantity may equal $+\infty$ . A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$ , and average cost optimal if $J_\theta = J$ .

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$ , distinguished states $z_k \in R_k$ , and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$ , the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$ .

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$ , $f$ is average cost optimal, and

J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.

Milestones

Proposition 4.5.3. For finite $S$ and stationary $e$ , $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$ .
Proposition 6.1.1. For every policy on a countable state space,

J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$ , $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$ . 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$ ; monotonicity and left continuity of $V_\alpha$ ; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$ .

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$ , a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$ . Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$ , but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$ . Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
$V_{\theta,\alpha}$ , $V_\alpha$ , $v_{\theta,n}$ , $J_\theta$ , $J^*_\theta$ , $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ( $w_\alpha$ , $w$ , $w^*$ , equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
The objects of Section 6.3 ( $p_k$ , $m_{i|k}$ , $c_{i|k}$ , $\pi_s$ , $W_\alpha$ ) are defined from $f$ . The distinguished states are a hypothesis quantified over.
A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$ , or state rationality as an equation p/q without requiring $q \ne 0$ . Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$ , and the denominator is required to be nonzero on $(0,1)$ .

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$ -valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
D. Blackwell, "Discrete dynamic programming", Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

13 thms3 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VIII: Computing Average Cost Optimal Policies by Approximating SequencesTextbook

Motivation

Control problems for queueing systems (admission control, service rate control, routing to parallel servers) are naturally modelled as Markov decision chains whose state is a vector of queue lengths. The state space is therefore denumerably infinite, and the performance measure of interest is usually the long-run average cost per slot. For such models the existence theory of average cost optimal stationary policies is well developed (Chapter 7 of Sennott's book), but existence gives no algorithm: an optimal policy is a function on an infinite set, and value iteration cannot be run on an infinite state space.

The approximating sequence method answers this by replacing the infinite model $\Delta$ with a sequence of finite models $\Delta_N$ on truncated state spaces $S_N$ , solving the average cost optimality equation in each, and passing to the limit. Chapter 8 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) gives a set of conditions, the (AC) assumptions, under which this limit procedure provably produces the minimum average cost and an average cost optimal policy of $\Delta$ .

Timeline. The approximating sequence method for the average cost criterion and the (AC) assumptions were introduced in Sennott (1997a), with further results in Sennott (1997b) (bibliographic notes, p. 194). The book collects these results, adds the four step verification template (Proposition 8.2.1), the finite-set augmentation route based on the (BOR) assumptions (Proposition 8.2.3), and the weakening (WAC) of Section 8.7, which Chapter 9 uses.

Setting

An MDC $\Delta$ has a countable state space $S$ , a finite nonempty action set $A_i$ in each state $i$ , a finite cost $C(i,a)\ge0$ , and transition probabilities $P_{ij}(a)$ . A general policy $\theta$ chooses actions at random using the whole past history. Its average cost is

J_\theta(i)=\limsup_{n\to\infty}\frac1n\sum_{t=0}^{n-1}E_\theta[C(X_t,A_t)\mid X_0=i],

and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)\in[0,\infty]$ . A policy is average cost optimal if $J_\theta\equiv J$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite sets $S_N$ increasing to $S$ and MDCs $\Delta_N$ on $S_N$ with the same actions and costs and with transition probabilities $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ . Write $v^N_n$ and $V^N_\alpha$ for the $n$ -horizon and discounted value functions of $\Delta_N$ .

The (AC) assumptions are:

(AC1) there are finite constants $J^N$ and finite functions $r^N$ on $S_N$ with

J^N+r^N(i)=\min_a\Big\{C(i,a)+\sum_{j\in S_N}P_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N; \tag{8.1}

(AC2) $\limsup_N r^N(i)<\infty$ ;
(AC3) $\liminf_N r^N(i)\ge -Q$ for a constant $Q\ge0$ ;
(AC4) $J^*:=\limsup_N J^N<\infty$ and $J^*\le J(i)$ for all $i$ .

The (WAC) assumptions of Section 8.7 allow $Q$ to depend on the state, at the price of integrability conditions along every stationary policy.

Formalization targets

Goal: Theorem 8.1.1

Under (AC), the limit $\lim_{N\to\infty}J^N$ exists and

J(i)=\lim_{N\to\infty}J^N\qquad\text{for all } i\in S,

and every limit point $e^*$ of stationary policies $e^N$ realizing the minimum in (8.1) is average cost optimal for $\Delta$ . The statement fixes no constants; it asserts the shape of the conclusion for any model satisfying (AC).

Milestones

Proposition 8.2.1 (the four step template): unichain and aperiodicity of the finite models, an $x$ standard policy at which the approximating sequence is conforming, a comparison of $v^N_n$ (or $V^N_\alpha$ ) with $v_n$ (or $V_\alpha$ ), and a lower bound on $v^N_n - v^N_n(x)$ together imply that the value iteration limits

r^N(i)=\lim_{n\to\infty}\big(v^N_n(i)-v^N_n(x)\big)

exist and satisfy (AC).

Corollary 8.2.2: on $S=\{0,1,2,\dots\}$ with $S_N=\{0,\dots,N\}$ and excess probability sent to $N$ , monotonicity of $v^N_n$ , $v_n$ and of the first passage moments of a $0$ standard policy suffices.
Proposition 8.2.3: an augmentation type approximating sequence that sends excess probability to a finite set of cheap states satisfies the template.
Proposition 8.5.1: in the single-server queue with Bernoulli( $p$ ) arrivals and constant service rate $a>p$ ,

J_{d(a)}=\frac{Hp(1-p)}{a-p}+\frac{pC(a)}{a}.

Proposition 8.7.1: the conclusions of Theorem 8.1.1 hold under (WAC).

Significance

The result itself. Theorem 8.1.1 is what turns the existence theory of Chapter 7 into a computation. It certifies that the minimum average costs of the truncations converge to the minimum average cost of the infinite model, that this cost is constant, and that the policies produced by value iteration on $\Delta_N$ converge, along subsequences, to an optimal policy for $\Delta$ . Propositions 8.2.1–8.2.3 reduce (AC) to properties that can be checked model by model; Section 8.3 checks them for queues with reject option, service rate control, and routing to parallel queues. Proposition 8.7.1 is the version used in Chapter 9 for models whose relative values are not uniformly bounded below. Proposition 8.5.1 gives the closed-form open-loop benchmark used in the numerical study of Section 8.5.

Formalizing it. All results are proved in the book; none has a machine-checked proof. A formalization would give the first verified convergence theorem for truncations of denumerable-state average cost MDPs, and would make the approximating sequence method usable as a certified reduction from infinite to finite models. The template results (8.2.1–8.2.3) additionally require a formal treatment of conformity of approximating Markov chains (Appendix C.4–C.5), which is of independent use.

Difficulty

The naive argument takes limits in (8.1) along $N$ : the minimum over $a$ and the finite sums pass to the limit only in the inequality direction, and only after a Fatou-type lemma for sums against the converging distributions $P_{ij}(a;N)$ with integrands $r^N$ that are neither bounded nor monotone. The lower bound $-Q$ in (AC3) is exactly what makes this possible; without it the limit inequality can fail. The limit inequality then produces only an average cost optimality inequality, and turning it into optimality of the limit policy requires a separate argument that a function bounded below and satisfying the inequality yields an upper bound on the average cost. Existence of $\lim_N J^N$ is not given: (AC4) controls only the limit superior, and the limit must be identified through every subsequence. For the template results, the difficulty is in the Markov chain side: the convergence of first passage times and costs of the truncated chains, which fails for general approximating sequences (Examples C.4.4, C.4.7).

Formalization scope

The Lean development is in the namespace SennottDP.AvgASM. The state space is any countable type; action sets are Finsets, assumed nonempty; costs are finite and nonnegative (ℝ≥0); transition probabilities are ℝ≥0∞-valued, with each row a probability distribution for admissible actions. All value functions and average costs take values in $[0,\infty]$ (ℝ≥0∞), and every infimum over policies ranges over the full class of history-dependent randomized policies. The $J^N$ and $r^N$ of (AC1) are real; the limits superior and inferior over $N$ in (AC2)–(AC4) and (WAC) are taken in EReal, so an unbounded sequence cannot produce a junk finite value. The equality $J(i)=\lim_N J^N$ is stated in EReal, which also asserts that $J(i)$ is finite. Quantities of $\Delta_N$ at states outside $S_N$ are junk values that affect only finitely many $N$ for each state.

A trivializing formalization is ruled out: $J^N$ and $r^N$ are the witnesses of (AC1), not free variables, the policies $e^N$ must realize the minimum in (8.1) for those witnesses, and the minimum average cost $J$ is an infimum over all policies, so the goal cannot be satisfied by choosing $J^*$ or the limit policy.

A complete development needs: the induced process law of a general policy; the average cost optimality inequality argument (Lemma 7.2.1); the finite-state average cost results of Chapter 6 (Propositions 6.4.1, 6.5.1, 6.6.3); a Fatou lemma for converging distributions (Proposition A.2.5); limit points of policy sequences (Proposition B.5); and, for the template results, the theory of $z$ standard chains and conformity (Appendix C.2–C.5). The Markov chain layer and the approximating sequence definitions are reusable beyond this mission. Contributions of any of these intermediate results as separate theorems are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997), 114–137 (cited as Sennott (1997a) in the book).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR — Mathematical Methods of Operations Research 45 (1997), 45–62 (cited as Sennott (1997b) in the book).

14 thms3 active users

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IX: Bounded Mean Residual Lifetimes Imply Finite Moments of All OrdersTextbook

Motivation

In a discrete-time queue the service of a customer lasts a random number $Y$ of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted $s$ slots and is not yet finished. The relevant random quantity is then the residual life $Y_s$ : the remaining service time given that $s$ slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on $Y$ and on the residual lives $Y_s$ .

Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where $Y$ is the lifetime of a component and $E[Y_s]$ is its expected remaining lifetime at age $s$ . This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.

Setting

Let $Y$ be a random variable with values in $\{1,2,3,\dots\}$ and distribution $u_y = P(Y = y)$ , $y \ge 1$ . Write $F(y) = P(Y \le y)$ and $F^*(y) = P(Y > y) = 1 - F(y)$ for $y \ge 0$ , so $F(0) = 0$ and $F^*(0) = 1$ . The $k$ -th moment is

E[Y^k] = \sum_{y \ge 1} y^k u_y \in [0,\infty].

For $s \ge 0$ with $F^*(s) > 0$ , the residual life $Y_s$ has distribution

P(Y_s = y) = P(Y = s + y \mid Y > s) = \frac{u_{s+y}}{F^*(s)}, \qquad y \ge 1,

with $Y_0 = Y$ ; its tail is $F^*_s(y) = F^*(s+y)/F^*(s)$ , and $E[Y_s]$ is the mean residual lifetime.

The distribution of $Y$ has bounded mean residual lifetimes (BMRL- $U$ , Definition 9.2.4) if there is a finite constant $U$ with

E[Y_s] \le U \qquad \text{for every } s \ge 0 \text{ with } F^*(s) > 0,

and it is BMRL if it is BMRL- $U$ for some $U$ .

Three families appear by name: the geometric distribution $\mathrm{geo}(\mu)$ of the number of Bernoulli( $\mu$ ) trials to the first success, $P(Y=y) = \mu(1-\mu)^{y-1}$ ; the negative binomial $\mathrm{neg\,bin}(\mu, r)$ of the number of trials to the $r$ -th success, $P(Y = y) = \binom{y-1}{r-1}\mu^r(1-\mu)^{y-r}$ for $y \ge r$ ; and the truncated Poisson $\mathrm{trun\,Pois}(\lambda)$ , $P(Y=y) = \frac{e^{-\lambda}}{1-e^{-\lambda}}\frac{\lambda^y}{y!}$ for $y \ge 1$ .

For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes $X_1, X_2, \dots$ are independent with common distribution $p_j$ , mean $\lambda = \sum_j j p_j$ and second moment $\lambda^{(2)} = \sum_j j^2 p_j$ , and $X(s) = X_1 + \dots + X_s$ is the number of arrivals in $s$ slots.

Formalization targets

Goal: Proposition 9.2.5

If the distribution of $Y$ is BMRL, then

E[Y^k] < \infty \qquad \text{for every } k.

The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of $Y$ to be finite.

Milestones

Proposition 9.2.1. $E[Y] = \sum_{y=0}^\infty F^*(y)$ and, for $k \ge 2$ ,

E[Y^k] = 1 + \sum_{z=0}^{k-1}\binom{k}{z}\left[\sum_{y=1}^\infty y^z F^*(y)\right]. \tag{9.4}

Remark 9.2.2. For $k \ge 2$ , $E[Y^k] < \infty$ if and only if $\sum_y y^{k-1}F^*(y) < \infty$ .
Proposition 9.2.3. For a positive integer $k$ , $E[Y^k] < \infty$ implies $E[Y_s^k] < \infty$ for all $s \ge 0$ .
Proposition 9.2.6. The geometric ( $0<\mu<1$ ), negative binomial ( $0<\mu<1$ , $r \ge 2$ ) and truncated Poisson ( $\lambda > 0$ ) distributions are BMRL.
Lemma 9.5.2. Under $\lambda^{(2)} < \infty$ ,

E[X(s)] = \lambda s, \qquad E[(X(s))^2] = \lambda^{(2)}s + \lambda^2 s(s-1). \tag{9.25}

Significance

The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on $\{1,2,\dots\}$ have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).

Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of $\mathbb N$ -valued random variables in $[0,\infty]$ , a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.

Difficulty

BMRL controls only first moments, of the conditional laws $Y_s$ ; the goal asks for moments of every order of $Y$ itself. Bounding $E[Y^k]$ by expanding $E[Y_s]$ for each fixed $s$ gives nothing, because each single bound is compatible with a heavy tail: the uniformity in $s$ is essential. The residual lives are also only defined where $P(Y > s) > 0$ , so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.

Formalization scope

$Y$ is represented by its law, a function $u : \mathbb N \to [0,\infty]$ with $\sum_y u_y = 1$ and $u_0 = 0$ (IsDistOnPos). $F^*$ , moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is $+\infty$ and "finite" means $< \infty$ . No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.
The residual life $Y_s$ is defined by (9.7) and is used only where $F^*(s) > 0$ ; BMRL- $U$ is required exactly at those $s$ , and $U$ is a finite nonnegative real. A formalization requiring the bound at every $s$ with a junk value of $E[Y_s]$ where $F^*(s) = 0$ is ruled out: the definitions never divide by $F^*(s) = 0$ in a used position, and bounded distributions remain BMRL.
The geometric and negative binomial laws count trials (support starting at $1$ and $r$ ), not failures as Mathlib's geometricPMF does.
Lemma 9.5.2 is stated on a probability space with measurable, mutually independent (iIndepFun) batch sizes of common law $p$ , expectations as lower Lebesgue integrals, and only assumption (BA1), $\lambda^{(2)} < \infty$ , which is the part of the book's (BA) that concerns arrivals.
Welcome contributions: the tail-sum identity (9.4) and its reindexing lemmas, the residual-life tail formula (9.8) and moment formula (9.9), each as a separate lemma; and proofs that the three named families are probability distributions on their supports.

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Section 9.2 (pp. 202–206) and Section 9.5 (pp. 214–215). DOI 10.1002/9780470317037
Moshe Shaked and J. George Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Section 2.A (the mean residual life order). DOI 10.1007/978-0-387-34675-5

8 thms3 active usersReviewed

The OR Formalization Drive

Missions

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

Motivation

Setting

Formalization targets

Goal: Theorem 5 (p. 29)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analysis and Algorithms for Service Parts Supply Chains III: Palm's Theorem for (s–1, s) PoliciesTextbook

Motivation

Setting

Formalization targets

Goal: Palm's theorem (Theorem 6, p. 39)

The proof's milestones (pp. 38–41)

Extensions in Section 3.1

Significance

Difficulty

Formalization scope

Selected references

Analysis and Algorithms for Service Parts Supply Chains V: Marginal Allocation and Risk PoolingTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 2 (correctness)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analysis and Algorithms for Service Parts Supply Chains VI: The Shortfall Distribution of Capacity-Limited SystemsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Analysis and Algorithms for Service Parts Supply Chains VIII: Bounds on Optimal Stock AllocationsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 15 (p. 237)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior I: Numerical Utility from the Axioms of Preference and MixtureTextbook

Motivation

Setting

Formalization targets

Goal: (A:V) and (A:W), p. 627

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior II: Games with Perfect Information Are Strictly DeterminedTextbook

Motivation

Setting

Formalization targets

Goal: 15.6.1 with (15:12)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

Setting

Formalization targets

Goal: (17:D), good strategies characterized by their supports

Milestones, in attack order

Significance

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