Operations Research

Motivation

The subgradient method for a convex function $f$ moves from $x_k$ against a subgradient $g_f(x_k)$, and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about $f$. When the optimal value $f^*$, or any level $c$ that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step

$$x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k),$$

which uses the current gap $f(x_k) - c$ to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".

Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).

Timeline:

• 1965–1969: Eremin introduces Fejér mappings for systems of convex inequalities.
• 1969: Polyak, Minimization of unsmooth functionals, proposes the step with the known optimal value and proves convergence and a linear rate under a sharp-minimum condition.
• 1975: Camerini, Fratta and Maffioli combine the Polyak step with a conjugate direction for Lagrangian relaxation.
• 1985: Shor's book collects these results in Section 2.4 (Theorems 2.10–2.16).

Setting

$E_n$ is the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$. A subgradient selection is a map $g_f$ with $g_f(x)$ a subgradient at every $x$; nothing else is assumed about it, in particular not continuity.

For a nonempty set $M \subseteq E_n$, a map $\varphi : E_n \to E_n$ is $M$-Fejér if $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$.

For a convex $f$ with $f^* = \inf f$ and a level $c \ge f^*$, let $M(c) = \{x : f(x) \le c\}$. Polyak's method (2.32) is the iteration $x_{k+1} = \varphi_c(x_k)$ with the map displayed above for $x \notin M(c)$ and $\varphi_c(y) = y$ on $M(c)$; the factor $\gamma$ is fixed in $(0, 2)$.

The conjugate-subgradient procedure (2.38), for a convex $f$ with minimum point $x^*$ and $f^* = f(x^*)$, is

$$x_{k+1} = x_k - h_k s_k, \quad h_k = \frac{[f(x_k) - f^*]\gamma_k}{\|s_k\|^2}, \qquad s_0 = g_f(x_0),\quad s_k = g_f(x_k) + \beta_k s_{k-1}.$$

Formalization targets

Goal: Theorem 2.11

If $0 < \gamma < 2$ and $M(c) \neq \emptyset$, then for any $x_0 \in E_n$

$$\exists k^* : x_{k^*} \in M(c) \qquad \text{or} \qquad \lim_{k \to \infty} x_k \text{ exists and lies in } M(c).$$

The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.

Milestones

1. Theorem 2.10. Iterates of a continuous $M$-Fejér map converge to a point of $M$.
2. Inequality (2.33). For $x_k \notin M(c)$ and $y \in M(c)$,

$$\|x_{k+1} - y\|^2 \le \|x_k - y\|^2 - \gamma(2-\gamma)\frac{[f(x_k) - c]^2}{\|g_f(x_k)\|^2} < \|x_k - y\|^2 .$$

3. Theorem 2.12. Under $f(x) - f^* \ge m\|x - x^*\|^2$ and an $L$-Lipschitz gradient near $x^*$, with $c = f^*$: $\|x_k - x^*\| \le q^k \|x_0 - x^*\|$, $q = (1 - \gamma(2-\gamma)m^2/L^2)^{1/2} < 1$.
4. Theorem 2.13. Under the sharp-minimum condition $f(x) - f(x^*) \ge m\|x - x^*\|$ and subgradients bounded by $L$ near $x^*$, with $c = f(x^*)$: $\|x_{k+1} - x^*\| \le q\|x_k - x^*\|$.
5. Theorem 2.14. If $\min \psi = d > 0$ and the method runs with $c = 0$, then $\lim_k \min_{0 \le i \le k} \psi(x_i) \le 2d/(2-\gamma)$.
6. Theorem 2.15. For (2.38) with $0 < \gamma_k \le 1$, $\beta_k \ge 0$: $(x_k - x^*, s_k) \ge (x_k - x^*, g_f(x_k))$.
7. Theorem 2.16. With the Camerini–Fratta–Maffioli coefficient $\beta_k$ and $0 \le \alpha_k \le 2$: $(x_k - x^*, s_k)/\|s_k\| \ge (x_k - x^*, g_f(x_k))/\|g_f(x_k)\|$.

Significance

Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With $c = f^*$ it yields a minimizer; with $c > f^*$ it solves the convex inequality $f(x) \le c$, and applied to $\psi = \max_i f_i^+$ it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates $f^*$ on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.

All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no $M$-Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.

Difficulty

The obvious argument for the goal is to observe that $\varphi_c$ is $M(c)$-Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and $\varphi_c$ depends on an arbitrary subgradient selection, which is discontinuous wherever $f$ is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance $\|x_k - y\|$, but convergence of the whole sequence to a single point of $M(c)$, and the fact that an accumulation point cannot lie outside $M(c)$, have to be obtained without continuity of the map.

