Dynamic Programming

Markov Chain Operations Research·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 4: Under Sennott's Conditions an Average-Cost Optimal Stationary Policy ExistsResearch Paper

Motivation

Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.

When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.

Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.

Setting

The state space is $S=\{0,1,2,\dots\}$ . For each state $i$ the set $U(i)$ of admissible actions is a nonempty compact subset of a metric space $A$ . Choosing $a\in U(i)$ in state $i$ costs $c(i,a)\ge0$ , and the next state is $j$ with probability $P(j\mid i,a)$ . For fixed $i,j$ , the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$ .

An admissible policy $\pi\in\Pi$ chooses the action at time $t$ according to a probability distribution $\pi_t(\cdot\mid h_t)$ concentrated on $U(x_t)$ , where $h_t=(x_0,a_0,\dots,x_t)$ is the history; it may use the whole history and may randomize. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$ , applied at every step. Given an initial state $i$ and a policy $\pi$ , the states and actions $(X_t,A_t)$ form a stochastic process with law $P^\pi_i$ and expectation $E^\pi_i$ .

For $\beta\in(0,1)$ , the discounted cost and the average cost of $\pi$ from $i$ are

J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N\,E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),

both in $[0,\infty]$ . The optimal values are $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ and $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$ , and the differential discounted value is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$ . A policy $f\in\Pi_{SD}$ is AC-optimal if $J(i,f)=J^*(i)$ for every $i$ .

Sennott's conditions (Assumptions 5.14–5.16) are:

$J^*_\beta(i)<\infty$ for all $i\in S$ and $\beta\in(0,1)$ ;
there is a nonnegative integer $L$ with $h_\beta(i)\ge-L$ for all $i$ and $\beta$ ;
there is $M:S\to\mathbb R_+$ with $h_\beta(i)\le M(i)$ for all $i$ and $\beta$ , and for each $i$ some $a(i)\in U(i)$ with $\sum_jP(j\mid i,a(i))M(j)<\infty$ .

Formalization targets

Goal: Theorem 5.9

\text{Under Assumptions 5.14–5.16, there is } f\in\Pi_{SD}\text{ with } J(i,f)=\inf_{\pi\in\Pi}J(i,\pi)\ \text{ for every } i\in S.

The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.

Milestones

Theorem 2.1 (i), (iii), countable form: the discounted cost optimality equation $J^*_\beta(i)=\inf_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)J^*_\beta(j)\}$ and a $\beta$ -discount optimal $f_\beta\in\Pi_{SD}$ .
Display (5.15): $(1-\beta)J^*_\beta(0)+h_\beta(i)=c(i,f_\beta(i))+\beta\sum_jP(j\mid i,f_\beta(i))h_\beta(j)$ .
The limit objects: along a subsequence $\beta_n\to1$ , $f_{\beta_n}\to f$ , $h_{\beta_n}\to h\ge-L$ pointwise, and $(1-\beta_n)J^*_{\beta_n}(i)\to\rho^*$ , a constant.
The average cost optimality inequality (ACOI) $\rho^*+h(i)\ge c(i,f(i))+\sum_jP(j\mid i,f(i))h(j)$ .
An ACOI along $f$ with $h$ bounded below gives $J(i,f)\le\rho$ .
Theorem A.2: the Abelian inequalities between Cesàro and Abel means (already on the platform).
$J(i,\pi)\ge\rho^*$ for every $\pi\in\Pi$ .

Significance

The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.

Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.

Difficulty

The obvious argument lets $\beta\to1$ in the discounted optimality equation (5.6). Two steps fail without more structure. First, $h_\beta$ need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum $\sum_jP(j\mid i,a)h_\beta(j)$ by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of $\Pi$ , which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.

Formalization scope

The Lean development uses the following representation and conventions.

States, actions, model. The state space is ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and $c(i,\cdot)$ , $P(j\mid i,\cdot)$ are continuous on $U(i)$ .
Policies. $\Pi$ consists of all history-dependent randomized policies, with admissibility required almost surely. $J^*$ and $J^*_\beta$ are infima over all of $\Pi$ , never over stationary policies only. Restricting the infimum to $\Pi_{SD}$ would drop the Tauberian half of the theorem and is not the paper's statement.
Costs. Costs are lower Lebesgue integrals in $[0,\infty]$ against the Ionescu-Tulcea path measure, and the average cost is a limsup in $[0,\infty]$ .
Explicit hypotheses. $h_\beta$ is a difference of real parts and is used only under Assumption 5.14, so it is never read off an infinite $J^*_\beta$ . The quantifiers over $i$ and $\beta$ in Assumption 5.15, implicit on the page, are universal, and $L$ is a natural number as printed. Every series $\sum_jP(j\mid i,a)h(j)$ carries a summability hypothesis or conclusion.
Corrected claim. Remark 5.8(a) as printed claims that any scalar $\rho$ satisfying the ACOI with $h$ bounded below is the optimal average cost. That is false ( $h\equiv0$ , $\rho=\sup c$ ), so only the inequality $J(i,f)\le\rho$ , which the proof uses, is stated.
Sequences. The milestones about limits are stated for any sequence $\beta_n\in(0,1)$ with $\beta_n\to1$ , not only increasing ones.

A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.

Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact $U(i)$ ; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37(4) (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
L. I. Sennott, A new condition for the existence of optimal stationary policies in average cost Markov decision processes, Oper. Res. Lett. 5 (1986) 17–23 (reference [155] of the survey; no stable link checked).
S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150] of the survey).
A. Federgruen, A. Hordijk, H. C. Tijms, Denumerable state semi-Markov decision processes with unbounded costs, average cost criterion, Stochastic Process. Appl. 9 (1979) 223–235 (reference [53] of the survey).
R. Sznajder, J. A. Filar, Some comments on a theorem of Hardy and Littlewood, J. Optim. Theory Appl. 75 (1992) (reference [176] of the survey, cited for Theorem A.2).

11 thms2 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: mikedeng1

Optimality of Affine Policies in Multistage Robust Optimization: In One-Dimensional Constrained Min-Max Control, Disturbance-Affine Policies with Affine Stage Costs Attain the Optimal ValueResearch Paper

Motivation

Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.

Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.

Setting

Fix a horizon $T$ and an initial state $x_1\in\mathbb R$ . For each stage $k=1,\dots,T$ there are a per-unit control cost $c_k\ge0$ , control bounds $L_k\le U_k$ , disturbance bounds $\underline w_k\le\overline w_k$ , and a state cost $h_k:\mathbb R\to\mathbb R$ that is convex and coercive. The state evolves as

x_{k+1}=x_k+u_k+w_k,\qquad u_k\in[L_k,U_k],\qquad w_k\in\mathcal W_k=[\underline w_k,\overline w_k].

The controller chooses $u_k$ after seeing $x_k$ ; the adversary then chooses $w_k$ . The min-max value $J_{mM}$ is the value of the nested problem $\min_{u_1}[c_1u_1+\max_{w_1}[h_1(x_2)+\min_{u_2}[\cdots]]]$ , computed by the Bellman recursion with $J^*_{T+1}\equiv0$ :

g_k(y)=\max_{w\in\mathcal W_k}\big[h_k(y+w)+J^*_{k+1}(y+w)\big],\qquad J^*_k(x)=\min_{L_k\le u\le U_k}\big[c_ku+g_k(x+u)\big],\qquad J_{mM}=J^*_1(x_1).

An affine control policy and an affine running cost at stage $k$ are

q_k(w)=q_{k,0}+\sum_{t=1}^{k-1}q_{k,t}w_t,\qquad z_k(w)=z_{k,0}+\sum_{t=1}^{k}z_{k,t}w_t,

so $q_k$ sees the disturbances before stage $k$ and $z_k$ those up to stage $k$ . Under these policies the state after stage $k$ is $x_1+\sum_{t\le k}(q_t(w)+w_t)$ .

Formalization targets

Goal: Theorem 3.1

There exist affine policies $q_k$ and affine costs $z_k$ such that, for every $k=1,\dots,T$ ,

L_k\le q_k(w)\le U_k\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_{k-1},

z_k(w)\ge h_k\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_k,

J_{mM}=\max_{w_1,\dots,w_k}\Big[\sum_{t=1}^k\big(c_tq_t(w)+z_t(w)\big)+J^*_{k+1}\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\Big].

At $k=T$ this says that affine policies are robustly feasible and attain the min-max value.

Milestones

Lemma 7.1 (with (8)–(9), P2): $J^*_k$ and $g_k$ are convex, and the optimal control is the clamp $\max(L_k,\min(U_k,y^*-x))$ for a minimizer $y^*$ of $c_ky+g_k(y)$ .
P3: the clamp is non-increasing and 1-Lipschitz.
Lemma 4.1: the maximum of $\theta_1+f(\theta_2)$ , $f$ convex, over a planar zonogon $\Theta=\pi([0,1]^k)$ is attained at one of the $k+1$ vertices on its right side.
Corollary 4.1: the maximum of $\theta_1+f(\theta_2)$ is unchanged when a polygon is replaced by its convex hull, its vertex set, its right side, or the zonogon hull of its vertices.
Lemma 4.2: after the optimal control is applied, the worst case is reached on the right side of $\operatorname{conv}\{\tilde v_0,\dots,\tilde v_k\}$ .
Lemma 4.4: the matching-and-alignment system (37) defining the affine controller is feasible, and its solutions satisfy $-b_i\le q_i\le0$ and $L\le q(w)\le U$ .
Lemma 4.8 and Lemma 4.9: the affine cost defined by system (51)–(53) dominates the convex cost, first at the hypercube vertices, then on the whole hypercube.

Significance

The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the $h_k$ are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most $k+1$ vertices, matching the $k+1$ coefficients of an affine policy.

The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of $c_ky+g_k(y)$ , and Lemma 4.3 is proved in one sub-case only.

Difficulty

Dynamic programming gives the optimal control as a function of the current state, $u^*_k(x_k)$ , which is piecewise affine in $x_k$ with up to three pieces. Since $x_k$ is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost $z_k$ that still dominates $h_k$ . Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all $2^k$ vertices of the disturbance box is overdetermined.

Formalization scope

Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 ( $c_k\ge0$ , $h_k$ convex and coercive) plus two disclosed additions, $L_k\le U_k$ and $\underline w_k\le\overline w_k$ : the page writes both as intervals but does not say they are nonempty. $J^*_k$ is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.

The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by $b_i$ , the hypothesis $b_i>0$ . Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.

Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true $J^*_{k+1}$ . The policies read only past disturbances (sums over $t<k$ , resp. $t\le k$ ). $J_{mM}$ is the Bellman value over all state-feedback controls, not the value of the affine problem.

The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.

Selected references

D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of Affine Policies in Multi-stage Robust Optimization, arXiv:0904.3986v1, 2009; Mathematics of Operations Research 35(2):363–394, 2010. https://arxiv.org/abs/0904.3986, https://doi.org/10.1287/moor.1100.0444
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2):491–531, 2012. https://doi.org/10.1007/s10107-011-0444-4
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995 (Chapter 7, zonotopes). https://doi.org/10.1007/978-1-4613-8431-1

11 thms2 active usersReviewed

Completed

Control Theory Markov Chain Operations Research·Captain: mikedeng1

Optimal Control of Markov Processes with Incomplete State Information 1: Reduction to Complete State Information on the Conditional State Distributions, with the Same Optimal LawResearch Paper

Motivation

A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.

K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.

Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.

Setting

The hidden state $x_t$ , $t = 1, \dots, N$ , takes values in a finite set $S$ . The controls $u = (u_1, \dots, u_r)$ range over a compact nonempty set $U \subset \mathbb R^r$ . The state moves by the transition probabilities $p_{ij}(u, t) = P\{x_t = j \mid x_{t-1} = i\}$ , which are continuous in $u$ . The state is observed through outputs $y_t$ in a finite set $Y$ , with $q_{ij} = P\{y_t = j \mid x_t = i\}$ , conditionally independent given the states. The law of $x_1$ is $p^1$ . An instantaneous cost $g(u, i, t)$ , continuous in $u$ , is paid at each time.

