Probability

Motivation

A many-server queue has $N$ identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers $N$ grows with the arrival rate $\lambda_N$ so that $\sqrt N(1-\lambda_N/N)\to\beta$: servers are almost fully used, yet only a vanishing fraction of customers waits.

• Halfin and Whitt (1981, Oper. Res. 29) identified the regime and proved a diffusion limit for exponential service times ($GI/M/N$).
• Puhalskii and Reiman (2000, Adv. Appl. Probab. 32) treated phase-type service distributions ($GI/PH/N$).
• Reed (2009, arXiv:0912.2837), the source of this mission, obtained the fluid and diffusion limits of the number in system for the $G/GI/N$ queue with a general service-time distribution, assuming only a finite mean. Its approach rests on a sample-path identity, the system equation (2.8), which writes the number in system of the $N$-server queue through quantities of an infinite-server queue fed by the same arrivals.

This mission formalizes that identity and the proposition that yields it.

Setting

Fix one realisation of the queue (Reed, §2, p. 6).

• There are $N$ servers. At time $0-$ there are $Q_0$ customers; the first $\min(Q_0,N)$ are in service, with residual service times $\tilde\eta_i$, and the other $(Q_0-N)^+$ wait.
• Customers then arrive at times $0\le\tau_1\le\tau_2\le\cdots$ (with $\tau_0=0$); the arrival process is $A(t)=\#\{i\ge1:\tau_i\le t\}$. Arrivals at time $0$ are counted in $A(0)$, so in general $Q(0)\ne Q_0$.
• The $i$-th customer to enter service after time $0-$ has service time $\eta_i$. Service is first come first served, so the first $(Q_0-N)^+$ of these are the initial waiting customers and the $i$-th arrival has service time $\eta_{(Q_0-N)^++i}$.
• $w_i\ge0$ is the waiting time of the $i$-th arrival and $\tilde w_i\ge0$ that of the initial customer $N+i$.
• $F$ is the service-time distribution, with tail $G=1-F$, and $F_0$ the residual service-time distribution, with tail $\bar F_0$; both are carried by $[0,\infty)$.

The number in system is (2.2):

$$Q(t)=\sum_{i=1}^{\min(Q_0,N)}1\{\tilde\eta_i>t\}+\sum_{i=1}^{(Q_0-N)^+}1\{\tilde w_i+\eta_i>t\}+\sum_{i=1}^{A(t)}1\{\tau_i+w_i+\eta_{(Q_0-N)^++i}>t\}.$$

Centring each indicator at its (conditional) mean produces the terms

$$W_0(t)=\sum_{i=1}^{\min(Q_0,N)}\big(1\{\tilde\eta_i>t\}-\bar F_0(t)\big),\qquad A_G(t)=\int_0^tG(t-s)\,dA(s),\qquad I(t)=\min(Q_0,N)\bar F_0(t)+(Q_0-N)^+G(t),$$

and $M_2(t)$, the analogous centred sum (2.5) over the customers who entered service after time $0-$. $A_G(t)$ is the conditional mean number in a $G/GI/\infty$ queue fed by the same arrivals.

A sample path is non-idling if for every $t\ge0$

$$(Q(t)-N)^+=\sum_{i=1}^{(Q_0-N)^+}1\{t<\tilde w_i\}+\sum_{i=1}^{A(t)}1\{\tau_i\le t<\tau_i+w_i\},$$

that is, the customers waiting at time $t$ are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served $N$-server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).

Formalization targets

Goal: the system equation (2.8), p. 9

For a non-idling sample path and every $t\ge 0$,

$$Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\int_0^t\big(Q(t-s)-N\big)^+\,dF(s).$$

Milestones

1. The first two equalities of the proof of Proposition 2.1 (p. 8): $\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\sum_{i\le A(t)}\int_0^\infty 1\{t-(\tau_i+w_i)<s\le t-\tau_i\}\,dF(s)$.
2. The "reverse argument" of the proof (p. 9): $\int_0^t\sum_{i\le(Q_0-N)^+}1\{\tilde w_i>t-s\}\,dF(s)=\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)$.
3. Proposition 2.1 (p. 8): for a non-idling path and $t\ge0$,

$$\sum_{i=1}^{A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\int_0^t(Q(t-s)-N)^+\,dF(s)-\sum_{i=1}^{(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big).$$

4. The decomposition (2.7) (p. 7): $Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)+\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)$.

Significance

The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing $Q-N=x+\int_0^t(Q(t-s)-N)^+dF(s)$ with $x=I+W_0+M_2+A_G-N$ shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of $z(t)=x(t)+\int_0^t(z(t-s)+a)^+dB(s)$. The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the $N$-server queue has no closed equation in terms of quantities whose limits are known.

Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the $G/GI/N$ queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.

Difficulty

