Operations Research

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

• Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
• Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
• Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$. The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$:

• $\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
• $v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
• $x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$, where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$.

Costs are a fixed order cost $K$, proportional order and shipment rates $c^d$ and $c^r$, a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$. After the paper's accounting transformation, the one-period cost is

$$c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),$$

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$, $D(v) = h^d v$, and, at $\alpha = 1$,

$$R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,$$

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$. The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$, $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH$^d$ has states $(\tilde y, v^d)$, orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$. Its minimal average cost is $a^d$. The outlet problem has states $x^r$, shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$. The policy $\pi^*$ orders by an optimal stationary policy of IH$^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$: up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$, the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$,

$$B(s \mid \pi^*) \le B(s \mid \pi).$$

Milestones

• Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$.
• Eq. (4) (p. 823), for $0 \le \alpha \le 1$: $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$.
• §3 claims (p. 828): with $c^r = 0$, $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$, $\hat P_n = P$, $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$.
• §3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$.
• Lemma 5 (p. 828): $B(s \mid \pi^*) = a$.
• Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$.

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$-type problem for the depot with a known convex penalty $P$, and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

• the class of measurable history-dependent policies;
• the expected costs of policies with unbounded one-period costs;
• the passage from history-dependent to Markov policies;
• the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$-convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

• value iteration for the whole system, divided by $n$, converges to $a^d + a^r$, which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$;
• the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
• $\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$, where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

• Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$. For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
• Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
• Standing assumptions (p. 821):
  • $K, h^d, h^r, p^r > 0$;
  • demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
• Added hypotheses.
  • States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$.
  • $c^d = c^r = 0$. The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$. The general-cost version is the paper's informal reduction and is not part of the goal.
  • Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$, which the paper names on p. 827; it holds automatically at $\alpha = 1$.
• Ruling out trivial readings.
  • $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH$^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
  • The goal quantifies over all measurable feasible policies, and $\pi^*$'s own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
  • A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$, including the existence of $x^{r*}$.
• Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$.

Selected references

• 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
• 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
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
• E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

The multi-secretary problem is the basic model of selecting under a budget from a stream of offers. Hiring a fixed number of candidates, accepting a fixed number of requests for a perishable resource, and admitting customers into a capacity-limited service all have this structure. Each item must be accepted or rejected on arrival, and the comparison point is the offline decision maker, who sees the whole sequence and keeps the best $k$ items. The gap between the two expected values is the regret.

A common class of heuristics in revenue management and online resource allocation does not react to the realised history. These policies fix in advance, period by period, a probability of accepting each type of item, and then follow it until the budget runs out; static bid-price and randomised-acceptance rules are of this kind (Talluri and van Ryzin 2004). Arlotto and Gurvich (arXiv:1710.07719v2, Theorem 1) show that when abilities take finitely many values, an adaptive policy has regret bounded uniformly in the horizon $n$ and the budget $k$. Their Theorem 3 shows that the restriction to non-adaptive policies costs order $\sqrt n$ over a wide range of budgets. Read together, these two results separate adaptive from non-adaptive control by an unbounded factor. This mission formalizes the non-adaptive half.

Setting

There are $n$ candidates with abilities $X_1,\dots,X_n$, independent and identically distributed on $m$ values $0<a_m<a_{m-1}<\dots<a_1$, with masses $f_j=\mathbb P(X_1=a_j)>0$ and $\sum_jf_j=1$. Write $\epsilon=\tfrac12\min_jf_j$ and $\bar F(a_j)=f_1+\dots+f_{j-1}$. The budget is $k$, with $0\le k\le n$.

The offline value is

$$V^*_{\mathrm{off}}(n,k)=\mathbb E\Big[\max\Big\{\textstyle\sum_tX_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\Big\}\Big].$$

A non-adaptive policy is a matrix $\pi=\{p_{j,t}\in[0,1]\}$. At time $t$, if budget remains and $X_t=a_j$, the candidate is selected with probability $p_{j,t}$, independently of everything else. The selection coins $B_t$ are then independent Bernoulli variables with $q_t=\mathbb E[B_t]=\sum_jp_{j,t}f_j$. The policy selects until $k$ coins have come up. Its value $V^\pi_{\mathrm{on}}(n,k)$ is the expected total ability selected, and

$$V^*_{\mathrm{na}}(n,k)=\sup_{\pi}V^\pi_{\mathrm{on}}(n,k).$$

The deterministic relaxation replaces the random counts $Z^n_j=\#\{t:X_t=a_j\}$ by their means. Its value is

$$DR(n,k)=\max\Big\{\textstyle\sum_ja_js_j:0\le s_j\le nf_j,\ \sum_js_j\le k\Big\},$$

