Probability

Motivation

Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers $n$ grows while the offered load stays within $O(\sqrt n)$ of $n$. Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).

Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for $k$ customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.

Context:

• Harrison & Zeevi (2004) studied the same multi-class many-server problem.
• Bell & Williams (2001) proved asymptotic optimality of a threshold policy for a two-server system in conventional heavy traffic.
• The present paper is the first to cover the QED regime with general costs and abandonment.

Setting

There are $k\ge1$ customer classes and $n$ identical servers.

Primitives.

• Arrivals. Class-$i$ customers arrive according to a renewal process $A^n_i$ with interarrival times $\check U_i(j)/\lambda^n_i$. Here the $\check U_i(j)$ are i.i.d., positive, of mean one and squared coefficient of variation $C^2_{U,i}$.
• Service. Service times are exponential with rate $\mu^n_i$, represented by Poisson processes $S^n_i$.
• Abandonment. Waiting customers abandon at rate $\theta^n_i\ge0$, represented by Poisson processes $R^n_i$.

State. $X^n_i(t)$ is the number of class-$i$ customers in the system, $\Psi^n_i(t)$ the number in service and $\Phi^n_i=X^n_i-\Psi^n_i$ the number waiting. The dynamics are

$$X^n_i(t)=X^{0,n}_i+A^n_i(t)-R^n_i\Big(\int_0^t\Phi^n_i\Big)-S^n_i\Big(\int_0^t\Psi^n_i\Big),\qquad \Psi^n,\Phi^n\in\mathbb Z^k_+,\quad \textstyle\sum_i\Psi^n_i\le n .$$

Policies.

• A scheduling control policy (SCP) is the process $\Psi^n$.
• It is admissible if it does not anticipate the future beyond the time of the next arrival: past information is independent of future primitive increments.
• It is work-conserving if no server idles while customers wait: $(\mathbb 1\cdot X^n-n)^+=\mathbb 1\cdot\Phi^n$.

Scaling and cost. In the QED scaling $n^{-1}\lambda^n_i\to\lambda_i$ with $\sum_i\lambda_i/\mu_i=1$. With $\rho_i=\lambda_i/\mu_i$ the centred processes are $\hat X^n=n^{-1/2}(X^n-\rho n)$, $\hat\Phi^n=n^{-1/2}\Phi^n$ and $\hat\Psi^n=n^{-1/2}(\Psi^n-\rho n)$. The cost is

$$C^n=E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n(t),\hat\Psi^n(t))\,dt .$$

The limiting control problem. It controls

$$X(t)=x+rW(t)+\int_0^t b(X(s),u(s))\,ds,\qquad b(x,u)=\ell+(\mu-\theta)(\mathbb 1\cdot x)^+u-\mu x,$$

where the control $u$ takes values in the simplex $\mathbb S^k$ and $W$ is a $k$-dimensional Brownian motion. The data are $r_i=(\lambda_iC^2_{U,i}+\lambda_i)^{1/2}$ and $\ell_i=\hat\lambda_i-\rho_i\hat\mu_i$. Its value $V(x)$ is the infimum of $E\int_0^\infty e^{-\gamma t}L(X,u)\,dt$, with $L(x,u)=\tilde L((\mathbb 1\cdot x)^+u,x-(\mathbb 1\cdot x)^+u)$.

HJB equation and the proposed policy. The HJB equation is $\tfrac12\sum_ir_i^2\partial_{ii}f+H(x,Df)-\gamma f=0$ with $H(x,p)=\inf_{u\in\mathbb S^k}[b(x,u)\cdot p+L(x,u)]$. Let $h$ be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to $\Theta[(\mathbb 1\cdot X^n-n)^+h(\hat X^n)]$, an integer rounding, and falls back to a static priority rule when that is infeasible.

Formalization targets

Goal: Theorem 2(i)

For a $C^2_{\mathrm{pol}}$ solution $f$ of the HJB equation, a measurable minimizer selection $h$, and initial states with $\hat X^{0,n}\to x$:

$$\lim_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^{n,*}_t,\hat\Psi^{n,*}_t)\,dt\;\le\;\liminf_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n_t,\hat\Psi^n_t)\,dt$$

This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.

Milestones

The milestones follow the proof:

• on the diffusion side, Proposition 2 (well-posedness), Proposition 4 (stability and moment bounds), Proposition 5(i)–(ii) (growth and continuity of $V$) and Theorem 3 ($V$ is the unique $C^2_{\mathrm{pol}}$ HJB solution, and an optimal Markov policy exists);
• on the queueing side, Proposition 1 (feedback rules give admissible SCPs), Lemmas 2–3 (moment bounds), Lemma 4(i)–(ii) (FCLT for the primitives and the fluid limit $(\bar\Psi^n,\bar\Phi^n)\Rightarrow(\rho,0)$), and Theorem 4(i)–(ii): $\liminf\ge V(x)$ always, and $\limsup\le V(x)$ under condition (49).