The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against $F$, of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer $i$'s service time falls in a window of length $w_i$" to "customer $i$ is waiting at time $t-s$", after which the sum over customers must be recognised, at each time $t-s$, as the waiting count of the non-idling identity, with the arrivals counted up to $A(t-s)$ rather than $A(t)$. A second point is the treatment of an atom of $F$ at $0$: the half-open windows $(t-\tau_i-w_i,\,t-\tau_i]$ and the closed integration range $[0,t]$ must match, and $G(x)=1$ for $x<0$ is used whenever a customer is still waiting.

Formalization scope

• Paths are data, not random. A sample path is a structure holding $N$, $Q_0$ and the sequences $\tilde\eta,\eta,\tau,w,\tilde w:\mathbb N\to\mathbb R$, indexed from $1$ as in the paper. The arrival times are primary and $A(t)$ is their counting function; for a counting process with $A(0-)=0$ this is the same data as the paper's $\tau_i=\inf\{t\ge0:A(t)\ge i\}$. The encoding has infinitely many arrivals, finitely many in each bounded interval.
• Distributions are probability measures $\mu$ (for $F$) and $\mu_0$ (for $F_0$) on $\mathbb R$ with no mass on $(-\infty,0)$, and $G(x)=\mu((x,\infty))$ for every real $x$. The paper's i.i.d. assumptions and the mean-$1$ assumption on $F$ are not used by these pathwise identities and are omitted.
• Integrals $\int_0^t\cdot\,dF(s)$ are over the closed interval $[0,t]$, an atom of $F$ at $0$ included; $A_G(t)$, a Stieltjes integral against the counting measure of arrivals, is the finite sum $\sum_{i\le A(t)}G(t-\tau_i)$.
• Non-idling is a hypothesis on the sample path, exactly the identity displayed above. No hypothesis mentions (2.8), Proposition 2.1 or an integral against $F$, and $Q$ is not a free function: it is defined by (2.2). Integrability of $s\mapsto(Q(t-s)-N)^+$ is part of what must be proved, not assumed. The hypotheses are jointly satisfiable, so the goal is not vacuous.
• Needed infrastructure: finite sums, set integrals of indicator functions against a finite measure on $\mathbb R$, and the identity $G(a)-G(b)=\mu((a,b])$. All of it is in Mathlib.

Related platform items: WhittEfficiency.IS.* (the $M/G/\infty$ queue with Poisson arrivals, the infinite-server object behind $A_G$) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.

Selected references

• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. arXiv:0912.2837v1. https://arxiv.org/abs/0912.2837 , https://doi.org/10.1214/09-AAP609
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29, 1981, 567–588. https://doi.org/10.1287/opre.29.3.567 (MR629195)
• A. A. Puhalskii and M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Adv. Appl. Probab. 32, 2000, 564–595. https://mathscinet.ams.org/mathscinet-getitem?mr=1778580

Motivation

Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.

The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is $-\infty$. This mission formalizes that statement.

Setting

There are $N \ge 1$ items $1, \dots, N$; item $1$ is the end item. Every item $i \ge 2$ has exactly one immediate successor $s(i)$ with $1 \le s(i) < i$, and $s(1) = 0$, so the items form a tree rooted at the end item. Write $A(i)$ for the set of all successors of $i$, $B(i)$ for the set of all its predecessors, and $P(i)$ for its immediate predecessors. Item $i$ has a lead time $l_i \in \mathbb N$, and its total lead time is $M_0 = 0$, $M_i = l_i + \sum_{k\in A(i)} l_k$; the items are indexed so that $M_{i-1} \le M_i$.

Time runs in periods $t = 1, 2, \dots$. The demands $\xi_1, \xi_2, \dots$ for the end item are independent, identically distributed, nonnegative, with a density and a finite mean $\lambda > 0$. In period $t$ a policy chooses the echelon inventory positions after ordering $Y_{1t}, \dots, Y_{Nt}$ as functions of the demands already observed. The position before ordering is $X_{it} = Y_{i,t-1} - \xi_{t-1}$, and the echelon stock on hand after arrivals is $X^l_{it} = Y_{i,t-l_i} - \sum_{r=t-l_i}^{t-1}\xi_r$; positions referring to periods before $1$ are read off given initial data $x^0$. Problem P asks for a policy satisfying

$$X_{it} \le Y_{it} \le X^l_{kt}\qquad\text{for all } k\in P(i) \text{ and all } i,t \tag{3}$$

that minimizes

$$E\Big\{\sum_{t=1}^\infty \alpha^{t-1}\Big(\sum_{i=1}^N \alpha^{l_i} h_i Y_{it} + \alpha^{l_1}(p+H_1)\int_{Y_{1t}}^\infty(\xi - Y_{1t})\,\varphi_1^{l+1}(\xi)\,d\xi\Big)\Big\} + \text{constant}, \tag{2}$$

where $h_i$ is the echelon holding cost of item $i$, $p$ the backlogging cost, $H_1$ the installation holding cost of the end item, $\alpha$ the discount factor and $\varphi_1^{l+1}$ the density of the demand over $l_1 + 1$ periods.

