Stochastic Systems

Motivation

A stochastic processing network (SPN) — buffers holding waiting work, activities that consume items from buffers and produce items into others, driven by stochastic arrivals and service requirements — is stable, in the sense of mission I's Definition 3.6, exactly when its ambient Markov chain is positive recurrent. That definition is correct, but it is a statement about an infinite-state continuous-time Markov chain, and Markov chains of that kind almost never admit a hand-computed stationary distribution or a directly verifiable positive-recurrence criterion for anything beyond the smallest examples. What is needed is a method that turns "is this specific queueing network, under this specific control policy, stable?" into a tractable, purely deterministic question. 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 this method in Chapter 6, and the theorem that licenses it — Theorem 6.2 — is introduced by the authors themselves as "the fulcrum that supports all other results developed in this book." Every stability theorem in the remaining eight chapters of the book (feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation, task allocation, packet networks) is an application of this one theorem to a model-specific fluid model.

The method traces to Rybko and Stolyar's 1992 study of a single two-station network and to J. G. Dai's 1995 unification of fluid-limit stability arguments across general queueing networks (Annals of Applied Probability 5, 49–77), with independent contemporaneous work by A. Stolyar for discrete state spaces and a parallel probabilistic route through reflecting Brownian motion due to Dupuis and Williams (1994). This mission formalizes the version of the argument specific to Dai and Harrison's general SPN framework.

Setting

Under a fixed control policy, an SPN with $I$ buffers and $J$ activities generates four continuous-time processes: the cumulative departure process $D(t) \in \mathbb{Z}_+^I$, the cumulative service-completion process $F(t) \in \mathbb{Z}_+^J$, the cumulative service-effort process $T(t) \in \mathbb{R}_+^J$, and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. The model's first-order data — the $I \times J$ material-requirement matrix $B$, the $I \times J$ expected-output matrix $\Gamma$, the vector $m$ of mean service times, the $K \times J$ capacity-consumption matrix $A$, the $K$-vector $b$ of server-pool capacities, and the vector $\lambda$ of external arrival rates — determine six basic relationships that Chapter 2 derives directly from the SPN's construction, and that this mission packages as IsFluidModelSolution.

To study scaling limits, Section 6.3 constructs, on one common probability space, a whole family of versions of the SPN's processes, one for each initial state $x$ of the ambient chain: the superscripted $D^x, F^x, T^x, Z^x$. Writing $|x|$ for the total initial buffer content, the fluid-scaled processes are

$$\big(\hat D^x, \hat F^x, \hat T^x, \hat Z^x\big)(t,\omega) := \tfrac{1}{|x|}\big(D^x, F^x, T^x, Z^x\big)(|x|t, \omega), \qquad t \ge 0.$$

A fluid limit path (Definition 6.6) is any limit of such a family, along a sequence of initial states with $|x_n| \to \infty$, uniform on compact time intervals (u.o.c.). A fluid model solution is any four-tuple satisfying the six equations above, whether or not it arises as an actual limit — a purely deterministic notion.

Formalization targets

Goal: Theorem 6.2 — fluid limit stability implies SPN stability

$$\text{fluid limit of the SPN is stable} \quad\Longrightarrow\quad \text{ambient Markov chain } X \text{ is positive recurrent},$$

where "fluid limit... is stable" (Definition 6.1) means: there is $\gamma > 0$ such that every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ has $\hat Z(t) = 0$ for all $t \ge \gamma |\hat Z(0)|$. This is the weakest possible target: it asserts only that fluid limit paths are eventually driven to zero, with no rate or further structure attached, and it is exactly the hypothesis every later chapter's Lyapunov argument is built to establish.

Supporting milestones

Theorem 6.5 (existence of fluid limits): along any sequence of initial states with $|x_n| \to \infty$, the fluid-scaled processes have a u.o.c.-convergent subsequence, and every such limit is automatically a fluid model solution — the bridge from the purely equational Definition 6.3 (used by every later chapter) to the genuinely stochastic Definition 6.1 (needed by this theorem). Its proof rests on two convergence lemmas (6.7: compactness of the scaled service-effort process via an equicontinuity argument; 6.8: the scaled completion process converges exactly when the scaled effort process does) and, behind Lemma 6.8, a uniform strong law of large numbers for a "delayed" random walk (Lemma 6.9). A separate uniform-integrability result (Lemma 6.10) supplies the remaining ingredient the goal theorem's proof needs to convert an almost-sure fluid-scale limit into the expectation bound mission I's Lemma 3.7 requires.