A control law chooses $u(t) = c(\eta_1, \dots, \eta_t, t) \in U$ from the outputs observed so far, $\eta(t) = (\eta_1, \dots, \eta_t)$ . With $u(t)$ moving $x_t$ to $x_{t+1}$ , a law determines the joint law of $(x_1, \dots, x_N, y_1, \dots, y_N)$ and the expected cost

EL = E \sum_{t=1}^N g(u(t), x_t, t). \tag{2.6}

Problem P.1 is to find an admissible law minimizing (2.6).

The conditional state distribution is $w_i(t) = P\{x_t = i \mid \eta(t)\}$ . It is updated by Bayes' rule: with $z^j(u, w)_i = \sum_s q_{ij}\, p_{si}(u, t+1)\, w_s$ and $\|z\| = \sum_i |z_i|$ , the output $\eta_{t+1} = j$ gives $w(t+1) = z^j(u(t), w(t)) / \|z^j(u(t), w(t))\|$ , and $\|z^j\|$ is the probability of that output. The cost-to-go $V_k(w)$ is the minimal expected cost of the steps $k, \dots, N$ when $x_k$ has distribution $w$ , with $V_{N+1} = 0$ . Problem P.2 controls the process $w(t)$ directly: a law chooses $u(t)$ from $w(1), \dots, w(t)$ to minimize $E\sum_{t=1}^N \sum_i g(u(t), i, t)\, w_i(t)$ .

Formalization targets

Goal: Theorem 3

P.1 has a solution if and only if P.2 has one. For every solution $(V, c^0)$ of the functional equation

V_k(w) = \min_{u \in U} \Big\{ \sum_i g(u, i, k)\, w_i + \sum_j V_{k+1}\Big(\frac{z^j(u, w)}{\|z^j(u, w)\|}\Big) \|z^j(u, w)\| \Big\}, \qquad V_{N+1} = 0, \tag{3.28}

with $c^0(w, k)$ attaining the minimum, the law

u(t) = c^0(w(t), t)

is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal $E_{\eta_1} V_1(w(1))$ .

Milestones

(3.20)–(3.25): the conditional distributions obey the Bayes recursion, and $\|z^j\| = P[y_{t+1} = j \mid \eta(t)]$ .
Theorem 1: the cost-to-go satisfies (3.28) with the minimum attained, and an optimal Markov law attains it.
Theorem 2: a solution of (3.28) gives an optimal law for P.1 with value (3.29).
Lemma 1: under $u(t) = c(w(t), t)$ , $\{w(t)\}$ is a Markov process with transition probabilities $P(y, \Gamma, u) = \sum_{k \in K} \|z^k(u, y)\|$ .
Proof of Theorem 3: the integral against this kernel is the sum in (3.28).

Significance

The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes $w(t)$ in real time, and the function $c^0$ can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.

Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.

Difficulty

The obvious argument is backward induction on the conditional distributions. The difficulty is that $w(t)$ depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than $w(t)$ must gain nothing. Restricting the comparison class to laws of the form $c(w(t), t)$ assumes this conclusion.

A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over $U$ are attained, which needs continuity of $V_{k+1}$ on the simplex. The weights $\|z^j(u, w)\|$ can vanish, and then the update $z^j/\|z^j\|$ is undefined.

Formalization scope

States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and $U$ is compact and nonempty. The law $p^1$ of $x_1$ is the datum in place of the paper's law of $x_0$ , since no control $u(0)$ exists. The transition from $x_t$ to $x_{t+1}$ uses $u(t)$ and the matrix $p(u(t), t+1)$ . Times $1, \dots, N$ are indexed by Fin N as $0, \dots, N-1$ .

The norm $\|\cdot\|$ is the $\ell^1$ norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When $\|z^j\| = 0$ the update is the zero vector and is always multiplied by $0$ .

The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights $\|z^j\|$ . "Given by Theorem 1" is read as " $c^0(w, k) \in U$ attains the minimum in (3.28)" (IsSolution328).

The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law $c^0(w(t), t)$ to be optimal in both problems, against every admissible law, with equal minimal values.

Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of $V_k$ on the simplex, and existence of solutions of (3.28).

Selected references

K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9
P. D. Joseph and J. T. Tou, On linear control theory, Transactions of the AIEE, Part II 80(4):193–196, 1961. https://doi.org/10.1109/TAI.1961.6371743

10 thms2 active usersReviewed

Completed

Control Theory Probability·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 6: A Canonical Policy Is Strong Average Optimal and Its Average Cost Is the Optimal OneResearch Paper

Motivation

A controlled Markov process (CMP), or Markov decision process, models a system that moves randomly between states while a controller chooses actions that influence both the cost incurred and the next state. When the planning horizon is long and no discounting is natural (queueing control, inventory, communication networks, maintenance), the criterion of interest is the long-run average cost. Average-cost problems are harder than discounted ones: the dynamic programming operator is no longer a contraction, and an optimal policy need not exist without structure.

The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organizes the theory by state space. For Borel state spaces and bounded costs, §6.1 follows Dynkin and Yushkevich and works with canonical triplets: a pair of bounded functions and a policy that make the policy optimal for every finite horizon with a fixed terminal cost. Theorem 6.3 is the statement that explains why this notion is the right one: a canonical triplet solves the average-cost problem.

Timeline. The notion of a canonical policy was introduced by Yushkevich (1973) and developed in Dynkin and Yushkevich's Controlled Markov Processes (1979, Chap. 7), which contains the substance of Theorem 6.3 (i)–(iii). Mandl (1974) introduced the discrepancy function that bears his name. The almost-sure statements (v)–(vi) are due to Georgin (1978). Coupled optimality equations for the multichain case go back to Howard (1960).

Setting

The model is a five-tuple $(S, A, U, P, c)$ . The state space $S$ and the action space $A$ are Borel spaces. For each state $x$ , $U(x)\subseteq A$ is a nonempty compact set of admissible actions, and $K = \{(x,a): a\in U(x)\}$ is measurable. $P(dy\mid x,a)$ is a transition kernel and $c$ a measurable one-stage cost, nonnegative on $K$ .

A policy $\pi = (\pi_t)$ chooses the action at time $t$ at random from a kernel $\pi_t(da\mid h_t)$ that may depend on the whole history $h_t = (x_0,a_0,\dots,x_t)$ and charges only $U(x_t)$ . The class of all such policies is $\Pi$ . Each policy and initial state $x$ determine a law $\mathcal P^\pi_x$ of the state–action process $(X_t, A_t)$ , with expectation $E^\pi_x$ .

For a horizon $N$ and a terminal cost $h$ ,

J_N(x,\pi,h) = E^\pi_x\Big[\sum_{t=0}^{N-1}c(X_t,A_t) + h(X_N)\Big],\qquad J_N(x,\pi)=J_N(x,\pi,0),\qquad J^*_N(x,h)=\inf_{\pi\in\Pi}J_N(x,\pi,h).

The average cost is $J(x,\pi)=\limsup_N \frac1N J_N(x,\pi)$ and the optimal average cost is $J^*(x)=\inf_{\pi\in\Pi}J(x,\pi)$ . The span of a bounded function is $\operatorname{span}(h)=\sup h-\inf h$ .

With $\mathcal M_b(S)$ the bounded measurable functions, a triplet $(\rho,h,\pi^*)$ with $\rho,h\in\mathcal M_b(S)$ and $\pi^*\in\Pi$ is canonical if

J_N(x,\pi^*,h) = J^*_N(x,h) = h(x)+N\rho(x)\qquad\forall N\in\mathbb N_0,\ x\in S. \tag{6.4}

A policy $\pi^*$ is strong average optimal if

\limsup_{N\to\infty}\frac1N J_N(x,\pi^*)\le\liminf_{N\to\infty}\frac1N J_N(x,\pi)\qquad\forall x\in S,\ \pi\in\Pi. \tag{6.5}

Formalization targets

Goal: Theorem 6.3 (i)–(iii)

Let $(\rho,h,\pi^*)$ be a canonical triplet and let $c$ be bounded on $K$ . Then for each $x\in S$ :

\text{(i)}\quad J_N(x,\pi^*)\le J_N(x,\pi)+\operatorname{span}(h)\quad\forall N,\ \forall\pi\in\Pi;

\text{(ii)}\quad \pi^* \text{ is strong average optimal};\qquad \text{(iii)}\quad J(x,\pi^*)=J^*(x)=\rho(x).

Steps toward the goal

The proof's milestones are: $J_N(x,\pi^*,h)\le J_N(x,\pi,h)$ ; the decomposition $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$ ; part (i) on its own; and $\rho(x)=\lim_N\frac1N J_N(x,\pi^*)$ .

Further targets: Theorem 6.3 (v)–(vi)

If $\rho\equiv\rho^*$ is constant and $\Phi(x,a)=c(x,a)+\int h(y)P(dy\mid x,a)-\rho^*-h(x)$ is Mandl's discrepancy function, then for every $\pi\in\Pi$ and $x$ ,

\limsup_{N\to\infty}\frac1N\sum_{t=0}^{N-1}c(X_t,A_t)\ge\rho^*\quad\mathcal P^\pi_x\text{-a.s.},

and the running average converges to $\rho^*$ almost surely if and only if $\frac1N\sum_{t<N}\Phi(X_t,A_t)\to0$ almost surely. Moreover $\pi^*$ is sample path average cost optimal. The intermediate milestones are $\Phi\ge0$ on $K$ , the almost-sure limit $\frac1N\sum c-\rho^*-\frac1N\sum\Phi\to0$ under every policy, and $\Phi(X_t,A_t)=0$ almost surely under $\pi^*$ .

Significance

The result. Theorem 6.3 reduces the average-cost problem on a general Borel space to finding a canonical triplet. Once one is found, $\rho$ is the optimal average cost from every initial state, possibly state-dependent as in multichain models, and the canonical policy is optimal in a strong sense: its worst-case long-run performance is no worse than the best-case long-run performance of any competitor, at every finite horizon up to the additive constant $\operatorname{span}(h)$ . With constant $\rho$ , optimality also holds path by path. The rest of §6 of the survey looks for conditions on $c$ and $P$ that produce a canonical triplet, and those results rely on this theorem.

Formalizing it. The result is classical and proved; it has no machine-checked proof that we know of. Formalization requires measure-theoretic infrastructure for history-dependent policies on Borel spaces (Ionescu-Tulcea path measures, finite-horizon costs, infima over all admissible policies) together with a strong law for bounded martingale differences for parts (v)–(vi). Both are reusable for any average-cost result on general state spaces.

Difficulty

Parts (i)–(iii) are short on paper; the work is in making every quantity genuine. The infimum $J^*_N$ ranges over a class of kernels, and turning (6.4) into a usable inequality needs the family bounded below. The decomposition of $J_N(x,\pi,h)$ needs integrability, which comes from the almost-sure confinement of the trajectory to $K$ , a consequence of admissibility under the path measure. Parts (v)–(vi) need the conditional expectation identity $E^\pi_x[c(X_t,A_t)+h(X_{t+1})-\rho^*-h(X_t)\mid H_t,A_t]=\Phi(X_t,A_t)$ from the Markov structure of the path measure, and a martingale strong law. The tempting shortcut of restricting to stationary or Markov policies is not available: $\pi^*$ and every competitor are arbitrary history-dependent randomized policies.

Formalization scope

