Why revenue-maximizing auctions matter

A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.

This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.

Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).

Setting

There are $N \ge 2$ potential buyers $i \in I = \{1,\dots,N\}$. Buyer $i$ values the good at $\theta_i$; if he receives it and pays $t_i$ his utility is $\theta_i - t_i$, and otherwise $-t_i$. The seller's utility is $\sum_i t_i$. The valuations $\theta_1,\dots,\theta_N$ are independent; $\theta_i$ has cumulative distribution function $F_i$ and density $f_i$ with $f_i(\theta_i) > 0$ on the common support $[\underline\theta, \bar\theta]$, where $0 \le \underline\theta < \bar\theta$. The type space is $\Theta = [\underline\theta,\bar\theta]^N$ and the joint density is $f(\theta) = \prod_i f_i(\theta_i)$.

A direct mechanism asks buyers to report their types and consists of an allocation rule $q : \Theta \to \Delta$, where $\Delta = \{(q_1,\dots,q_N) : 0 \le q_i \le 1,\ \sum_i q_i \le 1\}$, and payment rules $t_i : \Theta \to \mathbb R$. Its interim quantities are the expected allocation probability, payment and utility of buyer $i$ conditional on his own type:

$$Q_i(\theta_i) = \int_{\Theta_{-i}} q_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad T_i(\theta_i) = \int_{\Theta_{-i}} t_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad U_i = \theta_i Q_i - T_i.$$

The mechanism is incentive-compatible if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i,\theta_i,\theta_i'$ (truth-telling is a Bayesian Nash equilibrium) and individually rational if $U_i(\theta_i) \ge 0$ for all $i,\theta_i$. The virtual valuation of buyer $i$ is

$$\psi_i(\theta_i) = \theta_i - \frac{1 - F_i(\theta_i)}{f_i(\theta_i)},$$

and the distribution $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Myerson's optimal auction (Proposition 3.4)

Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue $\mathbb E[\sum_i t_i(\theta)]$ exactly when, for every buyer $i$,

$$q_i(\theta) = \begin{cases}1 & \text{if } \psi_i(\theta_i) > 0 \text{ and } \psi_i(\theta_i) > \psi_j(\theta_j) \text{ for all } j \ne i,\\ 0&\text{otherwise,}\end{cases}\qquad T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx,$$

the allocation identity holding for almost every $\theta$; and such a mechanism exists.

Milestones

1. Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
2. Lemmas 3.1–3.4: incentive compatibility makes $Q_i$ increasing and $U_i$ convex with $U_i' = Q_i$; payoff equivalence $U_i(\theta_i) = U_i(\underline\theta) + \int_{\underline\theta}^{\theta_i} Q_i$; revenue equivalence for $T_i$.
3. Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
4. Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$.
5. Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$.
6. Eqs. (3.4)–(3.5): expected revenue equals expected virtual surplus $\sum_i \int_\Theta q_i(\theta)\psi_i(\theta_i) f(\theta)\,d\theta$.
7. Proposition 3.5: a mechanism maximizes expected welfare $\mathbb E[\sum_i q_i(\theta)\theta_i]$ among incentive-compatible, individually rational mechanisms if and only if it gives the good to the highest value (almost everywhere) and $T_i(\theta_i) \le \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i}Q_i$.

Significance

The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price $\psi^{-1}(0)$ when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.

The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end $\underline\theta \ge 0$, Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on $[0,\bar v]$.

Difficulty

The obvious argument maximizes the virtual surplus $\sum_i q_i(\theta)\psi_i(\theta_i)$ pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every $Q_i$; the pointwise maximizer is feasible only because regularity makes $\psi_i$ increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every $\psi_i$ and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of $U_i$, with care at the endpoints of the type interval.

Formalization scope

Buyers form a finite type with at least two elements. The prior is the measure on $\mathbb R^N$ with density $\prod_i f_i(\theta_i)$ on $\Theta$ and no mass outside it; each $f_i$ is measurable, strictly positive on $[\underline\theta,\bar\theta]$ and integrates to $1$; $F_i(\theta_i) = \int_{\underline\theta}^{\theta_i} f_i$. Allocation and payment rules are total functions whose values on $\Theta$ are constrained, and $Q_i$, $T_i$ are prior expectations with the $i$-th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of $\psi_i$ on $[\underline\theta,\bar\theta]$ (Assumption 3.1).