Significance

The result itself. Theorem 6.2 converts a probabilistic stability question about an infinite-state Markov chain into a real-analysis question about a deterministic dynamical system: does every solution of a fixed, checkable system of equations reach zero in finite time, uniformly in its starting size? Every one of the book's remaining eight chapters answers a version of this question for a specific policy and concludes SPN stability via this theorem alone — none of them re-derives positive recurrence directly.

Formalizing it. No prior formalization of fluid limits, fluid models, or scaling-limit stability of any stochastic system exists on Prove2Me (q=fluid limit, q=fluid model, q=u.o.c. convergence, q=queueing network stability all return zero hits). This mission is a from-scratch formalization of the model data, the fluid equations, the per-state process family, and the two notions of fluid stability, together with the five supporting results and the goal theorem that connects them — the shared infrastructure the rest of the fourteen-mission series depends on.

Difficulty

The obvious shortcut — state Theorem 6.2 using fluid model stability (Definition 6.3, the purely equational notion) in place of fluid limit stability (Definition 6.1) — would produce a strictly easier, unfaithful theorem: fluid model solutions are not restricted to arise as actual scaling limits, so the genuine content of Theorem 6.2 (that convergence of a stochastic family forces a probabilistic conclusion) would be lost, and the theorem would reduce to a tautology once Theorem 6.5 is assumed. The two notions are visually almost identical in the book's own text ("$\gamma|\hat Z(0)|$-attraction to the origin," applied to two different objects) and keeping them distinct is this mission's central discipline. A second difficulty is that Mathlib has no existing theory of stochastic-process scaling limits, u.o.c. convergence, or the specific renewal/SLLN machinery (Lemma 6.9's uniform strong law for a state-dependent "delayed" random walk) the proof needs — every one of these had to be defined from the ground up rather than instantiated from a general framework.

Formalization scope

The ambient chain's state space is an arbitrary countable type, following mission 01; the per-state process family SPNProcessFamily takes $D^x, F^x, T^x, Z^x$ as given real-valued functions satisfying exactly the pathwise properties (Eqs. 2.31–2.32) that Section 6.4's proofs use, since Chapter 2's construction of these processes from primitive stochastic elements is that chapter's own "recap" of already-established facts, not a numbered result of Chapter 6. UOCConverges is stated by its direct $\varepsilon$-$N$-on-every-compact-interval meaning, and Lemma 6.9's "$\sup_x$" is likewise stated by its direct $\varepsilon$-$N$ meaning rather than a Lean supremum expression, because the state space may be countably infinite and an explicit supremum over an unbounded-above family of reals would silently collapse to a junk value of zero in that case — a real risk of trivializing the statement that this formalization avoids outright. A formalization that reused FluidModelStable as the goal theorem's hypothesis, or that dropped $|\hat Z(0)|=1$ from Theorem 6.5, would each be a trivializing shortcut of exactly the kind ruled out above. The five definitions (FluidEquationData, IsFluidModelSolution, SPNProcessFamily, FluidLimitPath, FluidLimitStable) are the primary reusable contribution — the shared vocabulary every later mission in the series restates in its own namespace, since drafts do not import one another. Contributions completing the six by sorry proofs 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
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• P. Dupuis and R. J. Williams, "Lyapunov functions for semimartingale reflecting Brownian motions," Annals of Probability 22 (1994), 680–702.

Motivation

A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.

The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.

Setting

An SPN has $I$ buffers, indexed $1, \dots, I$, and $J$ activities (service types), indexed $1, \dots, J$. External work arrives into buffer $i$ according to a counting process $E_i(t)$; activity $j$, whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the $I$ external arrival processes are independent Poisson processes with rates $\lambda_1, \dots, \lambda_I \ge 0$ (no arrivals into a buffer with rate $0$); for each activity $j$, the matched pairs of processing variables — service time and output vector, $(v_j(\ell), \varphi_j(\ell))_{\ell \ge 1}$ — form an i.i.d. sequence with finite means $m_j = \mathbb{E}[v_j(1)] > 0$ and $\Gamma_j = \mathbb{E}[\varphi_j(1)] \ge 0$; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the $J$ processing-variable sequences are, collectively, mutually independent.

Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process $N(t) \in \mathbb{Z}_+^J$ and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain $X = \{X(t), t \ge 0\}$ on a countable state space $\mathcal{X}$: a function $f : \mathcal{X} \to \mathbb{Z}_+^J \times \mathbb{Z}_+^I$ with $(N(t), Z(t)) = f(X(t))$ on every sample path, whose level sets $B(z) = \{x : f(x) = (n,z)\ \text{for some } n\}$ are finite for every buffer-content vector $z$, and which has at least one empty state $x^\ast$ with $f(x^\ast) = (0,0)$.

Formalization targets

Goal: Proposition 3.5 — equivalent definitions of stability

$$X \text{ positive recurrent} \iff X \text{ has a unique stationary distribution } \pi \iff Z(t) \text{ converges in distribution to a non-defective limit},$$

and, when these hold, for every bounded $h : \mathcal{X} \to \mathbb{R}$ and every initial distribution of $X(0)$,

$$\Pr\left\{ \lim_{t \to \infty} \frac{1}{t} \int_0^t h(X(s))\, ds = \bar h \right\} = 1, \qquad \bar h := \sum_{x \in \mathcal{X}} \pi(x)\, h(x).$$

Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.

Supporting milestones

Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts $E_i(t)/t \to \lambda_i$ and the processing-variable sample means $\frac{1}{n}\sum_{\ell \le n} v_j(\ell) \to m_j$, $\frac{1}{n}\sum_{\ell \le n} \varphi_j(\ell) \to \Gamma_j$ — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.

Significance

The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.

Formalizing it. No result in this mission or its milestones has a prior formal counterpart on Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and "irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined for a countable-state discrete-time chain — a different object from Assumption 3.1's continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time definition), not as a Lean dependency. This mission is a from-scratch formalization of the model (baseline stochastic assumptions, Markov representation) and of positive recurrence, stationary-distribution uniqueness, and distributional convergence for it.

Difficulty

The obvious first attempt — define $X$ as an arbitrary countable-state Markov chain and directly import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run convergence — fails because Mathlib currently has no general countable-state continuous-time Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC stationary-distribution result is unproven substrate, not applicable to a countably infinite state space). The formalization instead works at the level of the chain's embedded discrete-time jump chain, which is where Lean's PMF-based machinery is available, and states the three equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption 2.1(d)'s independence clause, which is a genuine three-way mutual independence of $\sigma$-algebras (initial processing variables, arrival process, and the collection of all $J$ processing-variable sequences), not the pairwise independence a careless reading might substitute — a weaker hypothesis here would silently make later derivations in the series unsound.