$S$ is a standard Borel space and $A$ a Borel space; $U(x)$ is nonempty and compact with measurable graph $K$ ; $c\ge0$ on $K$ (Assumption 2.1, which the paper assumes throughout). $c$ and $P$ are defined on $S\times A$ and only their values on $K$ enter.
$\Pi$ is the class of history-dependent randomized admissible policies (p. 285). Neither $\pi^*$ nor the competitors are restricted.
$\mathcal P^\pi_x$ is Mathlib's Kernel.trajMeasure. $J_N$ is a Bochner integral and $J^*_N$ a real infimum; every theorem assumes $c$ bounded on $K$ , which makes both genuine.
$J$ , $J^*$ , both sides of (6.5), and the sample path average cost $J_S$ are computed in EReal, so no limit superior or inferior is a junk value. Part (iii) is the two equalities $J(x,\pi^*)=J^*(x)$ and $J^*(x)=\rho(x)$ .
Part (iv) is not posed: its proof goes through value iteration under Assumptions 2.1–2.3, which Theorem 6.3 does not assume.
Part (vi) is stated under the hypothesis of (v), $\rho\equiv\rho^*$ constant. As printed it has no hypothesis on $\rho$ and is false: two absorbing states with costs $0$ and $1$ give a canonical triplet whose pathwise average costs differ by state.
The identity $J_N(x,\pi,h)=J_N(x,\pi)+E^\pi_x[h(X_N)]$ is stated for every $\pi$ ; the page writes it for $\pi^*$ and applies it to an arbitrary $\pi$ in the proof of (i).
The sentence "for a canonical policy $\pi^*$ , $\Phi(X_t,A_t)=0$ , $\mathcal P^\pi_x$ -a.s." is stated with $\mathcal P^{\pi^*}_x$ , the only reading that makes sense.
$\Phi\ge0$ is derived on the page from (6.7) via Theorem 6.2, which covers stationary $\pi^*$ ; here it is stated directly from the canonical triplet for arbitrary $\pi^*\in\Pi$ .
Sample path optimality quantifies over all initial laws (probability measures on $S$ ), as on p. 288.
None of the hypotheses is vacuous: the one-state, one-action model with zero cost and $\rho\equiv h\equiv0$ is a canonical triplet (checked in Lean). Strong average optimality is stated as limsup against liminf, not the weaker limsup against limsup.

Contributions welcome: a.s. confinement of trajectories to $K$ , integrability lemmas for $J_N$ , the Markov property of trajMeasure in the form above, and a strong law for bounded martingale differences.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018 (Theorem 6.3 on p. 318, its proof on pp. 318–319; (6.4), (6.5) on p. 316)
E. B. Dynkin, A. A. Yushkevich, Controlled Markov Processes, Springer-Verlag, New York, 1979 (reference [51] of the survey; Chap. 7).
A. A. Yushkevich, On a class of strategies in general Markov decision models, Theory Probab. Appl. 18 (1973) 777–779 (reference [204] of the survey).
P. Mandl, Estimation and control in Markov chains, Adv. Appl. Probab. 6 (1974) 40–60 (reference [124] of the survey).
J.-P. Georgin, Contrôle de chaînes de Markov sur des espaces arbitraires, Ann. Inst. H. Poincaré Sect. B 14 (1978) 255–277 (reference [72] of the survey).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, Cambridge, MA, 1960 (reference [95] of the survey).

12 thms2 active usersReviewed

Completed

Markov Chain Operations Research·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 1: Uniformly Bounded Differential Discounted Values Give a Bounded Solution of the Average Cost Optimality EquationResearch Paper

Motivation

Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.

Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.

Setting

A controlled Markov process on the countable state space $S=\{0,1,2,\dots\}$ consists of a metric space $\mathbf A$ of actions; for each state $i$ a nonempty compact set $U(i)\subseteq\mathbf A$ of admissible actions; a cost $c(i,a)\ge0$ ; and transition probabilities $P(j\mid i,a)$ . For fixed $i,j$ , the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$ .

An admissible policy $\pi$ chooses, at each time $t$ , a probability distribution on $U(X_t)$ that may depend on the whole past $(X_0,A_0,\dots,X_t)$ . The class of all of them is $\Pi$ , and $\Pi_{SD}$ is the class of stationary deterministic policies, maps $f$ with $f(i)\in U(i)$ . Each initial state $i$ and policy $\pi$ define a law $P^\pi_i$ of the trajectory, with expectation $E^\pi_i$ . For a discount factor $0<\beta<1$ ,

J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),

and $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ , $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$ . The differential discounted value function is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$ . A pair $(\rho,h)$ , $\rho\in\mathbb R$ , $h:S\to\mathbb R$ , solves the ACOE if

\rho+h(i)=\min_{a\in U(i)}\Big\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\Big\},\qquad i\in S.\tag{5.1}

In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue ( $J^*_\beta$ ), optAvg ( $J^*$ ), hRel ( $h_\beta$ ) and ACOE.

Formalization targets

Goal: Theorem 5.2 (p. 301)

Assume $J^*_\beta(i)<\infty$ for all $\beta\in(0,1)$ and $i\in S$ , and that there is $K>0$ with $|h_\beta(i)|\le K$ for all such $\beta$ and $i$ . Then there are $\rho\in\mathbb R$ , a bounded $h:S\to\mathbb R$ and a sequence $\beta_n\in(0,1)$ , $\beta_n\to1$ , with

(\rho,h)\text{ solves (5.1)},\qquad h(i)=\lim_{n\to\infty}h_{\beta_n}(i),\qquad \lim_{\beta\uparrow1}(1-\beta)J^*_\beta(i)=\rho\qquad(i\in S).

The goal does not assert that $\rho$ is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.

Milestones

Lemma 2.1 (p. 289): the dynamic programming map $T(v)(i)=\inf_{a\in U(i)}\{c(i,a)+\sum_jP(j\mid i,a)v(j)\}$ satisfies $T(v+k)=T(v)+k$ and is monotone.
Theorem 2.1 (i), (iii) (p. 289), in the countable model: $J^*_\beta=T_\beta J^*_\beta$ and a $\beta$ -discount optimal $f\in\Pi_{SD}$ exists.
Equation (5.6) (p. 301): $(1-\beta)J^*_\beta(0)+h_\beta(i)=\min_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)h_\beta(j)\}$ .
Theorem 5.1 (p. 299): a solution of (5.1) with $\lim_t\frac1tE^\pi_ih(X_t)=0$ gives $\rho=J(i,f)=J^*(i)$ for a minimizing selector $f$ ; minimizing selectors are average optimal; conversely, an average optimal $f$ with an irreducible positive recurrent chain is a minimizing selector.
Remark 5.1(a) (p. 300): a bounded solution of (5.1) satisfies the growth condition of Theorem 5.1.

Significance

Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant $\rho$ independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.

The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.

Difficulty

The obvious argument fixes a sequence $\beta_n\uparrow1$ , extracts a pointwise convergent subsequence of the bounded functions $h_{\beta_n}$ and of the bounded numbers $(1-\beta_n)J^*_{\beta_n}(0)$ , and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over $U(i)$ is not in general the minimum of the limits: the convergence of $a\mapsto\sum_jP(j\mid i,a)h_{\beta_n}(j)$ must be shown to be uniform on the compact set $U(i)$ , which requires more than pointwise continuity of each $P(j\mid i,\cdot)$ . Second, the subsequential limit $\rho$ could depend on the subsequence, so part (iii), a limit along all $\beta\uparrow1$ , needs an independent identification of $\rho$ , here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where $J^*_\beta$ is not the unique fixed point of $T_\beta$ .

Formalization scope

The state space is ℕ; state 0 is the reference state of $h_\beta$ . Policies are history-dependent randomized stochastic kernels with the admissibility constraint $\pi_t(U(x_t)\mid h_t)=1$ , and $J^*$ , $J^*_\beta$ are infima over all of them. Costs are lower Lebesgue integrals with values in $[0,\infty]$ , built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:

Finiteness of $J^*_\beta$ . The paper's bound $|h_\beta|\le K$ presupposes finite values; the goal assumes $J^*_\beta(i)<\infty$ , and (5.6) assumes it for its $\beta$ .
Convergent series in the ACOE. A solution of (5.1) requires every series $\sum_jP(j\mid i,a)h(j)$ , $a\in U(i)$ , to converge, and the minimum to be attained.
(5.2) over all policies. The paper prints the growth condition of Theorem 5.1 for $\pi\in\Pi_{SD}$ , but its conclusion $\rho=J^*(i)$ concerns all policies, and the proof uses the condition for arbitrary $\pi$ . It is stated for every $\pi\in\Pi$ , with integrability of $h(X_t)$ explicit.
Theorem 2.1 is cited without proof in the survey for Borel models; in the countable model its Assumptions 2.2–2.3 follow from the continuity assumptions of §5. Only parts (i) and (iii) are stated.
Lemma 2.1 is stated for functions bounded below (on discrete ℕ these are the lower semicontinuous functions bounded below), with convergent series.
Irreducible, positive recurrent (converse of Theorem 5.1): every state is reached with positive probability from every state, and every state has finite expected return time.

A formalization in which $J^*$ is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which $h_\beta$ is computed from $+\infty$ values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.

A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24 (reference [38] of the survey).
C. Derman, Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 37 (1966) 1545–1553 (reference [39]).
H. M. Taylor, Markovian sequential replacement processes, Ann. Math. Statist. 36 (1965) 1677–1694 (reference [177]).
S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423, and Arbitrary state Markovian decision processes, Ann. Math. Statist. 39 (1968) 2118–2122 (references [147], [148]).
S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150]).
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37 (1989) 626–633 (reference [156]).

9 thms2 active usersReviewed

Control Theory Operations Research Optimization+2·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$ , control space $C$ and observation space $Z$ ; a discount factor $\alpha>0$ ; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$ ; a Borel state transition kernel $t(dx'\mid x,u)$ ; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$ ; and a horizon $N$ . The initial state $x_0$ has distribution $p\in P(S)$ , $z_0\sim s_0(\cdot\mid x_0)$ , and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$ , $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$ . The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$ , where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$ , the cost

J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$ , for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$ . The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$ , constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$ , costs $\hat g_k$ and transitions $\hat t_k$ ; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$ . The initial distribution of $y_0$ is

\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$ .

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$ ,

J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),

and a Markov (PSI) policy that is optimal, $\varphi(p)$ -optimal or weakly $\varphi(p)$ - $\varepsilon$ -optimal for (PSI) is respectively optimal, optimal at $p$ , or $\varepsilon$ -optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$ -optimal (PSI) policy is $\varepsilon$ -optimal for (ISI). Here $\hat\pi$ is weakly $q$ - $\varepsilon$ -optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$ -optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$ .
Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$ .
Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$ .
Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
Proposition 10.4: $\varepsilon$ -optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$ .
Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$ -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$ -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$ , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$ , so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$ ; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$ , $(N,\hat N)$ , $(D,\hat D)$ are out of scope.
Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ( $\top-\top=\bot$ ) is never used where both terms can be infinite.
Spaces and measures. $S$ , $C$ , $Z$ , $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$ -algebras; $P(S)$ carries the weak topology and the Giry $\sigma$ -algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$ ; only stages $k<N$ are constrained.
Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

12 thms2 active usersReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case VII: The Finite-Horizon Borel Model — over Universally Measurable Policies J*_K = T^K(J_0)Textbook

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$ . The state space $S$ , control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$ . Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$ , the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ( $\{g<c\}$ is analytic for every real $c$ ), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$ .

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$ ; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$ -stage cost and optimal cost are

J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$ , and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$ , for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$ -th pair. The DP operators are

T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.

Formalization targets

Goal: Proposition 8.2

J^*_K=T^K(J_0),\qquad K=1,\dots,N,

under (F⁺) or (F⁻), where $J_0\equiv0$ . The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$ ), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$ ), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$ ), Lemma 8.4 (monotone and bounded convergence for $T_\mu$ ). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ( $J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$ .

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$ , choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$ -optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$ . Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
Stages are indexed $0,\dots,N-1$ , and a history is $k$ state–control pairs plus the current state.
$g$ is stored on $S\times C$ , but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$ , not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

14 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IV: The Generalized Abstract Model — Restricted Policy Classes under ContractionTextbook

Why restricted policy classes

Abstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping $H(x,u,J)$ : the cost of using control $u$ at state $x$ when the future is valued by the function $J$ . Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors $\mu:S\to C$ and $H$ is defined on all extended-real functions on $S$ .

That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which $H$ acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class $\tilde M$ and $H$ is only defined on a prescribed class $\tilde F$ of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.

Setting

The data are a state space $S$ , a control space $C$ , nonempty constraint sets $U(x)\subseteq C$ , and three restricted classes: sets of functions $F^*\subset\tilde F\subset F$ , where $F$ is the set of all functions $S\to[-\infty,\infty]$ , and a set $\tilde M$ of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ . The mapping $H:S\times C\times\tilde F\to[-\infty,\infty]$ is monotone: $J\le J'$ in $\tilde F$ implies $H(x,u,J)\le H(x,u,J')$ . For $\mu\in\tilde M$ and $J\in\tilde F$ ,