The following conventions are committed to:

• Measurability. The book omits measurability throughout. The comparison class for optimality consists of mechanisms with measurable $q_i, t_i$, integrable $t_i$, and integrable sections $\theta_{-i}\mapsto t_i(\theta_i,\theta_{-i})$. Without these hypotheses the Lean integrals would be $0$ and revenue comparisons would be meaningless.
• Almost-everywhere characterizations. Propositions 3.4 and 3.5 are printed with "for all $\theta \in \Theta$". Changing $q$ on a null set of type vectors changes neither incentives nor revenue nor welfare, so the "only if" directions hold only almost everywhere; they are stated for almost every $\theta$, and the existence of a mechanism satisfying the allocation rule at every $\theta$ is stated separately. The payment conditions hold for every $\theta_i$.
• Explicit formulas. The goal states Myerson's allocation rule and the payment formula $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ explicitly. Proposition 3.5 states the efficient rule $q_i(\theta) = 1$ iff $\theta_i > \theta_j$ for all $j \ne i$, and the payment inequality. A statement asserting only that some optimal mechanism exists, or only that the optimal auction is efficient, would not be this theorem.
• Revelation principle. A general mechanism has arbitrary measurable message sets and an outcome function giving allocation probabilities in $\Delta$ and expected transfers; equilibria are in pure type-contingent strategies. A version in which the mechanism is already direct would be trivial and is not the statement.
• Interim constraints. Incentive compatibility and individual rationality are Bayesian and interim, not dominant-strategy or ex post; the latter are the subject of a later mission.
• Endpoints in Lemma 3.2. Differentiability of $U_i$ and $U_i' = Q_i$ are stated at interior points of $[\underline\theta,\bar\theta]$.

The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.

Selected references

• Tilman Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.2, pp. 31–45. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• John G. Riley and William F. Samuelson, Optimal Auctions, American Economic Review 71(3), 381–392, 1981. https://www.jstor.org/stable/1802786
• William Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
• Partha Dasgupta, Peter Hammond and Eric Maskin, The Implementation of Social Choice Rules: Some General Results on Incentive Compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.

It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.

Setting

Mine A holds $x_0 \ge 0$ units of gold and mine B holds $y_0 \ge 0$. At time $t$ a proportion $\varphi_1(t) \in [0,1]$ of the machine's effort goes to A and $\varphi_2(t) = 1 - \varphi_1(t)$ to B (Eq. (7.3)). With $x(t), y(t)$ the gold remaining, $p(t)$ the probability that the machine still works and $f(t)$ the expected gold mined, the process is defined by Eq. (7.2):

$$\frac{dx}{dt} = -\varphi_1 r_1 x,\qquad \frac{dy}{dt} = -\varphi_2 r_2 y,\qquad \frac{dp}{dt} = -p\,(\varphi_1 q_1 + \varphi_2 q_2),\qquad \frac{df}{dt} = p\,(\varphi_1 r_1 x + \varphi_2 r_2 y),$$

with $x(0) = x_0$, $y(0) = y_0$, $p(0) = 1$, $f(0) = 0$. The mining rates $r_1, r_2$ and the failure rates $q_1, q_2$ are positive. The objective is the expected total gold $f(\infty) = \int_0^\infty f'(t)\,dt$.

In the three-choice problem (§ 12) a third decision $C$ removes gold from A at rate $r_3$ and from B at rate $r_4$, and fails at rate $q_3$. A control is a triple $\varphi_1, \varphi_2, \varphi_3 \ge 0$ with $\varphi_1 + \varphi_2 + \varphi_3 = 1$ (Eq. (12.2)). For a horizon $T$, the switching functions $K_1, K_2, K_3$ of Eq. (12.5) are computed along a control. For instance,

$$K_1(t) = -q_1\int_t^T f'(s)\,ds + r_1\,p(T)\,x(T) - r_1\int_t^T p'(s)\,x(s)\,ds.$$

They measure the first-order gain from shifting effort towards each decision at time $t$. The linear forms

$$C_1 = q_1 r_2 y - q_2 r_1 x,\qquad C_2 = q_1 r_4 y - (q_3 r_1 - q_1 r_3)x,\qquad C_3 = (q_3 r_2 - q_2 r_4) y - q_2 r_3 x$$