For Theorem 2.14 the level $c = 0$ lies strictly below the minimum, so $M(0) = \emptyset$, the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued on all of $E_n$ and ConvexOn ℝ Set.univ f.
• The subgradient selection is universally quantified; no theorem assumes continuity of it.
• Iterations are sequences x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.
• Polyak's step map is defined piecewise: it returns $x$ on $M(c)$ (as the book sets $\varphi_c(y) = y$) and at $g_f(x) = 0$. No statement relies on Lean's convention $x/0 = 0$. The same holds for $h_k$ when $s_k = 0$.
• $M(c) \neq \emptyset$ is a hypothesis of the goal: the book's proof picks $y \in M(c)$, and for $c = f^*$ not attained the conclusion is false (for $f = e^x$, $c = 0$, the method moves by $\gamma$ each step and diverges).
• "$\lim x_k \in M(c)$" is the existence of a limit in $M(c)$, not a statement about cluster points.
• $\gamma \in (0, 2)$ is stated in every theorem on Polyak's method; the book fixes this range at Theorem 2.11.
• Theorem 2.12's "strongly convex" is used through its displayed growth condition only; the statement is made for convex $f$ satisfying it, with $L > 0$ and $q$ computed with Real.sqrt.
• Theorem 2.13 assumes the bound $\|g\| \le L$ on subgradients in the ball, which is what the proof uses; a Lipschitz constant on the closed ball alone does not give it, and the printed statement fails without it.
• Theorem 2.14 is stated with "$\le 2d/(2-\gamma)$"; the printed "$=$" is false in general.
• Theorem 2.16's inequality is stated at indices where $s_k \neq 0$ and $g_f(x_k) \neq 0$.

A formalization in which $M(c)$ may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.

Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §2.4, pp. 36–42. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969, 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• I. I. Eremin, The relaxation method of solving systems of inequalities with convex functions on the left-hand side, Soviet Mathematics Doklady 6, 1965, 219–222.
• P. M. Camerini, L. Fratta, F. Maffioli, On improving relaxation methods by modified gradient techniques, Mathematical Programming Study 3, 1975, 26–34.

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$, $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$; $g_f(x)$ denotes an arbitrary subgradient at $x$, chosen once for each $x$. Let $M^*$ be the set of minimum points of $f$, assumed nonempty; for $x \in E_n$, $x^*(x)$ is the point of $M^*$ nearest to $x$.

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,$$

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

$$(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.$$

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$, asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$.

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$, $\sigma \ge \sqrt2$, $h_1 \ge \|x_0 - x^*\|/\sigma$, and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$, then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

$$\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots$$

Milestones

1. Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$,

$$\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .$$

2. Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
3. Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$.
4. Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$,

$$\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},$$

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$. 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$, the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$.

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$. The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$, so the iterates must be shown to stay in $Y$, and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$, $h_1$ being the chosen initial step (the book's "$k = 0, 1, 2, \dots$" in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$, never through $x/0 = 0$; the bounds are asserted for every $k$, which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$. The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$. In (2.16) the ratio is $1/(2\cos\varphi)$, as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$, which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$. In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$, nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
• J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
• L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$, finite nonempty action sets $A_i$, nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$, the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$. All of these lie in $[0,\infty]$.

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$. The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$. Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$. The ACOI and ACOE read

$$J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.$$

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$. The class $\Re(i,G)$ consists of the policies that, from $i$, enter $G$ with probability one in finite expected time $m_{iG}(\theta)$; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$. A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$.

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$. Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

$$D(e)=\{i: C(i,e)\le J+\varepsilon\},$$

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$.

Milestones

• Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$, hence (SEN2).
• Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
• Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
• Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$.
• Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
• Corollary 7.5.4: on $S=\{0,1,\dots\}$, increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
• Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$, reachable from $i$, when (7.33) holds.
• Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$, $c_{iG}$, $P_\theta(X_T=j)$, $Q^{(n)}_{ij}$) are computed from the history probabilities of the process. $V_\alpha$, $J_\theta$, $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$. $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$. Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$.

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$); Abelian limits of $\sum_t\alpha^tP(T=t)$; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, 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. doi:10.1002/9780470317037
• V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
• V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
• V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
• R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
• R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
• L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
• L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, for each state $i$ a finite nonempty action set $A_i$, a nonnegative finite cost $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$.

For an initial state $i$, the $n$-horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$, the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$, and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$. For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$. All these quantities lie in $[0,\infty]$.

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$. The (SEN) assumptions are:

• (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$;
• (SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$;
• (SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$.

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$. If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$, a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$, for each $i$, along some $\beta_n \to 1^-$.

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

$$J + h(i) \ge \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)h(j)\Big\}, \qquad i \in S;$$

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

• Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$.
• Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$.
• Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
• Proposition 7.2.4: (SEN) does not depend on the choice of $z$.
• Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
• Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$.

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$, as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$, so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$. Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$, and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$.

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$, proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
• L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
• R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
• S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
• H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
• E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

Motivation

Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)

$$J + h(i) = \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)\,h(j)\Big\},$$

whose solution gives both the minimum average cost $J$ and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum $n$-horizon costs $v_n$ and extract $J$ and $h$ from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.

Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function $V_\alpha$ as $\alpha \to 1^-$, which is the route that extends to countable state spaces in later chapters of the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a finite state space $S$; in each state $i$ a finite nonempty action set $A_i$; nonnegative costs $C(i,a)$; and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize; a stationary policy $e$ always chooses $e(i) \in A_i$ in state $i$ and induces a Markov chain with transitions $P_{ij}(e) = P_{ij}(e(i))$.

For a policy $\theta$ and initial state $i$: $v_{\theta,n}(i)$ is the expected cost of the first $n$ steps, $V_{\theta,\alpha}(i)$ the expected $\alpha$-discounted cost, and $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ the average cost. The value functions are the infima over all policies: $v_n$, $V_\alpha$ and the minimum average cost $J(i)$. A policy is average cost optimal if $J_\theta \equiv J$.

Section 6.2 of the book provides a stationary policy $f$ that is $\alpha$ discount optimal for all $\alpha$ close to $1$ (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function $w^*$. For a distinguished state $z$ put

$$h_\alpha(i) = V_\alpha(i) - V_\alpha(z), \qquad h(i) = \lim_{\alpha\to1^-} h_\alpha(i), \qquad d_n(i) = h(i) + nJ - v_n(i).$$

For a distinguished state $x$ the finite horizon relative value function is $r_n(i) = v_n(i) - v_n(x)$.

A positive recurrent class $R$ of a Markov chain is aperiodic if $P^{(n)}_{ij} \to \pi_j$ for $i, j \in R$, where $\pi$ is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation $\Delta^*$ with $0<\tau<1$ keeps states and actions, scales costs by $\tau$, and sets $P^*_{ij}(a) = \tau P_{ij}(a)$ for $j \ne i$, $P^*_{ii}(a) = \tau P_{ii}(a) + (1-\tau)$.

Formalization targets

Goal: convergence of value iteration (Proposition 6.6.3)

If $J(i) \equiv J$ and Assumption OPA holds, then for any distinguished state $x$

$$\lim_{n\to\infty}[v_n(x) - v_{n-1}(x)] = J, \qquad \lim_{n\to\infty} r_n(i) =: r(i) \text{ exists},$$

$(J, r)$ solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.

Milestones

1. Proposition 6.4.1: unichain structure, bounded $|V_\alpha(i) - V_\alpha(z)|$, or pairwise reachability imply $J(i) \equiv J$, with the implication diagram (6.26).
2. Theorem 6.4.2: under $J(i) \equiv J$, $h$ exists, solves the ACOE (6.31), yields optimal policies, $|d_n| \le L$ and $v_n/n \to J$.
3. Proposition 6.5.1: any finite solution $(F, r)$ of the ACOE (or of the inequality (6.36)) gives $J \equiv F$ and optimal policies, and differs from $h$ by constants on recurrent classes.
4. Lemma 6.6.2: on an aperiodic positive recurrent class of an optimal policy, $d_n$ converges to a constant.
5. Lemma 6.6.5 and Proposition 6.6.6: $\Delta^*$ has the same recurrent classes and steady states, all of them aperiodic, costs scaled by $\tau$; value iteration on $\Delta^*$ produces a solution $(J^*/\tau, r^*)$ of the ACOE of $\Delta$.

Significance

The ACOE with constant $J$ is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.

All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.

Difficulty

The ACOE itself is not the obstacle; convergence of $v_n(x) - v_{n-1}(x)$ is. Theorem 6.4.2 bounds $d_n$ but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity $v_n(x) - v_{n-1}(x)$ oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers $f_n$ need not converge.

Formalization scope

• The state type S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite $S$).
• $J$ constant is stated as $J(i) = J$ for all $i$, with $J \in \mathbb R_{\ge 0}$. The relative value $h$ is defined as the limit $\alpha \to 1^-$ of $h_\alpha$, not taken as an arbitrary solution of the ACOE; Theorem 6.4.2(i) asserts the limit exists. The Blackwell optimal policy $f$ enters as a hypothesis: any stationary policy discount optimal on an interval $(\alpha_0,1)$.
• min_a is Finset.inf' over $A_i$. Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies $f_n$ are any minimizers of $v_n(i) = \min_a\{C(i,a) + \sum_j P_{ij}(a) v_{n-1}(j)\}$.
• Aperiodicity of a class is the book's definition ($P^{(n)}_{ij} \to \pi_j$ on the class), with $\pi_j = 1/m_{jj}$. Assumption OPA quantifies over average cost optimal stationary policies only, not over all stationary policies.
• A trivializing formalization is ruled out: $h$, $r_n$, $d_n$ and $v_n$ are computed from the model, not free functions constrained by the ACOE, and the ACOE conclusions are equalities of real numbers with the minimum over the actual action sets.
• The model, criteria and Markov chain definitions restate those of mission IV of this series in their own namespace; they are reusable for any finite average cost result. Contributions of general Markov chain facts (convergence of $P^{(n)}$ on aperiodic classes, Cesàro limits $\frac1n\sum_t P^{(t)}$) are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, 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
• P. J. Schweitzer and A. Federgruen, The asymptotic behavior of undiscounted value iteration in Markov decision problems, Mathematics of Operations Research 2 (1977), 360–381. https://doi.org/10.1287/moor.2.4.360
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