T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).

A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ with every $\mu_k\in\tilde M$ ; their set is $\tilde\Pi$ . Given $J_0\in F^*$ with $J_0>-\infty$ , the $N$ -stage and infinite-horizon costs are

J_{N,\pi}=(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0),\qquad J_\pi(x)=\lim_{N\to\infty}J_{N,\pi}(x),

and the optimal costs are $J^*_N=\inf_{\pi\in\tilde\Pi}J_{N,\pi}$ and $J^*=\inf_{\pi\in\tilde\Pi}J_\pi$ . For a stationary policy $(\mu,\mu,\dots)$ write $J_\mu$ .

Five standing conditions tie the classes together: A.1 (every control $u\in U(x)$ is the value $\mu(x)$ of some $\mu\in\tilde M$ ), A.2 ( $F^*$ is closed under $T$ and under adding constants), A.3 ( $\tilde F$ is closed under every $T_\mu$ , $\mu\in\tilde M$ , and under adding constants), A.4 ( $\varepsilon$ -minimizing selectors for $T(J)$ , $J\in F^*$ , exist in $\tilde M$ ), and A.5 ( $\tilde F$ and $F^*$ are closed under pointwise limits). Assumption $\tilde C$ asks for a closed subset $\bar B$ of the space $B$ of bounded real functions with the sup norm $\|\cdot\|$ , containing $J_0$ and invariant under $T$ on $\bar B\cap F^*$ and under $T_\mu$ on $\bar B\cap\tilde F$ , such that every $J_\pi$ exists and is real, each $T_\mu$ is $\alpha$ -Lipschitz on $B\cap\tilde F$ , and every $m$ -fold composition $T_{\mu_0}\cdots T_{\mu_{m-1}}$ is a $\rho$ -contraction on $\bar B\cap\tilde F$ for some $\rho<1$ .

Formalization targets

Goal: Proposition 6.4 (p. 97)

Under A.1–A.5 and $\tilde C$ : $J^*\in\bar B\cap F^*$ is the unique fixed point of $T$ in $\bar B\cap F^*$ , with $T(J')\le J'\Rightarrow J^*\le J'$ and $J'\le T(J')\Rightarrow J'\le J^*$ ; each $J_\mu$ , $\mu\in\tilde M$ , is the unique fixed point of $T_\mu$ in $\bar B\cap\tilde F$ ;

\lim_{N\to\infty}\|T^N(J)-J^*\|=0\ \ (J\in\bar B\cap F^*),\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0\ \ (J\in\bar B\cap\tilde F);

a stationary $(\mu^*,\mu^*,\dots)\in\tilde\Pi$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$ ; and for every $\varepsilon>0$ some stationary policy in $\tilde\Pi$ satisfies $\|J^*-J_{\mu_\varepsilon}\|\le\varepsilon$ .

Milestones

In attack order:

Proposition 6.3(a) (p. 96) — under A.1–A.4 and the exact selection assumption, a uniformly $N$ -stage optimal policy exists iff the infimum in $T^{k+1}(J_0)(x)=\inf_{u\in U(x)}H[x,u,T^k(J_0)]$ is attained for each $x\in S$ and $k<N$ .
Proposition 6.5(a) (p. 97) — under A.1–A.5, $\tilde C$ and exact selection: if for each $x$ some policy in $\tilde\Pi$ is optimal at $x$ , then an optimal stationary policy exists in $\tilde\Pi$ .

Further results of the chapter

The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:

Proposition 6.2 — $\pi^*$ is uniformly $N$ -stage optimal iff $(T_{\mu_k^*}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$ ; such a policy forces $J^*_N=T^N(J_0)$ .
Proposition 6.1(a) — under Assumption $\tilde F.2$ and $J^*_k>-\infty$ : $J^*_N=T^N(J_0)$ and $N$ -stage $\varepsilon$ -optimal policies exist in $\tilde\Pi$ .
Proposition 6.1(b) — under Assumption $\tilde F.3$ and $J_{k,\pi}<\infty$ : $J^*_N=T^N(J_0)$ and $\{\varepsilon_n\}$ -dominated convergence to optimality.
Proposition 6.3(b) — compact level sets $U_k(x,\lambda)$ give both $J^*_N=T^N(J_0)$ and a uniformly $N$ -stage optimal policy.
Proposition 6.5(b) — compact level sets of the iterates $T^k(J)$ , $k\ge\bar k$ , give an optimal stationary policy.

Significance

Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary $\varepsilon$ -optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm $J^*_N=T^N(J_0)$ , and their hypotheses ( $\tilde F.3$ , exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.

The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case ( $F^*=\tilde F=F$ , $\tilde M=M$ ) of Chapters 3 and 4.

Difficulty

The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to $T$ on $\bar B$ . Here the obvious transcription fails at two points. First, $T$ maps $\bar B\cap F^*$ into itself but $T_\mu$ only maps $\bar B\cap\tilde F$ into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in $\tilde M$ : pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.

Formalization scope

Functions on $S$ are S → EReal. $H$ is a total Lean function, but monotonicity is assumed only on $\tilde F$ and every statement evaluates $H$ only at functions of $\tilde F$ . $J_\pi$ is limUnder; Assumption $\tilde C$ makes the limit exist. $B$ is Mathlib's $\ell^\infty(S,\mathbb R)$ ; a bound $\|G-G'\|\le c$ between extended-real functions means both are real everywhere and $|G(x)-G'(x)|\le c$ , which is how the book's convention $\infty-\infty=\infty$ reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. $J^*_N$ and $J^*$ are infima over $\tilde\Pi$ only, the $\varepsilon$ -optimality notions keep the book's two-case form at $-\infty$ , and $N$ is a positive integer.

The chapter collapses to Chapters 3–4 if $F^*=\tilde F=F$ or $\tilde M=M$ is built in; here $F^*$ , $\tilde F$ and $\tilde M$ are arbitrary and constrained only by A.1–A.5, and $J^*$ is never defined as a fixed point.

A complete development needs the $m$ -step contraction mapping theorem on a closed subset of $\ell^\infty$ , monotonicity lemmas for $T$ and $T_\mu$ , and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption $\tilde C$ contraction, are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 6. https://web.mit.edu/dimitrib/www/soc.html
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control and Optimization 15(3), 1977, 438–464. https://doi.org/10.1137/0315031
E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 1967, 165–177. https://doi.org/10.1137/1009030

7 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Discounted Dynamic Programming: An Optimal Stationary Plan Exists When the Action Set Is Essentially FiniteResearch Paper

Motivation

Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.

The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.

Setting

A state is an element $s$ of a nonempty standard Borel space $S$ , and an action is an element $a$ of a nonempty standard Borel space $A$ . The transition kernel $q(\cdot\mid s,a)$ gives a probability distribution for the next state after action $a$ in state $s$ . The reward $r(s,a,s')\in\mathbb R$ may depend on that next state $s'$ ; it is bounded and Borel measurable. Future rewards are discounted by $\beta$ with $0\le\beta<1$ . These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.

A plan $\pi=(\pi_1,\pi_2,\ldots)$ assigns a probability distribution of actions to each possible history before a decision. At stage $n$ , that history contains $n-1$ completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function $f_n:S\to A$ at each stage; a stationary plan uses the same function $f$ at every stage and is denoted $f^{(\infty)}$ . Starting from state $s$ , the plan has discounted expected return

I(\pi)(s)=\sum_{n=1}^{\infty}\beta^{n-1}\,\mathbb E_s^\pi\bigl[r(\sigma_n,\alpha_n,\sigma_{n+1})\bigr].

Here $\sigma_n$ and $\alpha_n$ are the state and action at stage $n$ . The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.

Two actions are equivalent at state $s$ when they have the same reward $r(s,a,s')$ for every next state $s'$ and the same transition measure $q(\cdot\mid s,a)$ . An action set is essentially countable by a Markov plan $(f_1,f_2,\ldots)$ if, for every $(s,a)$ , one of the actions $f_n(s)$ is equivalent to $a$ at $s$ . It is essentially finite by that plan if $S$ has a countable Borel partition $(S_n)$ such that, for $s\in S_n$ , one of $f_1(s),\ldots,f_n(s)$ is equivalent to every action $a$ at $s$ . A finite action set is a special case. Blackwell 1965, pp. 233–234.

Formalization targets

For a probability distribution $p$ on $S$ and $\varepsilon>0$ , $(p,\varepsilon)$ -optimality asks for a stationary $f$ with

p\{s:I(\pi)(s)>I(f^{(\infty)})(s)+\varepsilon\}=0\qquad\text{for every plan }\pi.

Theorem 6(b) asserts that such an $f$ always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform $\varepsilon$ -optimality statement: for every $\varepsilon>0$ there is a stationary $f$ with $I(\pi)(s)\le I(f^{(\infty)})(s)+\varepsilon$ for all $\pi,s$ . Its other targets identify the optimal return with the fixed point of the operator $U_\pi u=\sup_nT_{f_n}u$ and with the unique bounded solution of the optimality equation $u=\sup_{a\in A}T_au$ . Blackwell 1965, pp. 232–234.

The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary $f$ with exact optimality:

I(\pi)(s)\le I(f^{(\infty)})(s)\qquad\text{for every plan }\pi\text{ and state }s.

The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.

Significance

The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.

Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.

Difficulty

On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an $\varepsilon$ -optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.

Formalization scope

The Lean model uses nonempty StandardBorelSpace types for $S$ and $A$ . “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on $S\times A\times S$ , and $0\le\beta<1$ ; $\beta=0$ is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by $0$ in Lean, corresponding to the paper’s index $1$ . The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.

For the operator results, $M(S)$ means bounded and measurable real functions. The suprema defining $U_\pi$ and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps $M(S)$ into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece $n$ corresponds to the paper’s $S_{n+1}$ , with rules $f_1,\ldots,f_{n+1}$ .

An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.

Selected references

David Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 226–235, 1965. DOI: 10.1214/aoms/1177700285.

11 thms2 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case I: Finite-Horizon Abstract Dynamic Programming — the DP Algorithm Yields the N-Stage Optimal CostTextbook

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$ -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$ , ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$ , $u\in U(x)$ .

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$ . A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),

and let $T^k$ be the $k$ -fold composition of $T$ . A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$ -stage cost of $\pi$ and the $N$ -stage optimal cost are

J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).

A policy is uniformly $N$ -stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$ -stage optimal, and $N$ -stage $\varepsilon$ -optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$ .

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$ ), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ ), and F.3 (a quantitative selection property with a constant $\beta>0$ ).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$ ; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$ :

J^*_N=T^N(J_0),

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$ .

Milestones

Proposition 3.3: $\pi^*$ is uniformly $N$ -stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$ . Needs monotonicity only.
Corollary 3.3.1: a uniformly $N$ -stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$ .
Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$ -stage optimal policy exists.
Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$ .
Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$ .
Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$ , $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$ , policies with $\{\varepsilon_n\}$ -dominated convergence to optimality exist.
Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$ , the DP algorithm gives $J^*_N$ and $N$ -stage $\varepsilon$ -optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$ . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$ . The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$ -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$ , which is why F.3 and the definition of $\varepsilon$ -optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$ . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$ .

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$ , so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

12 thms2 active usersReviewed

Completed

Markov Chain Operations Research·Captain: mikedeng1

Discrete Dynamic Programming 2: A Stationary Policy Is Nearly Optimal as the Discount Factor Tends to 1 Exactly When It Maximizes x(g) and, Among Those, y(g)Research Paper

Motivation

A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor $\beta$ tends to $1$ the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats $\beta = 1$ as a limit of $\beta < 1$ : it expands the discounted return of a stationary policy in powers of $1-\beta$ and reads off which policies remain good as $\beta \to 1$ . The two leading coefficients of that expansion, the gain $x(f)$ and the bias $y(f)$ , became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).

Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all $\beta$ near $1$ (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through $x$ and $y$ . Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders ( $n$ -discount optimality).

Setting

There are finitely many states $s \in S$ and a finite nonempty set $A$ of actions. Action $a$ in state $s$ pays an income $i(s,a) \in \mathbb R$ and moves the system to $s'$ with probability $q(s' \mid s,a)$ . $F$ is the finite set of decision rules $f : S \to A$ . A policy is a sequence $\pi = \{f_1, f_2, \dots\}$ of decision rules; $f^{(\infty)}$ uses $f$ every day, and $(g, \pi)$ uses $g$ first and then $\pi$ . For $f \in F$ , $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s' \mid s,f(s)))_{s,s'}$ . The discounted return of $\pi$ is the vector