Formalization scope

The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate], not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives $n$-step iteration, Irreducible requires every state to reach every other in finitely many jump-chain steps); positive recurrence is mean return time under jump, defined via the standard first-return-time renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and Fin J → ℕ-valued, matching the book's $\mathbb{Z}_+^I$, $\mathbb{Z}_+^J$. A formalization that took IsStable to mean, say, only distributional convergence of $Z$ (dropping the chain-level characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate every other mission of the series is built on, and are the primary reusable contribution; contributions completing the by sorry proofs, particularly of the goal theorem (which the book proves via appeal to general CTMC theory in its Appendix D, not reproduced here), 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
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

Motivation

A jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.

Timeline:

• 1957: Jackson, Networks of Waiting Lines, constant external Poisson arrivals and multi-channel exponential servers; product-form equilibrium.
• 1963: Jackson, this paper: state-dependent total arrival rate $\lambda(S(\bar k))$, queue-length-dependent service rates $\mu(n, k)$, routings with self-loops and empty routings; Theorem (4.5).
• 1967: Gordon and Newell, Closed Queuing Systems with Exponential Servers, the closed-network analogue.
• 1979: Kelly, Reversibility and Stochastic Networks, the general theory of migration processes and partial balance.

Setting

There are $N \ge 1$ service centers, Center $1, \dots, N$. A state vector $\bar k = (k_1, \dots, k_N)$ has non-negative integer components, $k_n$ being the number of customers at Center $n$, and $S(\bar k) = k_1 + \dots + k_N$. The system $(N, L, M, R)$ is given by:

1. arrival rates $\lambda(K)$, $K = 0, 1, 2, \dots$: in state $\bar k$ a customer arrives at rate $\lambda(S(\bar k))$;
2. service rates $\mu(n, k)$: a service at Center $n$ completes at rate $\mu(n, k_n)$;
3. routing probabilities $r(m, n)$, $m \in [0, N]$, $n \in [1, N+1]$: an arriving customer's first center is $n$ with probability $r(0, n)$, its routing is empty with probability $r(0, N+1)$; after service at Center $m$ it moves to Center $n$ with probability $r(m, n)$ (possibly $n = m$) or leaves with probability $r(m, N+1)$.