with solution $s^*_j=\min\{nf_j,(k-n\bar F(a_j))_+\}$. The index policy takes its probabilities from $s^*$: $p_{j,t}=s^*_j/(nf_j)$.

Formalization targets

Goal: Theorem 3 (p. 25)

For every $\epsilon>0$, $m$ and $a$ there is $M=M(\epsilon,m,a)>0$ such that, for all masses with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)$ with $(f_1+\epsilon)n\le k\le(1-f_m-\epsilon)n$,

$$M\sqrt n\le V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{na}}(n,k).$$

The constant does not depend on the masses beyond $\epsilon$, nor on $n$ or $k$.

Milestones

• Lemma 2 (p. 8): binomial overshoot, $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ when $k$ exceeds the mean by $\varepsilon n$, and the symmetric bound.
• Remark 2 (pp. 10–11): $s^*$ solves the relaxation, and $V^*_{\mathrm{off}}\le DR$.
• Lemma 3 (p. 25): the index policy satisfies $DR-V^{\mathrm{id}}_{\mathrm{na}}\le\varepsilon^{-1}a_1\sqrt n$ when $k/n\ge\varepsilon$, so the order $\sqrt n$ is attained.
• Lemma 5 (p. 26): for a centred Bernoulli sum with variance $\varsigma^2$, $\mathbb E[(\pm N-\Upsilon\varsigma)_+]\ge\beta_1\varsigma-(2+3\sqrt2)$ with $\beta_1(\Upsilon)>0$, and $\mathbb E[(N+\Upsilon\varsigma)_+^2]\le\beta_2\varsigma^2$.
• Lemma 7 (p. 27): an optimal non-adaptive policy exists, and any optimal one has $f_1/2\le q_t\le1-f_m/2$ outside $2M\sqrt n$ periods, so $\sum_tq_t(1-q_t)\ge\tfrac{f_1f_m}4(n-2M\sqrt n)$.
• Lemma 4 (p. 25): for $k\le n(f_1-\epsilon)$ the non-adaptive regret is at most $a_2/(4\epsilon)$.
• Lemma 8 and Proposition 6 (p. 40): $\mathbb E[\mathfrak S^n_j]=s^*_j\pm M\sqrt n$, and $0\le DR-V^*_{\mathrm{off}}\le M\sqrt n$ in general and $\le a_1m/(4\epsilon')$ when $k/n$ is $\epsilon'$ away from the jump points of $\bar F$.

Significance

Theorem 3 is the lower half of the separation in Theorem 1 of the paper. The Budget-Ratio policy and the dynamic-programming policy have regret $O(1)$, uniformly in $(n,k)$, while every non-adaptive policy has regret $\Omega(\sqrt n)$ when $k/n$ lies strictly between $f_1$ and $1-f_m$. The order $\sqrt n$ of fluid and static randomised policies is therefore a property of the whole class, not of a poor choice inside it. Lemma 4 shows that the budget range cannot be removed: with a small budget a non-adaptive policy is as good as any.

The result is proved in the source but has not been machine-checked. A complete development would formalize, inside one finite probabilistic model: the binomial overshoot bound, a uniform anti-concentration estimate for Bernoulli sums, the structure of optimal non-adaptive policies, and the comparison with the offline sort. The source's proof of Theorem 3 also relies on a lemma that fails as printed (see Formalization scope), so a formal proof would close a real gap in the published argument.

Difficulty

The upper bound of order $\sqrt n$ (Lemma 3) follows from a variance computation. The lower bound must hold for every non-adaptive policy, including time-varying ones, and the obvious argument does not cover them. That argument compares a policy with the index policy and shows the index policy loses $\sqrt n$. A policy can, however, differ from the index policy by order $\sqrt n$ in its expected selection counts and still have regret of the same order. The step "small regret forces $s_j(\pi)\approx s^*_j$", which the source uses, is exactly the step that fails.

What has to be shown is that the selection count $\sum_tB_t$ of an optimal policy fluctuates by order $\sqrt n$, uniformly in the policy. A policy that runs out of budget early then misses top-value candidates late in the horizon, and one that keeps budget wastes slots. Both effects must be bounded below by a multiple of $\sqrt n$ that is uniform over all masses with the same $\epsilon$. Lemma 5 needs a normal approximation with an explicit, $q$-independent error. Lemma 7 needs the existence of an optimal policy, which is a maximisation over a continuum of matrices.

Formalization scope

The source is the arXiv preprint arXiv:1710.07719v2 (1 June 2018). Its printed page numbers equal the PDF page numbers.

• Indices. The value and mass vectors are a f : Fin m → ℝ. Lean index $j$ is the paper's index $j+1$, so a 0 $=a_1$ is the largest value and f (Fin.rev 0) $=f_m$ is the mass of the smallest. The standing assumptions of Sec. 2 are IsValues a (strictly decreasing, positive) and IsMasses f (positive, summing to one).
• Expectations. All expectations are finite sums over outcome sequences. For the offline problem these are $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ with weight $\prod_tf_{x_t}$. For a non-adaptive policy they are pairs $(X_t,B_t)$ with weight $\prod_tf_{x_t}\,p_{x_t,t}^{b_t}(1-p_{x_t,t})^{1-b_t}$. No measure theory is used.
• Selection rule. A candidate is selected iff its coin is $1$ and fewer than $k$ earlier coins were $1$. This equals the paper's "up to the stopping time $\nu$" for $k\ge1$. At $k=0$ the printed $\nu=1$ would allow a selection without budget, and the feasible rule is used.
• Suprema. $V^*_{\mathrm{na}}$ is a supremum over all matrices with entries in $[0,1]$, not over $0/1$ matrices or the index policy alone. $DR$ is the supremum of its linear program; it is not defined by the formula $\sum_ja_js^*_j$, which is a milestone.
• Index policy. $j_{\mathrm{id}}$ is the largest index with $\bar F(a_{j_{\mathrm{id}}})\le k/n$. As printed the defining inequality has no solution at $k=n$.
• Constants. Each constant is quantified after $(\epsilon,m,a)$ and before $(f,n,k)$. The goal's $M$ and Lemma 5's $\beta_1$ are strictly positive; with $M=0$ the goal would reduce to $V^*_{\mathrm{na}}\le V^*_{\mathrm{off}}$. Theorem 3 is posed for all $n$ in the range, as printed, without a threshold on $n$. Lemma 2 is stated in the multiplied form $(p+\varepsilon)n\le k$ of its proof. Lemma 4 adds $m\ge2$, so that $a_2$ exists.
• Disclosed gaps in the source. The source's proof of Theorem 3 relies on a lemma that fails as printed (Lemma 6, p. 26), so Lemma 6 is not part of this mission. The statement of Theorem 3 is posed as in the source. The printed argument for the second inequality of Lemma 7's (36) does not go through, and a corrected one also uses $a_{m-1}$. Lemma 7's constant is therefore quantified after all of $a$.

Contributions of any kind are welcome. Reusable pieces include binomial overshoot bounds, anti-concentration for sums of independent Bernoulli variables (for example via a Wasserstein normal approximation, which Mathlib lacks), and compactness arguments for optimal randomised policies.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719v2
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• N. Ross, Fundamentals of Stein's method, Probability Surveys 8, 2011. https://doi.org/10.1214/11-PS182
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

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

1. 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)]$.
2. Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$.
3. Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$.
4. Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
5. Proposition 10.4: $\varepsilon$-optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$.
6. 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

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$, the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$, by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$. For a state $j$, $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$, transient if $f_{jj} < 1$ for every $j$, and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$: $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$,