and the quantity $D = q_1 r_2 r_3 + q_2 r_1 r_4 - q_3 r_1 r_2$ (Eqs. (13.2)–(13.3)) organize the analysis.

Formalization targets

Goal: Chapter VIII, Theorem 1

For the two-choice process, the maximum of $f(\infty)$ is attained by the policy

$$\varphi_1 = 1 \text{ for } q_1 r_2 y < q_2 r_1 x,\qquad \varphi_2 = 1 \text{ for } q_1 r_2 y > q_2 r_1 x,\qquad \varphi_1 = \tfrac{r_2}{r_1+r_2},\ \varphi_2 = \tfrac{r_1}{r_1+r_2} \text{ for } q_1 r_2 y = q_2 r_1 x.$$

The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes $f(\infty)$ over all measurable controls with values in $[0,1]$.

Milestones

1. Eq. (10.1): $f_A(\infty) = r_1 x_0/(q_1 + r_1)$ and $f_B(\infty) = r_2 y_0/(q_2 + r_2)$ for the pure policies.
2. Lemmas 1–3 (§ 13): for a control that maximizes $f(T)$, almost everywhere, $K_i > K_j$ forces $\varphi_i = 1$ or $\varphi_j = 0$; a strictly largest $K_i$ forces $\varphi_i = 1$; a strictly beaten $K_i$ forces $\varphi_i = 0$.
3. Lemma 4 (§ 14): if $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant and $D \ne 0$, no optimal control mixes $A$, $B$ and $C$ on an interval.
4. Lemma 5 (§ 14): a mixture of exactly two decisions on an interval keeps the state on $C_1 = 0$, $C_2 = 0$ or $C_3 = 0$ respectively, with the proportions that hold $y/x$ fixed.
5. § 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$.
6. "Theorem 8" (§ 16, the chapter's third theorem): if $D < 0$ (with $r_3 > r_4$ and $x_0, y_0 > 0$), the three-choice problem is solved by the two-choice rule of Theorem 1, and every optimal control has $\varphi_3 = 0$ almost everywhere.

Significance

Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope $y/x$, and on the line $q_1 r_2 y = q_2 r_1 x$ it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: $D < 0$ means that $C$ removes gold at a higher failure cost than an equivalent mixture of $A$ and $B$.

On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.

Difficulty

The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and $B$ is preferred near the $y$-axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let $\varphi$ be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into "$C_k = 0$ on the interval".

Formalization scope

• Process by closed forms. No differential equations are formalized. With $\Phi_i(t) = \int_0^t \varphi_i$, the definitions are $x = x_0 e^{-r_1\Phi_1 - r_3\Phi_3}$, $y = y_0 e^{-r_2\Phi_2 - r_4\Phi_3}$, $p = e^{-\sum_i q_i\Phi_i}$, $f(T) = \int_0^T f'$. These are the unique absolutely continuous solutions of (7.2) and (12.1). The two-choice process is the three-choice one with $\varphi_3 = 0$.
• Controls are open-loop and measurable, with $\varphi_i \ge 0$ and $\sum_i \varphi_i = 1$. Decisions are indexed 0, 1, 2 for $A, B, C$.
• $f(\infty)$ is a lower Lebesgue integral with values in $[0,\infty]$. It has no junk value, and optimality is compared in $[0,\infty]$.
• Theorem 1's feedback rule is encoded as a predicate on open-loop controls: the rule holds along the control's own trajectory for almost every $t \ge 0$. The goal also asserts that such a control exists, which rules out the trivializing reading in which no control satisfies the rule and the optimality claim is vacuous.
• Horizon of Lemmas 1–5. § 12 considers only $T = \infty$, but the variation (12.4) and the switching functions (12.5) are written for a general $T$. Each lemma is formalized for both: every finite horizon $T$, with $K_i$ built from that horizon, and $T = \infty$, with $K_i$ given by (12.5) at $T = \infty$ (boundary term $0$).
• Implicit ranges. All rates $q_1, q_2, q_3, r_1, \dots, r_4$ are taken positive, and $x_0, y_0 \ge 0$. Lemmas 4–5 and "Theorem 8" take $x_0, y_0 > 0$, the open quadrant the book analyses. Lemma 4 carries the book's assumption that $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant ($q_1 r_3 < q_3 r_1$, $q_2 r_4 < q_3 r_2$). "Theorem 8" carries the standing assumption $r_3 > r_4$ of § 15.
• Misprint corrected. The value of the pure $C$-policy in the proof of Lemma 6 (§ 15, Eq. (1), p. 237) is printed $r_3 x_0/(q_2 + r_3) + r_4 y_0/(q_3 + r_4)$. The first denominator must be $q_3 + r_3$: for $x_0 = 1$, $y_0 = 0$, $q_2 = 1$, $q_3 = 2$, $r_3 = 1$ the process yields $1/3$, not $1/2$. The corrected identity is stated.
• Numbering. The third theorem of the chapter is printed "Theorem 8" and is cited that way.
• Left out. Theorem 2 ($D > 0$) specifies its solution only through Fig. 7 and an unspecified line $L$. Lemmas 6–8, 11 and the two Lemmas 12 describe regions of figures. The finite-horizon analysis of § 11 has no numbered result, and neither does the nonlinear utility of § 18.

Useful infrastructure: the derivative formulas (13.1) for the $K_i$, a first-variation lemma for $f(T)$ under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter VIII, pp. 222–244. https://doi.org/10.2307/j.ctv1nxcw0f
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
• J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

Motivation

The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level $\bar x$, computed from the demand distribution alone.

This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's $(s,S)$ theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.

Setting

A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is $x \ge 0$. The decision maker orders up to a level $y \ge x$, at cost $k(y-x)$ with $k > 0$. A demand $s \ge 0$ then arrives, with probability density $\varphi$: $\varphi(s) > 0$ for $s > 0$, $\int_0^\infty \varphi(s)\,ds = 1$, and $\int_0^\infty s\,\varphi(s)\,ds < \infty$. If $s \le y$, the next period starts with stock $y - s$. If $s > y$, the excess $s - y$ is bought at the penalty rate $p > 0$ and the next period starts with stock $0$. Costs one period ahead are multiplied by a discount factor $0 < a < 1$.

Write $f(x)$ for the minimal expected discounted cost from stock $x$. Enumerating the cases gives Bellman's equation (5.1):

$$f(x) = \min_{y \ge x} T(y,x,f),$$ $$T(y,x,f) = k(y-x) + a\Big[\int_y^\infty p(s-y)\varphi(s)\,ds + f(0)\int_y^\infty \varphi(s)\,ds + \int_0^y f(y-s)\varphi(s)\,ds\Big].$$

A policy assigns an order-up-to level $y(x) \ge x$ to each stock $x$. It is optimal when $y(x)$ attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.

Formalization targets

Goal: Chapter V, Theorem 1 (with (4b) corrected)

The equation has exactly one solution $f$ among measurable functions bounded on $[0,\infty)$. If $ap > k$, the equation

$$k = ap\int_{\bar x}^\infty \varphi(s)\,ds + ak\int_0^{\bar x}\varphi(s)\,ds$$

has exactly one root $\bar x \ge 0$, and for every $x \ge 0$ the minimum is attained at

$$y(x) = \max(x, \bar x).$$

If $ap \le k$, the minimum is attained at $y(x) = x$: never order.

Milestones

1. Chapter IV, Theorem 6 (proportional costs): existence and uniqueness of a solution bounded on every finite interval, its continuity, and convergence of $f_{n+1}(x) = \min_{y\ge x} T(y,x,f_n)$ from any non-negative continuous $f_0$.
2. Eq. (5.8): $\bar x$ is the unique root of $\int_0^{y}\varphi(s)\,ds = (ap-k)/a(p-k)$.
3. Appendix, Theorem 9: the renewal equation $u(x) = f(x) + \int_0^x u(x-s)\varphi(s)\,ds$ with $\int_0^\infty|\varphi| < 1$ has a unique locally bounded solution. The solution is the limit of successive approximations, satisfies a derivative identity, and is non-negative when $f, \varphi \ge 0$.
4. Theorem 3: in the undiscounted $n$-stage process with $p > k$, the optimal policy at each horizon is a constant stock level $\bar x_n$, and $\bar x_n$ increases with $n$.
5. Theorem 4: with a fixed stock-out charge $q$ added to the penalty, the constant-stock-level policy is still optimal when the last minimum of

$$\psi(y) = ky + a\Big[\int_y^\infty [p(s-y)+q]\varphi(s)\,ds - k\int_0^y (y-s)\varphi(s)\,ds\Big]$$

is its absolute minimum.

Significance

The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as $\int_0^{\bar x}\varphi = (ap-k)/a(p-k)$ gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through $\max(x,\bar x)$. This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.

As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.

Difficulty

Two steps resist the obvious argument. First, the minimization is over the unbounded set $y \ge x$, and the unknown $f$ enters through a convolution with $\varphi$. The operator $f \mapsto \min_{y\ge x}T(y,x,f)$ is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of $\max(x,\bar x)$ for $x > \bar x$ requires $f(y) + ky$ to be nondecreasing on $[\bar x,\infty)$. There $f$ is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at $\bar x$ is not enough, and neither is checking that the candidate function satisfies the equation at the single level $\bar x$.

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter. Integrals over $(y,\infty)$ are Lebesgue integrals and $\int_0^y$ are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes $\int_0^y f(y-s)\varphi(s)\,ds$ meaningful; without it a non-measurable function would make the integral default to $0$. "$\varphi(s) > 0$" is read as positivity on $(0,\infty)$.

Conventions and corrections, each stated in the items:

• Theorem 1, (4b) is printed "for $x \ge \bar x$, $y = \bar x$". Read literally, a stock $x > \bar x$ would be "ordered down" to $\bar x < x$, which violates $y \ge x$. The proof (p. 163, "the minimum occurs at $y = x$") and Theorem 4's (7) give $y = x$, which is what the goal states. The printed text reads: "(4) a. for 0 ≤ x ≤ x̄, y = x̄, b. for x ≥ x̄, y = x̄."
• The goal's uniqueness class is "uniformly bounded functions over $x \ge 0$" (p. 164). Chapter IV, Theorem 6 is stated in its own larger class.
• Theorem 4 gives no range for $q$; $q \ge 0$ is assumed. Its phrase "the last minimum of $\psi$ is the absolute minimum" is read as: $\bar x$ minimizes $\psi$ on $[0,\infty)$ and $\psi$ is nondecreasing on $[\bar x,\infty)$. The bracket of (6), unbalanced in print, is closed at the end.
• Theorem 3 assumes "$p > k$"; $k > 0$ and the density conditions of Theorem 1 are carried over.
• Theorem 9's derivative clause assumes $f$ continuously differentiable, where the book says "differentiable". The derivative identity is asserted for $x > 0$.

A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume $f$ is given, and does not take $\bar x$ as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at $\max(x,\bar x)$ for every $x \ge 0$.

Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at $x = \bar x$. Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for $\min_{y\ge x}T(y,x,\cdot)$ on bounded measurable functions.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter V and Chapter IV § 9. https://doi.org/10.2307/j.ctv1nxcw0f
• R. Bellman, I. Glicksberg, O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
• K. J. Arrow, T. Harris, J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906813
• A. Dvoretzky, J. Kiefer, J. Wolfowitz, The inventory problem: I. Case of known distributions of demand, Econometrica 20(2), 1952, 187–222. https://doi.org/10.2307/1907847
• A. F. Veinott, Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

Motivation

Many optimization problems in operations research are posed on an expectation: a two-stage or multistage stochastic program minimizes $f(x) = E\,F(x,\xi)$, where $F(\cdot,\xi)$ is convex but nonsmooth and the expectation cannot be computed exactly. What can be computed is a stochastic subgradient, a random vector whose mean is a subgradient of $f$. The stochastic subgradient method replaces the exact subgradient in the classical method by such a random vector. It was introduced by Yu. M. Ermoliev and N. Z. Shor in 1968 and developed by Ermoliev, Nurminski and others into a standard tool of stochastic programming; the same scheme, under the name stochastic (sub)gradient descent, underlies most of large-scale machine learning.

This mission formalizes Section 2.6 of N. Z. Shor, Minimization Methods for Non-Differentiable Functions (Springer 1985): the almost-sure convergence theorem for the stochastic subgradient method (Theorem 2.19), together with two deterministic results of the same section on perturbed and restarted variants of the subgradient method (Theorems 2.18 and 2.20).

Timeline, as recorded in the book:

• 1968, Ermoliev and Shor: the notion of a stochastic subgradient, introduced for a random search method for two-stage stochastic programs; the convergence theorem reproduced as Theorem 2.19.
• 1972, Bazhenov: convergence of a subgradient method with restarts for almost differentiable (in general nonconvex) functions, Theorem 2.18.
• 1976, Shepilov: stability of the subgradient method with respect to errors in the point where the subgradient is computed, Theorem 2.20.

Setting

$E_n$ is $n$-dimensional Euclidean space with inner product $(x,y)$. 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$; $M^*$ is the set of minimum points of $f$.

Stochastic subgradient method. Fix a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_k)_{k \ge 0}$, a deterministic starting point $x_0$, stepsize rules $h_k : E_n \to \mathbb{R}$ and random vectors $g_k : \Omega \to E_n$. The iterates are