The quantity of interest is the discounted echelon holding cost of item $i$ and its predecessors,

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}}.$$

GA(i) asks it to be positive for every item.

Formalization targets

Goal: Theorem 4(i), p. 574

If for some item $i$

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}} < 0,$$

then the minimal cost of Problem P is unbounded below: for every real $C$ there is a feasible policy whose cost is a real number less than $C$.

Milestones: the proof of Theorem 4(i), p. 578

1. The one-more-unit policy is feasible. Ordering extra units of every item $k$ of the subsystem $\{i\}\cup B(i)$ in period $M_m - M_k + 1$, where $M_m$ is the greatest total lead time in the subsystem, and holding them forever, preserves (3).
2. The total cost increase. For a non-end item $i$ and a policy of finite cost, $\delta$ extra units change the cost by exactly

$$\delta\,\alpha^{M_m - M_i}\,\frac{\alpha^{l_i}\big(h_i + \sum_{k\in B(i)} h_k\,\alpha^{-(M_{s(k)} - M_{s(i)})}\big)}{1-\alpha}.$$

Significance

Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is $-\infty$. Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.

The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.

Difficulty

The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of $i$, whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item $i = 1$ the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.

Formalization scope

• Periods start at Lean index $k = 0$ with $k = t - 1$; the discount weight $\alpha^{t-1}$ is $\alpha^k$, and coordinate $j$ of a demand path is $\xi_{j+1}$. Items are natural numbers $1..N$.
• Demand is the product law (Measure.infinitePi) of a probability measure $\nu$ on $\mathbb R$ with $\nu((-\infty,0)) = 0$, $\nu \ll$ Lebesgue, $\nu$ integrable and $\int x\,d\nu > 0$.
• Policies are history-dependent and measurable; feasibility (3) holds almost surely.
• Initial data $x^0_i(s)$, $s \ge 1$, the echelon position of item $i$ at the start of period 1 ordered $s$ periods ago or earlier, are assumed well formed: nonincreasing in $s$, and $x^0_i(s) \le x^0_k(s + l_k)$ for $k \in P(i)$. The paper takes this for granted; it is what makes Problem P feasible.
• Cost is (2) without its policy-independent constant, as an extended real $E[\sum(\alpha^{t-1}c_t)^+] - E[\sum(\alpha^{t-1}c_t)^-]$.
• Added restriction: $0 < \alpha < 1$. The page allows $\alpha = 1$, where the average cost is minimized and is defined only through a limit recipe.
• No sign condition is imposed on $h_i$, $p$ or $H_1$; neither the Assumption nor GA is a hypothesis.

In the extended reals, $\top - \top = \bot$: a policy whose positive and negative cost parts are both infinite gets the value $-\infty$. The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost $\bot$ would be trivially true and is ruled out. Milestone 2 is stated for $i \ge 2$, where the backlog term is unchanged.

Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.

Selected references

• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• 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
• 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

Motivation

Temporal-difference learning, TD($\lambda$), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of $K$ fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors $\phi(i)$, and counterexamples in which related algorithms diverge.

Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD($\lambda$) with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator $\Pi T^{(\lambda)}$ and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.

Timeline:

• 1988: Sutton introduces TD($\lambda$) and proves convergence in the mean for TD(0) on absorbing chains with linearly independent features.
• 1992: Dayan extends convergence in the mean to general $\lambda$.
• 1994: Jaakkola, Jordan and Singh, and Tsitsiklis, prove almost-sure convergence for lookup tables, using maximum-norm contraction.
• 1996: Tsitsiklis and Van Roy prove almost-sure convergence with linear function approximation and the error bound below.

Setting

A Markov chain $i_0, i_1, \dots$ lives on a finite or countably infinite state space $S$, with transition matrix $P = (p_{ij})$. A transition from $i$ to $j$ costs $g(i,j)$, and $\alpha \in (0,1)$ is a discount factor. The cost-to-go is

$$J^*(i) = E\Big[\sum_{t=0}^\infty \alpha^t g(i_t,i_{t+1}) \,\Big|\, i_0 = i\Big].$$

Basis functions $\phi_1,\dots,\phi_K : S \to \mathbb R$ give the feature vector $\phi(i) \in \mathbb R^K$ and the approximation $\tilde J(i,r) = r'\phi(i)$, written $\Phi' r$ as a vector over $S$.

Starting from an arbitrary $r_0$, TD($\lambda$) with $\lambda \in [0,1]$ and step sizes $\gamma_t$ forms the eligibility vector $z_t = \sum_{k=0}^t (\alpha\lambda)^{t-k}\phi(i_k)$ and the temporal difference $d_t = g(i_t,i_{t+1}) + \alpha\phi(i_{t+1})'r_t - \phi(i_t)'r_t$, and updates $r_{t+1} = r_t + \gamma_t d_t z_t$.

