Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks IX: Fluid Stability of the Proportionally Fair AllocationTextbook

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$ , the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$ . When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$ , a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ( $\varphi$ ) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$ , $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$ , which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$ , not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$ ) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

12 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks X: Maximal Stability of Proportionally Fair ControlTextbook

Motivation

Mission IX (09-proportional-fairness-core) formalized proportional fairness (PF) as a control policy and proved the technical core of its stability theory: under a load condition, the PF fluid model is stable (Theorem 10.5), via an entropy Lyapunov function that is genuinely not Lipschitz continuous — a departure from every other stability argument in J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org). A stability theorem for one fixed arrival-rate vector is, on its own, a narrower claim than practitioners actually want: real systems see load that changes over time, and a control policy worth adopting should not need re-tuning every time the mix of traffic shifts. This mission completes Theorem 10.5's proof and turns it into exactly that stronger guarantee — proportional fairness is maximally stable: stable throughout the entire region where any policy could be stable, without knowing the arrival rates in advance — and specializes the result to two concrete network families, bandwidth-sharing networks and queueing networks under head-of-line proportional processor sharing (HLPPS), that were already familiar from earlier in the book under different control policies.

Setting

Fix a unitary network operating under PF control with mean service times $m > 0$ , routing matrix $P$ , a partition of job classes into demand groups $\{\mathcal I(\ell), \ell \in \mathcal L\}$ , and a reduced allocation set $\tilde{\mathcal A} \subset \mathbb R^{\mathcal L}_+$ (all restated from mission IX, Definition 10.3). The entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38, mission IX) admits an alternative decomposition $\varphi = \sum_\ell \varphi_\ell$ in terms of the within-group entropy term

f(t) := \sum_{\ell\in\mathcal L}\sum_{i\in\mathcal I(\ell)} Z_i(t)\log\!\left(\frac{Z_i(t)}{Y_\ell(t)}\right), \qquad Y(t) := GZ(t) \quad \text{(Eq. 10.50)},

with the convention that the term for class $i$ is $0$ when $Z_i(t)=0$ . Here $D^+$ / $D^-$ denote the upper-right/upper-left Dini derivatives (Appendix A.4, Eqs. A.9-A.10): at a point where the ordinary derivative may not exist, these one-sided $\limsup$ s still let a Lyapunov-drift argument go through. A control policy is maximally stable (Section 5.7) for a network if its implementation does not depend on the arrival-rate vector $\lambda$ and it is stable for every $\lambda$ in the network's stability region $\Lambda^*$ — the largest region any policy could possibly stabilize.

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

\text{IsMaximallyStable}\Big(\lambda \mapsto \text{PFFluidStable}(\lambda, m, P, \mathrm{grp}, \tilde{\mathcal A})\Big)