V_\beta(\pi) = \sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\, r(f_{n+1}), \qquad 0 \le \beta < 1,

and $V_\beta(f)$ abbreviates $V_\beta(f^{(\infty)})$ . Vectors are compared coordinatewise; $w_1 > w_2$ means $w_1 \ge w_2$ and $w_1 \neq w_2$ . A policy is β-optimal if its return dominates that of every policy, and $U(\beta)$ is the return of a β-optimal policy. It is optimal if it is β-optimal for all $\beta$ sufficiently near $1$ , and nearly optimal if $U(\beta) - V_\beta(\pi) \to 0$ as $\beta \to 1$ .

For any Markov matrix $Q$ , the limit matrix $Q^*$ is the limit of $(I + Q + \cdots + Q^N)/(N+1)$ , and the deviation matrix is $H = (I - Q + Q^*)^{-1} - Q^*$ . For a rule $f$ , $Q^*(f)$ and $H(f)$ are those of $Q(f)$ , and

x(f) = Q^*(f)\, r(f), \qquad y(f) = H(f)\, r(f).

With $p(s,a)w = \sum_{s'} q(s' \mid s,a) w_{s'}$ , the set $G(s,f)$ consists of the actions $a$ with $p(s,a)x(f) > x_s(f)$ , or with $p(s,a)x(f) = x_s(f)$ and $i(s,a) + p(s,a)y(f) > x_s(f) + y_s(f)$ ; $E(s,f)$ consists of those with equality in both.

Formalization targets

Goal: Theorem 4(e)

For any $f_0$ with $G(s,f_0) = \varnothing$ for all $s$ :

x(f_0) \ge x(g)\ \ \forall g \in F;\qquad \exists f^* \in F^* := \{g : x(g) = x(f_0)\}\ \text{with}\ y(f^*) \ge y(g)\ \forall g \in F^*;

g^{(\infty)} \text{ is nearly optimal} \iff x(g) = x(f^*) \text{ and } y(g) = y(f^*).

Milestones and intermediate results

Milestones: Lemma 1(b) ( $\operatorname{rank}(I-Q) + \operatorname{rank} Q^* = S$ ), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).

The mission also states, as intermediate results:

Lemma 1(a), (c), (d): for every Markov matrix, convergence of the Cesàro means to a Markov $Q^*$ with $QQ^* = Q^*Q = Q^*Q^* = Q^*$ ; unique solvability of $Qx = x$ , $Q^*x = Q^*c$ ; nonsingularity of $I - Q + Q^*$ , $\sum_n \beta^n (Q^n - Q^*) \to H$ and the identities for $H$ .
Theorem 4(a): $V_\beta(f) = x(f)/(1-\beta) + y(f) + o(1)$ , with $x(f), y(f)$ the unique solutions of their linear systems; display (2), the same expansion for $(g, f^{(\infty)})$ .
Theorem 3 and its Corollary for fixed $\beta < 1$ , and the first assertion of 4(e).

Significance

Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income $x$ , then of the bias $y$ . It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.

The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.

Difficulty

Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where $Q^n$ does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single $f^*$ whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through $U(\beta)$ .

Formalization scope

States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's $f_1$ . $V_\beta$ is a real tsum. $Q^*$ is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; $H(\beta)$ is a matrix tsum, whose summability for $0 \le \beta < 1$ is part of Lemma 1(d); $H$ uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). $x(f)$ and $y(f)$ are defined by the closed forms $Q^*(f)r(f)$ and $H(f)r(f)$ from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along $\beta \to 1^-$ . "Nearly optimal" is encoded without $U$ : for every $\varepsilon > 0$ , for all β in some interval $(\beta_0, 1)$ , every policy's return is at most $V_\beta(\pi) + \varepsilon$ in every coordinate; this is equivalent to $U(\beta) - V_\beta(\pi) \to 0$ because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set $G(s,f)$ .

A formalization in which optimality or near optimality is tested only against stationary policies, or in which $Q^*$ is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.

Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.

Selected references

D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
B. L. Miller and A. F. Veinott, Discrete Dynamic Programming with a Small Interest Rate, Ann. Math. Statist. 40(2):366–370, 1969.
A. F. Veinott, Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Optimal Policies for a Multi-Echelon Inventory Problem: The Two-Echelon Optimal Cost Splits into the Isolated Installation-1 Cost Plus a Function of Echelon StockResearch Paper

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$ , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$ . The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$ , $\alpha\ge0$ .

The state at the start of a period is $(x_1,w_1,x_2)$ : $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$ . Installation 1 pays the expected holding and shortage cost (1),

L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$ ,

C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$ , $\hat C_0\equiv0$ :

\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$ ,

C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$ , as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$ , with $f_n$ of (7) (p. 480).
Convexity of every $f_n$ (§2 item 3, p. 478).
Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$ .
Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.

Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$ .

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$ . When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$ . The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$ . Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$ . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$ . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$ ; $\varphi\ge0$ with $\int_0^\infty\varphi=1$ ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$ ) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$ , no convexity of $\tilde L$ , no $K=0$ and no sign condition on $w_1$ is assumed.
Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$ ; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$ ; outside it the feasible set of (14) is empty.
The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$ , and $f_n\equiv0$ for $n\le2$ .

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$ , and of any milestone are welcome.

Selected references

A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

8 thms2 active usersReviewed

Completed

Graph Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Algorithm 97: Shortest Path: Floyd's Procedure Computes the Shortest Path Length Between Every Pair of PointsResearch Paper

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$ . The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$ ; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$ . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$ ; a missing link gives length $\infty$ . Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$ , this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$ , then row $j$ , then column $k$ , each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$ . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$ , using chains of one or more links. Its comment asserts

\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$ ,

\operatorname{shortestPath}(w)(i,j)=\infty.

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$ , every matrix $w$ with no negative cycle, and all points $i,j$ ,

\operatorname{shortestPath}(w)(i,j)=d_w(i,j).

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$ . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$ ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$ , the procedure changes that entry to $-2$ , although the shortest simple closed path has length $-1$ . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

6 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ .

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$ , whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$ ; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ .

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$ . For a fixed procedure $R$ started at $X_0 = i$ , let $W'_t$ and $W''_t$ be the expected costs at time $t$ . The ratio criterion is

\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.

For a single cost set $w$ with expected costs $W_t$ , the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$ .

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$ .

Steps of the proof (milestones)

Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$ .
For any procedure $R$ , $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$ .
Under Assumption A, for $R^* \in C''$ , $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$ .
For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$ , with $\pi$ the stationary distribution of $(p_{sj})$ .

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$ , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$ , $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$ ; $Q_R(i)$ with Derman's normalization ( $T+1$ terms divided by $T$ ); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$ ; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$ ; and membership of a procedure in $C'$ with probabilities $D$ . All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$ , which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$ ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$ .

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6):938–948, 1963. https://doi.org/10.1287/opre.11.6.938
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

7 thms2 active usersReviewed

Completed

Control Theory Linear algebra Markov Chain+2·Captain: mikedeng1

Bellman's Dynamic Programming IX: Markovian Decision Processes and the Maximal Perron RootTextbook

Motivation

Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of $N$ states, or the stocks of $N$ commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation

x_i(n+1) = \max_q \sum_{j=1}^N a_{ij}(q)\, x_j(n), \qquad x_i(0) = c_i,

and, in the limit of small time steps, to differential equations of the form $dx/dt = \max_q [A(q,t)x + b(q,t)]$ and, when two opposing controllers act, $dx/dt = \max_p \min_q[\dots]$ .

These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).

Setting

Fix $N \ge 1$ . Row $i$ of the matrix carries its own control $q_i$ , ranging over a set $S_i$ ; the joint control is $q = (q_1, \dots, q_N)$ in $S = S_1 \times \dots \times S_N$ , and $A(q) = (a_{ij}(q_i))$ . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over $q$ is then taken row by row.

The Perron root $\varphi(q)$ is the characteristic root of $A(q)$ of largest absolute value, the spectral radius of $A(q)$ as a complex matrix. The conditions (10.3) of the chapter are:

for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
$0 < a_{ij}(q) \le m < \infty$ on $S$ ;
$\varphi$ attains its maximum on $S$ .

For the continuous processes, $\|x\| = \sum_i |x_i|$ and $\|A\| = \sum_{i,j}|a_{ij}|$ , and a solution of $dx/dt = F(t,x)$ , $x(0)=c$ , on $[0,T]$ is a continuous $x$ with $x(t) = c + \int_0^t F(s, x(s))\,ds$ , which is the book's "satisfying the equation almost everywhere". The successive approximations are $x_0 = c$ , $x_{n+1}(t) = c + \int_0^t F(s, x_n(s))\,ds$ .

Formalization targets

Goal: Chapter XI, Theorem 2

Under (10.3) there is exactly one $\lambda > 0$ for which

\lambda y_i = \max_q \sum_{j=1}^N a_{ij}(q)\, y_j, \qquad i = 1,\dots,N,

has a solution with all $y_i > 0$ . That solution is unique up to a positive factor, and

\lambda = \max_{q \in S} \varphi(q).

Milestones

§ 4, Lemma. For row-wise maximized operators $T_1(x) = \max_q[b_1(q,t) + \int_0^t A(q,s)x\,ds]$ and $T_2(y)$ likewise, $\|T_1(x) - T_2(y)\| \le \max_q[\|b_1 - b_2\| + \int_0^t \|A(q,s)\|\,\|x-y\|\,ds]$ .
Theorem 1. If $\|A(q,t)\|, \|b(q,t)\| \le f(t)$ with $f$ locally integrable and the maximum is attained, then $dx/dt = \max_q[A(q,t)x + b(q,t)]$ , $x(0) = c$ , has a unique solution, the uniform limit of the successive approximations.
Theorem 3 (corrected). If moreover $\varphi$ has a unique maximizer on $S$ and $c \ge 0$ , $c \ne 0$ , then the recurrence satisfies $x_i(n) \sim a\,y_i\,\lambda^n$ with $a = a(c) > 0$ .
Theorem 4. The same well-posedness for $dx/dt = \max_p\min_q[A(p,q,t)x + b(p,q,t)] = \min_q\max_p[\dots]$ on $[0,T]$ .
Theorem 5. If $(Bp,q) \ge d > 0$ on probability vectors, the solution of $du/dt = \max_p\min_q[(Ap,q) - (Bp,q)u]$ satisfies

\lim_{t\to\infty} u(t) = \max_p \min_q \frac{(Ap,q)}{(Bp,q)} = \min_q \max_p \frac{(Ap,q)}{(Bp,q)} .

Significance

Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration $x(n+1) = \max_q A(q)x(n)$ : after normalization by $\lambda^n$ the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.

The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.

Difficulty

The map $y \mapsto \max_q A(q)y$ is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification $\lambda = \max_q \varphi(q)$ must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each $A(q)$ , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when $S$ is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in $t$ and Lipschitz in $x$ with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.

Formalization scope

Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row $i$ 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume $N \ge 1$ ; for $N = 0$ every $\lambda$ would qualify.

Conventions and repairs:

Theorem 3 prints "a unique q for which the maximum value of q is assumed". A control has no maximum value; the proof uses " $q^*$ ... the value of $q$ for which $\lambda = \varphi(q^*)$ ", so the hypothesis is uniqueness of the maximizer of $\varphi$ . For $c = 0$ the iterates vanish and $x_i(n) \sim a y_i\lambda^n$ fails, so $c \ne 0$ is assumed (the proof takes $c > 0$ "without loss of generality"). The asymptotic is stated as $x_i(n)/\lambda^n \to a y_i$ with $a > 0$ .
Theorems 1 and 4: the book's controls are functions of $t$ with the maximum outside the integral; since the maximization is pointwise (§ 4), the statements use pointwise sets and the integral of the pointwise maximum. Measurability of $t \mapsto F(t,x)$ is not stated in the book and is assumed. In Theorem 4 the max-min is taken row by row, and (2a) is encoded as the existence of a saddle point in each row.
§ 4 Lemma: " $\le \max_q[\dots]$ " is stated as " $\le [\dots]$ at some admissible joint $q$ ".
Theorem 5: the right-hand side is the max-min form; the equality of the two ratio values is part of the conclusion.

Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for $dx/dt = F(t,x)$ with an integrable Lipschitz constant, each reusable well beyond this mission.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter XI. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, "A Markovian decision process", Journal of Mathematics and Mechanics 6 (1957), 679–684.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
O. Perron, "Zur Theorie der Matrices", Mathematische Annalen 64 (1907), 248–263. https://doi.org/10.1007/BF01449896
B. Lemmens and R. Nussbaum, Nonlinear Perron–Frobenius Theory, Cambridge University Press, 2012. https://doi.org/10.1017/CBO9781139026079

9 thms2 active usersReviewed

Calculus of Variations Control Theory Numerical Analysis+2·Captain: mikedeng1

Bellman's Dynamic Programming VII: Convergence of Discrete Approximations in the Calculus of VariationsTextbook

Motivation

Chapter IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as $0 \le y \le x$ , is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).

That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.

Setting

A state $x(t) \ge 0$ evolves on a horizon $[0, T]$ under a control $y(t)$ with $0 \le y \le x$ , a running reward $F(x, y)$ and dynamics

\frac{dx}{dt} = G(x, y), \qquad x(0) = c .

Writing $y = \varphi x$ with a fractional control $0 \le \varphi \le 1$ turns $F$ and $G$ into $\tilde F(x, \varphi) = F(x, \varphi x)$ and $\tilde G(x, \varphi) = G(x, \varphi x)$ (phiForm). The continuous value is

f(c, T) = \sup_{\varphi} \int_0^T \tilde F(x(t), \varphi(t))\, dt,

over measurable $\varphi$ with values in $[0, 1]$ , where $x$ solves $x(t) = c + \int_0^t \tilde G(x(s), \varphi(s))\,ds$ on $[0, T]$ (IsTrajectory, contValue).

For $n = 1, 2, \dots$ the discrete problem uses step $1/n$ and $N = \lfloor Tn \rfloor$ steps (horizonSteps): for $\varphi_0, \dots, \varphi_N \in [0, 1]$ ,

x_0 = c, \quad x_{k+1} = x_k + \frac{\tilde G(x_k, \varphi_k)}{n}, \qquad J_N(\{\varphi_k\}, n) = \sum_{k=0}^{N} \frac{\tilde F(x_k, \varphi_k)}{n},

and $f(c, T, n) = \max J_N$ (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control $\varphi(t) = \varphi_k$ on $k/n \le t < (k+1)/n$ (stepControl).

The example of §§ 10–11 has a gain function $b$ with $b(0) = 0$ , $b'(0) = \infty$ , $b' > 0$ , $b'(y) \to 0$ as $y \to \infty$ , $b'' < 0$ (IsGainFunction; $b(y) = y^{1/2}$ is one), and value functions (uSeq)

u_0(c) = c, \qquad u_{N+1}(c) = \max_{0 \le v \le c}\,\bigl[c - v + u_N(c + b(v))\bigr].

Formalization targets

Goal: Chapter IX, Theorem 2 (corrected)

Assume (11): (a) $F$ and $G$ have continuous second partial derivatives; (b) $px \le G(x, y) \le qx + r$ for $x > 0$ , $0 \le y \le x$ ; (c) $G_y > 0$ throughout that region, or $G_y < 0$ throughout. Then for all $c \ge 0$ , $T > 0$ , the set of continuous payoffs is nonempty and bounded above, and

\lim_{n \to \infty} f(c, T, n) = f(c, T).

Milestones

Chapter IX, Theorem 1: the structure of $u_N$ . There are $v_N(c)$ and thresholds $c_N$ with $v_N$ decreasing in $c$ , $v_{N+1} > v_N$ , $c_N$ the unique fixed point of $v_N$ with $c_{N+1} > c_N$ , $u_N(c) = u_{N-1}(c + b(c))$ for $c \le c_N$ , $u_N(c) = c - v_N(c) + u_{N-1}(c + b(v_N(c)))$ for $c \ge c_N$ , and $u_N' \ge u_{N-1}'$ .
§ 12, Lemma (corrected): for $G$ Lipschitz on $[m, M] \times [0, 1]$ , the Euler states with a step control are within $\kappa / n$ of the exact solution on $[0, T]$ .
Eq. (12.13): $|J(\varphi) - J_N(\{\varphi_k\}, n)| \le B'/n$ for step controls.
Eq. (12.14): $f(c, T, n) \le f(c, T) + B'/n$ for all $n \ge 1$ .
Eq. (12.17): $f(c, T) \le \liminf_{n \to \infty} f(c, T, n)$ .

Milestones 3–5 are stated for $c > 0$ , as in the book's proof ("Given $c > 0$ and $T > 0$ "); the goal is stated for $c \ge 0$ , as in the theorem.

Significance

Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than $B'/n$ . The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold $c_N$ the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.

As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.

Difficulty

The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip $m \le x \le M$ ; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid $k/n$ , and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in $L^1$ , not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of $u_N$ and a strict comparison of marginal values across $N$ , and $u_N$ is not differentiable at $c = 0$ , where $b'(0) = \infty$ .

Formalization scope

States, controls and rewards are real; $F, G, b : \mathbb R \to \mathbb R$ (or $\mathbb R \to \mathbb R \to \mathbb R$ ), with the hypotheses imposed where the book imposes them. The conventions:

Misprint in (12.5). The print sets $N = [T/n]$ while using the step $1/n$ in (12.6) and the intervals $k/n \le t < (k+1)/n$ in the Lemma. Under the literal reading the discrete horizon $N/n$ tends to $0$ and Theorem 2 is false: for $F \equiv 1$ , $G(x, y) = y$ (which satisfies (11) with $p = 0$ , $q = 1$ , $r = 0$ , $G_y = 1$ ) and $T = 1$ , $f(c, 1) = 1$ but $f(c, 1, n) = 1/n$ for $n \ge 2$ . The mission uses $N = \lfloor Tn \rfloor$ and keeps the book's sum $\sum_{k=0}^{N}$ ; the range " $k = 0, \dots, n - 1$ " in (12.6) is read as $k = 0, \dots, N - 1$ .
Lemma. Its range " $0 \le t \le N$ " is read as $0 \le t \le T$ . The bounds $m \le x \le M$ are required of the solution $x(t)$ as well as of the sequence $x_k$ , since a Lipschitz condition on the strip says nothing about $G$ outside it; the proof of Theorem 2 supplies both bounds. The constant may depend on $m$ , $M$ and the Lipschitz constant.
Assumptions (11) are on the original $F(x, y)$ , $G(x, y)$ , with (11a) read as $C^2$ on $\mathbb R^2$ ; the problem is posed through $y = \varphi x$ .
"Max" over measurable controls is a supremum (the proof picks $\varepsilon$ -optimal controls). The goal asserts that the set of payoffs is nonempty and bounded above, so the Lean supremum cannot take its default value $0$ . Trajectories satisfy the integral equation with integrable right-hand side, and the reward is required integrable, so the Bochner integral's default $0$ cannot enter either.
Theorem 1. (5a) is read as non-strict monotonicity: for $N = 1$ the interior optimum solves $b'(v) = 1$ and is constant in $c$ . $v_N(c) \ge 0$ is required for $c \ge c_N$ , so that $v_N(c)$ is a feasible choice. (5f) presupposes differentiability and is stated where both derivatives exist.

A trivializing formalization is ruled out: the discrete and continuous values are defined from $F$ and $G$ by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.

Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter IX, §§ 10–12, pp. 256–263. DOI 10.2307/j.ctv1nxcw0f
I. Capuzzo-Dolcetta, On a discrete approximation of the Hamilton–Jacobi equation of dynamic programming, Applied Mathematics and Optimization 10 (1983) 367–377. DOI 10.1007/BF01448394
M. Bardi and I. Capuzzo-Dolcetta, Optimal Control and Viscosity Solutions of Hamilton–Jacobi–Bellman Equations, Birkhäuser, 1997. DOI 10.1007/978-0-8176-4755-1

8 thms2 active usersReviewed

Completed

Control Theory Operations Research Optimization+1·Captain: mikedeng1

Bellman's Dynamic Programming VI: Optimal Policies for the Continuous Gold-Mining ProcessTextbook

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

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.
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$ .
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.
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.
§ 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$ .
"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

11 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Bellman's Dynamic Programming V: Optimality of a Constant Stock Level for the Optimal Inventory EquationTextbook

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

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$ .
Eq. (5.8): $\bar x$ is the unique root of $\int_0^{y}\varphi(s)\,ds = (ap-k)/a(p-k)$ .
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$ .
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$ .
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

7 thms2 active usersReviewed

Completed

Functional Analysis Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming IV: Existence and Uniqueness for Functional Equations of Types One, Two and ThreeTextbook

Motivation

A multi-stage decision process is summarized by its optimal return function $f$ , which satisfies a functional equation. In Chapters I and II of Dynamic Programming (Princeton University Press, 1957), Richard Bellman proves existence and uniqueness for particular processes: allocation of resources, gold mining. Chapter IV abstracts these arguments into theorems about whole classes of equations. The same scheme reappears in later chapters (multi-stage games, the calculus of variations) and in every later treatment of dynamic programming.

Two points explain why the chapter is still worth formalizing. First, uniqueness is always claimed within a stated function class, and the choice of class is part of the theorem: an equation of this kind can have many solutions, and only one of them lies in the class that the process singles out. Second, the chapter covers equations that are not contractions in the supremum norm, in particular Type One, where the shrinking happens in the state rather than in the function values.

Setting

Let $D \subseteq \mathbb{R}^N$ carry the Euclidean norm $\|p\|$ , let $S$ be a nonempty set of decisions, and let $g, h : D \times S \to \mathbb{R}$ and $T : D \times S \to D$ . The general equation (1.1) is

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big].

Here $g$ is the one-stage return, $T(p,q)$ the next state and $h(p,q)$ a multiplier: a discount factor or a survival probability.

An equation is of Type One with constant $0 \le a < 1$ under the following conditions. $D$ contains the null vector $\theta$ . $g$ is bounded on bounded parts of $D$ , uniformly in $q$ , and $g(\theta, q) = 0$ . $|h| \le 1$ . $\|T(p,q)\| \le a\|p\|$ . Finally, with $v(c) = \sup_{\|p\| \le c}\sup_q |g(p,q)|$ , the series $\sum_{n \ge 0} v(a^n c)$ converges for every $c$ .

It is of Type Two under the following conditions. $g$ is bounded on bounded parts of $D$ . On each bounded part, $|h| \le a < 1$ for some $a$ . $T$ maps $D$ into $D$ , and either $\|T(p,q)\| \le \|p\|$ or $D$ is bounded.

The successive approximations are $f_0(p) = \sup_q g(p,q)$ and $f_{n+1}(p) = \sup_q[g(p,q) + h(p,q) f_n(T(p,q))]$ .

The equation of the third type of § 8 lives on the probability simplex $\Delta$ of distributions $p = (p_0, \dots, p_n)$ , with vertices $x_k$ . It reads

f(p) = \min\Big[\,1 + \sum_{k=0}^{n} p_k f(x_k),\ \min_{1 \le l \le M}\big[1 + f(T_l p)\big]\Big] \quad (p \ne x_0), \qquad f(x_0) = 0.

Each $T_l$ maps $\Delta$ into itself, and the $0$ -th coordinate of $T_l p$ is never $1$ . $f(p)$ is the minimal expected time to drive a system into state $0$ with certainty, by observing the state (cost $1$ , then continuing from the observed vertex) or by applying one of the operations $T_l$ (cost $1$ ).

Formalization targets

Goal: Chapter IV, Theorem 1

For a Type One equation there is exactly one solution on $D$ , among functions continuous at $\theta$ and zero there, of

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big] \ (p \ne \theta), \qquad f(\theta) = 0.