$$x_{k+1} = x_k - h_k(x_k)\, g_k, \qquad k = 0,1,\dots$$

In the book's notation $g_k = g_\omega(x_k)$: a random vector whose expectation, given the state at step $k$, is a subgradient of $f$ at $x_k$. In the Lean development the iterates are stochIter h G x₀ k ω.

Perturbed subgradient method (Shepilov). Given a subgradient selection $g_f$, points $\tilde x_k$ with $\|\tilde x_k - x_k\| \le \delta_k$, and steps $h_k > 0$: $x_{k+1} = x_k - h_k\, g_f(\tilde x_k)/\|g_f(\tilde x_k)\|$.

Restarted method (Bazhenov). For a function $f$ that is almost differentiable (Lipschitz on bounded sets, differentiable almost everywhere, with gradient continuous where it exists) and a selection $g_f(x)$ of almost-gradients (limit points of gradients at nearby points of differentiability), with $S_r = \{x : \|x - x^*\| \le r\}$: take the normalized step $\bar x_{k+1} = x_k - h_k\, g_f(x_k)/\|g_f(x_k)\|$ and restart from $x_0$ whenever $\bar x_{k+1}$ leaves $S_r$ (resetIter).

Formalization targets

Goal: Theorem 2.19 (p. 46)

Let $f$ be convex with a unique minimum point $x^*$. Suppose $E\{g_k \mid \mathcal F_k\}$ is a subgradient of $f$ at $x_k$, $E\{\|g_k\|^2 \mid \mathcal F_k\} \le c$, and almost surely $h_k(x_k) > 0$, $\sum_k h_k(x_k) = +\infty$, $\sum_k h_k^2(x_k) < \infty$. Then