for the single PF policy value (its implementation never depends on $\lambda$ ). This is the applied payoff of Theorem 10.5 (mission IX): combined with Theorem 6.2 (mission III, fluid stability implies SPN stability) and Corollary 5.6 (mission II, a $\lambda$ -independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single- $\lambda$ stability statement to the strongest form the book's own framework can express.

Supporting milestones

Lemmas 10.11-10.15 supply the remaining technical content of Theorem 10.5's proof that mission IX's own milestones left open: Lemma 10.11 is the uniform negative-drift bound $\sum_i \dot Z_i(t)\log(\dot D_i(t)/\alpha_i) \le -\varepsilon$ at every regular point with $Z(t) \ne 0$ ; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term $f$ ; Lemma 10.15 shows that positivity of the departure rate $\dot D_i(t)$ propagates from occupied classes to every class. Corollaries 10.17 and 10.18 specialize the goal to bandwidth-sharing networks and to HLPPS-controlled queueing networks, respectively.

Significance

The result itself. A stability theorem tied to one fixed $\lambda$ is of limited practical use: it would need to be re-verified every time the arrival-rate vector changes, which real traffic does constantly. Maximal stability removes that dependency entirely — a single policy, implemented without any knowledge of $\lambda$ , is guaranteed stable throughout the full region any control could stabilize. Corollaries 10.17 and 10.18 make this concrete for two network families with independent histories in the literature: bandwidth-sharing networks (the original motivation for proportional fairness, Kelly 1997) and queueing networks under HLPPS, connecting PF's static, utility-theoretic motivation to a scheduling rule that predates it.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=maximal%20stability, q=bandwidth%20sharing) finds no relevant hits on the platform. This mission formalizes the remaining entropy-Lyapunov lemmas, the within-group entropy term, the BWS and HLPPS network models (restated locally, since no other drafted chunk covers Sections 4.5-4.6), and the maximal-stability predicate, reusing only Mathlib's general real-analysis substrate (Dini derivatives via Filter.limsup) and definitions restated from missions II, III, V, and IX under this series' restate-not-import convention for concurrently-drafted chunks.

Difficulty

The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit $\lambda$ -dependent policy family and add "the policy doesn't actually depend on $\lambda$ " as a side hypothesis — obscures the point: a policy that is definitionally independent of $\lambda$ is a stronger and cleaner claim than one that happens to satisfy an extra equation. This formalization instead instantiates the abstract policy type at Unit, so $\lambda$ -independence holds by construction rather than as a hypothesis to verify, matching the book's own reading of Section 5.7's definition. A second difficulty is Lemma 10.13's Dini-derivative inequality (Eq. 10.56): the plain-text extraction of this display equation loses bracket and subscript structure that changes its meaning, so the exact grouping was confirmed against the PDF page directly and cross-checked against the book's own re-derivation of the same bracketed expression inside Lemma 10.14's proof. A third is Corollary 10.17's proof, which genuinely depends on three facts outside this chunk's own chapter portion (Proposition 4.4 and the Section 4.4 model translation, Proposition 5.1, Theorem 5.2); rather than silently assuming them or re-deriving their proofs from scratch, they are stated as explicit hypotheses of the milestone itself, so the item's actual content — deriving the two-sided conclusion — is exactly what remains to be proved.

Formalization scope

RestatedCore, RestatedFluidModel, and the maximal-stability predicate MaximalStability are restated verbatim (or, for MaximalStability, in shape) from missions IX, III/V, and II respectively, since concurrently-drafted chunks in this series do not import one another's Lean files even when they share a sub-namespace. New to this chunk: diniUpperLeft (Eq. A.10, needed alongside mission IX's diniUpperRight for Lemma 10.13's two-sided bound), the within-group entropy term withinGroupEntropy (Eq. 10.50, deliberately not named f, since the book's own f already denotes the unrelated PF optimization objective of Eq. 10.2 within the same chapter), and BWSNetworkData/QueueingNetworkDataHL/HLPPSFluidStable (Sections 4.5-4.6, restated locally since no drafted chunk's BRIEF.md covers them). The formalization does not admit a trivializing reading: IsMaximallyStable is instantiated with the genuine, non-vacuous predicate PFFluidStable/HLPPSFluidStable — the same predicate whose stability Theorem 10.5 (mission IX) already establishes on the load-condition region — never with a policy type or stability predicate engineered to make the maximal-stability claim vacuous. Contributions completing the eight by sorry proofs are welcome, particularly Lemma 10.13's Dini-derivative estimate (Section B.4's preliminary results) and Lemma 10.15's connectivity argument (Appendix B.9/B.17).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33–37.
F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.

13 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XI: Maximal Stability of Workload-Weighted Task AllocationTextbook

Motivation

Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.

Setting

A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class is a pair $(\ell,k)$ , a category routed to a specific server, with mean service time $m_{\ell k} > 0$ (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's relative processing speed. Tasks in category $\ell$ arrive according to a Markovian arrival process (MArP) with long-run average rate $\nu_\ell$ — a substantially more general model than the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks generated from a single job. Routing is by immediate commitment: each task is assigned to a server the instant it arrives, based only on its category and the current backlog, with no possibility of later reassignment. The workload of server $k$ at time $t$ (Eq. 11.7) is $W_k(t) := \sum_\ell m_{\ell k} Z_{\ell k}(t)$ , the locality-weighted total backlog assigned to it. Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category- $\ell$ task to any server achieving $\operatorname{argmin}_{k} m_{\ell k} W_k(t-)$ (Eq. 11.8, ties broken arbitrarily), where $W(t-)$ is the workload vector's left limit at the arrival instant.

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

If there exists $\lambda = (\lambda_{\ell k}) \ge 0$ with $\sum_k \lambda_{\ell k} = \nu_\ell$ for each category (Eq. 11.4) and $\sum_\ell m_{\ell k}\lambda_{\ell k} < 1$ for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.

Supporting milestones

Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full $G,R,A,b$ apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.

Significance

The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.

Formalizing it. A live prior-art check (GET /theorems?q=task+allocation, q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns one unrelated text-corpus-statistics result). This mission formalizes the task allocation model, WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per this series' convention for concurrently-drafted chunks) the minimal apparatus needed from missions I and III.

Difficulty

The obvious approach to Definition 11.3 — pick a canonical minimizer of $m_{\ell\cdot}W_\cdot(t-)$ , e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8) explicitly allows any minimizer; this mission instead states WWTA as domination over every server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem 11.4's "for almost all $\omega$ " existence claim is a measure-theoretic statement about a probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point $\omega$ together with the specific SLLN limit that argument needs — this mission follows the same precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself supply the type information Lean's typeclass resolution needs to identify an ambient measure. A third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw (pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof derives the needed consequence (Eq. 11.22, "server $k$ receives no more category- $\ell$ tasks in a neighbourhood of $t$ ") via an explicit $\varepsilon$ - $\delta$ argument from the discrete policy, which this mission takes as a documented hypothesis rather than re-deriving, since building the arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this chapter's own numbered results.

Formalization scope

Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index, avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/ FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes; PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3, specialized) used throughout this series. Contributions completing the five by sorry proofs are welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
J. Dean and S. Ghemawat, "MapReduce: simplified data processing on large clusters," Communications of the ACM 51 (2008), 107–113.
Q. Xie, A. Yekkehkhany, and Y. Lu, "Scheduling with multi-level data locality: throughput and heavy-traffic optimality," IEEE INFOCOM 2016.

10 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XII: Packet Networks, Subcriticality and Fluid LimitsTextbook

Motivation

Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.

Setting

A packet network (Section 12.1) has I packet classes and J activities (service types); activity $j$ transfers a packet from its input class $u(j)$ to its output class $d(j)$ (or removes it from the network if $d(j)=0$ ), giving an $I\times J$ input-output matrix $R$ . A processing plan for class $i$ (Definition 12.2) is a chain of activities from $i$ to exit; Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the system manager chooses a schedule $s\in\mathbb Z^J_+$ from a feasible set $S$ satisfying the packet-availability constraint $Bs\le z$ (the current buffer contents); $S$ is typically built (Section 12.2) from a link usage matrix $A$ and a set $C$ of feasible link configurations via $S_c := \{s : As\le c\}$ , $S := \bigcup_{c\in C} S_c$ . A Markovian control policy (Definition 12.3, Eq. 12.8) chooses $s(\tau) = f(Z(\tau-1), U(\tau))$ from the current buffer contents and an independent randomization variable; it is admissible if it never overdraws a buffer, and stable if the resulting discrete-time Markov chain $Z$ is irreducible and positive recurrent.

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

If the DTMC $Z$ under a Markovian policy $f$ is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then $Z$ is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.

Supporting milestones

Propositions 12.6-12.7 characterize the convex hulls $\langle S_c\rangle$ and $\langle S\rangle$ as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.

Significance

The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."

Formalizing it. A live prior-art check (GET /theorems?q=packet+network, q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent predicate for Markov chains, found a representationally distinct formalization (a row-function transition kernel rather than this series' own PMF-based jump-chain convention); this mission restates positive recurrence and irreducibility locally instead, consistent with every mission in this series since mission I. Everything else — the packet network model, schedules and configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit apparatus — is formalized from scratch.

Difficulty

The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all $\omega$ " quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an $\omega\in\Omega_1$ " rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope $\{Ax\le c\}$ — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.

Formalization scope

Classes, activities, links, schedules and configurations are represented via Fin-indexed types throughout; S and C are taken as Finsets (every worked example in the book has finitely many configurations, and the link usage matrix's single-1-per-column structure bounds each schedule component, so this is a genuine, if implicit, standing feature of the model rather than an added restriction). IsScheduleSetAt/IsScheduleSet characterize $S_c$ / $S$ via an ↔ against the underlying capacity constraint, rather than constructing them, matching how set-valued model data is handled elsewhere in this series. The formalization does not admit a trivializing reading: the ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality ( $A\hat s < \hat c$ ) exactly as Eq. 12.24 requires, not weakened to $\le$ . Contributions completing the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized- schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own Theorem 6.5 proof, adapted to discrete time).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

14 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XIII: Back-Pressure Control for Packet NetworksTextbook

Motivation

Mission XII (12-packet-networks-model) built the discrete-time, slotted packet-network model from scratch and proved the chapter's own version of the fluid-to-stochastic stability bridge (Theorem 12.10). That result is only useful once paired with an actual control policy whose fluid model can be shown stable. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly such a policy in Sections 12.4-12.5: back-pressure control (called max-weight when the network is single-hop), a rule that has become the default choice in the switching and wireless-scheduling literature because it requires no advance knowledge of arrival rates and achieves the largest possible stability region. This mission formalizes back-pressure control for the discrete-time packet network model and proves it maximally stable — the chapter's own counterpart to mission VIII's continuous-time Theorem 9.12.

Setting

At the start of each timeslot, having observed the current buffer contents $z$ , the max-weight/ back-pressure (MW/BP) policy solves $\max_{s\in S(z)} z\cdot Rs$ (Eq. 12.41), where $S(z) := \{s\in S : Bs\le z\}$ restricts the schedule set $S$ (mission XII) to what is actually available given $z$ . Equivalently (Eq. 12.42-12.43), writing $w_j(z) := z_{u(j)} - z_{d(j)}$ (with $z_0 := 0$ ) for the "weight" of activity $j$ , the policy maximizes $\sum_j w_j(z) s_j$ — the schedule that clears the most "backlog pressure" per timeslot. The policy is deterministic (no randomization variable is needed, since (12.41) is a genuine optimization problem, not one that inherently requires randomized tie-breaking).

Formalization targets

Goal: Theorem 12.16 — aperiodicity, irreducibility, and conditional positive recurrence

Consider a packet network satisfying (12.1) and Assumption 12.1, operating under back-pressure control. The DTMC $Z$ is aperiodic and irreducible unconditionally. If the stability condition (12.26) — the existence of $\hat s\in\langle S\rangle$ with $\lambda < R\hat s$ — is additionally satisfied, $Z$ is positive recurrent. This is the mission's headline result, and it packages both a structural fact (irreducibility/aperiodicity, needed regardless of load) and a conditional stability fact (positive recurrence, needed only under (12.26)) in one theorem.

Supporting milestones

Lemma 12.17 shows the optimization problem (12.41) always has a nonzero solution whenever the network is nonempty — the fact that back-pressure never "idles unnecessarily," which Lemma 12.18 uses to show every state can reach the empty state (hence irreducibility) and that state $0$ has period $1$ (hence aperiodicity, via (12.1)'s own assumption that no external arrivals is possible with positive probability). Lemma 12.20 is the back-pressure fluid equation (12.44), the discrete-time analog of mission VIII's Theorem 9.8: at each regular point, the fluid-scaled buffer content dotted with the fluid departure rate equals the maximum of that same dot product over the convex hull of the schedule set. Lemma 12.21 shows this fluid model is stable whenever (12.26) holds, via an explicit quadratic Lyapunov function.

Significance

The result itself. Theorem 12.16 shows that back-pressure control — a rule requiring no knowledge of arrival rates, computed fresh from the current buffer contents every timeslot — is maximally stable: combined with Theorem 12.8 and Proposition 12.9 (mission XII), it stabilizes every packet network arrival-rate vector that any policy could possibly stabilize. This is the discrete-time, slotted analog of mission VIII's Theorem 9.12, and the two proofs share their essential Lyapunov argument (the book's own text calls Lemma 12.21's proof "almost identical to that of Theorem 9.12"), even though the two chapters' back-pressure equations are built from different underlying objects — mission VIII's continuous-time allocation polytope versus this chapter's convex hull of a discrete schedule set.

Formalizing it. A live prior-art check (GET /theorems?q=back-pressure, q=max-weight) finds no relevant hits, matching mission VIII's own finding for the continuous-time version. This mission formalizes the back-pressure optimization problem and policy, the back-pressure fluid equation, and its stability from scratch, restating (per this series' convention for concurrently-drafted chunks sharing a sub-namespace) the minimal apparatus needed from mission XII: the packet network model, Assumption 12.1, the raw processes, fluid limit paths, the fluid equations (12.31)-(12.36), and the ambient-chain machinery, plus a new Aperiodic predicate this chunk needs that mission XII's own results do not.

Difficulty

The obvious approach to Lemma 12.20's back-pressure fluid equation — directly differentiate the discrete system equation — obscures the actual argument, which reduces a maximum over the (potentially non-polytope) discrete schedule set $S$ to a maximum over its convex hull $\langle S\rangle$ (justified because a linear functional on a compact polytope is maximized at an extreme point) and then shows that every schedule with a strictly smaller objective value than the maximizer contributes zero derivative to the usage-counting process $\hat T_s$ — the discrete-time analog of mission VIII's Lemmas 9.10-9.11. A second difficulty is connecting the maximum-over-a- finite-set at the fluid-scaled level to Definition 12.3's discrete, arrival-indexed back-pressure policy: this mission's own Lemma 12.20 item states the fluid-relevant consequence of the discrete policy as a documented hypothesis (mirroring mission XI's own scope decision for its structurally identical WWTA fluid equation) rather than re-deriving it from the raw stochastic recursion, which would require reconstructing infrastructure outside this chapter's own numbered results.

Formalization scope

The packet network model, Assumption 12.1, the raw processes, and the fluid-limit apparatus are restated verbatim from mission XII (12-packet-networks-model), since concurrently-drafted chunks sharing a sub-namespace do not import one another's Lean files. IsBPOptimal is phrased via domination over the feasible-at- $z$ schedule set, not sSup/argmax, per this series' junk-value-avoidance convention; the same convention is applied to the maximum over $\langle S\rangle$ in the back-pressure fluid equation. The formalization does not admit a trivializing reading: irreducibility and aperiodicity are the same non-vacuous renewal-theoretic notions used throughout this series (Aperiodic requires a genuine positive self-transition probability, not a vacuously-true condition), and the goal's positive-recurrence conjunct is genuinely conditional on (12.26), stated with the correct strict inequality rather than weakened to $\le$ . Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.17's hop-count induction and Lemma 12.20's extreme-point/zero-derivative argument (mirroring mission VIII's own Lemmas 9.10-9.11, adapted to discrete time).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

8 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XIV: Random Proportional Scheduling for Packet NetworksTextbook

Motivation

Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.

Setting

A packet network with fixed routing (Section 12.6) has I packet classes; each class i routes, after one hop of processing, deterministically to a single successor class or exits the network — encoded here as a function $\mathrm{route} : I \to I \cup \{\text{exit}\}$ . The K links are indexed by $\mathcal K$ , and a matrix $A$ assigns each class to the single link its next transfer uses; $\mathcal I(k)$ denotes the classes belonging to link $k$ . At the start of a timeslot, $z\in\mathbb Z^I_+$ is the vector of class-level packet counts and $y := Az$ the corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book): (a) solve the concave program $\psi(y) := \operatorname{argmax}\{\sum_k y_k\log(\hat c_k) : \hat c \in \langle C\rangle\}$ (Eq. 12.57), where $C$ is the finite set of feasible link configurations and $\langle C\rangle$ its convex hull; (b) randomize a link configuration $c$ with mean $\psi(y)$ ; (c) transfer $\min(c_k,y_k)$ packets over link $k$ ; (d) select which packets to transfer uniformly at random from each link's queue. This makes $Z=\{Z(\tau):\tau\in\mathbb Z_+\}$ a discrete-time Markov chain. The function $\psi$ is exactly the proportionally fair (PF) allocation function of Section 10.1, applied here with the link-level demand vector $y$ in place of the PF model's job-class demand vector.

Formalization targets

Goal: Theorem 12.28 — the load condition implies RPS stability

\rho < \hat c \text{ for some } \hat c \in \langle C\rangle, \quad \rho := A\alpha, \quad \alpha := R^{-1}\lambda \quad\Longrightarrow\quad \text{(a) the RPS fluid model is stable, and hence}

\text{(b) the discrete-time Markov chain } Z \text{ under RPS control is positive recurrent.}

Here $\lambda$ is the vector of external arrival rates, $\alpha$ the resulting vector of total (external plus internally routed) arrival rates into each class, and $R$ the input-output matrix determined by $\mathrm{route}$ . The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.

Supporting milestones

Lemma 12.23 is an almost-sure convergence result for a residual process $\xi^z_i(\tau) := \sum_{m=1}^\tau (s_i(m) - \hat s_i(m))$ tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to $(\hat Z_i(t)/\hat Y_k(t))\,\psi_k(\hat Y(t))$ . Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, $\langle C\rangle$ playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of $Z$ .

Significance

The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.

Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction: rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b) a direct instance of this mission's own Theorem 12.27. This is the payoff the whole proportional-fairness apparatus (missions IX-X) was built for.

Difficulty

The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a class-indexed process $\hat D_i(t)$ , while the chapter's own general fluid-equation machinery (Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own fixed-routing model, however, the book's remark that " $s(\tau)$ ... is an I-vector of actual packet transfers by class" (page 245) collapses this distinction: each class has a single associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4) already uses. Missing this identification is the natural way to get stuck restating Proposition 12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference sequences as an external fact rather than deriving it, so a faithful statement must commit to an explicit representation of "martingale difference sequence" (a filtration and Mathlib's Martingale predicate) even though no full measure-theoretic construction of the underlying probability space is attempted.

Formalization scope

Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's deterministic routing successor (none meaning exit), and the resulting input-output matrix $R$ and routing matrix $P$ are derived from it rather than taken as independent data (this chunk verifies $R = I - P^\top$ , the identity Proposition 12.26's reduction to the PF model relies on). The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated verbatim from mission IX, and the general packet-network fluid equations restated from mission XII, since concurrently-drafted chunks in this series never import one another's Lean files even within a shared sub-namespace. The formalization does not admit a trivializing reading: the load condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible configurations (not weakened to $\le$ or to a single configuration), RPSFluidStable quantifies over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is stated as a two-sided equivalence, not a one-directional inclusion that would understate "special case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit argument (mirroring mission XII's own Theorem 12.13 proof).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
N. S. Walton, "Concave switching in single and multihop networks," Queueing Systems 81 (2015), 265-299.
F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33-37.
W. Feller, An Introduction to Probability Theory and Its Applications, Volume II, 2nd edition, Wiley, 1971.

8 thms2 active usersReviewed

Analysis Operations Research Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 1: explicit Lipschitz bounds for the oblique reflection mapResearch Paper

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$ . Assume also $Q^k \to 0$ as $k\to\infty$ . With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$ , and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$ . For a path $x$ , $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$ , and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$ .

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).