The paper's standing Assumptions (2.1)–(2.4): (2.1) either all $\lambda(K) > 0$, or $\lambda(K) > 0$ exactly for $K \le K_0$; (2.2) $\mu(n, 0) = 0$ and $\mu(n, k) > 0$ for $k \ge 1$; (2.3) each row $\{r(m, n)\}_{n \in [1, N+1]}$ is a probability distribution; (2.4) the traffic equations

$$e(n) = r(0, n) + \sum_{m=1}^N e(m)\, r(m, n), \qquad n \in [1, N], \tag{2.5}$$

have a unique solution, and it is non-negative.

The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for $P(\bar k, t)$. An equilibrium state probability distribution is a probability distribution $p$ on state vectors such that $P(\bar k, t) \equiv p(\bar k)$ solves (3.1). With

$$W(K) = \prod_{i=0}^{K-1}\lambda(i), \quad w(\bar k) = \prod_{n=1}^N\prod_{i=1}^{k_n}\frac{e(n)}{\mu(n, i)}, \quad T(K) = \sum_{S(\bar k) = K} w(\bar k),$$

the constant $\pi$ is $\{\sum_{K \ge 0} W(K) T(K)\}^{-1}$ when the series converges and $0$ otherwise.

Formalization targets

Goal: Theorem (4.5)

If $\pi > 0$, then

$$p(\bar k) = \pi\, w(\bar k)\, W(S(\bar k)) \tag{4.6}$$

is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition $\pi > 0$ is the paper's.

Milestones

1. The series in (4.4) converges to a positive number or diverges to $+\infty$ (§4, p. 136).
2. If $\pi > 0$, (4.6) is a probability distribution (first claim of the proof sentence, p. 136).
3. (4.6) satisfies equations (3.1) at every state (second claim, p. 136).
4. Under bounded arrival rates, an equilibrium distribution is unique (§4, p. 135).

Companion

Theorem (6.3) in its case $K^* = 0$, $k_n^* = +\infty$: with constant arrival rate $\lambda(K) \equiv \lambda(0)$ and $p_n(0) > 0$ for every $n$, the equilibrium is $p(\bar k) = \prod_n p_n(k_n)$, $p_n$ being the normalized $w_n(k) = \prod_{i=1}^k \lambda(0)e(n)/\mu(n, i)$.

Significance

Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios $e(n)$, and that conditionally on the total $S(\bar k) = K$ it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate $\lambda(0)e(n)$; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking $\lambda(K) = 0$ for $K > K_0$ caps the population.

The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.

Difficulty

The balance equations are an infinite system in $\mathbb{Z}_{\ge 0}^N$. Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor $1 - r(n, n)$, and centers with $e(n) = 0$, where $w$ vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over $\mathbb{Z}_{\ge 0}^N$ by the finite fibres of $S$.

Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with $\pi > 0$ (e.g. $N = 1$, $\lambda(K) = 4^K$, $\mu(1,k) = 2\cdot 4^{k-1}$). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.

Formalization scope

Centers are Fin N with $N > 0$; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index $0$ in the first argument and $N + 1$ in the second. A structure JobshopSystem N bundles $\lambda, \mu, r, e$ with Assumptions (2.1)–(2.4) as fields; $e$ is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is $q \ge 0$, HasSum q 1, and Balance at every state. $\pi$ is defined with an explicit if Summable … then … else 0.

Explicit choices, each stated in the item where it applies:

• Correction of (3.1). The paper prints the arrival outflow as $\lambda(S(\bar k))$:

  $\dfrac{dP(\bar k, t)}{dt} = -[\lambda(S(\bar k)) + \sum_n \mu(n, k_n)(1 - r(n, n))]P(\bar k, t) + \dots$

  Its transition probabilities (p. 134) give $\lambda(S(\bar k))\sum_{n=1}^N r(0, n)$, since an arrival with an empty routing leaves the state unchanged. The two agree only when $r(0, N+1) = 0$, and with the printed coefficient Theorem (4.5) is false ($N = 1$, $r(0,1) = r(0,2) = 1/2$, $r(1,2) = 1$, constant rates, at $\bar k = 0$). The formalization uses the coefficient the transition probabilities give. It does not assume $r(0, N+1) = 0$: the paper allows empty routings.

• Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes $\exists \Lambda,\ \forall K,\ \lambda(K) \le \Lambda$. The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.

• Companion (6.3). System $(N, L, M, R)^*$ of §5 is not formalized in the paper and not here; only its case $K^* = 0$, $k_n^* = +\infty$ is stated.