Significance

The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given $h$, and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with $V(x)$.

Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:

• a counting-process model of the queue;
• a careful definition of non-anticipation;
• a pathwise controlled SDE;
• classical solvability of a semilinear elliptic HJB equation on $\mathbb R^k$;
• a weak-convergence argument in Skorokhod space.

Each of these is reusable well beyond this paper.

Difficulty

The obvious argument would show that $\hat X^n$ converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:

• the comparison class contains arbitrary non-Markov, history-dependent policies, so the queue does not converge to a single controlled diffusion;
• the optimal selector $h$ is in general discontinuous (for linear costs it is), so the proposed policy is not a continuous function of the state.

The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:

• uniform moment bounds;
• tightness of the integral processes;
• the convergence of stochastic integrals of Kurtz and Protter;
• and, for the proposed policy, the fact that the rounding $\Theta$ and the priority fallback perturb the minimizer by $O(n^{-1/2})$.

Existence of a classical HJB solution on all of $\mathbb R^k$, with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.

Formalization scope

The Lean development commits to the following conventions.

• Indexing and norms. Classes are Fin k with $k\ge1$; paper class $i$ is index $i-1$, so "class $k$" (highest priority, rounding remainder of $\Theta$) is the last index. Vectors are Fin k → ℝ and $\|\cdot\|$ is the paper's $\ell^1$ norm; the paper's $|\cdot|$ on vectors is read the same way.
• Probability space and paths. All systems share one complete probability space. Time is real and every condition is for $t\ge0$. The paper's "without loss" path regularity (finite arrival counts, Poisson paths $\mathbb Z_+$-valued, nondecreasing and càdlàg) holds for every $\omega$.
• Poisson processes are defined by independent Poisson increments; rate $0$ gives the zero process.
• Policies. A policy is a pair of real processes $(\Psi^n,X^n)$ with integer values. Admissibility is Definition 2 verbatim, with the future $\sigma$-field built from the next arrival time $\tau^n_i(t)$. Work conservation is (18).
• Costs and value are lower Lebesgue integrals in $[0,\infty]$, and $\lim$/$\liminf$ are taken there. The integrands are nonnegative under work conservation.
• Admissible systems range over sample spaces Ω : Type (universe 0). "Complete filtered probability space" means $P$ complete with all null sets in $\mathcal F_0$. Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the $(\mathcal F_t)$-Brownian property stated explicitly. $V$ is the infimum over systems and their controlled processes.
• Discount rate. $\gamma>0$ is a hypothesis; the paper leaves it implicit.
• Initial states are integer vectors $X^{0,n}\in\mathbb Z^k_+$ with $n^{-1/2}(X^{0,n}-\rho n)\to x$. The literal "$\hat X^{0,n}\in n^{-1/2}\mathbb Z^k$" would require $\rho_in\in\mathbb Z$. Assumption 1(ii) is not imposed: each policy chooses its own initial split.
• Lemma 3 is stated for all $n$ beyond a threshold that depends on the sequence, with constants $c,\bar m$ chosen before $x$ and the sequence. The printed all-$n$ bound with $c$ independent of $x$ fails when the early terms $\hat X^{0,n}$ are large.
• Weak convergence to a continuous limit uses the coupling form CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.

The goal hypothesizes $f$ and $h$ with the pointwise identity $b(x,h(x))\cdot Df(x)+L(x,h(x))=H(x,Df(x))$ for all $x$. An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where $\hat X^n$ lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing $k$, dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.

Not formalized:

• Lemma 4(iii) (tightness);
• Lemma 5 (Kurtz–Protter, which needs semimartingale theory absent from Mathlib);
• Lemma 6 (convergence of Stieltjes integrals at limit points);
• Proposition 5(iii);
• the nonpreemptive results, Theorem 2(ii)–(iii).

Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.

Selected references

• R. Atar, A. Mandelbaum, M. I. Reiman, Scheduling a multi class queue with many exponential servers: asymptotic optimality in heavy traffic, Ann. Appl. Probab. 14(3), 2004. https://arxiv.org/abs/math/0407058
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manuf. Serv. Oper. Manag. 5(2), 2003. https://doi.org/10.1287/msom.5.2.79.16071
• J. M. Harrison, A. Zeevi, Dynamic scheduling of a multiclass queue in the Halfin–Whitt heavy traffic regime, Oper. Res. 52(2), 2004. https://doi.org/10.1287/opre.1040.0109
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11(3), 2001. https://doi.org/10.1214/aoap/1015345343
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19(3), 1991. https://doi.org/10.1214/aop/1176990334

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

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

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

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

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

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

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

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, 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, 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. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

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

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