The last condition says that $y_j$ increases only when $z_j = 0$ . In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$ , where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$ .

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$ ,

|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}

\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}

\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$ .

Milestones

Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$ .
$\gamma = \|Q^n\| < 1$ (p. 338).
Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$ , the factor $\gamma$ for $k\ge n$ , and $\pi_x^k(y_1)\to\psi(x)$ .
Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$ , the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$ .
Remark (2.1): for $n=1$ , $Q=0$ the bounds are attained.
Remark (2.2): for two queues in series, (2.10) gives modulus $2$ , while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$ ).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$ , $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$ . The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$ .

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$ , left limits on $(0,T]$ , and (redundantly) bounded on $[0,T]$ . The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$ . $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$ . Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$ . With $Q=0$ , $n=2$ , $T=1$ , $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$ , one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$ . The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$ , which is used throughout. In dimension one the two norms coincide.
(2.8) prints $\phi(x_1)-\phi(x_1)$ . The formalization states $\phi(x_1)-\phi(x_2)$ .
(2.2)–(2.3) print the index range $1\le j\le J$ . The dimension is $n$ .
$x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$ , so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$ , so this covers the positive scaling of Harrison and Reiman.
Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 2: jump-diffusion heavy-traffic limit for long up and down timesResearch Paper

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$ , while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$ . Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$ th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$ , and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$ , starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$ . With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$ .

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$ , $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$ .

A sequence of networks is indexed by $n$ . The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$ . Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$ . The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$ , with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$ , which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$ , through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$ , with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$ , $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$ , $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$ ,

(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).

Here $\hat Z=\phi(\hat X)$ , $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$ , with $Q=p$ and

\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$ . The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$ .
Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$ .
The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$ .

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$ , and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$ , jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$ , and a solution satisfies $Z\ge 0$ .

Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$ . Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
$M_1$ . Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$ ). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$ , so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$ , as in its proof. The map on p. 346 is read as $\phi(X)=Z$ , $\psi(X)=\operatorname{diag}(\mu)Y$ , following (4.13). The reflection map allows $y(0)\ge 0$ , because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$ ; when $x(0)\ge 0$ this agrees with (2.2).
Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$ . For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$ , while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$ , and the almost-sure core of the proof for $J=1$ .

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$ , and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$ , continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022

10 thms1 active userReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems I: Finite Horizon Optimality and Approximating SequencesTextbook

Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each $i \in S$ a finite nonempty action set $A_i$ ; a finite cost $C(i,a) \ge 0$ ; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$ . A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$ , and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ : it may use the whole history and may randomize. Stationary policies $f$ ( $f(i) \in A_i$ ) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ( $\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$ . A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$ . For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$ , the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$ . Its value functions are $v^N_{\alpha,n}$ . In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$ . Assumption FH( $\alpha$ , $n$ ) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$ . A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$ .

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$ ,

\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$ .

Milestones

Proposition A.1.1: a probability average of $u$ is at least $\min u$ , with equality iff the distribution is concentrated on the minimizers.
Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$ , and the characterization of all optimal general policies.
Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$ .
Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$ , have limit points.
Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH( $\alpha$ , $n$ ), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$ . This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$ , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$ , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$ ; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$ , which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$ ; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$ ).

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

14 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems II: The Discount Optimality EquationTextbook

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$ . A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ ; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$ .

Fix a discount factor $\alpha \in (0,1)$ . For an initial state $i$ and a policy $\theta$ , the $n$ -horizon cost with terminal cost zero and the infinite horizon discounted cost are

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ , infima over all policies. All of these lie in $[0,\infty]$ . A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$ . The discount optimality equation is

W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}

With $W = V_\alpha$ , $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$ .

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$ ; and every stationary policy $f_\alpha$ with

C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ( $v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$ ); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$ ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$ ); then, beyond the goal, Corollary 4.1.5 ( $\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$ ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$ ), Proposition 4.3.1 ( $v_{\alpha,n} \uparrow V_\alpha$ , and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$ . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$ , where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
All values ( $v_{\theta,\alpha,n}$ , $V_{\theta,\alpha}$ , $v_{\alpha,n}$ , $V_\alpha$ , and the competing solutions $W$ ) are ℝ≥0∞-valued; $0 \cdot \infty = 0$ . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
$V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$ , and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems III: Approximating Sequences for the Discounted Cost CriterionTextbook

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC( $\alpha$ ), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$ . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; nonnegative finite costs $C(i,a)$ ; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$ . A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$ . A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$ . Fix a discount factor $\alpha\in(0,1)$ . The discounted cost of $\theta$ and the discounted value function are

V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),

both in $[0,\infty]$ , the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$ , probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$ . The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$ , $r\notin S_N$ , according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$ : $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$ .

Assumption DC( $\alpha$ ): for every $i\in S$ , $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$ .

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$ ) is discount optimal for $\Delta$ .

Milestones

Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
Proposition 4.7.1: bounded costs imply DC( $\alpha$ ).
Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$ -step transition probabilities.
Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$ .
Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC( $\alpha$ ) holds.
Corollary 4.7.5: the case of a single distinguished state $z$ , with the relative form of the optimality equation for $\Delta_N$ .
Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$ , then $V^N_\alpha\le V_\alpha$ on $S_N$ .

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$ -valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$ , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$ -valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$ . The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$ ; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$ , a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$ . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$ ) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC( $\alpha$ ) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$ .

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IV: Average Cost Optimal Stationary Policies Exist for Finite State SpacesTextbook

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , a finite nonempty action set $A_i$ in each state $i$ , nonnegative finite costs $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$ . A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$ .

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$ , define

the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$ , and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ ;
the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$ ;
the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ , its $\liminf$ version $J^*_\theta(i)$ , and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$ .

All infima range over all general policies, and every quantity may equal $+\infty$ . A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$ , and average cost optimal if $J_\theta = J$ .

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$ , distinguished states $z_k \in R_k$ , and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$ , the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$ .

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$ , $f$ is average cost optimal, and

J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.

Milestones

Proposition 4.5.3. For finite $S$ and stationary $e$ , $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$ .
Proposition 6.1.1. For every policy on a countable state space,