A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention $w$, $W$ or $\pi$, and equilibrium is neither defined as (4.6) nor as detailed or partial balance.

Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit $\lim_{t\to\infty} P(\bar k, t) = p(\bar k)$, which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).

Selected references

• J. R. Jackson, Jobshop-Like Queueing Systems, Management Science 10(1), 131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4), 518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• W. J. Gordon and G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/book/whole.pdf
• A. T. Bharucha-Reid, Elements of the Theory of Markov Processes and Their Applications, McGraw-Hill, 1960 (Theorem 2.9, p. 102, cited in footnote 5).

Motivation

A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.

The reflected process $Y=\overline X-X$, the distance of $X$ below its running maximum, is the drawdown of $X$. Its first passage above a level $k$ is the time at which a drawdown of size $k$ first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot $Y_{\tau_k}$ in closed form, in terms of the scale functions of $X$. This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.

Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of $(\tau_k,Y_{\tau_k})$ for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.

Setting

Let $X=\{X_t,t\ge0\}$ be a spectrally negative Lévy process on $(\Omega,\mathcal F,\mathbb P)$: it starts at $0$, has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$, and "$\psi(v)<\infty$" means that $e^{vX_1}$ is integrable. For such $v$, the tilted exponent is $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$.

The paper assumes throughout that $X$ has unbounded variation, or has bounded variation and a Lévy measure $\Lambda$ with $\Lambda(dx)\ll dx$.

For $q\ge0$, $\Phi(q)$ is the largest root of $\psi(\theta)=q$. The $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies

$$\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=\frac1{\psi(\theta)-q},\qquad\theta>\Phi(q).$$

For $q<0$ it is defined by the series $W^{(q)}=\sum_{k\ge0}q^kW^{\star(k+1)}$, where $W=W^{(0)}$ and $\star$ is convolution on $[0,\infty)$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$. The functions $W_v^{(p)}$ and $Z_v^{(p)}$ are the same objects built from $\psi_v$ instead of $\psi$.

Under $\mathbb P_{s,x}$ the process starts at $x$ with a prior maximum $s\ge x$. Its running maximum is $\overline X_t=\max\{s,\sup_{0\le u\le t}X_u\}$, and the reflected process is $Y=\overline X-X$, which starts at $z=s-x$. For $k>0$,

$$\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}.$$

Formalization targets

Goal: Theorem 1

For $u\ge0$ and $v$ with $\psi(v)<\infty$, with $z=s-x\ge0$ and $p=u-\psi(v)$,

$$\mathbb E_{s,x}\big[e^{-u\tau_k-vY_{\tau_k}}\big]=e^{-vz}\left(Z_v^{(p)}(k-z)-W_v^{(p)}(k-z)\frac{pW_v^{(p)}(k)+vZ_v^{(p)}(k)}{W_v^{(p)\prime}(k)+vW_v^{(p)}(k)}\right).$$

Here $v$ may be negative, so $p$ may be negative, which is where the series extension of $W$ enters.

Milestones

• (2) $\mathbb E[e^{\theta X_t}]=e^{t\psi(\theta)}$.
• Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ for every real $u$.
• Proposition 1, (9) and (10): for $x\in(a,b)$, the Laplace transforms of the exit time of $X$ from $(a,b)$ on the events of exit above and exit below.
• (13): the splitting of the goal's expectation at the first zero of $Y$.
• (14)–(15) and (16): the two expectations of (13).
• (22): the value $C$ of the functional for $Y$ started at $0$.
• Remark 6, (23): the stopped process whose martingale property is equivalent to Theorem 1.

Items (13)–(22) are stated under the proof's restriction $u\ge\psi(v)\vee0$. The goal is not.

Significance

The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size $k$ and of its overshoot. With $v=0$ it is the Laplace transform of the drawdown time. With $u=0$ it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.

The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.

Difficulty

The natural first idea is to treat $Y$ like $X$ and read off its exit from $[0,k)$ from the two-sided exit identities of Proposition 1. This works only until $Y$ first returns to $0$. Up to that time $Y$ is a copy of $-X$. After it, $Y$ is reflected at $0$, it is not a Lévy process, and no two-sided exit problem of $X$ describes it. The whole content of the theorem is the constant $C$ of (13), the value of the functional for $Y$ started at $0$, where the reflection acts at every instant. A second difficulty is the range of $(u,v)$. For $v<0$ the integrand $e^{-vY_{\tau_k}}$ is unbounded, because $Y$ can jump far above $k$. Its finiteness is part of the claim. So is the passage from the region $u\ge\psi(v)\vee0$, where every scale function in (12) comes from Definition 2, to all $u\ge0$, where $p$ can be negative.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a real process with $X_0=0$. $\mathbb P_x$ is encoded by the path $x+X$, and $\mathbb P_{s,x}$ by that path together with the prior maximum $s$. Random times take values in WithTop ℝ≥0, with $\infty$ as "never". The functional $e^{-u\tau_k-vY_{\tau_k}}$ and discount factors $e^{-qT}$ are set to $0$ where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.