$$P\Big(\lim_{k\to\infty} \|x_k - x^*\| = 0\Big) = 1 .$$

Milestones

1. Eq. (2.42), the conditional one-step inequality

$$E\{\|x_{k+1} - x^*\|^2 \mid \mathcal F_k\} \le \|x_k - x^*\|^2 + c\,h_k^2(x_k).$$

2. Proof of Theorem 2.19, pp. 46–47: with probability one $\|x_k - x^*\|^2$ converges to a finite limit (no divergence condition on the steps).
3. Theorem 2.20 (Shepilov): under $\delta_k \to 0$, $\sum h_k\delta_k < \infty$, $\sum h_k^2 < \infty$, $\sum h_k = \infty$, the perturbed method converges to a point of $M^*$.
4. Theorem 2.18 (Bazhenov): if $f(x^*) = \min_{S_r} f$ and $\inf_{S_r\setminus S_\varepsilon} (g_f(x), x - x^*) > 0$ for every $0 < \varepsilon < r$, the restarted method with $h_k \to 0$, $\sum h_k = \infty$ converges to $x^*$ from any $x_0 \in S_r$.

Significance

Theorem 2.19 is the basic justification of stochastic subgradient methods: without computing $f$ or any exact subgradient, the method reaches the minimizer with probability one, under stepsize conditions that are met by $h_k = 1/(k+1)$. It is the nonsmooth convex counterpart of the Robbins–Monro theorem and the prototype of the almost-sure convergence results for stochastic quasi-gradient methods used in stochastic programming. Theorem 2.20 shows that the deterministic method tolerates summable errors in the point where the subgradient is evaluated, which is what allows subgradients to be approximated by finite differences (Section 1.3). Theorem 2.18 extends the convergence of the normalized method to local minima of a class of nonconvex functions.