Let $\pi$ be the invariant distribution, $D = \mathrm{diag}(\pi)$, $\|J\|_D^2 = \sum_i \pi(i)J(i)^2$, and $L_2(S,D) = \{J : \|J\|_D < \infty\}$. Write $\Pi = \Phi'(\Phi D\Phi')^{-1}\Phi D$ for the $D$-orthogonal projection onto $\{\Phi'r\}$. The operator $T^{(\lambda)}$ averages $m$-stage truncated costs:

$$(T^{(\lambda)}J)(i) = (1-\lambda)\sum_{m=0}^\infty \lambda^m E\Big[\sum_{t=0}^m \alpha^t g(i_t,i_{t+1}) + \alpha^{m+1}J(i_{m+1}) \,\Big|\, i_0 = i\Big],$$

for $\lambda < 1$, and $T^{(1)}J = J^*$. The paper makes four assumptions:

1. the chain has a unique invariant distribution with $\pi(i) > 0$, $E_0[g^2] < \infty$, and finite $J^*$;
2. the $\phi_k$ are linearly independent with $E_0[\phi_k^2] < \infty$;
3. polynomial moment growth and summable mixing conditions, relative to coordinates $\sigma(i) \in \mathbb R^N$ of the states;
4. nonnegative, nonincreasing step sizes with $\sum\gamma_t = \infty$ and $\sum\gamma_t^2 < \infty$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1–4: $J^* \in L_2(S,D)$; for every $\lambda \in [0,1]$, TD($\lambda$) converges with probability 1, from every initial state and every $r_0$, to a vector $r^*$; $r^*$ is the unique solution of

$$\Pi T^{(\lambda)}(\Phi' r^*) = \Phi' r^*;$$

and

$$\|\Phi' r^* - J^*\|_D \le \frac{\|\Pi J^* - J^*\|_D}{1 - \alpha(1-\lambda)/(1-\lambda\alpha)}.$$

Milestones

• Lemma 1: $\|PJ\|_D \le \|J\|_D$.
• Lemma 2: $J^*$ is finite, lies in $L_2(S,D)$, and $J^* = \sum_t(\alpha P)^t\bar g$.
• Lemma 3: $T^{(\lambda)}$ maps $L_2(S,D)$ into itself and has a closed-form series.
• Lemma 4: $T^{(\lambda)}$ is a $\|\cdot\|_D$-contraction with modulus $\alpha(1-\lambda)/(1-\alpha\lambda)$.
• Lemma 5: $\Pi T^{(\lambda)}$ has a unique fixed point $\Phi'r^*$, with the error bound above.
• Lemma 6: steady-state moments of $\phi$ and $z_t$.
• Lemma 7: the steady-state mean step is $E_0[s(r,X_t)] = \Phi D(T^{(\lambda)}(\Phi'r) - \Phi'r)$.
• Lemma 8: $(r - r^*)'E_0[s(r,X_t)] < 0$ for $r \neq r^*$.
• Theorem 2: a stochastic approximation theorem with Markov noise.
• §6: $A = E_0[A(X_t)]$ is negative definite and $Ar^* + b = 0$.

Significance

Theorem 1 says that TD($\lambda$), run on-line along a single trajectory, converges for every $\lambda$, and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as $\lambda \to 1$ the limit approaches the best approximation $\Pi J^*$, and that for smaller $\lambda$ the error can grow by at most a factor $(1-\alpha\lambda)/(1-\alpha)$. The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, $\|\cdot\|_D$, which holds only when states are sampled along the chain.

The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:

• a Lean model of countable-state Markov chains with costs, their path law, the weighted space $L_2(S,D)$ and the projection $\Pi$, which is reusable for later work on linear TD, LSTD and approximate policy evaluation;
• the deterministic layer (Lemmas 1–5, 7, 8), which is self-contained functional analysis on $L_2(S,D)$;
• Theorem 2, a stochastic approximation theorem with Markov noise, which the paper quotes from Benveniste, Métivier and Priouret (1987) without proof. A formal proof of it would be a library result in its own right.

Difficulty

The obvious approach treats TD($\lambda$) as a noisy version of the deterministic iteration $\bar r_{t+1} = \bar r_t + \gamma_t\Phi D(T^{(\lambda)}(\Phi'\bar r_t) - \Phi'\bar r_t)$. It fails at the noise. The increments $s(r_t,X_t)$ are driven by the Markov process $X_t = (i_t,i_{t+1},z_t)$, not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with $z_{-1} = 0$ rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: $\Pi$ is a nonexpansion of $\|\cdot\|_D$ only because $D$ is the invariant distribution of the same chain that defines $T^{(\lambda)}$.

Formalization scope

$S$ is a countable type with the discrete $\sigma$-algebra, $P$ a Markov kernel ($p_{ij} = P(i)(\{j\})$, $P^m$ the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:

• $\alpha \in (0,1)$ and $\lambda \in [0,1]$;
• "with probability 1" is almost-sure convergence under the path law from each deterministic initial state;
• $J^*$ and $T^{(\lambda)}$ are defined by the page's path expectations, not by the series of Lemmas 2 and 3;
• $L_2(S,D)$ membership is summability of $\pi(i)J(i)^2$;
• Assumption 1(c) means absolute integrability of the discounted cost series;
• vector norms are Euclidean and matrix norms Frobenius (equivalent to the induced norm and used only under existential constants);
• $(\Phi D\Phi')^{-1}$ is Lean's matrix inverse, invertible under Assumptions 1(a) and 2;
• the steady-state process of Lemmas 6–8 is any two-sided chain on a probability space with the stationary finite-dimensional distributions.

Lean's integral of a non-integrable function and sum of a non-summable series are $0$. A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.

The development needs the following:

• Markov-chain path measures and stationary two-sided chains;
• Bochner integrals of vector-valued functions;
• the Cauchy–Schwarz inequality on $L_2(S,D)$;
• a Markov-noise stochastic approximation theorem.

Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from $\pi$ and $P$ (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.

Selected references

• J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT LIDS report LIDS-P-2322, 1996; IEEE Transactions on Automatic Control 42(5):674–690, 1997. https://doi.org/10.1109/9.580874
• A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990 (French original 1987). https://doi.org/10.1007/978-3-642-75894-2
• R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3:9–44, 1988. https://doi.org/10.1007/BF00115009
• P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8:341–362, 1992. https://doi.org/10.1007/BF00992701
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the convergence of stochastic iterative dynamic programming algorithms, Neural Computation 6(6):1185–1201, 1994. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous stochastic approximation and Q-learning, Machine Learning 16:185–202, 1994. https://doi.org/10.1007/BF00993306

Motivation

A single stock of one product often serves customers of different importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority patients for a blood bank. When stock runs low, the question is not only how much to order but how much of the remaining stock to hand to the less important customers now, and how much to hold back for more important demand that may still arrive. Stock rationing policies answer this question with critical rationing levels: demand of a class is served only while the stock stays above that class's level.

Topkis (1968) studied this problem as a finite-horizon dynamic program with $n$ demand classes, nonstationary costs and demands, and an arbitrary degree of backlogging. His Theorem 1 shows that, when each interval has either complete backlogging or none, a policy given by critical levels $\bar z_t^1 \ge \dots \ge \bar z_t^n$ is optimal. This mission concerns his Theorem 3, which treats the case of complete backlogging: the critical levels of a class do not depend on what happens in the classes below it.

Timeline. Veinott (1965) considered $n$ demand classes but imposed the policy with all critical levels equal to $0$. Topkis's 1966 report treated $n = 2$, partially duplicated independently by Evans (1968) and by Kaplan's 1966 report "Stock Rationing", in which, according to Topkis, the result of Theorem 3 was used implicitly. Topkis (1968) extended the analysis to $n$ classes and stated Theorem 3 explicitly.

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ is followed by $t - 1$ further intervals, and interval $k$ is the first. There are $n$ demand classes; class $n$ is the most important. In interval $t$ a random demand vector $d_t = (d_t^1, \dots, d_t^n) \ge 0$ with law $\mu_t$ and finite means arrives; demands in different intervals are independent. Given the stock $z$ and the outstanding demand $B = b + d_t$ (backlog $b$ plus new demand), the decision is the vector $u$, $0 \le u \le B$, of demand left unsatisfied; the stock drops to $w = z - \mathbf 1 \cdot (B - u) \ge 0$. A penalty $p_t \cdot u$ and a holding cost $h_t(w)$ are charged, and the backlog carried into the next interval is $a_t u$, with $a_t = 1$ for complete backlogging. At the end of the period a salvage cost $g_0(z, b) = v_1(z) + v_2(z - \mathbf 1 \cdot b)$ is charged.

The standing assumptions are: $h_t$ convex and continuous on $[0,\infty)$; $v_1$ convex and continuous on $[0,\infty)$; $v_2$ convex and continuous on $\mathbb R$ with $\lim_{w \to -\infty} D^+ v_2(w) > -\infty$; and $0 \le p_t^1 \le \dots \le p_t^n$. The minimal expected cost satisfies the recursion (1):

$$f_t(z, B) = \inf_{\substack{0 \le u \le B \\ w = z - \mathbf 1\cdot(B-u) \ge 0}} \big[p_t \cdot u + h_t(w) + g_{t-1}(w, a_t u)\big], \qquad g_t(z, b) = \mathbb E\, f_t(z, b + d_t).$$

With $\delta_j$ the $j$-th unit vector, the critical rationing level $\bar z_t^j$ is $+\infty$ if $w \mapsto p_t^j w + h_t(w) + g_{t-1}(w, a_t w \delta_j)$ is strictly decreasing on $[0, \infty)$, and is the smallest minimizer of that function on $[0,\infty)$ otherwise. $D^+$ denotes a right derivative.

Formalization targets

Goal: Theorem 3

Assume $a_{t+1} = a_t = \dots = a_1 = 1$ and that the demands of different classes are independent in each interval. Fix a class $j$. Then for two instances of the model that differ only in the penalties $p_i^m$ of the classes $m \le j - 1$ and in the demand distributions of the classes $m \le j$,

(a) the marginal quantities

$$D_z^+ g_t(z, z\delta_j) \quad\text{and}\quad D_\varepsilon^+ g_t\big(w, \varepsilon(\delta_j - \delta_s) + b\big)\big|_{\varepsilon = 0} \quad (s > j,\ b^s > 0)$$

coincide, and

(b) the critical rationing levels $\bar z_{t+1}^j$ coincide.

Milestones

1. The claim in the proof of Theorem 3 (p. 173): for $j < s$ and $B^s > 0$, $D_\varepsilon^+ g_t(z, \varepsilon(\delta_j - \delta_s) + B)|_{\varepsilon=0}$ is independent of $B^1, \dots, B^j$.
2. Theorem 3 (a) on its own, from which the page derives (b).

Significance

The result. Theorem 3 reduces the size of the problem. Under complete backlogging, class 1 demand does not influence any critical rationing level, and the class-$j$ critical levels can be found from a problem with only the $n - j + 1$ classes $j, \dots, n$, with a degenerate demand distribution for class $j$. Since computing the levels requires tabulating functions of several variables, which Topkis calls prohibitive for large $n$, this is the observation that makes the levels of the most important classes computable.

Formalizing it. The theorem is proved in the paper by a short sketch that points to two case formulas, (16) and (17), to Theorem 1 (c), and to an interchange of expectation and right derivative. A machine-checked proof would supply the induction, the case analysis and the interchange in full. No formalization of any part of Topkis's paper is known: the result is proved on paper, not formalized.

Difficulty

The obvious argument is an induction on $t$ showing that $g_t$ itself does not depend on the lower classes. It fails: $g_t$ does depend on the penalties and demands of every class, since lower-class demand is still served and penalized. Only certain directional derivatives are invariant, and these derivatives depend on the critical levels of every class $l \ge j$ and on the optimal rationing decision, which themselves change from one instance to the other unless the invariance is already known for the previous interval. The derivatives are one-sided, may be $-\infty$ at the boundary, and must be passed through an expectation.

Formalization scope

The Lean development, in namespace TopkisRation.Backlog, fixes these conventions:

• classes are Fin n (class $j$ of the paper is index $j-1$); intervals are natural numbers counted backwards; vectors are ordered pointwise;
• $f_t$ is defined by the recursion (1), with sInf for the infimum and the Bochner integral for $\mathbb E$, and every statement restricts to $z \ge 0$, $b \ge 0$;
• $D^+$ is an extended-real right derivative (a liminf of difference quotients); $D_z^+ g_t(z, z\delta_j)$ is the derivative along the ray in which the stock and the class-$j$ backlog move together;
• $\bar z_t^j$ takes values in $\mathbb R \cup \{+\infty\}$ and is specified by a predicate (smallest minimizer, or $+\infty$ for a strictly decreasing function), never by a real sInf;
• the limit in (B) is read as "$D^+ v_2$ is bounded below";
• independence of the classes in interval $i$ is independence of the coordinate maps under $\mu_i$.

"Does not depend on" is stated with two instances $M$, $M'$ that agree on every datum the conclusion uses except the freed ones: the same $k$, $v_1$, $v_2$, the same $h_i$ and the same $p_i^m$ for $m \ge j$ in intervals $i \le t+1$, and the same class-$m$ marginal law for $m > j$ in every interval. The penalty of class $j$ itself is not freed. Data of intervals beyond $t+1$ and the ordering cost are unconstrained. Part (b) is stated for arbitrary critical levels of the two instances; existence of critical levels is part of the paper's §1 and is not assumed away, so (b) is not vacuous. The goal does not assume the p. 173 claim, the case formulas (16)–(17), or Theorem 1. Encoding "does not depend" as "is a function of the remaining data" is ruled out.

Needed infrastructure: one-sided derivatives of convex functions and their monotone limits, interchange of right derivative and expectation for convex integrands, and the convexity and rationing-policy results of §1 (Theorem 1, Lemma 2). These are reusable for the other missions of this series. Contributions welcome: proofs of the milestones, a formal version of (16)–(17), and the existence of critical levels.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3):160–176, 1968. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5):761–778, 1965. https://doi.org/10.1287/opre.13.5.761
• R. V. Evans, Sales and restocking policies in a single item inventory system, Management Science 14(7):463–472, 1968. https://doi.org/10.1287/mnsc.14.7.463
• A. Kaplan, Stock Rationing, report, December 1966 (reference [4] of Topkis 1968).

Motivation

Many decision problems under uncertainty take the form of minimizing an expected cost $\varphi(x) = \mathbb E_\xi f(x, \xi)$ over a convex feasible set, where $\xi$ is a random parameter whose distribution can be sampled but not integrated in closed form. Evaluating $\varphi$ even approximately can cost exponentially many evaluations of $f$ in the dimension of $\xi$, so the classical deterministic notion of an approximate solution is unusable. A practical alternative, going back to Nemirovski and Yudin, asks for a random output $x$ whose expected objective value is close to the optimum: $\mathbb E\,\varphi(x) - \varphi^* \le \epsilon$. Stochastic subgradient methods achieve this; Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009)) shows that the same guarantee holds for a stochastic version of his method of simple dual averages, a scheme that aggregates all past subgradients in the dual space instead of taking projected steps with decreasing step sizes.

Dual averaging has since become a standard tool in stochastic and online convex optimization (regularized dual averaging, AdaGrad's primal-dual variant, distributed dual averaging). Section 6 of Nesterov's paper is the original statement of its expected-accuracy guarantee.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ and dual space $E^*$ with dual norm $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$. Let $Q \subseteq E$ be closed and convex, and let $d$ be a prox-function of $Q$: continuous on $Q$ and strongly convex on $Q$ with convexity parameter $\sigma > 0$,

$$d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x-y\|^2,$$

with prox-center $x_0 = \arg\min_{x\in Q} d(x)$ and $d(x_0) = 0$. For $\beta > 0$ and $s \in E^*$ the point $\pi_\beta(s) = \arg\min_{x \in Q}\{-\langle s, x\rangle + \beta d(x)\}$ is well defined. The scalar sequence $\hat\beta$ is given by $\hat\beta_0 = \hat\beta_1 = 1$ and $\hat\beta_{i+1} = \hat\beta_i + 1/\hat\beta_i$ for $i \ge 1$.

The stochastic problem is given by a probability space $(\Xi, \mu)$ and a cost $f : Q \times \Xi \to \mathbb R$ with $\varphi(x) = \mathbb E_\xi f(x,\xi)$ well defined on $Q$, and a minimizer $x^*$ of $\varphi$ over $Q$ with $\varphi^* = \varphi(x^*)$. Assumption 1: each $f(\cdot, \xi)$ is convex on $Q$. Assumption 2: a stochastic oracle returns a subgradient $f'(x, \xi)$ of $f(\cdot, \xi)$ at $x$, and $\|f'(x,\xi)\|_* \le L$ for all $x \in Q$, $\xi \in \Xi$.

The method of stochastic simple averages (SSA, (6.3)) fixes $\gamma > 0$, starts from $x_0$ and $s_0 = 0$, and for $k \ge 0$ draws a fresh independent sample $\xi_k \sim \mu$ and sets

$$s_{k+1} = s_k + f'(x_k, \xi_k), \qquad x_{k+1} = \pi_{\gamma\hat\beta_{k+1}}(-s_{k+1}).$$

Its deterministic counterpart, the method of simple dual averages (SDA, (2.21)), is the same recursion with arbitrary answers $g_k$ in place of $f'(x_k, \xi_k)$. The quality of the points $x_0,\dots,x_k$ is measured by the gap $\delta_k(D) = \max\{\sum_{i=0}^k\langle g_i, x_i - x\rangle : x \in Q,\ d(x)\le D\}$. Write $\boldsymbol\xi_k = (\xi_0, \dots, \xi_k)$ and $\mathbb E_{\boldsymbol\xi_k}$ for the expectation over these $k+1$ independent samples.

Formalization targets

Goal: Theorem 7 (p. 27)

For every $k \ge 0$,

$$\mathbb E_{\boldsymbol\xi_k}\Big(\varphi\Big(\frac{1}{k+1}\sum_{i=0}^k x_i\Big)\Big) - \varphi^* \le \frac{\hat\beta_{k+1}}{k+1}\Big(\gamma\, d(x^*) + \frac{L^2}{2\sigma\gamma}\Big).$$

Milestones

1. Theorem 2 (p. 11): for SDA with any answers $g_i$ and $L_k = \max_{i\le k}\|g_i\|_*$, $\delta_k(D) \le \hat\beta_{k+1}(\gamma D + L_k^2/(2\sigma\gamma))$ for $D \ge 0$, and, if some $x^* \in Q$ satisfies $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$, $\|x_k - x^*\|^2 \le \frac2\sigma d(x^*) + L_k^2/(\sigma^2\gamma^2)$.
2. (6.5) (p. 26): along every sample path, $\frac{1}{k+1}\tilde\delta_k(D) \le \frac{\hat\beta_{k+1}}{k+1}(\gamma D + \frac{L^2}{2\sigma\gamma})$.
3. Display after (6.5) (p. 26): for $D \ge d(x^*)$, the gap of a run dominates $\frac1{k+1}\sum_i\langle f'(x_i,\xi_i), x_i - x^*\rangle$, which dominates $\frac1{k+1}\sum_i[f(x_i,\xi_i) - f(x^*,\xi_i)]$.
4. (6.6) (p. 26): $\mathbb E_{\boldsymbol\xi_k}(\frac1{k+1}\delta_k(D)) \ge \frac1{k+1}\sum_i\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) - \varphi^*$.
5. p. 27, first display: $\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) = \mathbb E_{\boldsymbol\xi_k}\varphi(x_i)$ for $i \le k$.
6. p. 27, display before Theorem 7: $\frac1{k+1}\sum_i\mathbb E\varphi(x_i) \ge \mathbb E\varphi(\frac1{k+1}\sum_i x_i)$, together with the averaged identity.

Significance

Theorem 7 gives an explicit, non-asymptotic bound on the expected optimality gap of the averaged SSA point. Since $\hat\beta_{k+1} \approx \sqrt{2k}$, the bound is $O(1/\sqrt k)$, the optimal rate for nonsmooth stochastic convex optimization with bounded subgradients. Two features distinguish it from the classical stochastic subgradient bound: it holds in an arbitrary norm with a non-Euclidean prox-function (for example the entropy on the simplex with the $\ell_1$ norm), and the feasible set $Q$ need not be bounded, since only $d(x^*)$ enters. The constant is explicit and $\gamma$ can be tuned to $\gamma = L/\sqrt{2\sigma d(x^*)}$.

The result is proved in the paper; to our knowledge no machine-checked proof of Theorem 7 or of the dual averaging bounds of the paper exists. A formalization yields a reusable verified analysis of dual averaging in a general normed space, a template for expectation bounds over i.i.d. sample paths of an adaptive algorithm, and checked constants.

Difficulty

The pathwise part is a consequence of the deterministic Theorem 2, which itself rests on the general Dual Averaging bound (the companion mission's Theorem 1) and on the strong convexity estimates for $\pi_\beta$. The probabilistic part looks routine on paper but is where formal arguments break: the iterate $x_i$ is a function of $\xi_0, \dots, \xi_{i-1}$, and the identity $\mathbb E f(x_i, \xi_i) = \mathbb E\varphi(x_i)$ requires measurability of the whole run and a Fubini argument on the product space. Measurability of the run in turn depends on continuity of the argmin map $\pi_\beta$, and integrability of $\varphi(\bar x_k)$ and of the gap is not assumed but must be derived from the uniform bound $L$ and the boundedness of the iterates. Pathwise bounds alone do not suffice: (6.5) controls the gap on each sample, not $\varphi(\bar x_k)$.

Formalization scope

Theorem numbers and page numbers refer to source.pdf, the author's revised CORE discussion-paper version (September 2005) of the Math. Program. article; printed pages equal PDF pages.

• $E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, and $\langle s, x\rangle$ is s x. Strong convexity is Mathlib's StrongConvexOn Q σ d, which is exactly (1.8); $\sigma > 0$.
• $\pi$ is a map ℝ → StrongDual ℝ E → E with the hypothesis that $\pi_\beta(s)$ lies in $Q$ and minimizes $-\langle s, x\rangle + \beta d(x)$ for every $\beta > 0$; no choice function is used.
• $\hat\beta$ is defined by recursion with $\hat\beta_0 = \hat\beta_1 = 1$. The gap is a real supremum over $\mathcal F_D = \{x\in Q : d(x)\le D\}$, used only for $D \ge 0$, where the set is nonempty and bounded.
• Indices start at 0; $x_0$ is the prox-center. The run is a function of a sample path $\omega : \mathbb N \to \Xi$; $\mathbb E_{\boldsymbol\xi_k}$ is the integral against the product measure $\mu^{\otimes(k+1)}$ on $\Xi^{k+1}$ (the law of $k+1$ i.i.d. copies of $\xi$), with the finite sample padded to a sequence that the iterates never read.
• $f$ and $f'$ are functions on $E \times \Xi$ whose values off $Q$ are irrelevant; the subgradient inequality is relative to $Q$. Integrability of $f(x, \cdot)$ for $x \in Q$, and joint measurability of $f$ and $f'$, are explicit hypotheses. The paper uses measurability tacitly; without it a Lean integral of a non-measurable function is $0$ and the goal could become false.
• A statement for a fixed sample path, or with $\mathbb E\varphi(\bar x_k)$ replaced by a pathwise quantity, is a different and weaker theorem and does not count. Integrability of the run is not assumed: it is part of what must be proved.

A complete development needs the deterministic dual averaging analysis (Lemma 1, Lemma 2, Theorem 1 of the paper, restated here only through Theorem 2), measurability and continuity of $\pi_\beta$, and Fubini on finite products of probability spaces. The dual averaging lemmas and the product-measure lemmas for adaptive sample paths are reusable beyond this mission. Proofs of any milestone, and supporting lemmas on measurability of the SSA run, are welcome.

Selected references

• Yu. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009), 221–259. https://doi.org/10.1007/s10107-007-0149-x
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009), 1574–1609. https://doi.org/10.1137/070704277
• L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010), 2543–2596. https://jmlr.org/papers/v11/xiao10a.html