Readings of the paper's informal words:

• "Lévy process": the paths start at $0$, are càdlàg and have no positive jumps for every $\omega$, not only almost surely.
• "We exclude the case that X has monotone paths": the paths are neither almost surely nondecreasing nor almost surely nonincreasing.
• "unbounded variation": not of bounded variation. The standing assumption is "bounded variation implies (AC)".
• "$\Lambda(dx)\ll dx$": for every Lebesgue-null Borel $A$, almost surely no nonzero jump in $(0,1]$ lands in $A$. The Lévy measure is not constructed.
• "$\psi(v)<\infty$": $e^{vX_1}$ is integrable.
• "the largest root": the supremum of the nonnegative roots.
• "the unique function": a definite description by choice.
• "analytic extension": the series (5) for real negative index. Complex indices are out of scope.
• "$W'$": the derivative at $k>0$.
• "is a martingale" in (23): a martingale for the natural filtration of $X$.
• Misprint: (23) prints $vZ_v^{(q)}(k)$, and the statement uses $vZ_v^{(p)}(k)$.

The scale functions are defined from the exponent $\psi$ of the given $X$. A formalization in which $W$ is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which $W_v^{(p)}$ is defined as $e^{-vx}W^{(p+\psi(v))}(x)$, which would make Remark 4 a tautology.

Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996. https://www.cambridge.org/core/books/levy-processes/
• J. Bertoin, Exponential decay and ergodicity of completely asymmetric Lévy processes in a finite interval, Ann. Appl. Probab. 7(1), 156–169, 1997. https://doi.org/10.1214/aoap/1034625254

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Motivation

Average-cost criteria are standard in inventory, queueing and maintenance models that run indefinitely. For a Markov decision process (MDP), the central object is the average-cost optimality equation (ACOE). It couples a constant $w$ (the optimal long-run cost per period) with a relative value function $\tilde u$. A stationary policy that attains the minimum in the ACOE is average-cost optimal. When the state space is uncountable, the one-step cost is unbounded and the transition probability is only weakly continuous, the ACOE is not automatically available.

Feinberg, Kasyanov and Zadoianchuk (2012) proved that under their Assumptions W* and B the weaker average-cost optimality inequality (ACOI) holds. For setwise continuous transition probabilities, Hernández-Lerma and Lasserre (1996, Theorem 5.5.4) gave conditions for the ACOE via equicontinuity. Feinberg and Lewis (2015) established the ACOI and optimality of $(s,S)$ policies for periodic-review inventory control with setup costs and general demand. Feinberg and Liang (2022, online 2017) extended the equicontinuity condition to weakly continuous transitions and used it to show that the inventory problem satisfies the full equation, not just the inequality.

Setting

An MDP has a state space $\mathbb X$ and an action space $\mathbb A$ (Borel subsets of Polish spaces). It has a one-step cost $c:\mathbb X\times\mathbb A\to\mathbb R\cup\{+\infty\}$, bounded below, and a transition probability $q(dy\mid x,a)$. A policy chooses actions from the observed history, possibly at random. A stationary policy is a measurable map $\phi:\mathbb X\to\mathbb A$. For a discount factor $\alpha\in[0,1)$:

• $v_\alpha(x)$ is the infimum over all policies of the expected total discounted cost from $x$;
• $m_\alpha=\inf_x v_\alpha(x)$;
• $u_\alpha=v_\alpha-m_\alpha$ is the discounted relative value function.

The average cost of a policy is $w^\pi(x)=\limsup_N \frac1N\mathbb E^\pi_x\sum_{t<N}c(x_t,a_t)$, and $w(x)=\inf_\pi w^\pi(x)$. Set $\underline w=\liminf_{\alpha\uparrow1}(1-\alpha)m_\alpha$. For a sequence $\alpha_n\uparrow1$, define

$$\tilde u(x)=\liminf_{n\to\infty,\ y\to x}u_{\alpha_n}(y).$$