It is the pointwise limit of the successive approximations from $f_0 = \sup_q g$ , and also from any $f_0$ that is continuous and zero at $\theta$ and bounded on bounded parts of $D$ . If $g$ , $h$ and $T$ are continuous in $p$ on bounded portions of $D$ , uniformly in $q$ , the solution is continuous on every bounded portion of $D$ .

Milestones

Lemma 1 (the fundamental inequality): for nonnegative measures $dG$ ,

|f_2(p) - F_2(p)| \le \sup_q\Big[\,|g - h| + \int_{D} |f_1 - F_1|\,dG\Big].

Theorem 2: a Type Two equation has a unique solution bounded in every finite part of $D$ , obtained by successive approximations and continuous under the same conditions as in Theorem 1.
Theorem 3 (stability, Type One): $\sup_{\|p\| \le c} |F - f| \le \sum_{n \ge 0} u(a^n c)$ , where $u(c) = \sup_{\|p\| \le c}\sup_q |G - g|$ .
Theorem 4 (stability, Type Two, corrected): $\sup_{\|p\| \le c} |F - f| \le u(c)/(1-a)$ .
Lemma 2: two bounded solutions of the third-type equation satisfy $\sup_{p} |f(p) - g(p)| = \max_k |f(x_k) - g(x_k)|$ .
Theorem 5: if $\sum_{k=1}^n (T_l p)_k \le c_1 < 1$ for every $l$ and $p$ , the third-type equation has a unique bounded solution, and it is positive off $x_0$ .

Significance

Theorem 1 guarantees that the optimal return of a process whose decisions shrink the state is well defined and computable by iteration. It applies without assuming that the supremum over decisions is attained and without regularity of the maximizing decision. Theorems 3 and 4 give quantitative continuous dependence of the solution on the reward. This is what justifies approximating a process by a simpler one. Theorem 5 is a uniqueness result for an undiscounted minimum-time problem, where no contraction in the supremum norm is available.

All of these results are classical and proved in the book. None is formalized: the platform's related statements treat finite state spaces with a fixed policy (FoundationsML.ReinforcementLearning.bellman_equations_unique_solution), or Karlin's compact-decision-set setting with nonnegative rewards and an explicit vanishing-tail hypothesis (KarlinDP.Deterministic.unique_solution_of_vanishing_tail), or finite-state stochastic shortest paths (BertsekasDP.ssp_main_theorem). This mission adds machine-checked versions over a continuum of states and an arbitrary decision set, with the function classes stated exactly.

Difficulty

For Type One, the natural idea is to apply the Banach fixed-point theorem in the space of bounded functions. That fails: $|h| \le 1$ allows no contraction in the supremum norm, and the solution need not be bounded on $D$ . Contraction happens only along trajectories, $\|T(p,q)\| \le a\|p\|$ , so every estimate must be localized to balls $\|p\| \le c$ and summed along radii $a^n c$ . Uniqueness then rests on continuity at $\theta$ rather than on a global norm.

The suprema over an arbitrary, possibly infinite, decision set are not attained in general, so no argument may select a maximizing decision. For the third-type equation, neither a contraction nor a shrinking of the state is available: the operations $T_l$ need not move $p$ towards $x_0$ . Uniqueness among bounded solutions requires controlling how long a solution can keep choosing an operation other than observation.

Formalization scope

The state space is EuclideanSpace ℝ (Fin N), $D$ is a Set, the decision set is a nonempty type S, and functions are total, EuclideanSpace ℝ (Fin N) → ℝ. Only their values on $D$ matter, and uniqueness is asserted on $D$ . The equation is encoded with IsLUB, so the supremum is genuine and has no junk value. The successive approximations and the radii $v(c)$ , $u(c)$ use real iSup/sSup, evaluated only where the book's boundedness conditions hold. "Continuous at $\theta$ " is continuity within $D$ .

Conventions and corrections:

In Type One the book writes "for some $a < 1$ ". The formalization takes $0 \le a < 1$ , which loses no generality.
Condition (1a) of both types is read for every radius $c_1$ .
"Continuous in $p$ in any bounded portion of $D$ , uniformly for all $q$ " is read as uniform equicontinuity on each $\{p \in D : \|p\| \le c\}$ . For closed $D$ this is the pointwise reading.
Theorem 4 is printed with " $|F(p) - (p)|$ ", a misprint for $|F(p) - f(p)|$ . As printed, it is also false under the bounded-domain alternative of Type Two. Take $N = 1$ , $D = [-2,2]$ , $T \equiv 2$ , $h \equiv \tfrac12$ , $g \equiv 0$ , and $G = 1$ at $p = 2$ , $G = 0$ elsewhere. Then $|F(0) - f(0)| = 1$ while $u(1)/(1-a) = 0$ . The formal statement adds that $T$ maps $\{p \in D : \|p\| \le c\}$ into the ball of radius $c$ . This holds for every $c$ under the first alternative, where the statement is the book's.
Lemma 1 is stated for nonnegative measures $dG(p,q,\cdot)$ on $\mathbb{R}^N$ , integrated over $D$ . The right-hand supremum may be infinite, so it is expressed through its real upper bounds.
In § 8 the number of states is written both $N+1$ and $n+1$ ; the formalization uses $n+1$ , with $M \ge 1$ transformations indexed by Fin M.

A trivializing formalization would state uniqueness among all solutions of the equation, which is false because constants solve it when $g = 0$ and $h = 1$ . Equally trivializing would be to encode the supremum with a junk-valued sSup, so that unbounded return sets pass for solutions. Both are excluded: the class is part of each statement, and the equation is an IsLUB.

Theorem 6 of the chapter (the optimal inventory equation) is not part of this mission; it is treated in the inventory mission of the series. Welcome contributions include a reusable library for localized successive approximations and the equicontinuity lemmas that the continuity statements need.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010, Chapter IV. https://doi.org/10.2307/j.ctv1nxcw0f
S. Karlin, "The structure of dynamic programming models", Naval Research Logistics Quarterly 2 (1955), 285–294. https://doi.org/10.1002/nav.3800020408
D. P. Bertsekas and J. N. Tsitsiklis, "An analysis of stochastic shortest path problems", Mathematics of Operations Research 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$ . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$ , or is destroyed without mining anything with probability $1 - p_1$ . Bonanza has the corresponding data $p_2$ and $r_2$ . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$ -stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$ . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$ , yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$ , $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$ ), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$ , $\sum_k p_{ik} < 1$ , $0 \le c_{ik} \le 1$ , $c_{ik} + c'_{ik} = 1$ , equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$ , (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
Theorem 2: for $0 \le p_i < 1$ , $0 \le r_i \le 1$ , the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$ , the B-branch when the reverse inequality holds, and both on equality.
Theorem 3: the same rule for two mines with $K$ outcomes per use.
Theorem 5: for each $N$ , the $N$ -stage process has exactly two decision regions: a sector along the $x$ -axis where A is optimal and a sector along the $y$ -axis where B is optimal, separated by a ray through the origin.
Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$ .
Theorem 7: if $g$ solves (5.1) with an added term $h$ , then $|f - g| \le \max_R|h|/q$ on every rectangle $R$ , where $q = \min(1-p_1, 1-p_2)$ .

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$ -stage process is a word in $n$ letters whose number of candidates grows like $n^N$ . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$ , and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$ -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$ , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$ ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$ -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$ .

Choices made explicit:

Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$ , $0 \le r_i \le 1$ .
The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$ .

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming II: Fibonacci Search for the Maximum of a Unimodal FunctionTextbook

Motivation

Many optimization routines contain an inner step that maximizes a function of one variable whose values are expensive to compute: a line search inside a multivariate method, a tuning parameter chosen by simulation, a stage of a dynamic program in which each evaluation requires solving a subproblem. When the only structural information is that the function has a single peak, the natural question is how to place the evaluations so that the peak is pinned down as tightly as possible with a fixed budget. Richard Bellman's Dynamic Programming (1957) takes up this question in Chapter I, § 22, as an illustration of the functional-equation method, and answers it with the Fibonacci numbers.

Timeline.

1953. J. Kiefer, Sequential minimax search for a maximum (Proc. Amer. Math. Soc. 4, 502–506), proves that Fibonacci search is minimax optimal among sequential procedures for a unimodal function on an interval. doi:10.1090/S0002-9939-1953-0055639-3
1957. Bellman, Dynamic Programming, Chapter I, § 22 (pp. 34–36), recasts the result in the language of the principle of optimality: Theorem 11 for the continuous problem and Theorem 12 for its discrete version.

Setting

Let $L > 0$ . A function $f : [0, L] \to \mathbb R$ is strictly unimodal with maximum at $m \in [0, L]$ if $f$ is strictly increasing on $[0, m]$ and strictly decreasing on $[m, L]$ . No continuity is assumed, and the peak may sit at an endpoint. The point $m$ is then the unique maximizer of $f$ .

A search procedure is a finite decision tree. At each internal node it names a point $x$ at which $f$ is evaluated and moves to a subtree chosen by the observed value $f(x)$ ; at a leaf it announces a closed interval $[a, b]$ . The $k$ -th evaluation point may depend on all values seen so far, but on nothing else about $f$ . The cost of the procedure on $f$ is the number of evaluations along the path that $f$ determines.

The procedure locates the maximum on $[0, L]$ within unit length using at most $n$ values if, for every strictly unimodal $f$ on $[0, L]$ with maximum at $m$ , it evaluates $f$ at most $n$ times and announces $[a, b]$ with $b - a \le 1$ and $m \in [a, b]$ . Write $\mathcal L_n$ for the set of lengths $L > 0$ for which such a procedure exists, and following Bellman's Eq. (22.1),

F_n = \sup \mathcal L_n .

The book's Fibonacci numbers are $F_0 = F_1 = 1$ , $F_n = F_{n-1} + F_{n-2}$ for $n \ge 2$ (in Lean, bookFib).

In the discrete version, $f$ is defined on the points $0, 1, \dots, N-1$ , strictly increasing up to its maximizer $m$ and strictly decreasing after it. $K_n$ is the largest $N$ for which some procedure evaluates at most $n$ values and then names $m$ exactly, for every such $f$ .

Formalization targets

Goal: Chapter I, Theorem 11

\sup \mathcal L_n = F_n \qquad \text{for every } n \ge 0 .

The supremum is not attained once $n \ge 2$ (with two evaluations every length $2 - \varepsilon$ is searchable, the length $2$ is not), which is why the statement is about the supremum rather than a maximum.

Milestones

$\sup \mathcal L_1 = 1$ : one value carries no information (proof of Theorem 11, p. 34).
$\sup \mathcal L_2 = 2$ (p. 35).
Eq. (22.3): for $n \ge 2$ every $L \in \mathcal L_n$ satisfies $L < F_{n-1} + F_{n-2}$ .
For $n \ge 2$ every $0 < L < F_{n-1} + F_{n-2}$ lies in $\mathcal L_n$ (p. 36).
Eq. (22.4): $F_{20} > 10{,}000$ , hence for every $L > 0$ twenty evaluations locate the maximum within an interval of length $10^{-4} L$ .
Eqs. (22.5)–(22.6): with $r_{1,2} = (1 \pm \sqrt5)/2$ ,

F_n = \frac{r_2 - 1}{r_2 - r_1} r_1^{\,n} + \frac{1 - r_1}{r_2 - r_1} r_2^{\,n}, \qquad \frac{F_{n+1}}{F_n} \to r_1 .

Theorem 12, corrected: $K_0 = K_1 = 1$ , $K_2 = 2$ , $K_3 = 4$ , and

K_n = F_{n+1} - 1 \qquad (n \ge 3).

Significance

The result. Theorem 11 is an exact minimax statement: $n$ evaluations shrink the interval of uncertainty for the peak of a unimodal function by a factor of at most $F_n \approx r_1^{\,n}/\sqrt5$ , and no adaptive rule, however clever, does better. It certifies Fibonacci search as optimal and golden-section search as asymptotically optimal, which is the reason these methods are the default line searches when derivatives are unavailable. Eq. (22.4) quantifies the rate: twenty evaluations give four decimal digits.