J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$ , $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$ . 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$ ; monotonicity and left continuity of $V_\alpha$ ; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$ .

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$ , a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$ . Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$ , but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$ . Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
$V_{\theta,\alpha}$ , $V_\alpha$ , $v_{\theta,n}$ , $J_\theta$ , $J^*_\theta$ , $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ( $w_\alpha$ , $w$ , $w^*$ , equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
The objects of Section 6.3 ( $p_k$ , $m_{i|k}$ , $c_{i|k}$ , $\pi_s$ , $W_\alpha$ ) are defined from $f$ . The distinguished states are a hypothesis quantified over.
A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$ , or state rationality as an equation p/q without requiring $q \ne 0$ . Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$ , and the denominator is required to be nonzero on $(0,1)$ .

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$ -valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
D. Blackwell, "Discrete dynamic programming", Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

13 thms3 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VIII: Computing Average Cost Optimal Policies by Approximating SequencesTextbook

Motivation

Control problems for queueing systems (admission control, service rate control, routing to parallel servers) are naturally modelled as Markov decision chains whose state is a vector of queue lengths. The state space is therefore denumerably infinite, and the performance measure of interest is usually the long-run average cost per slot. For such models the existence theory of average cost optimal stationary policies is well developed (Chapter 7 of Sennott's book), but existence gives no algorithm: an optimal policy is a function on an infinite set, and value iteration cannot be run on an infinite state space.

The approximating sequence method answers this by replacing the infinite model $\Delta$ with a sequence of finite models $\Delta_N$ on truncated state spaces $S_N$ , solving the average cost optimality equation in each, and passing to the limit. Chapter 8 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) gives a set of conditions, the (AC) assumptions, under which this limit procedure provably produces the minimum average cost and an average cost optimal policy of $\Delta$ .

Timeline. The approximating sequence method for the average cost criterion and the (AC) assumptions were introduced in Sennott (1997a), with further results in Sennott (1997b) (bibliographic notes, p. 194). The book collects these results, adds the four step verification template (Proposition 8.2.1), the finite-set augmentation route based on the (BOR) assumptions (Proposition 8.2.3), and the weakening (WAC) of Section 8.7, which Chapter 9 uses.

Setting

An MDC $\Delta$ has a countable state space $S$ , a finite nonempty action set $A_i$ in each state $i$ , a finite cost $C(i,a)\ge0$ , and transition probabilities $P_{ij}(a)$ . A general policy $\theta$ chooses actions at random using the whole past history. Its average cost is

J_\theta(i)=\limsup_{n\to\infty}\frac1n\sum_{t=0}^{n-1}E_\theta[C(X_t,A_t)\mid X_0=i],

and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)\in[0,\infty]$ . A policy is average cost optimal if $J_\theta\equiv J$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite sets $S_N$ increasing to $S$ and MDCs $\Delta_N$ on $S_N$ with the same actions and costs and with transition probabilities $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ . Write $v^N_n$ and $V^N_\alpha$ for the $n$ -horizon and discounted value functions of $\Delta_N$ .

The (AC) assumptions are:

(AC1) there are finite constants $J^N$ and finite functions $r^N$ on $S_N$ with

J^N+r^N(i)=\min_a\Big\{C(i,a)+\sum_{j\in S_N}P_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N; \tag{8.1}

(AC2) $\limsup_N r^N(i)<\infty$ ;
(AC3) $\liminf_N r^N(i)\ge -Q$ for a constant $Q\ge0$ ;
(AC4) $J^*:=\limsup_N J^N<\infty$ and $J^*\le J(i)$ for all $i$ .

The (WAC) assumptions of Section 8.7 allow $Q$ to depend on the state, at the price of integrability conditions along every stationary policy.

Formalization targets

Goal: Theorem 8.1.1

Under (AC), the limit $\lim_{N\to\infty}J^N$ exists and

J(i)=\lim_{N\to\infty}J^N\qquad\text{for all } i\in S,

and every limit point $e^*$ of stationary policies $e^N$ realizing the minimum in (8.1) is average cost optimal for $\Delta$ . The statement fixes no constants; it asserts the shape of the conclusion for any model satisfying (AC).

Milestones

Proposition 8.2.1 (the four step template): unichain and aperiodicity of the finite models, an $x$ standard policy at which the approximating sequence is conforming, a comparison of $v^N_n$ (or $V^N_\alpha$ ) with $v_n$ (or $V_\alpha$ ), and a lower bound on $v^N_n - v^N_n(x)$ together imply that the value iteration limits

r^N(i)=\lim_{n\to\infty}\big(v^N_n(i)-v^N_n(x)\big)

exist and satisfy (AC).

Corollary 8.2.2: on $S=\{0,1,2,\dots\}$ with $S_N=\{0,\dots,N\}$ and excess probability sent to $N$ , monotonicity of $v^N_n$ , $v_n$ and of the first passage moments of a $0$ standard policy suffices.
Proposition 8.2.3: an augmentation type approximating sequence that sends excess probability to a finite set of cheap states satisfies the template.
Proposition 8.5.1: in the single-server queue with Bernoulli( $p$ ) arrivals and constant service rate $a>p$ ,

J_{d(a)}=\frac{Hp(1-p)}{a-p}+\frac{pC(a)}{a}.

Proposition 8.7.1: the conclusions of Theorem 8.1.1 hold under (WAC).

Significance

The result itself. Theorem 8.1.1 is what turns the existence theory of Chapter 7 into a computation. It certifies that the minimum average costs of the truncations converge to the minimum average cost of the infinite model, that this cost is constant, and that the policies produced by value iteration on $\Delta_N$ converge, along subsequences, to an optimal policy for $\Delta$ . Propositions 8.2.1–8.2.3 reduce (AC) to properties that can be checked model by model; Section 8.3 checks them for queues with reject option, service rate control, and routing to parallel queues. Proposition 8.7.1 is the version used in Chapter 9 for models whose relative values are not uniformly bounded below. Proposition 8.5.1 gives the closed-form open-loop benchmark used in the numerical study of Section 8.5.

Formalizing it. All results are proved in the book; none has a machine-checked proof. A formalization would give the first verified convergence theorem for truncations of denumerable-state average cost MDPs, and would make the approximating sequence method usable as a certified reduction from infinite to finite models. The template results (8.2.1–8.2.3) additionally require a formal treatment of conformity of approximating Markov chains (Appendix C.4–C.5), which is of independent use.

Difficulty

The naive argument takes limits in (8.1) along $N$ : the minimum over $a$ and the finite sums pass to the limit only in the inequality direction, and only after a Fatou-type lemma for sums against the converging distributions $P_{ij}(a;N)$ with integrands $r^N$ that are neither bounded nor monotone. The lower bound $-Q$ in (AC3) is exactly what makes this possible; without it the limit inequality can fail. The limit inequality then produces only an average cost optimality inequality, and turning it into optimality of the limit policy requires a separate argument that a function bounded below and satisfying the inequality yields an upper bound on the average cost. Existence of $\lim_N J^N$ is not given: (AC4) controls only the limit superior, and the limit must be identified through every subsequence. For the template results, the difficulty is in the Markov chain side: the convergence of first passage times and costs of the truncated chains, which fails for general approximating sequences (Examples C.4.4, C.4.7).

Formalization scope

The Lean development is in the namespace SennottDP.AvgASM. The state space is any countable type; action sets are Finsets, assumed nonempty; costs are finite and nonnegative (ℝ≥0); transition probabilities are ℝ≥0∞-valued, with each row a probability distribution for admissible actions. All value functions and average costs take values in $[0,\infty]$ (ℝ≥0∞), and every infimum over policies ranges over the full class of history-dependent randomized policies. The $J^N$ and $r^N$ of (AC1) are real; the limits superior and inferior over $N$ in (AC2)–(AC4) and (WAC) are taken in EReal, so an unbounded sequence cannot produce a junk finite value. The equality $J(i)=\lim_N J^N$ is stated in EReal, which also asserts that $J(i)$ is finite. Quantities of $\Delta_N$ at states outside $S_N$ are junk values that affect only finitely many $N$ for each state.

A trivializing formalization is ruled out: $J^N$ and $r^N$ are the witnesses of (AC1), not free variables, the policies $e^N$ must realize the minimum in (8.1) for those witnesses, and the minimum average cost $J$ is an infimum over all policies, so the goal cannot be satisfied by choosing $J^*$ or the limit policy.

A complete development needs: the induced process law of a general policy; the average cost optimality inequality argument (Lemma 7.2.1); the finite-state average cost results of Chapter 6 (Propositions 6.4.1, 6.5.1, 6.6.3); a Fatou lemma for converging distributions (Proposition A.2.5); limit points of policy sequences (Proposition B.5); and, for the template results, the theory of $z$ standard chains and conformity (Appendix C.2–C.5). The Markov chain layer and the approximating sequence definitions are reusable beyond this mission. Contributions of any of these intermediate results as separate theorems are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997), 114–137 (cited as Sennott (1997a) in the book).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR — Mathematical Methods of Operations Research 45 (1997), 45–62 (cited as Sennott (1997b) in the book).

14 thms3 active users

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IX: Bounded Mean Residual Lifetimes Imply Finite Moments of All OrdersTextbook

Motivation

In a discrete-time queue the service of a customer lasts a random number $Y$ of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted $s$ slots and is not yet finished. The relevant random quantity is then the residual life $Y_s$ : the remaining service time given that $s$ slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on $Y$ and on the residual lives $Y_s$ .

Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where $Y$ is the lifetime of a component and $E[Y_s]$ is its expected remaining lifetime at age $s$ . This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.

Setting

Let $Y$ be a random variable with values in $\{1,2,3,\dots\}$ and distribution $u_y = P(Y = y)$ , $y \ge 1$ . Write $F(y) = P(Y \le y)$ and $F^*(y) = P(Y > y) = 1 - F(y)$ for $y \ge 0$ , so $F(0) = 0$ and $F^*(0) = 1$ . The $k$ -th moment is