Assumption EC for $\{\alpha_n\}$ has two parts:

1. the family $\{u_{\alpha_n}\}$ is equicontinuous;
2. some measurable $U\ge u_{\alpha_n}$ has $\int U\,dq(\cdot\mid x,a)<\infty$ for all $x,a$.

The inventory problem has inventory level $x\in\mathbb R$ (negative means backlog) and order quantity $a\ge0$. Inventory evolves by $x_{t+1}=x_t+a_t-D_{t+1}$, with i.i.d. nonnegative demands $D$. The cost is

$$c(x,a)=K\,I_{\{a>0\}}+\bar c\,a+\mathbb E[h(x+a-D)],$$

with setup cost $K\ge0$, unit cost $\bar c>0$, and convex $h$ with $h(x)\to\infty$ as $|x|\to\infty$. Let $\alpha^*=1+\lim_{x\to-\infty}h(x)/(\bar cx)$ and $H(x)=\bar cx+\mathbb E[h(x-D)]+\mathbb E[\tilde u(x-D)]$. A function $f$ is $K$-convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)+\lambda K$ for $x\le y$ and $\lambda\in(0,1)$. An $(s,S)$ policy orders up to $S$ whenever the inventory is below $s$.

Formalization targets

Goal: Theorem 4.5

For every sequence of nonnegative discount factors $\alpha_n\uparrow1$ with $\alpha_1>\alpha^*$, the inventory MDP satisfies Assumption EC. Along a subsequence, $u_{\alpha_{n_k}}\to\tilde u$, and some stationary $\phi$ satisfies

$$w+\tilde u(x)=K I_{\{\phi(x)>0\}}+H(x+\phi(x))-\bar cx=\min\Big\{\min_{a\ge0}[K+H(x+a)],\,H(x)\Big\}-\bar cx .$$

Moreover:

• $\tilde u$ and $H$ are $K$-convex, continuous and inf-compact;
• the $(s,S)$ policy built from a minimizer of $H$ satisfies the equation;
• so do the limits $(s^*,S^*)$ of discount-optimal thresholds.

Milestones

1. Lemma 3.3: for equicontinuous families, the pointwise and joint lower limits coincide.
2. Theorem 3.2: Assumptions W*, B and EC imply the ACOE for a general MDP.
3. The cited facts used in §4:
   • Assumptions W* and B hold for the inventory problem;
   • the sets $\mathbb X_\alpha$ of minimizers of $v_\alpha$ lie in a bounded interval (4.4);
   • discount-optimal $(s_\alpha,S_\alpha)$ policies (Theorem 4.3);
   • their average-cost limits (Theorem 4.4);
   • the renewal bounds (4.11)–(4.12).
4. Lemma 4.6: an explicit dominating function $U$.
5. Lemma 4.7: equicontinuity of $\{u_{\alpha_n}\}$ for the inventory problem.

Significance

The ACOE is stronger than the ACOI. It identifies the optimal actions of an average-cost problem as the minimizers of a one-step lookahead with $\tilde u$, and it makes $\tilde u$ a genuine relative value function: $\tilde u$ is the pointwise limit of the discounted relative values along a subsequence. For inventory control, Theorem 4.5 gives three further conclusions:

• the $K$-convexity and continuity of the average-cost relative value function;
• that an optimal $(s,S)$ policy can be computed from $H$ by the same argmin rule that works for discounted costs;
• that limits of discount-optimal thresholds solve the average-cost problem.

The results are proved in the paper, and in the cited works of Feinberg and coauthors for the cited milestones. None is formalized. There is no formal library of MDPs on Borel spaces with history-dependent randomized policies. This mission builds that layer (strategic measures via Ionescu Tulcea, discounted and average costs, Assumptions W*, B and EC) and states the general ACOE theorem on it. A proof of the goal would also require formal proofs of the cited inventory results of Feinberg–Lewis (2015) and Feinberg–Liang (2017a), which are milestones here.

Difficulty

One obvious route is to pass to the limit in the discounted optimality equation $v_\alpha=\min_a[c+\alpha\int v_\alpha\,dq]$. After subtracting $m_\alpha$, this needs two things: convergence of $u_{\alpha_n}$, and exchanging limit and integral. Pointwise lower limits give only the inequality (ACOI). The reverse inequality needs actual convergence of a subsequence and a dominating function. For weakly continuous $q$, convergence of $\int u_{\alpha_n}\,dq$ additionally requires uniform convergence on compacts, which is where equicontinuity enters.