All four results are proved in the literature. To the best of the platform search (September 2026), none is machine-checked: the platform has almost-sure convergence theorems for smooth stochastic approximation under ODE-type hypotheses (Borkar–Meyn) and in-expectation bounds for stochastic gradient descent, neither of which covers this recursion. A formal proof of the goal would give a reusable almost-sure convergence argument for nonsmooth stochastic methods on top of Mathlib's martingale theory.

Difficulty

The deterministic proof of convergence of the subgradient method compares $\|x_{k+1}-x^*\|^2$ with $\|x_k - x^*\|^2$ along the whole trajectory. With random directions this comparison holds only in conditional expectation, and the term $h_k(g_k - E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ is not controlled pathwise. Taking expectations of the one-step inequality and summing gives only bounds on $E\|x_k - x^*\|^2$, which do not yield almost-sure convergence. Moreover the stepsize $h_k(x_k)$ depends on the random iterate, so the conditions $\sum h_k^2(x_k) < \infty$ and $\sum h_k(x_k) = \infty$ hold only almost surely, not uniformly, and the iterates need not be square-integrable. Identifying the almost-sure limit as $0$ requires using the uniqueness of the minimizer to bound $(E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ away from zero outside a neighbourhood of $x^*$.

In Theorems 2.18 and 2.20 the difficulty is that the distance to $x^*$ is not monotone: steps taken near the solution, or with a perturbed subgradient, can increase it, and a restart can move the iterate far away.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere); convexity is ConvexOn ℝ Set.univ f; uniqueness of $x^*$ is a separate hypothesis.
• Probabilistic model. The book assumes the distribution of $g_\omega(x_k)$ is determined by $x_k$ and independent of the past, and remarks this is inessential. The formalization uses a filtration: $g_k$ is $\mathcal F_{k+1}$-measurable, each $h_k$ is Borel measurable, $x_0$ is deterministic, and the hypotheses are on conditional expectations given $\mathcal F_k$. This contains the book's model.
• Condition (iii) is printed as $E\|g_\omega(x_k)\|^2 \le c$; the proof uses the conditional bound in (2.42), and the formalization assumes the conditional bound $E\{\|g_k\|^2\mid\mathcal F_k\} \le c$ almost surely.
• Every expectation carries an integrability hypothesis ($g_k$ and $\|g_k\|^2$ integrable), so no conditional expectation defaults to Lean's junk value $0$. The one-step milestone assumes $\|x_k - x^*\|^2$ integrable and a bounded stepsize rule at that step, and concludes integrability of $\|x_{k+1}-x^*\|^2$.
• Conditions (i)–(ii) on the random stepsizes are required almost surely. "With probability one $\lim\|x_k - x^*\| = 0$" is ∀ᵐ ω ∂μ, Tendsto (fun k => ‖x k ω - x*‖) atTop (𝓝 0).
• Division by zero. In Theorems 2.18 and 2.20 the normalized step is undefined when the subgradient vanishes; the formalization skips the step (the iterate is repeated) by an explicit branch, not through Lean's convention $x/0 = 0$. When the subgradient never vanishes the sequences are exactly the book's.
• The printed display (2.42) has $x_k$ where $x_{k+1}$ is meant on its left-hand side; the corrected inequality is stated.
• A trivializing formalization, for instance dropping the integrability hypotheses so that the conditional expectations vanish, or quantifying the stepsize conditions so that they cannot hold, is excluded by the hypotheses above; the hypotheses are satisfiable (deterministic subgradients of $f(x) = \|x\|$ with $h_k = 1/(k+1)$).
• Mathlib supplies conditional expectation (MeasureTheory.condExp), filtrations, and almost-sure convergence of $L^1$-bounded (sub/super)martingales; the supermartingale convergence theorem the book cites from Doob is used from Mathlib, not restated. A Robbins–Siegmund-type lemma for nonnegative almost-supermartingales would be the natural reusable contribution. The almost-differentiability and subgradient definitions duplicate drafts of other missions in this series.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Section 2.6, pp. 44–47. https://doi.org/10.1007/978-3-642-82118-9
• Yu. M. Ermoliev and N. Z. Shor, A random search method for two-stage problems of stochastic programming and its generalization, Kibernetika (Kiev), no. 1, 90–92, 1968.
• L. G. Bazhenov, On the conditions for convergence of methods for minimizing almost differentiable functions, Kibernetika (Kiev), no. 4, 71–72, 1972.
• M. A. Shepilov, On a method of generalized gradient for finding the absolute minimum of a convex function, Kibernetika (Kiev), no. 4, 52–57, 1976.
• Yu. M. Ermoliev, Methods of Stochastic Programming, Nauka, Moscow, 1976.
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, pp. 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (supermartingale convergence theorem).

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).