E[Y^k] = \sum_{y \ge 1} y^k u_y \in [0,\infty].

For $s \ge 0$ with $F^*(s) > 0$ , the residual life $Y_s$ has distribution

P(Y_s = y) = P(Y = s + y \mid Y > s) = \frac{u_{s+y}}{F^*(s)}, \qquad y \ge 1,

with $Y_0 = Y$ ; its tail is $F^*_s(y) = F^*(s+y)/F^*(s)$ , and $E[Y_s]$ is the mean residual lifetime.

The distribution of $Y$ has bounded mean residual lifetimes (BMRL- $U$ , Definition 9.2.4) if there is a finite constant $U$ with

E[Y_s] \le U \qquad \text{for every } s \ge 0 \text{ with } F^*(s) > 0,

and it is BMRL if it is BMRL- $U$ for some $U$ .

Three families appear by name: the geometric distribution $\mathrm{geo}(\mu)$ of the number of Bernoulli( $\mu$ ) trials to the first success, $P(Y=y) = \mu(1-\mu)^{y-1}$ ; the negative binomial $\mathrm{neg\,bin}(\mu, r)$ of the number of trials to the $r$ -th success, $P(Y = y) = \binom{y-1}{r-1}\mu^r(1-\mu)^{y-r}$ for $y \ge r$ ; and the truncated Poisson $\mathrm{trun\,Pois}(\lambda)$ , $P(Y=y) = \frac{e^{-\lambda}}{1-e^{-\lambda}}\frac{\lambda^y}{y!}$ for $y \ge 1$ .

For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes $X_1, X_2, \dots$ are independent with common distribution $p_j$ , mean $\lambda = \sum_j j p_j$ and second moment $\lambda^{(2)} = \sum_j j^2 p_j$ , and $X(s) = X_1 + \dots + X_s$ is the number of arrivals in $s$ slots.

Formalization targets

Goal: Proposition 9.2.5

If the distribution of $Y$ is BMRL, then

E[Y^k] < \infty \qquad \text{for every } k.

The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of $Y$ to be finite.

Milestones

Proposition 9.2.1. $E[Y] = \sum_{y=0}^\infty F^*(y)$ and, for $k \ge 2$ ,

E[Y^k] = 1 + \sum_{z=0}^{k-1}\binom{k}{z}\left[\sum_{y=1}^\infty y^z F^*(y)\right]. \tag{9.4}

Remark 9.2.2. For $k \ge 2$ , $E[Y^k] < \infty$ if and only if $\sum_y y^{k-1}F^*(y) < \infty$ .
Proposition 9.2.3. For a positive integer $k$ , $E[Y^k] < \infty$ implies $E[Y_s^k] < \infty$ for all $s \ge 0$ .
Proposition 9.2.6. The geometric ( $0<\mu<1$ ), negative binomial ( $0<\mu<1$ , $r \ge 2$ ) and truncated Poisson ( $\lambda > 0$ ) distributions are BMRL.
Lemma 9.5.2. Under $\lambda^{(2)} < \infty$ ,

E[X(s)] = \lambda s, \qquad E[(X(s))^2] = \lambda^{(2)}s + \lambda^2 s(s-1). \tag{9.25}

Significance

The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on $\{1,2,\dots\}$ have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).

Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of $\mathbb N$ -valued random variables in $[0,\infty]$ , a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.

Difficulty

BMRL controls only first moments, of the conditional laws $Y_s$ ; the goal asks for moments of every order of $Y$ itself. Bounding $E[Y^k]$ by expanding $E[Y_s]$ for each fixed $s$ gives nothing, because each single bound is compatible with a heavy tail: the uniformity in $s$ is essential. The residual lives are also only defined where $P(Y > s) > 0$ , so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.

Formalization scope

$Y$ is represented by its law, a function $u : \mathbb N \to [0,\infty]$ with $\sum_y u_y = 1$ and $u_0 = 0$ (IsDistOnPos). $F^*$ , moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is $+\infty$ and "finite" means $< \infty$ . No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.
The residual life $Y_s$ is defined by (9.7) and is used only where $F^*(s) > 0$ ; BMRL- $U$ is required exactly at those $s$ , and $U$ is a finite nonnegative real. A formalization requiring the bound at every $s$ with a junk value of $E[Y_s]$ where $F^*(s) = 0$ is ruled out: the definitions never divide by $F^*(s) = 0$ in a used position, and bounded distributions remain BMRL.
The geometric and negative binomial laws count trials (support starting at $1$ and $r$ ), not failures as Mathlib's geometricPMF does.
Lemma 9.5.2 is stated on a probability space with measurable, mutually independent (iIndepFun) batch sizes of common law $p$ , expectations as lower Lebesgue integrals, and only assumption (BA1), $\lambda^{(2)} < \infty$ , which is the part of the book's (BA) that concerns arrivals.
Welcome contributions: the tail-sum identity (9.4) and its reindexing lemmas, the residual-life tail formula (9.8) and moment formula (9.9), each as a separate lemma; and proofs that the three named families are probability distributions on their supports.

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Section 9.2 (pp. 202–206) and Section 9.5 (pp. 214–215). DOI 10.1002/9780470317037
Moshe Shaked and J. George Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Section 2.A (the mean residual life order). DOI 10.1007/978-0-387-34675-5

8 thms3 active usersReviewed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems X: Average Cost Optimization of Continuous Time Markov Decision ChainsTextbook

Motivation

Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.

This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.

Setting

A random variable $X$ has the exponential distribution with rate $\mu>0$ if $P(X\le t)=1-e^{-\mu t}$ for $t\ge0$ . A function $r(\delta)$ is $o(\delta)$ if $r(\delta)/\delta\to0$ as $\delta\to0^+$ .

A continuous time Markov decision chain (CTMDC) $\Psi$ has a countable state space $S$ and, for each $i\in S$ , a finite nonempty action set $A_i$ . Choosing $a\in A_i$ in state $i$ incurs an instantaneous cost $G(i,a)\ge0$ and a cost rate $g(i,a)\ge0$ in effect until the next transition. The time until the next transition is exponential with rate $\nu(i,a)>0$ , so its mean is $\tau(i,a)=1/\nu(i,a)$ ; the next state is $j$ with probability $P_{ij}(a)$ , where $P_{ii}(a)=0$ . A policy $\theta$ chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy $e$ chooses $e(i)$ in state $i$ . With $C_n$ the cost and $T_n$ the time of the first $n$ transition periods, the average cost and the minimum average cost are

J^\Psi_\theta(i)=\limsup_{n\to\infty}\frac{E_\theta[C_n\mid X_0=i]}{E_\theta[T_n\mid X_0=i]},\qquad J^\Psi(i)=\inf_\theta J^\Psi_\theta(i).

Assumption (CTB) requires constants $\tau$ and $B$ with $0<\tau<\inf_{i,a}\tau(i,a)\le\sup_{i,a}\tau(i,a)\le B<\infty$ . The auxiliary MDC $\Delta$ has the same states and actions, costs $C(i,a)=G(i,a)\nu(i,a)+g(i,a)$ , and transition probabilities $P^*_{ij}(a)=\tau\nu(i,a)P_{ij}(a)$ for $j\ne i$ , $P^*_{ii}(a)=1-\tau\nu(i,a)$ . Its average cost $J^\Delta_\theta(i)=\limsup_n n^{-1}\sum_{t<n}E_\theta[C(X_t,Y_t)]$ and minimum average cost $J^\Delta(i)$ are those of Chapter 2. Assumption (CTAC) is $J^\Delta(\cdot)\le J^\Psi(\cdot)$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ for $\Delta$ uses finite state spaces $S_N$ increasing to $S$ and transition probabilities $P^*_{ij}(a;N)$ on $S_N$ converging to $P^*_{ij}(a)$ . The (AC) assumptions ask for constants $J^N$ and functions $r^N$ on $S_N$ solving

J^N+r^N(i)=\min_{a\in A_i}\Big\{C(i,a)+\sum_{j\in S_N}P^*_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N,\ N\ge N_0,\tag{10.21}

with $\limsup_N r^N(i)<\infty$ , $\liminf_N r^N(i)\ge-Q$ for a constant $Q\ge0$ , and $\limsup_N J^N=:J^*<\infty$ , $J^*\le J^\Delta(i)$ .

Formalization targets

Goal: Theorem 10.3.3

Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of $\Delta$ :

J^*=\lim_{N\to\infty}J^N\ \text{exists and}\ J^\Delta(i)=J^\Psi(i)=J^*\quad(i\in S),

and every limit point $e^*$ of a sequence $e^N$ of stationary policies realizing the minimum in (10.21) satisfies $J^\Delta_{e^*}=J^\Delta$ and $J^\Psi_{e^*}=J^\Psi$ . The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.

Milestones

Proposition 10.1.2: $P(X>x+y\mid X>y)=P(X>x)$ for $x,y>0$ , and $P(X\le\delta)=\mu\delta+o(\delta)$ .
Proposition 10.1.3: for independent exponentials, $P(X_1\le\delta,X_2\le\delta)=o(\delta)$ , $P(X_1<X_2)=\mu_1/(\mu_1+\mu_2)$ , and $\min(X_1,X_2)$ is exponential with rate $\mu_1+\mu_2$ .
Lemma 10.3.1: if $z$ is bounded below and $Z\tau(i,e)+z(i)\ge G(i,e)+g(i,e)\tau(i,e)+\sum_jP_{ij}(e)z(j)$ for all $i$ (10.15), then $J^\Psi_e\le Z$ .
Lemma 10.3.2: $(Z,w)$ satisfies $Z+w(i)\ge C(i,e)+\sum_jP^*_{ij}(e)w(j)$ (10.20) if and only if $(Z,\tau w)$ satisfies (10.15).
Proposition 10.4.1: in the M/M/1 queue with arrival rate $\lambda$ , holding cost $H(i)=Hi$ and service cost rate $c(a)$ , the policy that always serves at rate $a>\lambda$ has average cost $\rho_ac(a)+H\rho_a/(1-\rho_a)$ , $\rho_a=\lambda/a$ .

Significance

The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.

The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.

Difficulty

The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for $\Delta$ may change action in every time slot, including slots where the state does not change, while a policy for $\Psi$ acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound $J^\Psi\ge J^*$ therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point $e^*$ to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function $z$ is only bounded below, so the telescoping of expectations must be justified without integrability of $z$ from above.

Formalization scope

The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with $P_{ii}(a)=0$ ) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions $z,w,r^N$ are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so $+\infty$ is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of $n$ transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from $P_{i\cdot}(a)$ ; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality $\tau<\inf\tau(i,a)$ of (CTB) is kept strict (as a positive margin); weakening it to $\le$ would make $P^*_{ii}(a)$ vanish or turn negative.