For the inventory problem the hard step is equicontinuity itself. The functions $u_\alpha$ are not uniformly Lipschitz. It must be shown that costs from two nearby starting inventories stay close uniformly in $\alpha$. This comparison runs through the time until inventory falls below the reorder point, and it is controlled by renewal-theoretic bounds on the number of demand arrivals.

Formalization scope

The Lean development lives in the namespace FeinbergLiang.ACOE. It commits to the following conventions.

• Spaces. $\mathbb X,\mathbb A$ are separable metric spaces with standard Borel σ-algebras. This is the paper's "Borel subsets of Polish spaces", up to homeomorphism. The inventory case is $\mathbb X=\mathbb R$, $\mathbb A=\mathbb R_{\ge0}$. The integer case $\mathbb X=\mathbb Z$, $\mathbb A=\mathbb N_0$ is out of scope, as are Corollary 4.8 and Theorem 4.9.
• Costs and infinities. The cost is stored as a real lower bound plus a $[0,\infty]$-valued part. Every value function ($v_\alpha$, $m_\alpha$, $u_\alpha$, $w$, $\underline w$, $\tilde u$) is the $[0,\infty]$-valued part, with the explicit real shift described in the definitions. $u_\alpha$ equals $v_\alpha-m_\alpha$ whenever $m_\alpha<\infty$, which Assumption B guarantees. $\alpha^*$ is an extended real and may be $-\infty$. $G_\alpha$ and $H$ are extended-real valued, and each theorem using them concludes their finiteness. Likewise the ACOE conclusions include $\underline w<\infty$ and $\tilde u<\infty$, so an equation of the form $\infty=\infty$ can never satisfy them.
• Policies. $v_\alpha$ and $w$ are infima over all history-dependent randomized policies, with trajectory laws given by Mathlib's Ionescu Tulcea kernel Kernel.trajMeasure. They are never defined as solutions of an optimality equation.
• Readings of informal words.
  1. "$\alpha_n\uparrow1$" means values in $[0,1)$, nondecreasing, with limit $1$; "nonnegative discount factors" is the lower end of $[0,1)$.
  2. The paper's $\alpha_1$ is Lean's α 0.
  3. "Equicontinuous" is Mathlib's Equicontinuous, applied to the real values of $u_{\alpha_n}$ together with their finiteness.
  4. "$\liminf_{n\to\infty,y\to x}$" is the lower limit along the product filter atTop ×ˢ 𝓝 x.
  5. "Uniform on each compact subset" is TendstoUniformlyOn on every compact set.
  6. "$=\min$" in (3.3) and (4.10) means the middle term is attained and is a lower bound for all actions.
  7. "Assumption EC for the sequence" is a property of a given sequence.
  8. "Can be selected as an $(s^*,S^*)$ policy" is stated for every limit of discount-optimal thresholds along a further subsequence, with $\tilde u$ that of Theorem 3.2(i).
  9. "Can be selected as an $(s,S)$ policy" is stated for every minimizer $S$ of $H$.
  10. Theorem 4.4's "optimality inequality (4.8)" is read as the ACOI (3.1) for the $(s^*,S^*)$ policy.
• Standing assumptions. The paper's "without loss of generality $h\ge0$ and $h(0)=0$" is a pair of hypotheses of the inventory model. This is the paper's normalization, not an addition.
• Not trivializable. Defining $v_\alpha$ through its optimality equation, restricting policies to stationary ones, or dropping the finiteness conclusions would make the goal a different, weaker statement. The definitions rule each of these out.

Contributions welcome: proofs of the milestones, especially the general Theorem 3.2 and the renewal estimates behind Lemmas 4.6–4.7. The Borel-space MDP definitions are reusable by later average-cost and discounted MDP missions.

Selected references

• E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control, Annals of Operations Research 317 (2022) 569–586. https://doi.org/10.1007/s10479-017-2561-9
• E. A. Feinberg, P. O. Kasyanov and N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probability, Mathematics of Operations Research 37(4) (2012) 591–607. https://doi.org/10.1287/moor.1120.0555
• E. A. Feinberg and M. E. Lewis, On the convergence of optimal actions for Markov decision processes and the optimality of (s, S) policies for inventory control, preprint arXiv:1507.05125, 2015. https://arxiv.org/abs/1507.05125
• E. A. Feinberg and Y. Liang, Structure of optimal policies to periodic-review inventory models with convex costs and backorders for all values of discount factors, Annals of Operations Research (2017a). https://doi.org/10.1007/s10479-017-2548-6
• O. Hernández-Lerma and J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0