The solution concept of von Neumann and Morgenstern — today usually called a stable set — was the first general answer to the question of what a rational outcome of a many-player cooperative game should be. It was introduced in Theory of Games and Economic Behavior (1944), and Chapter VI of that book states it exactly (§30) and then tests it on the smallest nontrivial case: the essential zero-sum three-person game (§32). The complete determination of all solutions of that game, (32:A)–(32:B) on p. 288, is the book's first full answer to "what are all the solutions of a given game?", and it is the result that made visible the two features every later discussion of stable sets has had to address: a game can have many solutions, and a solution can be an infinite set of imputations that discriminates against one player.

Stable sets remain an active topic in cooperative game theory: Lucas (1968) showed that some games have no stable set, and the literature on existence, uniqueness and structure (for example Shapley 1971 on convex games, whose core is the unique stable set) builds on the definitions formalized here.

Setting

A zero-sum $n$-person game with players $I = \{1, \dots, n\}$ is described by its characteristic function $v(S)$, a real number for each set $S \subseteq I$ of players, satisfying (25:3:a)–(25:3:c):

$$v(\ominus) = 0,\qquad v(-S) = -v(S),\qquad v(S \cup T) \geqq v(S) + v(T)\ \text{ for } S \cap T = \ominus .$$

An imputation is a vector $\vec\alpha = \{\alpha_1, \dots, \alpha_n\}$ with $\alpha_i \geqq v((i))$ for each player and $\sum_i \alpha_i = 0$ (30:1), (30:2). A set $S$ is effective for $\vec\alpha$ if $\sum_{i \in S} \alpha_i \leqq v(S)$ (30:3). An imputation $\vec\alpha$ dominates $\vec\beta$, $\vec\alpha \succ \vec\beta$, if some nonempty set $S$ is effective for $\vec\alpha$ and $\alpha_i > \beta_i$ for all $i \in S$ (30:4). A solution is a set $V$ of imputations such that no element of $V$ dominates another element of $V$ (30:5:a) and every imputation outside $V$ is dominated by some element of $V$ (30:5:b).

Two characteristic functions $v, v'$ are strategically equivalent if $v'(S) = v(S) + \sum_{k\in S}\alpha^0_k$ for constants with $\sum_k \alpha^0_k = 0$ (27:1), (27:2). Every $v$ is strategically equivalent to exactly one reduced function $\bar v$ (27:A); the game is inessential if $\bar v \equiv 0$ and essential otherwise (27.3).

For three players, an essential game in reduced form with the unit chosen so that $\gamma = 1$ has

$$\text{(32:1)}\qquad v(S) = 0,\ -1,\ 1,\ 0 \quad\text{when } S \text{ has } 0, 1, 2, 3 \text{ elements},$$

and its imputations are the points of the fundamental triangle $\alpha_1, \alpha_2, \alpha_3 \geqq -1$, $\alpha_1 + \alpha_2 + \alpha_3 = 0$.

Formalization targets

Goal: the complete list of solutions, (32:A) + (32:B)

For the game (32:1), a set $V$ is a solution if and only if either

$$V = \bigl\{\{-1, \tfrac12, \tfrac12\},\ \{\tfrac12, -1, \tfrac12\},\ \{\tfrac12, \tfrac12, -1\}\bigr\}\qquad\text{(32:6), (32:B)}$$