$$[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},$$

that is $p_{i0} = \alpha_i$, $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ for $j > i+1$. In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

$$\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],$$

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

$$\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .$$

Together: ergodic for $\rho < 1$, recurrent-null for $\rho = 1$, transient for $\rho > 1$. The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

1. Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$, the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$.
2. Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
3. Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$.
4. Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ($i \ne 0$) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$, and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

• The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
• States are indexed from $0$, as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$), so the statement is not vacuous.
• $\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$: an infinite mean gives $\rho = 0$, and that chain is ergodic.
• The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$. Milestones 2–4 carry them, as the paper's standing assumptions (§1).
• Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$.
• Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
• Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$, and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
• D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

Motivation

Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.

Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).

Timeline:

• 1965: Blackwell, discounted dynamic programming on Borel spaces with Borel-measurable data, case (D).
• 1966: Strauch, negative dynamic programming, case (N), with Borel-measurable data.
• 1978: Bertsekas and Shreve, Chapter 9: lower semianalytic costs and universally measurable policies, in all three cases (P), (N), (D).
• 1979: Shreve and Bertsekas, the journal account of universally measurable policies.

Setting

An infinite horizon stochastic optimal control model (SM) is an eight-tuple $(S, C, U, W, p, f, \alpha, g)$. The state space $S$, the control space $C$ and the disturbance space $W$ are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint $U$ assigns to each state $x$ a nonempty set $U(x) \subseteq C$, and the set $\Gamma = \{(x,u) \mid u \in U(x)\}$ is analytic. The disturbance kernel $p(dw \mid x, u)$ is a Borel stochastic kernel and the system function $f : SCW \to S$ is Borel. The discount factor is $\alpha > 0$, and the one-stage cost $g : \Gamma \to [-\infty, \infty]$ is lower semianalytic: each sublevel set $\{g < c\}$ is analytic. The state moves by $x_{k+1} = f(x_k, u_k, w_k)$, with transition kernel $t(B \mid x, u) = p(\{w \mid f(x,u,w) \in B\} \mid x, u)$.