The average cost $J^\Psi_\theta$ is a ratio of expectations, not the expectation of a ratio, and the infimum $J^\Psi$ ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.

A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, 1994. https://doi.org/10.1002/9780470316887
S. A. Lippman, Applying a new device in the optimization of exponential queuing systems, Operations Research 23(4), 687–710, 1975. https://doi.org/10.1287/opre.23.4.687
D. Gross and C. M. Harris, Fundamentals of Queueing Theory, 3rd ed., John Wiley & Sons, 1998.

11 thms3 active users

Completed

Analysis Probability·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XI: The Generalized Dominated Convergence Theorem for Approximating DistributionsTextbook

Motivation

Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) studies Markov decision chains with countably many states, finite action sets and unbounded nonnegative costs. Its main computational device, the approximating sequence method (Definition 2.5.1, p. 28), replaces the countable state space $S$ by an increasing sequence of state spaces $S_N$ and the transition law out of each state by distributions $P_j(N)$ on $S_N$ that converge pointwise to the original law. Every convergence argument of that method has the same shape: a sum $\sum_{j\in S_N} P_j(N)\,u(j,N)$ , an expected cost or value under the $N$ -th approximating model, must be shown to converge to $\sum_{j\in S} P_j\,u(j)$ , or at least to satisfy a one-sided bound in the limit.

Appendix A, Sections A.1–A.2 (pp. 270–278), collects the analysis results used for this. The author proves them for sums over countable sets rather than general integrals, so they need no measure theory, and the proofs of the discounted-cost and average-cost approximation theorems (Chapters 4 and 8) cite them. This mission formalizes that appendix section as a self-contained unit.

Setting

Let $S$ be a countable set and $(P_j)_{j\in S}$ a probability distribution on $S$ : $P_j\ge 0$ and $\sum_j P_j=1$ . Values of functions are extended reals in $[-\infty,\infty]$ , with the convention $0\cdot\infty=0$ . For $u:S\to[-\infty,\infty]$ , the weighted sum is

\sum_{j\in S}P_j\,u(j)=\sum_{j\in S}P_j\,u^+(j)-\sum_{j\in S}P_j\,u^-(j),

which is well defined, in $(-\infty,\infty]$ , whenever the negative parts have finite weighted sum. In Lean this is wsum P u.

A family of approximating distributions for $(P_j)$ consists of

an increasing sequence of subsets $S_0\subseteq S_1\subseteq\cdots$ of $S$ with $\bigcup_N S_N=S$ ;
for each $N$ , a probability distribution $(P_j(N))_{j\in S_N}$ on $S_N$ ;
pointwise convergence $\lim_{N\to\infty}P_j(N)=P_j$ for every $j\in S$ .

Since the sets increase to $S$ , a fixed state $j$ lies in $S_N$ for every large $N$ , so $\liminf_N u(j,N)$ and $\lim_N u(j,N)$ make sense for a function $u(j,N)$ defined only for $j\in S_N$ . In Lean these three conditions are the structure ApproxDist P SN Q, with Q N j $=P_j(N)$ .

Formalization targets

Goal: Theorem A.2.6 (Generalized Dominated Convergence Theorem), p. 278

Under the approximating-distribution hypotheses, let $u(j,N)$ and $w(j,N)$ be finite with $|u(j,N)|\le w(j,N)$ for $j\in S_N$ , let $u(j,N)\to u(j)$ and $w(j,N)\to w(j)$ for every $j$ , and assume

\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,w(j,N)=\sum_{j\in S}P_j\,w(j)<\infty.

Then

\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)=\sum_{j\in S}P_j\,u(j).

Milestones, in the book's order