or, for some player $i$ and some $c$ with

$$-1 \leqq c < \tfrac12 \qquad\text{(32:8)},$$

$V$ is the set of all imputations with $\alpha_i = c$ ((32:7), (32:7*), (32:7**), (32:A)). Both directions are part of the goal.

Milestones

For general $n$ (§31): domination is irreflexive (31:K); an inessential game has exactly one imputation and an essential game infinitely many (31:I); solutions are never empty (31:J); in an essential game every imputation is dominated by one it does not dominate (31:L); an undominated imputation exists iff the game is inessential (31:M); a one-element solution exists iff the game is inessential, and it is then the only solution (31:P); strategic equivalence induces an isomorphism of imputations, effective sets, domination and solutions (31:Q).

For the three-person game (§32): domination is the coordinate condition (32:4) on two of the three players; two mutually undominated imputations agree in one coordinate (32:5); the set (32:6) is a solution (32:B); every set (32:7) with $c$ in the range (32:8) is a solution (32:A).

Significance

The goal is the first complete classification of the stable sets of a game. It shows that solutions are not unique and need not be finite: next to the symmetric three-point solution there is a one-parameter family, for each of the three players, of solutions that fix that player's payoff at $c$ and let the other two bargain freely. The book's interpretation of these "discriminatory" solutions (§33) as standards of behaviour is one of the lasting ideas of the theory. The general-$n$ results of §31 fix the trivial case completely: an inessential game has a unique, one-point solution, so every essential game has only solutions with at least two elements and an empty core. (31:Q) justifies working with reduced forms throughout the later chapters.

The results are proved in the book; none has a machine-checked proof on the platform as of this writing. The existing stable-set definitions on the platform concern feasible payoff vectors $a(N) \leqq v(N)$ of a superadditive game, not imputations of a zero-sum game, so this mission also provides the book's definitions in the form every later chapter of the series (decomposition, simple games, general games) uses.

Difficulty

The "if" direction of the goal is a finite case analysis per set, but (30:5:b) must be checked for every imputation outside the set, with the dominating element chosen as a function of it. The "only if" direction is the substance: from an arbitrary solution — a possibly infinite, a priori unstructured subset of the triangle — one must derive that it is exactly one of the listed sets. The book's argument is geometric (Figures 54–60) and leans on pictures of dominated regions; the delicate points are the exclusion of the limiting position $c = \tfrac12$, where a single point of the triangle stays undominated, and the proof that a solution with two points on a horizontal line and one point off it must be exactly (32:6). The endpoint $c = -1$ is included and must be handled; the endpoint $c = \tfrac12$ is excluded and must be refuted.

Formalization scope

Players are Fin n (the book's player $i$ is index $i-1$; for three players $1, 2, 3$ are 0, 1, 2), coalitions are Finset (Fin n), characteristic functions are Finset (Fin n) → ℝ, imputations are vectors Fin n → ℝ. The domination relation is defined on all vectors but every statement restricts it to imputations; solutions are sets of imputations and (30:5:b) quantifies over imputations only.

Standing hypotheses instantiated in the statements:

• every general-$n$ result of §31 assumes that $v$ satisfies (25:3:a)–(25:3:c) (IsCharFunction v), the book's standing assumption for "a zero-sum $n$-person game";
• "inessential" is the book's definition (reduced form identically $0$, 27.3.1), not the criterion (27:B); "essential" is its negation;
• the three-person results are stated for the reduced form (32:1) with $\gamma = 1$ exactly, as in §32; the transfer to arbitrary essential three-person games via (31:Q) and the choice of unit is not part of the goal;
• the range of $c$ is the half-open interval (32:8).

Domination requires all three clauses of (30:4): dropping "$S$ not empty" makes every imputation dominate every other through $S = \ominus$ and turns the goal into a statement about the empty solution; the definitions keep all three. The general-$n$ statements carry the characteristic-function hypotheses because without them a set function with no imputation has the empty set as a vacuous solution.

The dimension claim "an $(n-1)$-dimensional continuum" in (31:I) is not formalized; only "infinitely many imputations" is. Contributions welcome: proofs of the milestones, a proof of the transfer of the goal to all essential three-person games through (31:Q), and reusable lemmas on domination via two-element coalitions.

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), §§25–27, 30–32. https://doi.org/10.1515/9781400829460
• W. F. Lucas, A game with no solution, Bulletin of the American Mathematical Society 74 (1968), 237–239. https://doi.org/10.1090/S0002-9904-1968-11901-9
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1 (1971), 11–26. https://doi.org/10.1007/BF01753431