A policy $\pi = (\mu_0, \mu_1, \dots)$ chooses $u_k$ at random from a universally measurable stochastic kernel $\mu_k(du_k \mid x_0, u_0, \dots, x_k)$ concentrated on $U(x_k)$; $\Pi'$ is the set of all policies. A policy is Markov if each $\mu_k$ depends only on $x_k$, and it is stationary if, moreover, $\mu_k = \mu$ for all $k$. Writing $q_k(\pi, p_x)$ for the law of $(x_k, u_k)$ started from $x_0 = x$, the cost of $\pi$ and the optimal cost are

$$J_\pi(x) = \sum_{k=0}^\infty \alpha^k \int g\, dq_k(\pi, p_x), \qquad J^*(x) = \inf_{\pi \in \Pi'} J_\pi(x).$$

For $J : S \to [-\infty, \infty]$, the dynamic programming operators are

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

The three cases are (P) $g \ge 0$ on $\Gamma$; (N) $g \le 0$ on $\Gamma$; (D) $\alpha < 1$ and $|g| \le b$ on $\Gamma$ for some real $b$.

Formalization targets

Goal: the optimality equation (Proposition 9.8, Eq. (22))

Under each of (P), (N) and (D),

$$J^* = T(J^*).$$

Milestones

• $J^*$ is lower semianalytic (Corollary 9.4.1).
• For a stationary policy, $J_\mu = T_\mu(J_\mu)$ (Proposition 9.9).
• Optimality tests for stationary policies: under (P) or (D), $(\mu, \mu, \dots)$ is optimal iff $J^* = T_\mu(J^*)$ (Proposition 9.12); under (N) or (D), iff $J_\mu = T(J_\mu)$ (Proposition 9.13).
• Under (N) or (D), value iteration from $0$ converges to $J^*$, and under (D) it converges uniformly from every bounded lower semianalytic start (Proposition 9.14).

Further statements of the mission

• Markov policies suffice: at each state some Markov policy matches any policy's cost (Proposition 9.1), so $J^* = \inf_{\pi \in \Pi} J_\pi$ (Corollary 9.1.1).
• Partial converses of the optimality equation: $J \ge T(J)$, $J \ge 0$ gives $J \ge J^*$ under (P); $J \le T(J)$, $J \le 0$ gives $J \le J^*$ under (N); a bounded solution of $J = T(J)$ equals $J^*$ under (D) (Proposition 9.10). The analogous statements for $T_\mu$ and $J_\mu$ (Proposition 9.11).

Significance

The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for $\varepsilon$-optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.

All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.

Difficulty

Under (D), $T$ is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals $J^*$ requires knowing that $J^*$ belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: $\lim_k J_k(0) = 0$ while $J^*(0) = \infty$). Even when each $J_k$ is Borel, $J^*$ may fail to be (Example 2). So $J^* = T(J^*)$ cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines $T$.

The book's route lifts (SM) to a deterministic model on the space of probability measures $P(S)$, where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.

Formalization scope

The draft fixes the following conventions.

• Spaces. Borel spaces are topological spaces homeomorphic to Borel subsets of complete separable metric spaces, carrying their Borel $\sigma$-algebras. Analytic sets are Mathlib's AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.
• Extended reals. Values lie in EReal. The book's convention $\infty - \infty = -\infty + \infty = \infty$ is implemented explicitly, because Mathlib's EReal sets $\bot + \top = \bot$. The integral of an extended-real function is $\int f^+ - \int f^-$ with the same convention.
• Policies. These are sequences of universally measurable stochastic kernels on the history spaces $S_0C_0 \cdots S_k$, charging $U(x_k)$ with mass one. The laws of $(x_0, u_0, \dots, x_k, u_k)$ are built recursively from the kernels.
• Costs. $J_\pi$ is the series $\sum_k \alpha^k \int g\, dq_k$, computed as the difference of the series of positive and negative parts. Under each of (P), (N), (D) it coincides with the integral of the total discounted cost. $J^*$ is the infimum over all policies.
• Case labels. Each statement carries the case labels the book attaches to it, as hypotheses on the model.
• Scope. Only the (SM) statements are formalized. The deterministic model (DM) on $P(S)$ is the book's proof device and enters no statement.

The goal admits a trivializing formalization that this draft rules out. $J^*$ is not defined as a fixed point of $T$, nor as the limit of $T^k(0)$; it is the infimum of the costs of all policies, which under (P) can differ from that limit.

A complete development needs universally measurable kernels and their compositions on product spaces, measurability of $x \mapsto \int f(x, y)\, q(dy \mid x)$ for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996. Chapter 9. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

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