Proposition A.1.3: $\liminf$ commutes with a minimum over a finite nonempty set; $\lim$ does too when all limits exist.
Proposition A.1.5: $\liminf_N\sum_{j\in G}u(j,N)\ge\sum_{j\in G}\liminf_N u(j,N)$ for finite $G$ and $u>-\infty$ , when the right side has no indeterminate form.
Proposition A.1.7: the same inequality for countable sums of $[0,\infty]$ -valued terms.
Proposition A.1.8: the same, with the left sum over $S_N$ increasing to $S$ .
Proposition A.1.10: $\liminf u_n\le\liminf w_n/n\le\limsup w_n/n\le\limsup u_n$ for $w_n=\sum_{k<n}u_k$ .
Proposition A.2.1 (Fatou's lemma): $\liminf_N\sum_jP_j u(j,N)\ge\sum_jP_j\liminf_N u(j,N)$ for $u\ge -L$ .
Theorem A.2.3 (dominated convergence, with a convergent dominating sequence $w(j,N)$ ) and Corollary A.2.4 (fixed dominating function).
Proposition A.2.5 (generalized Fatou's lemma):

\liminf_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)\ \ge\ \sum_{j\in S}P_j\,\liminf_{N\to\infty}u(j,N)\qquad(u\ge -L\text{ on }S_N).

Corollary A.2.7: bounded convergence under approximating distributions.

Significance

The results. Proposition A.2.5 and Theorem A.2.6 are the two limit interchanges the approximating sequence method needs. The generalized Fatou inequality gives the lower bound on limits of value functions of the approximating models, and the generalized dominated convergence theorem identifies the limit of expected costs when a dominating function is available. Corollary A.2.7 gives the bounded case, and Proposition A.1.3 moves limits inside the minimization of an optimality equation. Proposition A.1.10 compares Cesàro averages with the sequence itself, which the average-cost chapters use.

Formalizing them. All statements are classical and proved in the book. A.1.7, A.2.1, A.2.3 and A.2.4 are, after translation, instances of Mathlib's Fatou lemma (MeasureTheory.lintegral_liminf_le) and dominated convergence theorem for a discrete measure. The mission states them in the book's discrete, extended-real form so later chapters can cite them by number. The versions in which the distribution and its support change with $N$ (A.2.5–A.2.7) are not in Mathlib in this form; the generalized dominated convergence theorem appears in the measure-theoretic literature (Royden, Real Analysis, Ch. 4) but has no Lean formalization. None of these statements has been formalized for this book.

Difficulty

For the generalized results, Mathlib's Fatou lemma and dominated convergence theorem do not apply directly: they fix one measure, while here both the weights $P_j(N)$ and the support $S_N$ change with $N$ . The dominating function $w(j,N)$ also changes with $N$ and is not integrable uniformly in $N$ ; only the convergence of its expectations is assumed. For small $N$ , $\sum_{j\in S_N}P_j(N)w(j,N)$ may even be infinite, and then $\sum_{j\in S_N} P_j(N)u(j,N)$ has no value.

A second difficulty is bookkeeping in the extended reals. Lower limits may be $\pm\infty$ , products use $0\cdot\infty=0$ , and a sum with a $+\infty$ term and a $-\infty$ term is undefined. The inequality of Proposition A.1.5 holds only when that indeterminate form is excluded. The bound $u\ge -L$ in A.2.1 and A.2.5 cannot be dropped: Examples A.1.9 and A.2.2 of the book show the inequalities fail without it.

Formalization scope

Types. $S$ is any type with [Countable S]. Probabilities are ℝ≥0∞-valued with ∑' j, P j = 1, and $P_j(N)$ is Q N j. Extended-real values are EReal, and nonnegative extended values (A.1.7, A.1.8) are ℝ≥0∞. Limits and lower and upper limits are along atTop in ℕ. The book's $N\ge N_0$ convention (Remark A.1.2) needs nothing extra, since only large $N$ matter.
Sums over $S_N$ are sums over $S$ of (SN N).indicator (Q N) times the function. Values of $u(j,N)$ and $P_j(N)$ for $j\notin S_N$ never enter any statement, and the hypotheses on $u$ ( $u\ge -L$ , $|u|\le w$ ) are imposed only on $S_N$ , as in the book.
Weighted sums are wsum, the difference of the weighted positive and negative parts, each in [0,∞]. When both are infinite the book's sum is undefined and wsum returns $-\infty$ . Every sum used in a hypothesis or conclusion is defined, except possibly for finitely many $N$ in limit statements, where it does not matter.
Limits of $u(j,N)$ and $w(j,N)$ are taken in EReal, since the book allows extended-real limits (p. 271). The hypotheses force them to be finite wherever $P_j>0$ .
Ruled out. Statements in which wsum returns its junk value $-\infty$ could make an inequality trivial. Every left-hand side here is a lower limit of sums whose negative parts are bounded, or a limit of eventually defined sums, so no statement holds only because of that junk value. Real-valued tsum with its junk value $0$ is not used anywhere.
Welcome contributions. A proof of A.1.7 from lintegral_liminf_le for the counting measure, and lemmas relating wsum to Mathlib's tsum and to integrals against Measure.sum (fun j => P j • dirac j), can be reused by the other missions of this series.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Appendix A, pp. 270–278. https://doi.org/10.1002/9780470317037
H. L. Royden, Real Analysis, 3rd ed., Macmillan, 1988, Chapter 4 (Fatou's lemma, generalized Lebesgue convergence theorem).
The Mathlib Community, The Lean Mathematical Library, CPP 2020, https://doi.org/10.1145/3372885.3373824 (MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence).

12 thms3 active usersReviewed

Completed

Analysis Probability·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XII: A Tauberian Theorem Linking Abel and Cesàro Means of Nonnegative SeriesTextbook

Motivation

In the theory of Markov decision chains two cost criteria dominate: the discounted cost, in which a cost incurred at time $n$ is weighted by $\alpha^n$ for a discount factor $\alpha \in (0,1)$ , and the average cost, the long-run cost per unit time. A standard route to average cost optimal policies is to solve the discounted problem and let $\alpha \to 1^-$ . That route needs a precise link between the two criteria for a single sequence of expected costs $u_0, u_1, u_2, \dots \ge 0$ : the discounted cost multiplied by $1-\alpha$ on one side, the running average on the other. Appendix A.4 of Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) supplies this link as Theorem A.4.2, and the book invokes it whenever it passes from discounted to average cost (for instance in Chapter 6, where it is applied to $u_n = E_\theta[C(X_n, A_n)]$ ).

The result belongs to classical summability theory.

Abelian direction. Convergence of averages implies convergence of the power-series (Abel) means: a consequence of Abel's and Frobenius's theorems on power series (19th century).
Tauber (1897). The first converse, under a growth condition on the terms.
Hardy and Littlewood (1914). The converse for Cesàro means of nonnegative terms, the "Hardy–Littlewood Tauberian theorem".
Karamata (1930). A short proof of that converse by polynomial approximation, reproduced in Titchmarsh, The Theory of Functions (1939, pp. 227–229). The book follows this proof.
Widder (1941). The continuous-time (Laplace transform) version.
Sennott (1986b). A proof of the discrete statement, cited by the book as its source for Theorem A.4.2.

Setting

Let $u_0, u_1, u_2, \dots$ be nonnegative terms $u_n \in [0, \infty]$ with $u_0 < \infty$ . For $\alpha \in [0, \infty)$ the power series

U(\alpha) = \sum_{n=0}^{\infty} \alpha^n u_n \in [0, \infty]

always has a sum, possibly $+\infty$ , because its partial sums increase. Its radius of convergence is $R = (\limsup_{n} u_n^{1/n})^{-1} \in [0,\infty]$ . The partial sums are $w_n = \sum_{k=0}^{n-1} u_k$ for $n \ge 1$ . Two ways of averaging the sequence are compared:

the Cesàro means $w_n / n$ , as $n \to \infty$ ;
the Abel means $(1-\alpha) U(\alpha)$ , as $\alpha \to 1^-$ (from below).

For the constant sequence $u_n \equiv B$ both equal $B$ . In the Lean development these are U, radius, w, cesaroMean and abelMean in the namespace SennottDP.Tauberian, all valued in ℝ≥0∞. The proof also uses the function $r$ of Fig. A.1, equal to $0$ on $(0, e^{-1})$ and to $1/x$ on $[e^{-1}, 1)$ .

Formalization targets

Goal: Theorem A.4.2

\liminf_{n\to\infty} \frac{w_n}{n} \le \liminf_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{n\to\infty} \frac{w_n}{n}, \tag{A.28}

and the following are equivalent: (i) all terms in (A.28) are equal and finite; (ii) $\lim_n w_n/n$ exists and is finite; (iii) $\lim_{\alpha \to 1^-} (1-\alpha)U(\alpha)$ exists and is finite.

No growth or boundedness condition on $u_n$ is assumed: nonnegativity is the only Tauberian condition.

Milestones

Remark A.3.3: the geometric series. $R = 1$ , $U(\alpha) = B/(1-\alpha)$ and $B\sum_n n\alpha^n = B\alpha/(1-\alpha)^2$ .
Remark A.3.1: inside the radius of convergence, $U$ is differentiable term by term, and the derived series has the same radius.
Eq. (A.31): $\big(\sum \alpha^n\big) U(\alpha) = \sum_n \alpha^n w_{n+1} = U(\alpha)/(1-\alpha)$ .
Eq. (A.28): the Abelian inequalities on their own.
Eq. (A.26): $\int_0^1 r = 1$ .
Lemma A.4.1: continuous $s^* \le r \le s$ with integrals within $\varepsilon$ of $1$ .
Eqs. (A.35)–(A.36): if the Abel means tend to $L < \infty$ , then $(1-\alpha)\sum_n \alpha^n u_n f(\alpha^n) \to L\int_0^1 f$ for $f(x) = x^k$ .
The same statement for every $f$ continuous on $[0,1]$ .
The same statement for $f = r$ .
Example A.5.1: a $0/1$ block sequence with $\liminf w_n/n = 1/2$ and $\limsup w_n/n = 2/3$ (Choice One) or $1$ (Choice Two), for which the middle inequality of (A.28) is strict.

Significance

The result itself. Theorem A.4.2 lets every statement about $\lim_{\alpha\to1^-}(1-\alpha)V_\alpha$ for a discounted value be read as a statement about long-run average cost, and conversely. The strict cases of Example A.5.1 show why the book must work with $\liminf$ and $\limsup$ rather than limits: average costs of policies need not exist as limits, even for bounded costs.

Formalizing it. Mathlib contains Abel's theorem for convergent series (Mathlib/Analysis/Complex/AbelLimit.lean) and Cesàro convergence of convergent sequences, but no Tauberian theorem. The pinned checkout has no file mentioning "Tauberian", and neither does the platform. The mathematics has been proved since 1914. Formalizing it here adds:

a machine-checked Hardy–Littlewood–Karamata theorem for nonnegative $[0,\infty]$ -valued sequences;
the $\liminf$ / $\limsup$ comparison (A.28) with infinite values allowed;
a reusable component for the average cost chapters of this series.

Difficulty

The Abelian inequalities (A.28) follow from rearranging the series. The converse (iii) ⇒ (ii) does not: the first idea, recovering $w_n/n$ from $(1-\alpha)U(\alpha)$ at $\alpha = 1 - 1/n$ , fails, because knowing $U$ near $1$ controls only weighted averages of all the $u_k$ , not a sharp truncation. Some positivity argument is unavoidable, since the converse fails for signed sequences (for example $u_n = (-1)^n n$ ). The sharp truncation at $n \approx (-\ln\alpha)^{-1}$ corresponds to the discontinuous weight $r$ . Passing from polynomial weights to the jump function $r$ requires uniform approximation together with the nonnegativity of the $u_n$ at every step.

The infinite values add bookkeeping. A single $u_{n_0} = \infty$ makes every term of (A.28) infinite, and $R < 1$ forces $U(\alpha) = \infty$ on $(R,1)$ .

Formalization scope

Conventions the statements commit to:

Values. Terms $u : \mathbb{N} \to [0,\infty]$ (ℝ≥0∞) with $u_0 \ne \infty$ . $U$ , the Abel means, $w_n$ and the Cesàro means are ℝ≥0∞-valued, with ℝ≥0∞ sums (no summability side conditions).
Limits. $\liminf$ and $\limsup$ are those of the complete lattice $[0,\infty]$ , never real liminf. "Exists and is finite" means convergence in $[0,\infty]$ to some $L \ne \infty$ .
Discount factor. $\alpha \in \mathbb{R}_{\ge 0}$ , and $\alpha \to 1^-$ is the filter 𝓝[<] 1.
Index $n = 0$ . $n \to \infty$ is atTop on $\mathbb{N}$ ; the value $w_0/0 = 0$ is irrelevant.
The equivalence is List.TFAE.
The function $r$ . Its value at the jump is $r(e^{-1}) = e$ (Fig. A.1).
Continuity. In Lemma A.4.1 and in the continuous-weight step, continuity is required on the closed interval $[0,1]$ , which is what the Weierstrass approximation step uses. The book writes " $(0,1)$ ".
Finite terms. Remark A.3.1 is stated for finite terms, which the book's discussion of the radius presumes.

A trivializing formalization is ruled out. Real-valued $\liminf$ / $\limsup$ would make (A.28) hold by junk values on unbounded sequences; hypotheses such as boundedness of $u_n$ would replace the theorem by an easier special case; and a definition of "exists and is finite" allowing $L = \infty$ would make (ii) hold for $u_n = n$ . None of these is used. As sanity checks: for $u_n \equiv 1$ all four terms of (A.28) equal $1$ , and for $u_n = n$ all equal $\infty$ and (i)–(iii) all fail.

A complete development needs:

Cauchy products of $[0,\infty]$ -valued power series;
the Weierstrass approximation theorem, which Mathlib has (polynomialFunctions.topologicalClosure);
interval integrals of step-like functions;
$\liminf$ / $\limsup$ manipulation along 𝓝[<] 1.

Reusable beyond this mission: the ℝ≥0∞ power-series toolkit and the Karamata argument for general continuous weights (milestone 8). Contributions welcome: proofs of any milestone, and alternative proofs of (iii) ⇒ (ii).

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix A.3–A.5, pp. 279–287. https://doi.org/10.1002/9780470317037
E. C. Titchmarsh, The Theory of Functions, 2nd ed., Oxford University Press, 1939, pp. 227–229 (Karamata's proof).
J. Karamata, "Über die Hardy–Littlewoodschen Umkehrungen des Abelschen Stetigkeitssatzes", Mathematische Zeitschrift 32 (1930), 319–320.
G. H. Hardy and J. E. Littlewood, "Tauberian theorems concerning power series and Dirichlet's series whose coefficients are positive", Proc. London Math. Soc. (2) 13 (1914), 174–191.
D. V. Widder, The Laplace Transform, Princeton University Press, 1941.
L. I. Sennott, "A new condition for the existence of optimum stationary policies in average cost Markov decision processes — unbounded cost case", Proc. 25th IEEE Conference on Decision and Control, Athens, 1986, pp. 1719–1721 (cited by the book as Sennott 1986b).
T. M. Liggett and S. A. Lippman, "Short notes: Stochastic games with perfect information and time average payoff", SIAM Review 11 (1969), 604–607. https://doi.org/10.1137/1011093

14 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIII: Lyapunov Criteria and z Standard Markov Chains with CostsTextbook

Motivation

Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the $z$ standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.

The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).

Setting

A Markov chain $\Gamma$ on a countable set $S$ is given by transition probabilities $P_{ij}\ge 0$ with $\sum_j P_{ij}=1$ . $X_t$ is the state at time $t$ and $P^{(t)}_{ij}$ the $t$ -step transition probability ( $P^{(0)}_{ij}=\delta_{ij}$ ). State $i$ leads to $j$ if $P^{(t)}_{ij}>0$ for some $t\ge0$ ; states that lead to each other communicate, which partitions $S$ into communicating classes.

For a nonempty $G\subseteq S$ the first passage time from $i$ is $T_{iG}=\min\{t\ge1: X_t\in G\}$ given $X_0=i$ , and $m_{iG}=E[T_{iG}]\in[0,\infty]$ ; $m_{ij}$ is the case $G=\{j\}$ and $m_{ii}$ the expected return time. The taboo probability $_G P^{(t)}_{ik}$ is the probability of going from $i$ to $k$ in $t$ steps without visiting $G$ at the intermediate times, and $_G u_{ik}$ is the expected number of visits to $k$ at times $0\le t<T_{iG}$ . A state is transient if $P(T_{ii}<\infty)<1$ and positive recurrent if $m_{ii}<\infty$ ; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is $\pi_j=(m_{jj})^{-1}$ (zero when $m_{jj}=\infty$ ).

Each state carries a finite cost $C(i)\ge0$ . The expected average cost over $[0,n-1]$ from $i$ is

J^{(n)}_i=\frac1n\,E\Big[\sum_{t=0}^{n-1}C(X_t)\,\Big|\,X_0=i\Big]=\frac1n\sum_{t=0}^{n-1}\sum_j P^{(t)}_{ij}C(j),

$c_{iG}$ is the expected cost $E[\sum_{t=0}^{T_{iG}-1}C(X_t)\mid X_0=i]$ of a first passage (defined when $m_{iG}<\infty$ ), and $J_R=\sum_{j\in R}\pi_jC(j)$ is the average cost on a positive recurrent class $R$ . The chain is $z$ standard (Definition C.2.5) if for a distinguished state $z$

m_{iz}<\infty\quad\text{and}\quad c_{iz}<\infty\qquad\text{for all } i\in S.

Formalization targets

Goal: Proposition C.2.6

If $\Gamma$ is $z$ standard, then $S$ is the union of a positive recurrent class $R\ni z$ and a set of transient states, $J_R<\infty$ , and

\lim_{n\to\infty}J^{(n)}_i=J_R\qquad\text{for every } i\in S.

The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.

Milestones

Proposition C.1.2: $\pi$ is the unique stationary distribution of a positive recurrent class, and $\pi_j=e_{ij}/m_{ii}=\pi_ie_{ij}$ .
Proposition C.1.4: the first-step equations (C.2)–(C.4) for taboo probabilities, visit counts and $m_{iG}$ ; $\sum_{i\in G}\pi_im_{iG}=1$ for $G$ inside a positive recurrent class; $m_{ij}<\infty$ within such a class.
Proposition C.1.5: if $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ off $G$ , then $m_{iG}\le y(i)/\epsilon$ .
Corollary C.1.6: the same with $G=\{z\}$ and $\sum_jP_{zj}y(j)<\infty$ makes $z$ positive recurrent.
Proposition C.2.1: on a positive recurrent class, $J^{(n)}_i\to J_R=c_{ii}/m_{ii}$ .
Proposition C.2.2: $c_{iG}=\sum_kC(k)\,{}_Gu_{ik}$ , the first-step equation (C.13), and $J_R=\sum_{i\in G}\pi_ic_{iG}$ .
Proposition C.2.3 and Corollary C.2.4: the cost drift condition $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ off a finite set bounds $c_{iG}\le r(i)+Fm_{iG}$ , and gives $c_{zz}<\infty$ .
Remark C.2.7: the hypotheses of C.1.6 and C.2.4 together imply the chain is $z$ standard; so do irreducibility, positive recurrence and finite average cost.

Significance

Proposition C.2.6 is what makes the $z$ standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.

All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.

Difficulty

The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate $n$ times and let $n\to\infty$ " must be made rigorous for $[0,\infty]$ -valued expectations.

The central difficulty is part (iii) of the goal for transient initial states. On the class $R$ , the limit of $J^{(n)}_i$ is a renewal reward theorem over successive returns to $z$ ; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding $J^{(n)}_i$ between $J_R$ and the average over the first $n$ steps of the chain started in $z$ , fails because $P^{(t)}_{ij}$ need not converge (periodic classes) and because finite $c_{iz}$ does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.

Formalization scope

The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be $\infty$ . The first passage time is $T_{iG}\ge1$ ; $m_{iG}$ is the expectation of $T_{iG}$ from its law (and $\infty$ when $P(T_{iG}<\infty)<1$ ), not defined by the recursion (C.4), so that (C.4) is a theorem. $_Gu_{ik}$ counts visits at times $0\le t<T_{iG}$ . $c_{iG}$ is computed over first passage paths and is used only when $m_{iG}<\infty$ , as in the book. $\pi_j$ is $(m_{jj})^{-1}$ , which the book states equals the Cesàro limit $\lim_nQ^{(n)}_{jj}$ . $J^{(n)}_i$ is meaningful for $n\ge1$ , and limits are taken in $[0,\infty]$ . The drift conditions $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ and $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ are written in the equivalent additive form $\sum_jP_{ij}y(j)+\epsilon\le y(i)$ , which is equivalent for finite $y$ and makes the case $\sum_jP_{ij}y(j)=\infty$ fail, as it does in the book.

A trivializing formalization, such as defining $m_{iG}$ or $c_{iG}$ by the equations (C.4) or (C.13), defining $J_R$ as the limit of $J^{(n)}_i$ , or allowing a $z$ standard chain whose return time or return cost to $z$ is infinite, is ruled out: $z$ standard requires $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ including $z$ , and each quantity is defined from path probabilities.

Needed infrastructure: path-sum manipulation in $[0,\infty]$ (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the $z$ standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, pp. 292–302. doi:10.1002/9780470317037
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967. doi:10.1007/978-3-642-62015-7
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. doi:10.1214/aoms/1177728976
S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. doi:10.1017/CBO9780511626630
D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. I, McGraw-Hill, 1982.

12 thms3 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$ , $T_{iG}\ge 1$ is the first passage time to $G$ . The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$ . The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$ . The mean first passage time is $m_{iG}=E[T_{iG}]$ , infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$ . A state $i$ is positive recurrent when $m_{ii}<\infty$ , and the steady state probability is $\pi_i=m_{ii}^{-1}$ . On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$ . The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ . Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$ , and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$ , a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$ . The quantities of $\Gamma_N$ are written $m_{iG}(N)$ , $c_{iG}(N)$ , $\pi_i(N)$ and $J(i)(N)$ . An AS is conforming (for a $z$ standard $\Gamma$ ) if, for large $N$ , $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$ . It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$ .

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$ :

P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$ .

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$ ,

\text{every ATAS that sends excess probability to } G \text{ is conforming},

and if $G\subseteq R$ it is also conforming on $R$ . No rate of convergence and no constants are involved, and $G$ need not contain $z$ .

Milestones

Proposition C.4.2: for fixed $t$ , $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$ ; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$ .
Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$ .
Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$ .
Proposition C.4.6: on a positive recurrent class, convergence of $\pi$ , of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$ , of $c_{zz}$ and of all $c_{iG}$ are equivalent.
Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$ , and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$ .

Further results

Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$ , the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$ .
Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$ , the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$ . First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$ , a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$ , and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$ , $c_{iG}$ , $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$ . $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$ , the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$ . $\Gamma_N$ is built as an MC on the subtype of $S_N$ , and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$ . Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ( $N<N_0$ or a state outside $S_N$ ). For fixed states this affects finitely many $N$ , and all statements are limits, $\liminf$ s or eventual equalities. All convergence is in $[0,\infty]$ . The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$ .

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$ , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$ , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

10 thms2 active usersReviewed

Analysis Operations Research Probability+1·Captain: mikedeng1

Elements of Queueing Theory I: The Swiss Army Formula of Palm CalculusTextbook

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of `P⁰_N`

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

11 thms1 active userReviewed

Queueing and Stochastic Networks

Missions

Processing Networks IX: Fluid Stability of the Proportionally Fair AllocationTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Processing Networks X: Maximal Stability of Proportionally Fair ControlTextbook

Motivation

Setting

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Processing Networks XI: Maximal Stability of Workload-Weighted Task AllocationTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Processing Networks XII: Packet Networks, Subcriticality and Fluid LimitsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Processing Networks XIII: Back-Pressure Control for Packet NetworksTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 12.16 — aperiodicity, irreducibility, and conditional positive recurrence

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Processing Networks XIV: Random Proportional Scheduling for Packet NetworksTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 12.28 — the load condition implies RPS stability

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Diffusion approximations for open queueing networks with service interruptions 1: explicit Lipschitz bounds for the oblique reflection mapResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Diffusion approximations for open queueing networks with service interruptions 2: jump-diffusion heavy-traffic limit for long up and down timesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1, case J=1J=1J=1

Milestones

Significance

Difficulty

Goal: Theorem 4.1, case $J=1$