Formalizing it. The theorem has been proved since 1953; the work here is a machine-checked proof of the full minimax statement over all adaptive procedures, including the lower bound. That half is a statement about every decision tree and requires an adversary argument, which is exactly the kind of reasoning that is informal in the book and easy to get wrong. The discrete Theorem 12 is misprinted in the book (see below), so a formal proof also settles the correct values. We are not aware of an existing formalization of the optimality of Fibonacci search in Lean or another proof assistant. The Binet formula and the ratio limit are in Mathlib for Mathlib's indexing (Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop); milestone 6 only transfers them to the book's indexing.

Difficulty

The upper bound $L < F_{n-1} + F_{n-2}$ must hold for every procedure, not only for procedures that follow the "compare two points, discard a piece, keep the surviving point" pattern of the book's figures. A procedure may place its second point depending on the first value, may re-evaluate points, may evaluate outside $[0, L]$ , and may branch on the exact values rather than on their order. The book's argument tacitly restricts to that pattern, so the lower bound has to be established for arbitrary trees, where the information carried by exact values, repeated or wasted evaluations and branch-dependent placements all have to be accounted for. The bookkeeping is delicate because the surviving sets are half-open or open intervals, and whether the endpoints are included decides that the supremum is not attained.

The naive attempt of proving a bound only for "one new point per step inside the current bracket" procedures does not prove the goal: the goal quantifies over all decision trees.

Formalization scope

Model fixed. Deterministic adaptive procedures (decision trees branching on the exact real value observed), exact function values, cost equal to the number of evaluations; this is one of the models that Bellman's footnote 8 alludes to ("It is actually not easy to specify precisely what we mean by an optimal search procedure"). Functions are ℝ → ℝ, constrained only on $[0, L]$ ; evaluations outside $[0, L]$ are allowed and useless.
Output. A closed interval $[a, b]$ with $a \le b$ , $b - a \le 1$ containing the maximizer. It need not lie inside $[0, L]$ or have length exactly one; for $L \ge 1$ this is equivalent to Bellman's "sub-interval of unit length".
Indexing. The book's $F_n$ is a separate definition bookFib with $F_0 = F_1 = 1$ ; in Mathlib's indexing $F_n$ is Nat.fib (n + 1). The goal is stated for every $n \ge 0$ ; the book calls $F_0$ a convention, and in this model $\sup \mathcal L_0 = 1$ agrees with it.
Sup, not max. Theorem 11 is stated with IsLUB, never as "a procedure exists for $L = F_n$ ", which is false for $n \ge 2$ . Theorem 12 is stated with IsGreatest, which asserts that the maximum exists.
Implicit ranges. Eq. (22.3) is stated unconditionally for all $n \ge 2$ (the book proves it under the induction hypothesis). "Within $10^{-4}$ of the original interval length" is read as an interval of length at most $10^{-4} L$ .
Misprint corrected. Theorem 12 prints $K_n = 1 + F_n$ for $n \ge 3$ . On seven points, four evaluations suffice: evaluate points 3 and 5; if $f(3) > f(5)$ the peak is among points 1–4 with $f(3)$ known, and evaluating point 2 and then point 1 or 4 finds it; the case $f(5) > f(3)$ is symmetric, and $f(3) = f(5)$ forces the peak at point 4. So $K_4 \ge 7 > 6 = 1 + F_4$ . The mission states $K_n = F_{n+1} - 1$ for $n \ge 3$ , which agrees with the printed $K_3 = 4$ and keeps all printed initial values. The printed text is kept verbatim in the milestone.
Ruling out trivializations. The procedure never sees $f$ except through the values it requests, and it must succeed for every strictly unimodal $f$ with one fixed tree; "some interval of length one contains the maximizer" with no procedure, or a procedure allowed to depend on $f$ , would make the problem trivial and is not what is stated.
Contributions welcome. A reusable decision-tree framework for query-complexity lower bounds, lemmas about which finite sets of observed values are consistent with a strictly unimodal function, and the Fibonacci search tree itself as a construction.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter I, § 22, pp. 34–36. doi:10.2307/j.ctv1nxcw0f
J. Kiefer, Sequential minimax search for a maximum, Proceedings of the American Mathematical Society 4 (1953), 502–506. doi:10.1090/S0002-9939-1953-0055639-3

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming I: Existence and Uniqueness for the Multi-Stage Allocation EquationTextbook

Motivation

Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.

When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.

Setting

A quantity $x \ge 0$ is split into $y \in [0,x]$ , assigned to a first activity with return $g(y)$ , and $x - y$ , assigned to a second activity with return $h(x-y)$ . After the stage the first allocation has been reduced to $ay$ and the second to $b(x-y)$ , and the process continues with the quantity $ay + b(x-y)$ . Writing

T(f,y) = g(y) + h(x-y) + f\big(ay + b(x-y)\big),

the total return $f(x)$ of the infinite process satisfies the allocation equation (Bellman's (8.1))

f(x) = \max_{0 \le y \le x} T(f,y), \qquad x \ge 0.

The standing hypotheses of Chapter I, Theorem 1 are:

$g$ and $h$ are continuous on $[0,\infty)$ and $g(0) = h(0) = 0$ ;
with $m(x) = \max_{0 \le y \le x} \max(|g(y)|, |h(y)|)$ and $c = \max(a,b)$ , the series $\sum_{n=0}^\infty m(c^n x)$ converges for every $x \ge 0$ ;
$0 \le a < 1$ and $0 \le b < 1$ .

The successive approximations from an initial function $f_0$ are $f_{N+1}(x) = \max_{0 \le y \le x} T(f_N, y)$ . A policy is a function $y_0(x)$ with $0 \le y_0(x) \le x$ ; its return is the total of the stage returns obtained by using $y_0$ at every stage.

In Lean all objects live in the namespace BellmanDP.Allocation: allocT is $T$ , allocM is $m$ , AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence $f_N$ , and policyReturn is the return of a policy.

Formalization targets

Goal: Chapter I, Theorem 1

Under the three hypotheses, there is a function $f$ with

f(x) = \max_{0 \le y \le x}\big[g(y) + h(x-y) + f(ay + b(x-y))\big] \quad (x \ge 0), \qquad f(0) = 0,\ f \text{ continuous at } 0,

this $f$ is continuous on $[0,\infty)$ , and every solution continuous at $0$ with value $0$ there coincides with $f$ on $[0,\infty)$ .

Milestones

Theorem 2 — from any $f_0$ continuous on $[0,\infty)$ with $f_0(0) = 0$ , the successive approximations converge to $f$ uniformly on every finite interval.
Theorem 3 — started from the return of a continuous policy, the successive approximations increase monotonically and converge to $f$ uniformly on every finite interval.
Lemma 1 — if $G(x,y)$ is jointly concave on $x,y \ge 0$ , then $x \mapsto \max_{0 \le y \le x} G(x,y)$ is concave.
Theorem 4 — if $g$ and $h$ are convex, $f$ is convex and for each $x$ the maximum is attained at $y = 0$ or $y = x$ .
Theorem 5 — if $g$ and $h$ are strictly concave, $f$ is strictly concave and the maximizing $y$ is unique for every $x$ .
Theorem 9 — for the general equation $f(x) = \max_{0\le y\le x}[u(x,y) + f(ay+b(x-y))]$ , the continuous solutions for returns $u$ and $v$ satisfy $|f(x) - F(x)| \le \sum_{n \ge 0} D(c^n x)$ , where $D(z)$ is the maximum of $|u - v|$ over $0 \le y \le x \le z$ .

Significance

Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at $0$ uniqueness fails: when $g = h = 0$ , every constant function and the indicator of $(0,\infty)$ solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.

These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form $f(x) = \max_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with a contracting transition $\tau$ .

Difficulty

The equation is not a contraction in the supremum norm on $[0,\infty)$ : $g$ and $h$ may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, $ay + b(x-y) \le cx$ , which propagates a local estimate near $0$ out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at $0$ alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative $g,h$ gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter any hypothesis or conclusion. Continuity at $0$ is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on $[0,\infty)$ .
The maximum in the equation is encoded as IsGreatest of $\{T(f,y) : 0 \le y \le x\}$ , so a solution attains its maximum at every $x \ge 0$ . The maxima inside definitions ( $m$ , $f_{N+1}$ , the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.
The later theorems refer to "the solution" of Theorem 1 by quantifying over solutions that are continuous at $0$ and vanish there; they never quantify over arbitrary solutions of the equation, for which the conclusions are false.
Theorem 3's "converges uniformly" is stated uniformly on every finite interval $[0,R]$ , the sense in which Theorem 2 and the series (11.10) used in its proof converge. Its initial function is defined explicitly as the series of stage returns along the trajectory of the policy.
Theorem 4's " $y$ will equal $0$ or $x$ " is stated as: an endpoint is a maximizer. It does not say every maximizer is an endpoint, which fails for $g = h = 0$ .
Each theorem carries its own parameter range as printed: $0 \le a, b < 1$ for Theorems 1–5, $0 < a, b < 1$ for Theorem 9.
Not included: Theorem 6 (the policy structure under strict concavity, which uses $f'$ without a hypothesis making $f$ differentiable), Theorems 7 and 8 (explicit solutions), Theorem 10 (the multi-dimensional process), and Theorems 11–12 on Fibonacci search, which form a separate mission.

Welcome contributions: a general existence-and-uniqueness theorem for equations $f(x) = \sup_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with $\|\tau(x,y)\| \le c\|x\|$ , and a lemma that parametric maxima over $[0,x]$ of continuous functions are continuous in $x$ .

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. https://doi.org/10.2307/j.ctv1nxcw0f — Chapter I, §§ 8–14 and 18, pp. 11–29.
R. Bellman, "On the theory of dynamic programming", Proceedings of the National Academy of Sciences 38 (1952), 716–719. https://doi.org/10.1073/pnas.38.8.716

10 thms2 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VII: The (BOR) Assumptions and Positive Recurrence of Optimal PoliciesTextbook

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.

15 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VI: The (SEN) Assumptions and the Average Cost Optimality InequalityTextbook

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

12 thms2 active usersReviewed

Completed

Dynamical Systems Optimization·Captain: Lucas

Lindgren 2022: Dynamic-Programming Price Adjustment and Lyapunov StabilityResearch Paper

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$ , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$ , and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$ . Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$ ; the aggregate expenditure is

E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,

whose value function is $J(t,p)$ . The Hamiltonian (eq. (8)) is

H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$ , and the HJB equation (eq. (10)) reads

\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$ . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$ .

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$ , then on any interval $[t,T]$ on which

E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$ , it is strictly positive on $[t,T)$ .

Milestones

Eq. (4): under the normalization $\langle p,p\rangle=1$ , $\langle p,\dot p\rangle=0$ .
Eq. (9): for $m>0$ , $v$ minimizes $H$ if and only if $mv=-\nabla J$ .
Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .

Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$ .
Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$ .

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$ , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$ , $J=ap^2+cs$ , $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

8 thms2 active usersReviewed

Dynamic Programming

Missions

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 4: Under Sennott's Conditions an Average-Cost Optimal Stationary Policy ExistsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.9

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimality of Affine Policies in Multistage Robust Optimization: In One-Dimensional Constrained Min-Max Control, Disturbance-Affine Policies with Affine Stage Costs Attain the Optimal ValueResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Control of Markov Processes with Incomplete State Information 1: Reduction to Complete State Information on the Conditional State Distributions, with the Same Optimal LawResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 6: A Canonical Policy Is Strong Average Optimal and Its Average Cost Is the Optimal OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.3 (i)–(iii)

Steps toward the goal

Further targets: Theorem 6.3 (v)–(vi)

Significance

Difficulty

Formalization scope

Selected references

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 1: Uniformly Bounded Differential Discounted Values Give a Bounded Solution of the Average Cost Optimality EquationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2 (p. 301)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 10.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case VII: The Finite-Horizon Borel Model — over Universally Measurable Policies J*_K = T^K(J_0)Textbook

Motivation

Setting

Formalization targets

Goal: Proposition 8.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case IV: The Generalized Abstract Model — Restricted Policy Classes under ContractionTextbook

Why restricted policy classes

Setting

Formalization targets

Goal: Proposition 6.4 (p. 97)

Milestones

Further results of the chapter