Operations Research Probability Statistics·Captain: mikedeng1

Stochastic Orders IV: The Increasing Convex and Increasing Concave OrdersTextbook

Comparing location and spread together

Chapter I's usual stochastic order compares "how large" two random variables tend to be; Chapter III's convex order compares "how spread out" they are, holding the mean fixed. Chapter IV's increasing convex and increasing concave orders combine the two: $X \le_{icx} Y$ says $X$ is both smaller and less variable than $Y$ in a single comparison, without forcing equal means. These are the orders a decision-maker with risk-averse (concave-utility) or risk-loving (convex-cost) preferences actually uses to rank random outcomes, since expected utility is exactly an expectation of an increasing concave or convex function. This mission formalizes both orders and their coupling characterization: the submartingale/supermartingale analogue, one chapter over, of Chapter III's Strassen martingale coupling for the plain convex order.

The increasing convex and increasing concave orders

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$ , and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the increasing convex order, written $X \le_{icx} Y$ , if

E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every increasing convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist,}

and smaller than $Y$ in the increasing concave order, $X \le_{icv} Y$ , if the same holds for every increasing concave $\varphi$ . Taking $\varphi(x)=x$ (increasing and both convex and concave) gives $E[X]\le E[Y]$ under either order — unlike the convex order, no equality of means is forced. Two equivalent tail-integral characterizations (Theorem 4.A.2) make the orders tractable: $X\le_{icx}Y$ iff $\int_x^\infty \bar F(u)\,du \le \int_x^\infty \bar G(u)\,du$ for every $x$ , and $X\le_{icv}Y$ iff $\int_{-\infty}^x F(u)\,du \ge \int_{-\infty}^x G(u)\,du$ for every $x$ , where $\bar F,\bar G$ and $F,G$ are the survival and distribution functions.

Formalization targets

Goal: the submartingale-coupling characterization (Theorem 4.A.5, increasing convex case)

X \le_{icx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]\ge\hat X\text{ a.s.}

Furthermore, $\hat X,\hat Y$ can be chosen so that $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$ ). This is the increasing-convex analogue of Chapter III's Theorem 3.A.4: instead of a martingale, $\{\hat X,\hat Y\}$ need only be a submartingale — the copy of $Y$ is, conditionally on the copy of $X$ , at least a fair randomization of it. The book states its proof is "similar to the proof of Theorem 3.A.4" and calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Companion: the supermartingale-coupling characterization (Theorem 4.A.5, increasing concave case)

The same theorem's other bracketed case: $X \le_{icv} Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$ , $\hat Y=_{st}Y$ , and $\{\hat Y,\hat X\}$ a supermartingale, $E[\hat X\mid\hat Y]\le\hat Y$ a.s. — note the swapped roles of $\hat X$ and $\hat Y$ in the conditioning relative to the increasing-convex case, not merely a flipped inequality. Drafted as a separate Lean theorem from the goal (see Formalization scope), since the two conditioning structures are genuinely different predicates, not sign-flipped rewrites of one another.

Supporting milestones

Theorem 4.A.1, the duality relation: $X\le_{icx}Y \iff -X\ge_{icv}-Y$ , and $X\le_{icv}Y\iff -X\ge_{icx}-Y$ — the increasing-order analogue of Theorem 3.A.12(a)'s duality for the plain convex order.
Theorem 4.A.2, the tail-integral characterizations above, for integrable $X,Y$ .
Theorem 4.A.8(d), closure under convolution: independent $X_i\le_{icx}Y_i$ (resp. $\le_{icv}$ ) for $i=1,\dots,m$ gives $\sum_i X_i \le_{icx} \sum_i Y_i$ (resp. $\le_{icv}$ ) — the increasing-order analogue of Chapter III's Theorem 3.A.12(d), which the book itself says "can be proven as in Theorem 3.A.12."

Significance

The increasing convex and concave orders are the natural language of expected-utility comparisons: a risk-averse agent with concave utility $u$ prefers $Y$ to $X$ exactly when $X\le_{icv}Y$ implies $E[u(X)]\le E[u(Y)]$ for every increasing concave $u$ — the order is defined precisely so that "every risk-averse agent with increasing utility agrees" collapses to one comparison. In operations research this underlies stochastic dominance of the second kind in portfolio and inventory models, and the increasing-convex order similarly formalizes "second-order stochastic dominance for costs" used to compare random cost/loss distributions under risk-loving or regret-averse preferences. The submartingale-coupling characterization is what turns the intractable "for every increasing convex $\varphi$ " quantifier into a single explicit construction, exactly as Strassen's theorem does for the plain convex order — and, being the direct chapter-IV successor to Chapter III's coupling theorem in this series, it fixes the second data point for what a "coupling-characterization" mission in this book's series looks like when the order being characterized is not symmetric between the two variables' roles.

No platform prior art exists: GET /theorems?q=increasing+convex, q=increasing+concave, and q=submartingale return zero genuinely matching hits (the one submartingale hit, a bandit subgaussian maximal inequality, uses Doob's inequality for a concentration bound, not this order). This mission restates the increasing convex/concave orders and their coupling characterization as a foundational, self-contained pair of definitions, parallel in structure to Chunk 03's convex-order mission but independently drafted (drafts cannot import each other's Lean).

Difficulty

The chief formalization risk is the one this chapter's own brief flags explicitly: the book states Theorem 4.A.5 as a single statement with bracketed alternatives (" $X\le_{icx}Y$ [ $X\le_{icv}Y$ ] iff … $\{\hat X,\hat Y\}$ is a submartingale [ $\{\hat Y,\hat X\}$ is a supermartingale] …"), and the two cases are not symmetric rewrites of each other — the conditioning variable in E[Ŷ|X̂]≥X̂ swaps to E[X̂|Ŷ]≤Ŷ in the concave case, not just a flipped inequality on the same conditioning. A Lean statement that tried to unify both cases with a single Or or a naive sign-flip would either conflate two different predicates or silently state the wrong condition for one of the two cases. The duality theorem (4.A.1) compounds this risk in the other direction: its content is exactly that $\le_{icx}$ and $\ge_{icv}$ are related (by negating the variables), so a formalization that makes this equivalence provable by unfolding definitions (rather than as a genuine ↔ between two independently-stated predicates) would trivialize the one theorem whose entire content is that relationship.

Formalization scope

Random variables are measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, matching this series' convention; IcxOrder μ ν X Y and IcvOrder μ ν X Y are drafted as two separate definitions (not one order parametrized by an Or of function classes), each quantifying over Monotone φ ∧ ConvexOn ℝ Set.univ φ (resp. ConcaveOn) with the two expectations' existence stated as explicit Integrable hypotheses inside the ∀, exactly as Chunk 03's ConvexOrder. Equality in law is ProbabilityTheory.IdentDistrib. The goal's submartingale condition uses Mathlib's conditional-expectation notation X̂ ≤ᵐ[ρ] ρ[Ŷ | m] with m the σ-algebra generated by X̂; its companion's supermartingale condition uses ρ[X̂ | m'] ≤ᵐ[ρ] Ŷ with m' generated by Ŷ instead — the conditioning variable is genuinely swapped between the two theorems, matching the book's own bracket ordering {X̂,Ŷ} vs. {Ŷ,X̂}. The "Furthermore" clause in both is kept (not dropped), via Mathlib's ProbabilityTheory.condDistrib, restated as the relevant conditional-distribution kernel's survival function being monotone at every threshold — the same shape Chapter I's UsualOrder and Chunk 03's goal theorem use, necessarily restated locally since drafts cannot import another mission's definitions.

Theorem 4.A.1 (duality) and Theorem 4.A.8(d) (convolution closure) are each drafted as a single Lean theorem with two independent conjuncts (an ∧ of two ↔s, or of two implications), one per bracketed case, since the book states both cases as the two halves of one theorem sharing every hypothesis — this is not the same shape as the goal/companion split, where the two cases have genuinely different internal structure (the swapped conditioning) rather than a shared statement instantiated at two function classes. A trivializing formalization this mission rules out: stating Theorem 4.A.1's duality by relabeling IcvOrder as IcxOrder applied to negated arguments (making the equivalence a rfl or single simp unfolding) rather than keeping the two orders as independently-defined predicates whose relationship is the theorem's actual content.

This mission draws on no platform prior art (searches for "increasing convex", "increasing concave", and "submartingale" as of 2026-09-18 return zero genuine matches — the sole submartingale hit is an unrelated bandit concentration inequality via Doob's inequality). Reusable beyond this mission: the IcxOrder/IcvOrder definition pattern and the submartingale/supermartingale coupling shape parallel Chunk 03's ConvexOrder martingale-coupling pattern closely enough that a future chapter needing "coupling characterization of a location-and-spread order" (none of the remaining chapters currently in this series' first wave) could restate the same shape with minimal adaptation.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 4 (Univariate Monotone Convex and Related Orders), §4.A. https://doi.org/10.1007/978-0-387-34675-5
This series' Chunk 03 (StochasticOrders.Convex), for the plain convex order and Strassen's martingale coupling this chapter's submartingale/supermartingale coupling directly generalizes.

9 thms4 active users

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

First-Order and Stochastic Optimization Methods for Machine Learning IV: Variance-Reduced Mirror Descent for Finite-Sum ProblemsTextbook

Motivation

Empirical-risk-minimization objectives in machine learning are finite sums: $\Psi(x) = \frac{1}{m}\sum_{i=1}^m f_i(x) + h(x)$ , one smooth term $f_i$ per training example (or per worker, in a distributed setting), plus a simple nonsmooth regularizer $h$ . Chapter 4's basic stochastic mirror descent handles this by sampling a single random component gradient $\nabla f_{i_t}(x)$ as an unbiased estimator of $\nabla f(x)$ — but that estimator's variance is a constant throughout the algorithm, which caps the achievable convergence rate. Variance-reduced mirror descent asks a sharper question: can an unbiased finite-sum gradient estimator be built whose variance itself vanishes as the algorithm approaches the optimum? The answer — periodic full-gradient snapshots combined with single-component corrections — is the SVRG-style idea this mission formalizes in Lan's general-norm mirror-descent framework, with an explicit, sampling-distribution-dependent constant rather than a generic $O(\cdot)$ .

Setting

Fix a closed convex set $X$ in a real normed space $E$ , and the finite-sum composite problem $\min_{x\in X}\{\Psi(x):=f(x)+h(x)\}$ (Eq. (5.3.1)), where $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ is the average of $m$ smooth convex component functions, each with $L_i$ -Lipschitz gradient $\nabla f_i$ ( $\|\nabla f_i(x)-\nabla f_i(y)\|_*\le L_i\|x-y\|$ ), and $h$ is a simple, possibly nondifferentiable convex function. $f$ is possibly $\mu$ -strongly convex, $\mu\ge0$ (Eq. (5.3.2)); this mission's goal takes $\mu=0$ (§5.3.1, "Smooth Problems Without Strong Convexity"). A fixed probability distribution $Q=\{q_1,\dots,q_m\}$ on the component indices governs the algorithm's random sampling, and

L_Q := \frac{1}{m}\max_{i=1,\dots,m}\frac{L_i}{q_i}

is the section's key aggregate smoothness constant (Eq. (5.3.4)), replacing the plain average $L$ wherever component-wise variance enters the analysis. Variance-reduced mirror descent (Algorithm 5.6) is a multi-epoch method: each epoch of length $T_s$ recomputes a full gradient $\nabla f(\tilde x)$ at a snapshot point $\tilde x$ , then runs $T_s$ inner iterations using the estimator $G_t := \big(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(\tilde x)\big)/(q_{i_t}m) + \nabla f(\tilde x)$ and the mirror-descent-with-composite-term update $x_{t+1}:=\arg\min_{x\in X}\{\gamma[\langle G_t,x\rangle+h(x)]+V(x_t,x)\}$ , where $V$ is the Bregman divergence of a fixed distance-generating function, exactly as in Chapters 3-4.

Formalization targets

Goal — Corollary 5.8

With $\theta=1$ , $\gamma=1/(16L_Q)$ , and the doubling epoch schedule $T_1=7$ , $T_s=2T_{s-1}$ (Eq. (5.3.17)),

\mathbb E[\Psi(\bar x_S)-\Psi(x^*)] \le \frac{8}{2^{S-1}}\left[\frac{11}{4}\big(\Psi(x_0)-\Psi(x^*)\big)+16L_Q\,V(x_0,x^*)\right]

for every epoch count $S\ge1$ , where $\bar x_S$ is the weighted average of the epoch snapshots (Eq. (5.3.16)).

Supporting milestones, in attack order

Lemma 5.12 — the per-component gradient-variation bound $\frac1m\sum_i\frac1{mq_i}\|\nabla f_i(x)-\nabla f_i(x^*)\|_*^2 \le 2L_Q[\Psi(x)-\Psi(x^*)]$ , the basic smoothness consequence from which the estimator's variance bound is built.
Lemma 5.13 — unbiasedness ( $\mathbb E[\delta_t]=0$ ) and two variance bounds ( $\mathbb E[\|\delta_t\|_*^2]\le 2L_Q[\dots]$ and $\le 4L_Q[\dots]$ ) for the variance-reduced estimator's error $\delta_t:=G_t-\nabla f(x_t)$ .
Lemma 5.14 — the one-step progress bound combining Lemma 5.13's variance control with the mirror-descent update's three-point inequality.
Theorem 5.6 — the general epoch-level convergence bound (with an arbitrary epoch-length schedule $T_s$ and stepsize $\gamma$ satisfying $4L_Q\gamma\le1$ ) that Corollary 5.8 instantiates.

Every constant is exactly the book's: $L_Q$ 's own sampling-distribution-dependent definition (never specialized to uniform $q_i=1/m$ ), and Corollary 5.8's explicit $8/2^{S-1}$ , $11/4$ , $16L_Q$ — not a generic $O(\cdot)$ — are all taken verbatim.

Significance

This is the series' first genuinely finite-sum result: unlike Chapters 3-4's single abstract objective $f$ , here $f$ is structurally a named average of $m$ component functions, and the sampling distribution $\{q_i\}$ over those components is a first-class free parameter of both the algorithm and the analysis (not fixed to uniform sampling) — $L_Q$ itself depends on this choice, and a formalization that hard-codes $q_i=1/m$ would understate what Lemma 5.12's own proof needs. Getting Theorem 5.6/Corollary 5.8 right also requires keeping two nested indices straight: inner iterations $t$ within an epoch, and outer epoch counts $s$ , with the convergence bound stated in terms of the epoch count $S$ alone — and keeping the two "gap" quantities $\Psi(x_0)-\Psi(x^*)$ (an objective-value gap) and $V(x_0,x^*)$ (a Bregman-divergence gap) distinct throughout, since they enter Corollary 5.8's final bound with different explicit coefficients ( $11/4$ vs. $16L_Q$ ) and neither generically bounds the other.

No result on the platform models a finite-sum objective with $m$ named component functions sampled by a general index distribution $\{q_i\}$ , a variance-reduction snapshot/anchor point, or this specific SVRG-style estimator, as of 2026-09-18 (q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, q=mirror descent finite sum — see Prior art below).

Difficulty

The central difficulty is Theorem 5.6's own epoch-weight sequence $w_s$ : the book defines $w_s:=(1-4L_Q\gamma)(T_{s-1}-1)-4L_Q\gamma T_s$ explicitly only for $s\ge2$ (Eq. (5.3.14)), yet the displayed sums $\sum_{s=1}^S w_s$ in (5.3.15)-(5.3.16) run from $s=1$ . A 2026-09-19 revision found that this, combined with the epoch snapshot $\tilde x_s$ being constrained only by membership in $X$ and not tied to the algorithm's own dynamics, made the originally drafted statements false, not merely incomplete: an adversarial, unboundedly-large- $\Psi$ , $\omega$ -independent $\tilde x_1$ together with $w_1\to\infty$ violates the stated conclusion. The fix restores the connection via an auxiliary epoch-boundary sequence and the per-epoch progress inequality Theorem 5.6's own proof derives from Lemma 5.14 (see epoch_convergence_bound's hepoch hypothesis), and resolves $w_1$ by extending (5.3.14)'s domain to $s\ge1$ via a fixed "epoch 0" length $T_0$ — w_1 is no longer left free beyond positivity. finite_sum_variance_reduced_rate instantiates $T_0:=T_1/2=3.5$ concretely, reproducing the arithmetic Corollary 5.8's own proof is internally consistent with ( $w_1 = 3/4(3.5-1)-1/4\cdot7 = 1/8$ , matching the closed form $(1/8)T_1-3/4=1/8$ ) — this was previously only a documented-but-unresolved observation, not yet a stated hypothesis.

Formalization scope

All five items are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching the mirror-descent chunks' general-norm convention (never specialized to Euclidean space or squared distance) — $V$ is a free two-point function throughout, and each $\nabla f_i$ , $\nabla f$ , $G_t$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed. This is the trivializing formalization this mission rules out: hard-coding $q_i=1/m$ (uniform sampling) or $V(x,y)=\frac12 \|x-y\|^2$ (Euclidean Bregman divergence) would understate both $L_Q$ 's dependence on the sampling distribution (the whole point of Lemma 5.12's bound) and the general-norm apparatus the rest of this book series shares.

Ψ(x_0)-Ψ(x^*) and V(x_0,x^*) are kept as two syntactically distinct terms throughout — never conflated or bounded one by the other — matching Corollary 5.8's own two separate coefficients. Corollary 5.8's own explicit constants ( $8/2^{S-1}$ , $11/4$ , $16L_Q$ ) are stated verbatim rather than left as an unspecified $O(\cdot)$ , per Hard Rule 6.

Left out of scope, for time: the gradient-computation-count complexity bound (Eq. (5.3.19), an $O(\cdot)$ statement about total oracle calls, not a convergence-rate inequality on $\Psi$ ) and §5.3.2's strongly-convex case (Theorem 5.7, a geometric-decay bound $\Delta_s\le\rho\Delta_{s-1}$ under $\mu>0$ ) are natural continuations reusing this mission's variance_reduced_progress_bound milestone, not attempted here.

Prior art

q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, and q=mirror descent finite sum were all searched on 2026-09-18. The only topically-adjacent hit across all six queries is ShiOptRates.Stochastic.variance_purchase_ classical ("Classical variance reduction is cost-neutral..."), which models plain minibatch SGD on a smooth objective with an i.i.d.-noise oracle characterized by a single scalar variance $\hat\sigma^2$ and a minibatch-size trade-off — no finite-sum structure with $m$ named component functions, no sampling distribution $\{q_i\}$ , no snapshot/anchor point $\tilde x$ , and a different question (cost-neutrality of minibatch size vs. this mission's convergence rate for a fixed variance-reduction scheme). Not reused; every item in this mission is drafted fresh.

Selected references

G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 5, §5.3. https://doi.org/10.1007/978-3-030-39568-1
R. Johnson, T. Zhang, "Accelerating stochastic gradient descent using predictive variance reduction," Advances in Neural Information Processing Systems (NeurIPS), 2013 (the SVRG estimator this section's gradient estimator generalizes to the composite mirror-descent setting).
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.

10 thms4 active users

Completed

Markov Chain Operations Research·Captain: naimengye

Stochastic Networks III: Loss Networks and the Erlang Fixed PointTextbook

Motivation

Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.

The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link $j$ is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.

Setting

The links are $\mathcal{J} = \{1,\dots,J\}$ , link $j$ carrying $C_j$ circuits. A route $r$ belongs to a set $\mathcal{R}$ of $R$ routes, and the link-route incidence matrix $A$ records how much of each link a route needs: a call on route $r$ requires $A_{jr}$ circuits from link $j$ and is lost if any link has fewer than $A_{jr}$ free. (The classical case is $A$ a $0$ – $1$ matrix and $A_{jr}=1$ exactly when $j\in r$ ; from section 3.3 the book allows any non-negative integers.)

Calls requesting route $r$ arrive as a Poisson process of rate $\nu_r$ , independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing $n_r$ for the number of calls in progress on route $r$ , the process $n=(n_r)$ is Markov on

S(C)=\{n\in\mathbb{Z}_+^{R} : An\le C\},

and is called a loss network with fixed routing.

Write $E(\nu,C)$ for Erlang's formula, $E(\nu,C)=\dfrac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}$ , published in mission I of this series. The Erlang fixed point equations are

E_j \;=\; E\!\left((1-E_j)^{-1}\sum_r A_{jr}\,\nu_r\prod_i (1-E_i)^{A_{ir}},\; C_j\right), \qquad j=1,\dots,J. \tag{3.7}

The factor $(1-E_j)^{-1}$ removes link $j$ 's own thinning from the product, so in the $0$ – $1$ case the argument is $\sum_{r\ni j}\nu_r\prod_{i\in r\setminus\{j\}}(1-E_i)$ , the reduced load offered to link $j$ .

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

\exists!\,(E_1,\dots,E_J)\in[0,1]^J \text{ satisfying } (3.7).

The goal fixes no formula for $E$ and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube $[0,1]^J$ ; uniqueness is the substance.

Supporting levels

The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution $\pi(n)=G(C)\prod_r \nu_r^{n_r}/n_r!$ on $S(C)$ ; and the acceptance probability $1-L_r=G(C)/G(C-Ae_r)$ . Then the optimization side: that $E(\nu,C)$ and the utilization $\nu(1-E(\nu,C))$ are strictly increasing in $\nu$ , which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on $B$ , equation (3.6).

Significance

The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by $\int_0^{y_j}U(z,C_j)\,dz$ . That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector $B$ coming from the maximum-probability problem.

Formalizing it. Nothing here is open. What the mission produces is the loss network model in Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked statement of the object the reduced-load approximation computes. It is also where this series' earlier missions pay off: the uncapacitated network is literally the open migration process of mission II with $\lambda\equiv 0$ , $\mu\equiv 1$ , $\varphi_j(n)=n$ , and the exact distribution (3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I published.

Difficulty

Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization $\nu\bigl(1-E(\nu,C)\bigr)$ is strictly increasing in $\nu$ , which is itself a milestone here.

A second, formal difficulty: the equations involve $(1-E_j)^{-1}$ , so a solution with $E_j=1$ would be meaningless. It is worth checking before starting that no such solution exists for $C_j\ge 1$ , rather than assuming it.

Formalization scope

Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only $0$ – $1$ ), capacities are natural numbers, and arrival rates are positive reals. The feasible set $S(C)$ is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.

Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route $r$ is $n_r$ and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; $G(C)$ is the reciprocal of the sum in the book's notation. Capacities are assumed at least $1$ in the goal: a link with no circuits blocks everything, $E(\nu,0)=1$ identically, and the factor $(1-E_j)^{-1}$ would then be undefined rather than merely large.

The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.

Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the $0$ – $1$ equations (3.1) of section 3.2; the utilization function $U(y,C)$ and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.

Selected references

Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 3 (pp. 49–82); Lemma 3.4, equation (3.3), Theorems 3.10 and 3.20, equations (3.1), (3.5)–(3.9). DOI 10.1017/cbo9781139565363
F. P. Kelly, Loss networks, Annals of Applied Probability 1 (1991), 319–378. DOI 10.1214/aoap/1177005872
F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18 (1986), 473–505. DOI 10.2307/1427303
R. B. Cooper and S. Katz, Analysis of alternate routing networks with account taken of the nonrandomness of overflow traffic, Bell Telephone Laboratories memorandum, 1964.
Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1 on truncation.

14 thms4 active usersReviewed

Completed

Markov Chain Probability·Captain: Shuze Chen

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$ ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.

Setting

All chains live on a finite state space $V$ with a transition matrix $P$ ; $P^t(x,\cdot)$ is the time- $t$ distribution from $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A coupling of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$ .

Given a metric-like cost $\rho$ on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:

\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.

Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$ , the path metric $\rho(x,y)$ is the least total length of a $G$ -path from $x$ to $y$ .

For the colorings application: a $q$ -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.

Formalization targets

Goal

Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$ -colorings, if $q>2\Delta$ then

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.

Milestones

Lemma 14.3 and Remark 14.2 — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
Theorem 14.6, path coupling (Bubley–Dyer) — if for every edge $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$ .
Corollary 14.7 — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$ , where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
Theorem 14.12, approximate counting — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$ -colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.

Significance

The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$ -hard counting problems.

Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.

Difficulty

The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.

Formalization scope

The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$ " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
R. Bubley, M. Dyer, Path coupling: a technique for proving rapid mixing in Markov chains, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
M. Jerrum, A very simple algorithm for estimating the number of k-colorings of a low-degree graph, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
M. Jerrum, L. Valiant, V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X

9 thms4 active usersReviewed

Completed

Markov Chain Probability·Captain: Shuze Chen

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

A reversible Markov chain is an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$ , and the Matthews method bounding cover times by hitting times with harmonic-number precision.

Setting

A network is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities

P(x,y)=c(x,y)/c(x)

where $c(x)=\sum_y c(x,y)$ , and $c_G=\sum_x c(x)$ . A function $h$ is harmonic at $x$ if $h(x)=\sum_y P(x,y)h(y)$ . The voltage with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ , the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$ , and the effective resistance is $R(a\leftrightarrow z)=\|I\|^{-1}$ . A flow from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$ ; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$ . Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$ , their expectations, the Green's function $G_{\tau_z}(a,x)$ , the maximal hitting time $t_{\mathrm{hit}}$ , and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.

Formalization targets

Goal

\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).

This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.

Milestones

Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$ ); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$ ); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$ ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$ ); Proposition 11.4 (the matching Matthews lower bound over subsets).

Significance

The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.

Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.

Difficulty

The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.

Formalization scope

Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.

Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057
A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, The electrical resistance of a graph captures its commute and cover times, STOC 1989. https://doi.org/10.1145/73007.73062
P. Matthews, Covering problems for Markov chains, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894

15 thms4 active usersReviewed

Completed

Markov Chain Probability·Captain: Shuze Chen

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$ . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$ , so nothing in the subject can be formalized before this mission is.

This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$ ). Later missions in the series build on the definitions published here.

Setting

A chain on a finite state space $\Omega$ is presented by its transition matrix, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$ . A distribution is a row vector $\mu$ with nonnegative entries summing to $1$ ; one step of the chain carries $\mu$ to $\mu P$ , and the $t$ -step transition probabilities are the entries of the matrix power $P^t$ .

The chain is irreducible if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$ . The period of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$ , and the chain is aperiodic if every state has period $1$ . A distribution $\pi$ is stationary if $\pi P = \pi$ , and $\pi$ and $P$ are in detailed balance (the chain is reversible) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$ .

Trajectory events over a finite horizon are finite sums of path weights: a length- $t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$ , with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$ , and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$ , formalized as a tsum over $t$ .

Formalization targets

Goal

$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$

This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.

Milestones toward and around the goal

The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with

\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1

(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).

Significance

The result itself. Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.

Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.

Difficulty

The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$ , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.

Formalization scope

States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$ , which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$ ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.

Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. R. Norris, Markov Chains, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html

20 thms4 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Learning Unknown Service Rates in Queues 3: In Heavy Traffic Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least D(μ)(K−1) log t / (4 log log t) Up to Time (K−1)D(μ)/(4ε)Research Paper

Motivation

A switch network is a set of $U$ queues served by $K\ge U$ servers. In every time slot each server can serve at most one queue, so a scheduler must pick a matching of queues to servers. Such systems model input-queued packet switches, crowdsourcing platforms that route job types to worker types, and wireless links with unknown channel quality. When the success probability of each queue–server link is unknown, the scheduler has to learn it from the services it observes while the queues are building up. This makes switch scheduling a multi-armed bandit problem in which the cost is not cumulative reward but queue length.

Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377, Operations Research 2021) measure a scheduler by its queue-regret: the expected difference between its queue lengths and those of a genie that knows the best matching. They show that the queue-regret has two regimes. In the late stage, once the queues regularly empty, it decays like $1/t$ (their Theorem 3, the subject of a sibling mission). In the early stage it grows like $\log t/\log\log t$ , as the regret of a classical bandit does, and the system is then effectively unstable. This mission is about the early stage, made precise in the paper's Theorem 8: in heavy traffic, where the arrival rates are close to the best service rates, every reasonable policy pays logarithmic queue-regret for a long time.

The lower-bound technique descends from Lai and Robbins (1985): a policy that does well on every instance must explore each sub-optimal link about $\log t/\mathrm{KL}$ times, a count obtained by a change of measure and the Bretagnolle–Huber inequality.

Setting

Queues are indexed by $u\in[U]$ and servers by $k\in[K]$ . In every slot $t\ge1$ , queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ , and link $(u,k)$ offers a service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$ . All of these are independent and i.i.d. over slots. Notation:

$\mu^*_u=\max_k\mu_{uk}$ , attained at $k^*_u$ ;
$\epsilon_u=\mu^*_u-\lambda_u$ and $\Delta_{uk}=\mu^*_u-\mu_{uk}$ ;
$\Delta=\min_{u,k\ne k^*_u}\Delta_{uk}$ , $\mu_{\min}=\min\mu_{uk}$ and $\mu^*=\max\mu_{uk}$ ;
$\bar\epsilon=\frac1U\sum_u\epsilon_u$ .

Assumption 1 asks that every queue have a unique best server and that the best servers of distinct queues be distinct. Assumption 2 is $\epsilon_u>0$ for every $u$ . Assumption 3 draws the initial queue vector from the stationary law of the genie queues.

A scheduler picks a matching $\kappa(t)$ , so queue $u$ is served by server $\kappa_u(t)$ . Its decision may use the past schedules, the services observed on the scheduled links, and private randomness. The queues evolve as $Q_u(t)=(Q_u(t-1)+A_u(t)-R_{u\kappa_u(t)}(t))^+$ . The genie always schedules $k^*$ and has queues $Q^*_u(t)$ . The queue-regret is $\Psi_u(t)=\mathbb E[Q_u(t)-Q^*_u(t)]$ . The schedule counts are $T_{uk}(t+1)=\sum_{s=1}^t\mathbb 1\{\kappa_u(s)=k\}$ .

A policy is $\alpha$ -consistent ( $\alpha\in(0,1)$ ) if on every instance $\mathbb E[T_{uk}(t+1)]\le C\,t^{\alpha}$ for all $u$ and all $k\ne k^*_u$ , with a constant $C$ that may depend on the instance. The key constant is

D(\mu)=\frac{\Delta}{\mathrm{KL}\big(\mu_{\min},\frac{\mu^*+1}{2}\big)},

where $\mathrm{KL}$ is the Bernoulli Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 8 (p. 18)

Fix $\mu$ , an $\alpha$ -consistent policy and $\gamma>1/(1-\alpha)$ . There exist constants $\tau$ and $C_1$ , the same for every arrival vector $\lambda$ , such that, with $T_0=\max\{C_1K^\gamma,\tau\}$ and $\eta=(K-1)D(\mu)/(2T_0)$ :

\bar\epsilon<\tfrac\eta2\ \Longrightarrow\ \frac1U\sum_u\Psi_u(t)\ge\frac{D(\mu)}4(K-1)\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{4\bar\epsilon}\Big],

\epsilon_u<\eta\ \Longrightarrow\ \Psi_u(t)\ge\frac{D(\mu)}4\max\{U-1,2(K-U)\}\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{2\epsilon_u}\Big].

Milestones

Lemma 18 (Bretagnolle–Huber, p. 37), referenced from the platform.
Lemma 19 (p. 37): for $t>\tau$ , $\mathbb E[T_{uk}(t+1)]+\sum_{u'\ne u}\mathbb 1\{k^*_{u'}=k\}\mathbb E[T_{u'k^*_u}(t+1)]\ge\frac{(1-\alpha)\log t-\log(4KC)}{\mathrm{KL}(\mu_{\min},(\mu^*+1)/2)}$ .
Corollary 20 (p. 39): the summed forms of Lemma 19, with factors $U(K-1)D(\mu)$ , $(U-1)D(\mu)$ and $(K-U)D(\mu)$ .
Lemma 22 (p. 42): $\Psi_u(t)\ge\sum_{k\ne k^*_u}\Delta_{uk}\mathbb E[T_{uk}(t+1)]-\epsilon_u t$ for any policy.

Significance

Theorem 8 complements the late-stage $1/t$ lower bound. Together they show that queue-regret goes through a phase transition. Up to time of order $K/\epsilon$ , the queue-regret of any consistent policy grows like $\log t/\log\log t$ . Since the left end of the window does not move as $\epsilon\to0$ while the right end grows like $1/\epsilon$ , the heavily loaded regime is exactly where learning costs are visible in queue lengths. The theorem also explains why algorithms designed for the late stage (Q-UCB, Q-ThS in the same paper) cannot avoid this early cost.

The formalization adds a machine-checked statement of a lower bound whose constants are pinned down precisely. In particular it states which quantities $\tau$ and $C_1$ may depend on (see below). Along the way it builds a reusable model of a learning switch scheduler: randomized, history-dependent policies, the coupled genie system and the stationary initial law. It also provides a Lai–Robbins-type count bound (Lemma 19) for matching bandits. The results are proved on paper in the held preprint (§9.2). To the best of the platform's records none of them has been formalized.

Difficulty

The obvious route to Theorem 8 is to bound the queue-regret below by the regret of the corresponding bandit. That fails, because queue-regret is not cumulative: an empty queue forgives past mistakes. The proof therefore needs the stationary start (Assumption 3), so that $\mathbb E[Q^*_u(t)]=\mathbb E[Q_u(0)]$ and the sub-optimal schedules show up as a drift (Lemma 22). This holds only up to a load term $\epsilon_u t$ , which limits the window.

The count bound (Lemma 19) requires a change of measure between two instances that swap the best servers of two queues. It needs a chain rule for the KL divergence of adaptively collected observations, where the policy's own randomness must cancel. Neither the swapped instances nor the trajectory law are standard Mathlib objects.

Formalization scope

Queues are Fin U and servers are Fin K, with $1\le U\le K$ and $K\ge2$ . $K=1$ is trivial, and for it $\Delta$ is an empty minimum.
Slots are 1-based. Matchings are embeddings Fin U ↪ Fin K.
Probability space. The randomness is a product of independent uniforms on $[0,1]$ per slot (arrivals, link services, one private scheduler seed), i.i.d. over slots. Bernoulli variables arise by thresholding. The initial state is drawn independently.
Policies see only past schedules and the services on scheduled links (p. 6), plus a private uniform. This covers every randomized, history-dependent policy, and each choice is required to be measurable in the seed.
The genie shares the initial state, arrivals and services of the policy's system. Queue-regret is a Lebesgue integral of $Q_u(t)-Q^*_u(t)$ , a difference bounded by $t$ .
Assumption 3 is the product of the geometric laws $(1-\rho_u)\rho_u^n$ , $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$ . This is the stationary law of the printed recursion.
α-consistency quantifies over every instance with entries in $[0,1]$ satisfying Assumption 1. The constant is chosen after the instance, and the definition does not mention $\lambda$ , because the schedule does not depend on it.
$D(\mu)$ and $1/\mathrm{KL}$ are set to $0$ when $\mu^*=1$ , where the divergence is infinite.
Lemma 19 and Corollary 20 carry $C>0$ , which is without loss of generality. Corollary 20(c)'s sum $\sum_{k>U}$ is the sum over servers that are optimal for no queue.
Constants of Theorem 8. The paper says $\tau,C_1$ are "independent of $(\lambda,\mu)$ ". Its proof supports independence of $\lambda$ only, so the formal statement chooses $\tau,C_1$ after $\mu$ and the policy but before $\lambda$ . Choosing them after $\lambda$ would trivialize the theorem, since a huge $C_1$ makes the hypothesis $\bar\epsilon<\eta/2$ unsatisfiable. The formal $\tau$ also exceeds $e$ , so that $\log\log t>0$ on the window, and $t$ ranges over integers.
Assumptions. Assumptions 1–3 appear exactly where the paper uses them: Lemma 22 and Theorem 8 assume all three, Lemma 19 and Corollary 20 only Assumption 1.

The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9. Welcome contributions include the KL chain rule for adaptively scheduled Bernoulli observations, stationarity of the geometric law for the genie chain, and measurability of the trajectory.

Selected references

S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021; preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
S. Bubeck, V. Perchet, P. Rigollet, Bounded regret in stochastic multi-armed bandits, COLT 2013. https://arxiv.org/abs/1302.1611

9 thms3 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Learning Unknown Service Rates in Queues 1: Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least λ_min D(μ)(1−α)(K−1)/(8t) for Infinitely Many tResearch Paper

Motivation

Many service systems must route work to servers whose quality is not known in advance: crowdsourcing platforms matching job types to worker types, wireless schedulers assigning users to channels, call centers routing request classes to agent pools. Learning the unknown service rates is a multi-armed bandit problem, but the cost of a bad decision is not a lost reward. It is a longer queue, and a queue can recover from past mistakes when it empties. Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377v4, Operations Research 2021, doi:10.1287/opre.2020.1995) measure the cost of learning by the queue-regret, the expected excess queue length relative to a genie that knows the rates. Their analysis shows two regimes. Early on the regret grows like a bandit regret. After the system has learned enough to stabilize, queues regenerate and the regret decays. This mission formalizes their lower bound for the second regime: no reasonable learning policy can make the late-stage queue-regret decay faster than $1/t$ .

The lower bound adapts the classical consistency-based bandit lower bounds of Lai and Robbins (1985) and their non-asymptotic, hypothesis-testing form (Bubeck, Perchet and Rigollet 2013) to queue dynamics. The step from counts of suboptimal schedules to queue lengths is specific to queues.

Setting

A switch has $U$ queues and $K\ge U$ servers. Time is slotted, $t=1,2,\dots$ . In slot $t$ queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ , and the link between queue $u$ and server $k$ offers a service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$ . All of these are independent, and i.i.d. over slots. A problem instance is the pair $(\lambda,\mu)$ , with every entry in $[0,1]$ .

In every slot the scheduler picks a matching $\kappa(t)$ : queue $u$ is assigned server $\kappa_u(t)$ , and distinct queues get distinct servers. The scheduler knows neither $\lambda$ nor $\mu$ . Its decision in slot $t$ may use the past schedules, the services observed on the scheduled links in slots $1,\dots,t-1$ , and its own randomness. Queue $u$ receives $S_u(t)=R_{u\kappa_u(t)}(t)$ and evolves as

Q_u(t)=\big(Q_u(t-1)+A_u(t)-S_u(t)\big)^+ .

Assumption 1 (unique optimal matching) says that each queue $u$ has a unique best server $k^*_u$ , and that $u\ne u'$ implies $k^*_u\ne k^*_{u'}$ . The genie always schedules $k^*$ . Its queues $Q^*$ start from the same $Q(0)$ and see the same arrivals and offered services, with $S^*_u(t)=R_{uk^*_u}(t)$ . The queue-regret of queue $u$ is $\Psi_u(t)=\mathbb E[Q_u(t)-Q^*_u(t)]$ .

Write $\mu^*_u=\mu_{uk^*_u}$ , $\Delta_{uk}=\mu^*_u-\mu_{uk}$ , $\Delta=\min_{u,k\ne k^*_u}\Delta_{uk}$ , $\mu_{\min}=\min_{u,k}\mu_{uk}$ , $\mu^*=\max_{u,k}\mu_{uk}$ , $\lambda_{\min}=\min_u\lambda_u$ . With the Bernoulli divergence $\mathrm{KL}(p,q)=p\log\frac pq+(1-p)\log\frac{1-p}{1-q}$ , display (2) of the paper defines

D(\mu)=\frac{\Delta}{\mathrm{KL}\big(\mu_{\min},\tfrac{\mu^*+1}{2}\big)} .

Let $T_{uk}(t+1)=\sum_{s=1}^t\mathbf 1\{\kappa_u(s)=k\}$ . For $\alpha\in(0,1)$ , a policy is $\alpha$ -consistent (Definition 2) if for every instance with a unique optimal matching there is a constant $C(\lambda,\mu)$ with $\mathbb E[T_{uk}(t+1)]\le C(\lambda,\mu)\,t^\alpha$ for all $u$ and all $k\ne k^*_u$ . Consistency rules out policies tuned to one instance, such as "always schedule a fixed matching", which would have zero regret on that instance and linear regret elsewhere.

Formalization targets

Goal: Theorem 3 (p. 12)

For every instance with a unique optimal matching, every law of the initial queue lengths, every $\alpha\in(0,1)$ and every $\alpha$ -consistent policy:

\frac1U\sum_{u\in[U]}\Psi_u(t)\;\ge\;\frac{\lambda_{\min}}{8}D(\mu)(1-\alpha)(K-1)\cdot\frac1t\quad\text{for infinitely many } t,

\Psi_u(t)\;\ge\;\frac{\lambda_{\min}}{8}D(\mu)(1-\alpha)\max\{U-1,\,2(K-U)\}\cdot\frac1t\quad\text{for infinitely many } t,\ \text{for each } u.

Milestones

Lemma 18 (p. 37), the Bretagnolle–Huber inequality $P(\mathcal A)+Q(\mathcal A^c)\ge\frac12e^{-\mathrm{KL}(P\|Q)}$ . It is already proved on the platform and enters as a reference.
Lemma 19 (p. 37). For $t>\tau$ : $\mathbb E[T_{uk}(t+1)]+\sum_{u'\ne u}\mathbf 1\{k^*_{u'}=k\}\mathbb E[T_{u'k^*_u}(t+1)]\ge\frac{(1-\alpha)\log t-\log(4KC)}{\mathrm{KL}(\mu_{\min},(\mu^*+1)/2)}$ .
Corollary 20 (p. 39). The same bound summed over all queues, over one queue, and over the servers that are optimal for no queue.
Lemma 21 (p. 41). For any policy, $\Psi_u(t)\ge\lambda_u\sum_{k\ne k^*_u}\Delta_{uk}\,\mathbb P[\kappa_u(t)=k]$ .
Fact 1 (p. 42). If $\sum_{m\le n}a_m\ge C\log n$ eventually, then $a_n\ge C/(2n)$ infinitely often.

A companion item, Lemma 1 (p. 10), states $\Psi_u(t)\le\sum_{l=1}^t\mathbb E[S^*_u(l)-S_u(l)]$ : queue-regret never exceeds the bandit regret.

Significance

Theorem 3 shows that the paper's Q-UCB algorithm, whose late-stage queue-regret is $O(\log^3 t/t)$ (Theorem 5), is optimal in its dependence on $t$ up to polylogarithmic factors. It also separates queue-regret from bandit regret. The bandit regret of a consistent policy grows like $\log t$ , while the queue-regret decays to zero. The cost of learning in a queue is transient, but it cannot vanish faster than $1/t$ . The theorem holds for every initial law of the queues, so it does not depend on the system starting in steady state.

The proof is complete in the source (§9.1, pp. 37–42). As far as we know none of it is machine-checked. A formal development would also give the first formal bandit lower bound in which the consistency class must contain the alternative instances of a change-of-measure argument, here instances with two optimal servers swapped, together with a reusable model of a learning scheduler on a switch.

Difficulty

The obvious route is to bound the regret of each slot by the probability of a suboptimal schedule (Lemma 21), and to bound the number of suboptimal schedules from below by a Lai–Robbins argument. Both steps resist direct proof.

For the first step, $Q$ and $Q^*$ share arrivals and services but are not ordered pathwise, because the policy's services are independent across links. A comparison exists only in distribution.

For the second step, the alternative instance must again satisfy Assumption 1, so a single service rate cannot simply be raised. When server $k$ is the best server of another queue $u'$ , the best servers of $u$ and $u'$ must be swapped, and the divergence decomposition then involves two links.

The final step goes from a cumulative bound to an "infinitely often" bound, and only from a logarithmic lower bound on partial sums. A lower bound on cumulative regret does not give a bound for every large $t$ .

Formalization scope

Queues and servers are Fin U and Fin K (0-based), with $1\le U\le K$ . The hypothesis $K\ge2$ is added: for $K=1$ the policy and the genie coincide and both sides are zero, and the minimum defining $\Delta$ would range over an empty set. Slots are 1-based.

The probability space is canonical: $\Omega=\mathbb N^U\times\text{Seed}^{\mathbb N}$ with law $\nu\otimes\mathrm{Unif}^{\otimes\mathbb N}$ . A seed holds one uniform per arrival, one per link and one for the scheduler, and $A_u(t)=\mathbf 1\{W_u(t)\le\lambda_u\}$ , $R_{uk}(t)=\mathbf 1\{V_{uk}(t)\le\mu_{uk}\}$ . A policy maps the history of past schedules and observed services, together with a private uniform seed, to a matching. The only constraint is measurability in the seed, so every randomized history-dependent policy is covered. The law $\nu$ of $Q(0)$ is arbitrary, as the paper notes after Theorem 3, so Assumption 3 is not used. Assumption 2 (stability under the optimal matching, $\lambda_u<\mu^*_u$ for every $u$ ), which the paper assumes whenever queue-regret is evaluated (p. 8), is a hypothesis of Theorem 3 and of Lemmas 1 and 21. Lemma 19 and Corollary 20 concern schedule counts, which do not depend on the arrival rates.

$\Psi_u(t)$ is a Bochner integral of $Q_u(t)-Q^*_u(t)$ , which is bounded by $t$ . Expected counts are integrals under the seed law, since the schedule never observes arrivals or $Q(0)$ . $D(\mu)$ and $1/\mathrm{KL}$ are set to $0$ when $\mu^*=1$ , where the divergence is $+\infty$ . Corollary 20(c)'s $\sum_{k>U}$ becomes the sum over servers outside the range of $k^*$ . Fact 1 is stated for every real sequence: the printed "bounded" is not needed and does not hold in the application. "For infinitely many $t$ " is ∃ᶠ t in atTop.

$\alpha$ -consistency quantifies over every service matrix in $[0,1]^{U\times K}$ satisfying Assumption 1, and its constant is chosen after the instance. Requiring consistency on the given instance only would make Theorem 3 false, because the genie's own policy has $\Psi\equiv0$ . A constant chosen before the instance would make the hypothesis unsatisfiable.

A complete development needs the canonical seed space and its measurability, a chain rule for the KL divergence of the history laws, the Bretagnolle–Huber inequality (available), and an elementary harmonic-sum estimate. The switch model and the consistency class are reusable for the paper's early-stage lower bound and its upper bound. Proofs of any milestone, and alternative proofs of Lemma 21 that avoid the coupling, are welcome.

The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9.

Selected references

S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021. Preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377v4
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. https://doi.org/10.1016/0196-8858(85)90002-8
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009 (Lemma 2.6). https://doi.org/10.1007/b13794
S. Bubeck, V. Perchet, P. Rigollet, Bounded regret in stochastic multi-armed bandits, COLT 2013. https://arxiv.org/abs/1302.1611

8 thms3 active usersReviewed

Markov Chain Probability·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 5: PD(α, θ) Is a Y_1^θ-Tilt of Independent beta(θ + nα, 1) Ratios, and (Y_n) Is a Markov ChainResearch Paper

Motivation

The two-parameter Poisson–Dirichlet distribution $\mathrm{PD}(\alpha,\theta)$ is a law on decreasing sequences $V_1 \ge V_2 \ge \cdots > 0$ with $\sum_n V_n = 1$ . It describes the ranked frequencies of species in Bayesian nonparametric models (the Pitman–Yor process), the ranked lengths of excursions of Bessel processes and bridges, and the ranked cycle or block sizes in random combinatorial structures. The case $\alpha = 0$ is Kingman's one-parameter family $\mathrm{PD}(\theta)$ , the law of the ranked frequencies in the Ewens sampling formula.

For $\mathrm{PD}(0,\theta)$ , Vershik and Shmidt ([67]) and Ignatov ([34]) found a Markov description: the residual fractions $Y_n = V_n/(V_n + V_{n+1} + \cdots)$ form a homogeneous Markov chain, and the law is the $Y_1^\theta$ -tilt of a stationary chain built from independent $\mathrm{beta}(\theta,1)$ ratios. For $\mathrm{PD}(\alpha,0)$ , Proposition 8 of Pitman and Yor shows that the ratios $R_n = V_{n+1}/V_n$ themselves are independent $\mathrm{beta}(n\alpha,1)$ variables. Theorem 38 of Pitman and Yor (Ann. Probab. 25 (1997) 855–900) unifies both descriptions for the whole two-parameter family.

Timeline. Vershik and Shmidt (1977, 1978, [66, 67]) and Ignatov (1982, [34]) described the size-ordered $\mathrm{PD}(0,\theta)$ frequencies through the Markov chain $(Y_n)$ ; Ignatov showed that results of Vervaat and Watterson give the normalizing constant $K_{0,\theta} = \Gamma(\theta+1)e^{\theta\gamma}$ (132). Much of this was known earlier for $\theta = 1$ , the case arising in combinatorics and number theory. Perman, Pitman and Yor (1992, [51]) proved the absolute continuity of $\mathrm{PD}(\alpha,\theta)$ with respect to $\mathrm{PD}(\alpha,0)$ (Proposition 14 here). Pitman and Yor (1997) announced the two-parameter Markov description as Theorem 15 and proved it as Theorem 38 for $0<\alpha<1$ , quoting the case $\alpha = 0$ (Remark 40).

Setting

Fix $0 < \alpha < 1$ and $\theta > -\alpha$ . The beta distribution $\mathrm{beta}(a,b)$ ( $a,b>0$ ) has density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$ . Let $\tilde Y_1, \tilde Y_2, \dots$ be independent with $\tilde Y_n \sim \mathrm{beta}(1-\alpha, \theta+n\alpha)$ , and put $\tilde V_1 = \tilde Y_1$ , $\tilde V_n = (1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ . The ranked values $V_1 \ge V_2 \ge \cdots$ of $(\tilde V_n)$ have, by Definition 1, the law $\mathrm{PD}(\alpha,\theta)$ ; $P_{\alpha,\theta}$ denotes a probability under which $(V_n)$ has this law, and $E_{\alpha,\theta}$ its expectation.

From $(V_n)$ define the ratios $R_n = V_{n+1}/V_n$ (21), the residual fractions $Y_n = V_n/(V_n+V_{n+1}+\cdots)$ (45), and $\Sigma_1 = (1-V_1)/V_1$ . Conversely, from ratios define

Y_n = (1 + R_n + R_nR_{n+1} + \cdots)^{-1} \qquad (125).

The local time is $L = \lim_{n\to\infty} nV_n^\alpha$ (24).

The comparison law $P^*_{\alpha,\theta}$ makes $R_1, R_2, \dots$ independent with $R_n \sim \mathrm{beta}(\theta+n\alpha,1)$ , and $Y_n$ is then defined by (125). Constants and functions:

K_{\alpha,\theta} = \Gamma(\theta+1)\Gamma(1-\alpha)^{\theta/\alpha}, \qquad C_{\alpha,\theta} = \frac{K_{\alpha,\theta}}{\Gamma(\theta/\alpha+1)}, \qquad \psi_\alpha(\lambda) = 1 + \alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}dx.

Formalization targets

Goal: Theorem 38 for $0<\alpha<1$

E_{\alpha,\theta}[f(Y_1,Y_2,\dots)] = K_{\alpha,\theta}\,E^*_{\alpha,\theta}[Y_1^\theta f(Y_1,Y_2,\dots)] \qquad (137)

for every nonnegative product measurable $f$ ; under both $P_{\alpha,\theta}$ and $P^*_{\alpha,\theta}$ the sequence $(Y_n)$ is a Markov chain with the same forward transition probabilities, with density

\frac{P(Y_{n+1}\in dy_{n+1}\mid Y_n = y_n)}{dy_{n+1}} = \alpha\,y_n^{-\alpha-1}(1-y_n)^{n\alpha+\theta-1}\frac{r(\alpha,\theta+n\alpha,y_{n+1})}{r(\alpha,\theta+n\alpha-\alpha,y_n)} \qquad (139)

on $0<y_n<1$ , $0<y_{n+1}<y_n/(1-y_n)$ , where $r(\alpha,\theta,y)\,dy = \Gamma(\theta/\alpha+1)y^\theta P^*_{\alpha,\theta}(Y_1\in dy) = C^{-1}_{\alpha,\theta}P_{\alpha,\theta}(V_1\in dy)$ (140); and the $P^*_{\alpha,\theta}$ law of $\Sigma_1$ is infinitely divisible with

E^*_{\alpha,\theta}[e^{-\lambda\Sigma_1}] = \psi_\alpha(\lambda)^{-(\theta/\alpha+1)} \qquad (141).

Milestones

Proposition 8 ( $P_{\alpha,0} = P^*_{\alpha,0}$ on the ratios), Proposition 14 (the density $C_{\alpha,\theta}L^{\theta/\alpha}$ of $\mathrm{PD}(\alpha,\theta)$ relative to $\mathrm{PD}(\alpha,0)$ ), the moments (30) of $L$ , the representation (143) of $L$ through the ratios, the finite-dimensional change of measure (144), its limit (145), Proposition 37 (independent ratios give a Markov chain $(Y_n)$ , with co-transition density (128)), the parameter shift (146), and the conditional Laplace transform of $\Sigma_1$ given $X_1 = LV_1^{-\alpha}$ .

Significance

The result. Theorem 38 reduces the size-ordered $\mathrm{PD}(\alpha,\theta)$ frequencies to a product of independent beta variables, up to a density $K_{\alpha,\theta}Y_1^\theta$ that depends on $Y_1$ alone. Any functional of the ranked frequencies can therefore be computed under a product measure. The Markov property gives the joint density of $Y_1,\dots,Y_n$ (Corollary 41), the laws of individual $V_n$ (148), and the asymptotics of $Y_n$ and $\Sigma_n$ in §7.3 of the paper. Part (iii) identifies the law of $(1-V_1)/V_1$ under $P^*_{\alpha,\theta}$ , which determines the density of the largest frequency $V_1$ under $\mathrm{PD}(\alpha,\theta)$ .

The formalization. The result has been proved since 1997; none of it is machine-checked. The mission formalizes the paper's own route: absolute continuity (Proposition 14), the beta product structure (Proposition 8), and a limit of finite-dimensional density ratios. It produces reusable statements about real-valued Markov chains defined through conditional laws, and about changes of measure between infinite products. Note that the printed (139) omits the factor $\alpha$ ; the formal statement includes it (see Formalization scope).

Difficulty

The finite-dimensional change of measure (144) is an exact computation, but its density $(R_1\cdots R_n)^\theta$ degenerates as $n\to\infty$ . Passing to the limit (145) requires identifying the limit of the rescaled densities $n^{\theta/\alpha}(R_1\cdots R_n)^\theta$ with $L^{\theta/\alpha}Y_1^{-\theta}$ , and an almost sure limit of densities does not by itself give the identity of expectations. A second obstacle is that the Markov property of $(Y_n)$ under $P_{\alpha,\theta}$ does not follow from any independence under $P_{\alpha,\theta}$ itself; it is transported from $P^*_{\alpha,\theta}$ through a density that is a function of $Y_1$ only, and the transported kernels must be shown to be the same. Part (iii) needs the Laplace transform of $1/V_1$ conditioned on $X_1$ , which comes from the Poisson structure of $\mathrm{PD}(\alpha,0)$ .

Formalization scope

Sequences are ℕ → ℝ, 0-based: V ω k is $V_{k+1}$ , Yseq v k and YofR r k are $Y_{k+1}$ . " $(V_n)$ has $\mathrm{PD}(\alpha,\theta)$ law" (HasPD) means that measures of preimages of measurable sets agree with those of the ranked stick-breaking map under an independent beta product (IsStickLaw); ranking counts exceedances with Set.encard. $P^*_{\alpha,\theta}$ is any probability measure on ℕ → ℝ with independent coordinates of the stated beta laws (IsStarLaw); it is defined directly as a product, never through $P_{\alpha,\theta}$ . The local time $L$ is a random variable given with its defining almost sure limit (24). A Markov chain with forward kernels $\kappa_n$ (IsMarkovWith) is stated through the defining identity $E[g(Y_1..Y_n)h(Y_{n+1})] = E[g(Y_1..Y_n)\int h\,d\kappa_n(Y_n)]$ ; Theorem 38 (ii) asks for one family of Markov kernels serving both laws. The function $r$ of (140) is a hypothesis: any function giving the density of $Y_1$ under each $P^*_{\alpha,\theta+k\alpha}$ .

Committed deviations: the goal is the case $0<\alpha<1$ , the case the paper proves (the case $\alpha=0$ is quoted from [67], [34]); (139) carries the factor $\alpha$ that Bayes' rule from (128), (146) and the beta densities produces, and that Corollary 41's $\alpha^{n-1}$ confirms; (30) omits its middle expression $C^pE(\Sigma^{-\alpha p})$ . Every expectation of a nonnegative quantity is a lower Lebesgue integral, so no identity can hold through the junk value of a non-integrable Bochner integral; no law is written as Measure.map of a possibly non-measurable function; no limit is taken with limUnder; and the parameter range $0<\alpha<1$ , $\theta>-\alpha$ is a hypothesis of every statement that uses it.

Contributions welcome: the product-measure and beta-density computations behind (144) and (146), the limit passage (145), the Markov property of functions of independent sequences (Proposition 37), and the transfer of a Markov property through a density depending on the first coordinate.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2) (1997), 855–900. https://doi.org/10.1214/aop/1024404422
A. M. Vershik and A. A. Shmidt, Limit measures arising in the theory of groups, I, Theory Probab. Appl. 22 (1977), 79–85; II, Theory Probab. Appl. 23 (1978), 36–49 (references [66], [67] of the paper; no link verified).
Ts. Ignatov, On a constant arising in the theory of symmetric groups and on Poisson–Dirichlet measures, Theory Probab. Appl. 27 (1982), 136–147 (reference [34] of the paper; no link verified).
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92 (1992), 21–39. https://doi.org/10.1007/BF01205234

15 thms3 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 2: Kesten's Theorem for R = Q + MR — Unique Stationary Law, Power Tails with Explicit C±, and C₊ + C₋ > 0 iff Q ≢ (1 − M)cResearch Paper

Motivation

The random difference equation

R \overset{\mathcal L}{=} Q + MR,\qquad R \text{ independent of } (Q,M),

describes the stationary state of the affine recursion $R_n = Q_n + M_n R_{n-1}$ driven by independent copies of a random pair $(Q,M)$ . It appears wherever a quantity is multiplied by a random factor and then receives a random increment: the discounted value of a stream of random cash flows (a perpetuity), the stationary volatility of ARCH and GARCH models in financial econometrics (de Haan, Resnick, Rootzén and de Vries 1989), random walks in random environment, and the stationary laws of random coefficient autoregressions. In all of these, the question that matters for risk is the size of the tail $P(R>t)$ .

Timeline:

1973. Kesten proves, in a multivariate setting, that the stationary solution has power-law tails, $P(R>t)\sim C_+t^{-\kappa}$ , where $\kappa$ solves $\mathbf E|M|^\kappa=1$ ; the constants are not identified, and the proof of the key renewal step (his Theorem 4) runs to nine pages.
1979. Vervaat gives a full account of existence, uniqueness and moments of the solution in dimension one.
1980–1981. Grincevičius proves a maximal inequality of Lévy type for the partial sums of the recursion.
1986. Letac formulates a general principle for existence and uniqueness of solutions of random equations $R\overset{\mathcal L}{=}\Psi(R)$ .
1991. Goldie proves an implicit renewal theorem (Theorem 2.3, the subject of the first mission of this series) and deduces from it a new proof of Kesten's one-dimensional theorem, with explicit formulas for the constants $C_\pm$ and a necessary and sufficient condition for them not to vanish (Theorem 4.1).
2016. Buraczewski, Damek and Mikosch survey the theory, in which Kesten's theorem in Goldie's form is the central result.

Setting

Let $(Q,M)$ be a pair of real random variables with joint law $\mu$ on $\mathbb R^2$ . No independence between $Q$ and $M$ and no sign condition on either is assumed. A probability law $\rho$ on $\mathbb R$ is a law for $R$ satisfying (1.1) if the law of $Q+MR$ equals $\rho$ when $R$ has law $\rho$ and is independent of $(Q,M)$ .

A law on $\mathbb R$ is arithmetic if it is concentrated on a lattice $\{n\lambda:n\in\mathbb Z\}$ for some $\lambda>0$ , and nonarithmetic otherwise. For $\kappa>0$ , the conditions of Lemma 2.2 on $M$ are

\mathbf E|M|^\kappa = 1,\qquad \mathbf E|M|^\kappa\log^+|M|<\infty,

and that the conditional law of $\log|M|$ given $M\ne0$ is nonarithmetic. Under them

m := \mathbf E|M|^\kappa\log|M| \in (0,\infty).

With $x^+=x\vee0$ and $x^-=(-x)\vee0$ , the constants of Theorem 4.1 are, when $M\ge0$ a.s.,

C_\pm = \frac{\mathbf E\big(((Q+MR)^\pm)^\kappa-((MR)^\pm)^\kappa\big)}{\kappa m},

and otherwise $C_+=C_-=\frac{1}{2\kappa m}\mathbf E\big(|Q+MR|^\kappa-|MR|^\kappa\big)$ , where $R$ has the stationary law and is independent of $(Q,M)$ .

Formalization targets

Goal: Theorem 4.1

Assume the conditions of Lemma 2.2 and $\mathbf E|Q|^\kappa<\infty$ . Then there is a unique law $\rho$ for $R$ satisfying (1.1); the expectations defining $C_\pm$ are finite; and

\lim_{t\to\infty} t^\kappa P(R>t) = C_+,\qquad \lim_{t\to\infty} t^\kappa P(R<-t) = C_-,

with $C_\pm$ as above. Finally

C_++C_->0 \iff P\big(Q=(1-M)c\big)<1 \ \text{ for each fixed } c\in\mathbb R.

Milestones

In the order the proof uses them:

Corollary 2.4: the implicit renewal theorem with the moment conditions (2.16)–(2.17) and constants (2.18)–(2.20), for a general random function $\Psi$ in place of $t\mapsto Q+Mt$ .
Lemma 9.4: tail-difference integrals against $t^{\kappa-1}dt$ versus moment differences.
The elementary inequalities (9.26)–(9.27).
(4.8): for $\kappa>1$ , $\mathbf E|R|^{\kappa-1}<\infty$ with an explicit bound.
(2.16)–(2.17) for $\Psi(t)=Q+Mt$ : the moment differences are integrable.
Proposition 4.2 (Grincevičius's maximal inequality) and its consequence (4.6).
The lower bound $P(|\Pi_n|>e^t\text{ for some }n)\ge\delta e^{-\kappa t}$ for the products $\Pi_n=M_1\cdots M_n$ .
Under the condition $P(Q=(1-M)c)<1$ for each $c$ , $t^\kappa P(|R|>t)$ stays bounded away from $0$ .

Significance

The result. Theorem 4.1 identifies the tail exponent of the stationary solution as the root $\kappa$ of $\mathbf E|M|^\kappa=1$ , which depends on $M$ alone, and expresses the tail constants as expectations under the stationary law. The constants yield the bounds of Corollary 4.3 and closed forms when $\kappa$ is an integer (Corollaries 4.4, 4.5). The dichotomy between $M\ge0$ a.s. (different left and right constants) and $P(M<0)>0$ (equal constants) is visible only through these formulas. The positivity criterion tells when the power tail is really there: it fails exactly when the recursion has a deterministic fixed point $c$ . Tail estimates for GARCH processes, perpetuities in insurance mathematics and random walks in random environment are applications of this statement.

Formalizing it. The theorem has been proved since 1973 and in the present form since 1991; it is open only as a formalization. No machine-checked proof of Kesten's theorem, of the implicit renewal theorem, or of the underlying nonarithmetic key renewal theorem on the whole line is known to this mission. The work consists of formalizing Goldie's proof, which assembles the implicit renewal theorem with moment estimates, a maximal inequality and a Cramér–Lundberg-type lower bound for a random walk with negative drift.

Difficulty

The obvious argument is to write $R=\sum_{k\ge1}\Pi_{k-1}Q_k$ and estimate the tail of each term. It fails because $\mathbf E|M|^\kappa=1$ makes every term contribute tails of the same order $t^{-\kappa}$ , and the sum of infinitely many such contributions is exactly what has to be computed; termwise bounds give the right exponent at best, not the limit or the constant. A second natural idea, applying the renewal theorem directly to $P(R>t)$ , needs integrability of a tail difference that is not evident, because $\mathbf E|R|^\kappa$ is infinite whenever $C_++C_->0$ ; the moment differences $((Q+MR)^+)^\kappa-((MR)^+)^\kappa$ must be controlled without either term being integrable. The positivity half is a separate problem: the formula for $C_\pm$ is a difference of two infinite-looking quantities, and showing it is positive requires a lower bound on the tail that does not come from the formula.

Formalization scope

Everything is stated in terms of laws. The joint law of $(Q,M)$ is a probability measure $\mu$ on $\mathbb R\times\mathbb R$ (first coordinate $Q$ , second $M$ ); a law for $R$ satisfying (1.1) is a probability measure $\rho$ on $\mathbb R$ that equals the image of $\mu\otimes\rho$ under $((q,m),r)\mapsto q+mr$ , and uniqueness is among all probability measures on $\mathbb R$ , with no moment restriction. Expectations involving $R$ and $(Q,M)$ are integrals against $\mu\otimes\rho$ , which is what makes $R$ independent of $(Q,M)$ . The conditions of Lemma 2.2 are stated for the law of $M$ , with $\mathbf E|M|^\kappa$ and $\mathbf E|M|^\kappa\log^+|M|$ as lower Lebesgue integrals and the conditional law of $\log|M|$ taken given $M\neq0$ . " $P(R>t)\sim C_+t^{-\kappa}$ " is the limit statement $t^\kappa P(R>t)\to C_+$ , which the paper prescribes and which includes $C_+=0$ . Milestones on sequences use independent copies $(Q_n,M_n)$ on an arbitrary probability space carrying them, stored 0-based.

The statement does not reduce to a trivial one: the ratio form $P(R>t)/(C_+t^{-\kappa})\to1$ (undefined when $C_+=0$ ), existence of some fixed point without uniqueness, the positivity criterion as a one-way implication, and tail limits asserted for an arbitrary random variable rather than for the stationary law are all excluded. One correction to the source is built in: Lemma 9.4's (9.17) is printed as an equality, which fails for independent identically distributed non-degenerate $X$ , $Y$ ; the inequality the proof establishes is stated.

A complete development needs: convolution and image measures of products on $\mathbb R^2\times\mathbb R$ ; the key renewal theorem on the whole line for nonarithmetic laws with positive mean (the content of the first mission of this series); existence and uniqueness for contractive random affine maps; Lévy-type maximal inequalities; and ladder-height estimates for random walks with negative drift whose steps may equal $-\infty$ . The renewal-theoretic and random-walk components are reusable well beyond this mission. Contributions of any milestone, and of supporting lemmas such as the moment bounds for perpetuities, are welcome.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Annals of Applied Probability 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
L. de Haan, S. I. Resnick, H. Rootzén and C. G. de Vries, Extremal behaviour of solutions to a stochastic difference equation with applications to ARCH processes, Stochastic Processes and their Applications 32(2):213–224, 1989. https://doi.org/10.1016/0304-4149(89)90076-8
D. Buraczewski, E. Damek and T. Mikosch, Stochastic Models with Power-Law Tails: The Equation X = AX + B, Springer, 2016. https://doi.org/10.1007/978-3-319-29679-1

13 thms3 active usersReviewed

Bandit Algorithms Operations Research·Captain: mikedeng1

On the Gittins Index for Multiarmed Bandits 2: A Policy Falls Short of the Gittins Policy by at Most Its Expected Discounted Gap Between the Greatest Gittins Index and That of the Bandit It PlaysResearch Paper

Motivation

The multiarmed bandit problem asks how to allocate a single resource, one play at a time, among several alternative projects whose states evolve only when they are worked on. It models the scheduling of jobs on a single machine, the design of sequential clinical trials and many problems of research planning. Gittins and Jones showed that it is optimal to play, at each time, a project of greatest Gittins index, a number computed from that project alone (Gittins and Jones 1974; Gittins 1979).

In practice the Gittins index policy is often replaced by a heuristic: indices are computed approximately, or a policy is constrained by operational rules. A practitioner then needs to know how much value is lost. R. Weber's paper On the Gittins index for multiarmed bandits (Ann. Appl. Probab. 1992) gives a short proof of the index theorem through prevailing charges, and in its Section 5 derives from it two suboptimality bounds. This mission formalizes the second of them, Theorem 3, which bounds the loss of an arbitrary policy using Gittins indices only.

Timeline. Gittins and Jones (1974) and Gittins (1979) prove optimality of the index policy by an interchange argument; Whittle (1980) gives a proof by retirement options; Glazebrook (1982) bounds the suboptimality of policies in terms of Gittins indices, the bound Weber calls "usually weaker than (6)"; Glazebrook (1990) gives the prevailing-charge bound that is Weber's Theorem 2; Weber (1992) proves the index theorem by prevailing charges and states Theorems 2–4.

Setting

There are $k$ bandit processes. Bandit $i$ has a state $x_i(t)$ in a state space $S$ ; at each epoch $t = 0, 1, 2, \dots$ the gambler plays one bandit $j(t)$ , receives a reward with mean $r(x_{j(t)}(t))$ , the state of bandit $j(t)$ moves according to a Markov transition kernel $P$ , and the states of all other bandits are unchanged. Rewards are nonnegative and uniformly bounded, and $0 < \beta < 1$ is a discount factor. A policy $\pi$ chooses $j(t)$ , possibly at random, as a function of everything observed so far. Its value from the initial state vector $x$ is the expected total-discounted reward

V_\pi(x) = E_\pi\Big[\sum_{t=0}^\infty \beta^t r\big(x_{j(t)}(t)\big) \,\Big|\, x(0) = x\Big]. \tag{1}

The fair charge $\gamma(y)$ of a state $y$ is the largest ratio of expected discounted reward to expected discounted time that a stopping time $\tau \ge 1$ of a single bandit started at $y$ can achieve,

\gamma(y) = \sup_{\tau \ge 1} \frac{E\big[\sum_{t=0}^{\tau-1}\beta^t r(x(t)) \mid x(0)=y\big]}{E\big[\sum_{t=0}^{\tau-1}\beta^t \mid x(0)=y\big]},

and Weber's Gittins index is $G(y) = \gamma(y)/(1-\beta)$ . A Gittins index policy $\pi^*$ plays, at every epoch, a bandit with the greatest index, ties broken arbitrarily. Theorem 1 of the paper, already formalized on Prove2Me as BanditAlgorithm.gittins_index_theorem, states that every Gittins index policy maximizes $V_\pi(x)$ .

The model, the fair charge and the Gittins index policy are the published GittinsIndex definitions of Shuze Chen, and the history truncation used to write round expectations is from Harry_Xu's GittinsTerminalPotential.

Formalization targets

Goal: Theorem 3

For a Gittins index policy $\pi^*$ , every policy $\pi$ and every initial state vector $x$ ,

V_{\pi^*}(x) - V_\pi(x) \le E_\pi\left[\sum_{t=0}^\infty \beta^t\Big(\max_i G_i\big(x_i(t)\big) - G_{j(t)}\big(x_{j(t)}(t)\big)\Big) \,\middle|\, x(0)=x\right]. \tag{7}

The right-hand side is computed along the trajectory of $\pi$ alone: in each epoch it charges the gap between the greatest index and the index of the bandit $\pi$ actually plays.

Milestones

The proof compares, for each $t$ , two policies built from $\pi$ : $\pi^*(t)$ , identical to $\pi$ before time $t$ and a Gittins index policy from $t$ on, and $\pi(t)$ , identical to $\pi$ up to and including time $t$ , which then continues playing $j(t)$ until its fair charge drops below its value at time $t$ and is a Gittins index policy thereafter.

Switching to Gittins later never hurts. If $\sigma'$ is identical to $\sigma$ through time $t$ and a Gittins index policy from $t+1$ on, then $V_\sigma(x) \le V_{\sigma'}(x)$ ; in particular $V_{\pi(t)}(x) \le V_{\pi^*(t+1)}(x)$ .
Equation (8).

V_{\pi^*(t)}(x) - V_{\pi(t)}(x) \le \beta^t E_\pi\left[\frac{\max_i \gamma_i(x_i(t)) - \gamma_{j(t)}(x_{j(t)}(t))}{1-\beta} \,\middle|\, x(0)=x\right].

Significance

The result. Theorem 3 turns any per-epoch guarantee about the index of the bandit played into a guarantee on value. If a policy always plays a bandit whose Gittins index is within $\varepsilon$ of the greatest, it loses at most $\varepsilon/(1-\beta)$ ; this is the form in which index heuristics, approximate index computations and constrained index policies are analysed. The open Prove2Me goal AllocationIndices.eps_index_policy_near_optimal (Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices, Theorem 4.18, after Glazebrook 1982) is a bound of this kind for $\varepsilon$ -index policies and follows from (7); it is a separate item and is not part of this mission. Unlike Theorem 2 of the same paper, the bound (7) involves only Gittins indices, not prevailing charges or rewards.

Formalizing it. Theorem 3 is proved in the paper; no machine-checked proof exists. The mission produces a formal statement of the bound on top of the published Markov bandit model and Theorem 1, together with the two intermediate statements of Weber's proof, which have uses of their own: optimality of switching to the index policy after any finite prefix of play is the dynamic-programming form of the index theorem.

Difficulty

The informal proof is half a page, and its key sentence is that the difference of the charges paid by $\pi^*(t)$ and $\pi(t)$ at any later time is never more than the gap at time $t$ . Making it rigorous requires the value-to-go of a history-dependent randomized policy after a fixed time, the fact that both policies from time $t$ on are fair games in which expected discounted reward equals expected discounted charge, and a pathwise comparison of two interleavings of charge sequences. The naive reading, that $\pi(t)$ loses only the single epoch $t$ , is wrong: playing $j(t)$ at time $t$ commits the policy to a whole run of $j(t)$ , and the bound accounts for the entire run through the factor $1/(1-\beta)$ . Telescoping (8) over $t$ also needs $V_{\pi^*(t)}(x) \to V_\pi(x)$ as $t \to \infty$ , which rests on bounded rewards and $\beta < 1$ .

Formalization scope

The Lean development uses the published BanditAlgorithm model, in which all bandits share one state space $S$ (a standard Borel space), one kernel $P$ and one reward $r$ ; Weber's bandits with different state spaces are encoded by taking the disjoint union. Time is 0-indexed in both. The committed readings of the paper's phrases are:

" $\pi^*$ is the optimal (Gittins) policy" is any policy satisfying IsGittinsIndexPolicy; it is not assumed to be built from $\pi$ .
$R_j(x_j(t))$ is represented by its conditional mean $r(x_j(t))$ , and " $E_\pi[\sum_t \beta^t \cdots]$ " by the series of per-epoch expectations $\sum_t \beta^t E_\pi[\cdots]$ , the published value convention.
The index in (7) is $G = \gamma/(1-\beta)$ (weberIndex), and (8) is written with $\gamma$ (gittinsIndex) divided by $1-\beta$ , as on the page.
$\pi^*(t)$ and $\pi(t)$ are predicates on a policy (IsSwitchToGittinsAt, IsRunThenGittinsAt), and (8) is stated for every pair of policies satisfying them. "Identical to $\pi$ for times less than $t$ " is rounds $n < t$ ; "plays $j(t)$ at time $t$ " and "identical through time $t$ " are rounds $n \le t$ . "Drops below" is strict.
The standing assumptions of Section 1 (nonnegative, uniformly bounded rewards and $0<\beta<1$ ) are hypotheses of every theorem, as are measurability of $r$ and of $y \mapsto \gamma(y)$ , which the paper takes for granted.

Using the fair charge $\gamma$ in place of $G$ in (7) would make the bound false by the factor $1-\beta$ ; dropping the measurability of $\gamma$ would let the expectation degenerate to $0$ and make the bound claim that every policy is optimal. Neither is the statement posed here, and a constant-index or one-armed instance, where both sides vanish, only checks that the hypotheses are satisfiable.

Theorem 1 is referenced, not posed. Theorem 2 (the prevailing-charge bound) and Theorem 4 (submodularity of the optimal value in the set of bandits) are missions 1 and 3 of this series; this mission does not depend on them. Weber's definition of an index consistent policy (p. 1028) is not formalized here: the proof of (8) needs the fair-game property in the form of Remark 2 (continue while the fair charge exceeds the prevailing charge), which differs from the definition's "initial value" after an interruption. Contributions welcome: a measurable greatest-index selection, value-to-go decompositions for history-dependent policies, and the fair-game identity for index-consistent play are reusable beyond this mission.

Selected references

R. Weber, On the Gittins index for multiarmed bandits, The Annals of Applied Probability 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
K. D. Glazebrook, Procedures for the evaluation of strategies for resource allocation in a stochastic environment, Journal of Applied Probability 27, 215–220, 1990.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19, 716–722, 1982.
J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms3 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs: A Variable-Rate Queue Has an Average Cost Optimal Stationary Policy Whenever λ < max aβResearch Paper

Motivation

Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).

Timeline:

1962–1970. Derman and Ross obtain average cost optimal stationary policies from the vanishing discount approach when the relative values $h_\alpha$ are bounded.
1986. Sennott treats the queue with variable service rates under bounded costs and gives a first discrete-time Tauberian argument (Operations Research 34, 1986a; 1986b).
1989. This paper: Assumptions 1–3, the Theorem, the Markov chain test of Propositions 4–5, and applications to a packet system and to the queue with variable service rates (Proposition 8).

Setting

A Markov decision chain has states $i=0,1,2,\dots$ ; in state $i$ a finite nonempty set $A_i$ of actions; a cost $0\le C(i,a)<\infty$ ; and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may depend on the whole history and may randomize; a stationary policy $f$ chooses $f(i)\in A_i$ in state $i$ . For $0<\alpha<1$ , $V_{\theta,\alpha}(i)$ is the expected total $\alpha$ -discounted cost from $i$ and $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , possibly infinite. The average cost of $\theta$ is

g_\theta(i)=\limsup_{N\to\infty}\frac1N\,E_\theta\Big[\sum_{t=0}^{N-1}C(X_t,a_t)\,\Big|\,X_0=i\Big].

A stationary policy $f$ is average cost optimal if there is a finite constant $g$ with $g=g_f(i)\le g_\theta(i)$ for every policy $\theta$ and every state $i$ .

The queue with variable service rates (Example 2). Time is slotted; $p_i$ is the probability of $i$ arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables $a$ and serves at rate $a\beta\in(0,1)$ , so that the customer in service leaves during the slot with probability $a\beta$ ; there is no decision in state $0$ . From state $i\ge1$ the next state is $i-1+k$ with probability $a\beta p_k+(1-a\beta)p_{k-1}$ ( $p_{-1}=0$ ), and from $0$ it is $j$ with probability $p_j$ . The cost structure: $B(a)>0$ ; $Q$ a polynomial of degree $n\ge0$ , nonnegative and increasing on $i\ge0$ ; $C(0)=Q(0)$ and $C(i,a)=Q(i)+B(a)$ for $i\ge1$ . The arrival moments are $\lambda^{(k)}=\sum_i i^kp_i$ and $\lambda=\lambda^{(1)}$ .

Formalization targets

Goal: Proposition 8

If $\lambda^{(n+1)}<\infty$ , then

\lambda<\max_a(a\beta)\ \Longrightarrow\ \text{there is an average cost optimal stationary policy},

and

\lambda<\min_a(a\beta)\ \Longrightarrow\ g+h(i)=\min_a\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\quad i\ge0,

with $g$ the optimal average cost, $g=\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)$ , and $h$ bounded below.

Milestones

Propositions 1–3 (p. 627): $V_\alpha$ solves the discount optimality equation, is its minimal nonnegative solution, and is the limit of value iteration (already proved on the platform, referenced).
The Lemma (p. 628): discount optimal stationary policies along $\alpha_n\to1$ have a stationary limit point.
Lemmas A1 and A2 (p. 632): the comparison between solutions of the optimality inequality and average costs, and $\limsup_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)\le g_\theta(i)$ .
The Theorem (p. 628): under Assumptions 1–3, any limit point $f$ from the Lemma is average cost optimal, with the optimality inequalities (5); under Assumption 3*, the optimality equation (6).
Propositions 4, 5 and the Corollary (pp. 629–630): the Markov chain criteria that yield Assumptions 1, 3 and 3* from one well-behaved stationary policy.
Two steps of the proof of Proposition 8 (p. 631): $V_\alpha(i)$ is increasing in $i$ (hence Assumption 2), and the drift of $r(i)=Ai^{n+1}$ is a polynomial of degree at most $n$ with leading coefficient $A(n+1)(\lambda-a\beta)$ , display (14).

Significance

Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.

All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.

Difficulty

The obvious route takes a limit of $h_\alpha=V_\alpha-V_\alpha(0)$ along a sequence $\alpha_n\to1$ and passes to the limit in the discount optimality equation. With unbounded costs and unbounded $h_\alpha$ the sum $\sum_jP_{ij}(a)h_\alpha(j)$ is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of $V_\alpha$ and a Lyapunov drift computation whose leading term, $A(n+1)(\lambda-a\beta)i^n$ , has to dominate a cost polynomial of the same degree.

Formalization scope

The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:

costs, discounted values and average costs lie in $[0,\infty]$ ; $V_\alpha$ may be infinite unless Assumption 1 is assumed;
$h_\alpha$ is a real number, used only together with Assumption 1;
the constants $N$ and $M_i$ of Assumptions 2–3 are explicit and chosen before $i$ and $\alpha$ ; Assumption 3* uses the same $M$ ;
"average cost optimal" always carries a finite constant $g\ge0$ and compares with all policies, not only stationary ones;
sums $\sum_jP_{ij}(a)h(j)$ against a real function are extended reals (positive part minus negative part);
"ergodic" means positive recurrent (no aperiodicity);
in the queue, every decision is formally available in state $0$ with identical cost $Q(0)$ and identical transitions, which represents "no decision in state 0"; $\lambda<\max_a(a\beta)$ is "for some $a$ " and $\lambda<\min_a(a\beta)$ "for every $a$ ".

The second half of the goal is not "there exist $g$ and $h$ satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties $g$ to the optimal average cost and $\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha$ and requires $h$ bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals $p_0=3/4$ , $p_1=1/4$ , one rate $a\beta=1/2$ , $Q(i)=i+1$ , $B=1$ ), so the goal is not vacuous.

A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on $\prod_iA_i$ , first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

L. I. Sennott, Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs, Operations Research 37(4):626–633, 1989. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970.
A. G. Pakes, Some Conditions for Ergodicity and Recurrence of Markov Chains, Operations Research 17(6):1058–1061, 1969. https://doi.org/10.1287/opre.17.6.1058
A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey, SIAM J. Control Optim. 31(2):282–344, 1993. https://doi.org/10.1137/0331018

22 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Quality Control under Markovian Deterioration 3: Sufficient Conditions for a Three-Region Optimal Policy and for an Optimal Policy That Never InspectsResearch Paper

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$ . The discount factor is $\beta\in(0,1)$ . Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$ . Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$ . The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$ . Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$ . The three current-plus-continuation costs are

\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$ . A stationary rule is $\beta$ -optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$ . If

\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$ , inspects for $P_1\le P<P_2$ , and revises for $P\ge P_2$ . The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$ . If revision is optimal somewhere, the conclusion includes $P_2\le1$ . This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$ . Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$ . It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$ , exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$ . The last quotient in Corollary 3.6 divides by $\pi$ , so that second inequality is stated under $\pi>0$ ; the first inequality, and the main theorem, cover $\pi=0$ . If $\pi=1$ , then $\Delta=0$ . Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

8 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Quality Control under Markovian Deterioration 2: Never Inspecting or Revising Is Optimal Exactly When R ≥ C/(1 − β(1 − π))Research Paper

Motivation

A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.

The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.

Setting

There are two underlying states: good and bad. The current state is hidden, and $P\in[0,1]$ is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and $C$ in the bad state, so its expected immediate cost is $CP$ . A good process becomes bad with probability $\pi$ in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to $T(P)=P+\pi-\pi P$ . These are the conventions of the paper's Section 3 Ross 1971, p. 590.

The other actions are inspection, at cost $I$ , and revision, at cost $R$ . Inspection reveals the current state: the next belief is $1$ when the state was bad and $\pi$ when it was good. Revision returns the process to the good state before its next transition, so the next belief is $\pi$ . The standing parameter conditions are $0<\beta<1$ , $0\le\pi\le1$ , and $0<C<I<R$ ; $\beta$ is the discount factor. The paper explicitly assumes $C<I<R$ and a discount factor in $(0,1)$ . Positive $C$ states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.

For a future-cost function $W$ , the three Bellman alternatives at belief $P$ are $CP+\beta W(TP)$ , $I+\beta P W(1)+\beta(1-P)W(\pi)$ , and $R+\beta W(\pi)$ . Their minimum defines one step of finite-horizon value iteration, beginning with $V^0=0$ . The limit $V_\beta(P)$ is the optimal discounted cost. Write $R^0$ for the rule that always produces without inspection, and define its cost from the actual discounted series $\psi(P)=\sum_{n=0}^{\infty}\beta^n C T^nP$ Ross 1971, equations (3)–(5).

Formalization targets

The first target establishes that value iteration converges on $[0,1]$ , gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of $R^0$ :

T^nP=1-(1-P)(1-\pi)^n,\qquad \psi(P)=\frac{C}{1-\beta}-\frac{C(1-P)}{1-\beta(1-\pi)}.

The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for $P_1,P_2\in[0,1]$ ,

|V_\beta(P_1)-V_\beta(P_2)|\le \frac{C|P_1-P_2|}{1-\beta(1-\pi)}.

The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold

R\ge\frac{C}{1-\beta(1-\pi)}.

Below that threshold, revision is the unique minimizing action for beliefs sufficiently near $1$ from the left Ross 1971, pp. 591–592.

Significance

The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.

Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.

Difficulty

The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near $P=1$ requires control of the value as the belief varies; pointwise action comparison at $P=1$ does not itself establish an interval Ross 1971, pp. 591–592.

Formalization scope

The Lean model uses real parameters and a real belief restricted to $[0,1]$ . It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from $V^0=0$ , so $V^1=\min\{CP,I,R\}$ matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.

The discounted-optimality claim for $R^0$ means $\psi(P)=V_\beta(P)$ for every $P\in[0,1]$ . The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near $1$ ” means a one-sided neighborhood within $[0,1]$ . The second inequality in Corollary 3.6 is stated only when $\pi>0$ , because division by $\pi=0$ has a default value in Lean. The first inequality and Theorem 3.4 retain the $\pi=0$ case.

The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of $R^0$ are computed from the model data.

Selected references

Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587.

8 thms3 active usersReviewed

Convex Optimization Markov Chain Operations Research·Captain: mikedeng1

An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand: Adaptive(α, β) Has Per-Period Regret O(N(L)^(−1/3)) at α = β = 1/2Research Paper

Motivation

Periodic-review inventory systems with lost sales and a positive replenishment lead time are a basic model of retail and spare-parts operations: demand that cannot be met from stock is lost, and an order placed today arrives $\tau$ periods later. Even with a known demand distribution the optimal policy depends on the whole vector of outstanding orders and is intractable for long lead times, so practice and theory fall back on base-stock (order-up-to) policies, which are asymptotically optimal as the lost-sales penalty grows relative to the holding cost (Huh, Janakiraman, Muckstadt and Rusmevichientong, Management Science 2009).

Computing the best base-stock level still requires the demand distribution. In many settings the distribution is unknown and, worse, demand is censored: the manager records sales, $\min\{D_t, I_t\}$ , and never sees the demand lost to a stockout. The paper behind this mission, Huh, Janakiraman, Muckstadt and Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand (working paper of February 8, 2007; published in Mathematics of Operations Research 2009, DOI 10.1287/moor.1080.0367), gives an algorithm that learns the optimal base-stock level from sales data alone and bounds its regret against the best base-stock policy. It extended the zero-lead-time adaptive newsvendor analyses (e.g. Huh and Rusmevichientong, Math. Oper. Res. 2009) to positive lead times, where the inventory process is a Markov chain on $\mathbb R^\tau$ .

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative, continuous random variable $D$ with $E[D] > 0$ and distribution function $F$ . The inventory vector in period $t$ is

X_t = (Q_{t-1}, \dots, Q_{t-\tau+1}, I_t) \in \mathbb R^\tau_+,

the $\tau - 1$ outstanding orders and the on-hand inventory $I_t$ ; its inventory position is $X_t \cdot \mathbf 1^\tau$ . Under the order-up-to- $S$ policy the manager orders $Q_t = [S - X_t\cdot\mathbf 1^\tau]^+$ , demand $D_t$ is realized, and

I_{t+1} = [I_t - D_t]^+ + Q_{t-\tau+1}.

A period with on-hand inventory $y$ costs, in expectation, $C(y) = h\,E[y - D]^+ + b\,E[D - y]^+$ , with holding cost $h$ and lost-sales penalty $b$ . The long-run average cost of level $S$ is

C(I_\infty(S)) = \lim_{T\to\infty} \frac1T \sum_{t=1}^T E[C(I_t(S))],

and $S^*$ denotes a level minimizing it over $S \ge 0$ . Write $\gamma(S) = \mathcal P[D \le S/(\tau+1)]$ .

The algorithm $\textsc{Adaptive}(\alpha,\beta)$ runs in cycles $k = 1, 2, \dots$ of length $T_k = \lceil k^\beta\rceil$ ; $N(L) = \sum_{k\le L} T_k$ . Cycle $k$ uses a fixed level $S_k$ . From sales data it computes a sample-path derivative $I'$ by a recursion over the last $\tau$ periods, forms a gradient estimate $H_k \in \{h, -b, 0\}$ from the last period of the cycle, and sets $S_{k+1} = P_{[\underline M, \overline M]}(S_k - \epsilon_k H_k)$ with $\epsilon_k = (\overline M - \underline M)/(\max\{b,h\}k^\alpha)$ . The inventory is carried over between cycles. The regret after $L$ cycles is

\Lambda(L) = E\Big[\sum_{k=1}^L\sum_{j=1}^{T_k} C(I_{(k,j)})\Big] - C(I_\infty(S^*))\,N(L).

Formalization targets

Goal: Theorem 10, corrected

Under Assumption 1 ( $0 \le \underline M \le S^* \le \overline M$ and $\gamma(\underline M) > 0$ ) and infinite support of $D$ , for $\alpha,\beta \in (0,1)$ and $L \ge 1$ , with $N = N(L)$ and $\nu = \max\{1 - \gamma(\underline M)^{2\tau}, F(\overline M), 1/e\}$ ,

\frac{\Lambda(L)}{N} \le (b+h)\Big[(\overline M - \underline M)\Big(\frac{4}{N^{\frac{1-\alpha}{1+\beta}}} + \frac{4/(1-\alpha)}{N^{\frac{\alpha}{1+\beta}}} + \frac{C_3}{N^{\frac1{1+\beta}}}\Big) + \overline M\,\frac{24\tau/\ln(1/\nu)}{N^{\frac{\beta}{1+\beta}}}\Big],

with $C_3 = 12(4\tau)^{1/\beta}\Gamma(1/\beta)(1/\beta)/(\ln(1/\nu))^{1/\beta}$ . At $\alpha = \beta = 1/2$ this is $O(N^{-1/3})$ .

Milestones

Lemma 5 (tail of $D_1 + \dots + D_t$ ), Lemma 6 (the inventory position falls to $S$ ), Theorem 7 (existence, independence of the start, convexity and differentiability of $C(I_\infty(S))$ , and existence of $S^*$ with $\gamma(S^*) > 0$ ), Theorem 11 (projected stochastic gradient descent with biased gradients), Lemmas 12 and 13 (sums over cycles of length $\lceil k^\beta\rceil$ ), Lemma 14 (the regret $\Lambda_1$ from $S_k \ne S^*$ ) and Lemma 15 (the transient regret $\Lambda_2$ ).

Significance

The theorem gives a nonparametric, sales-only policy whose average cost approaches that of the best base-stock policy at an explicit polynomial rate, uniformly over demand distributions satisfying Assumption 1. Its ingredients are reusable: an explicit geometric ergodicity rate for the lost-sales base-stock chain, convexity of the long-run base-stock cost in $S$ , and a regret bound for projected gradient descent whose gradients are biased by Markov dependence.

The result is published; to our knowledge none of it has been machine-checked. The mission formalizes the regret bound, which requires Markov-chain ergodicity on a continuous state space, long-run averages, and stochastic approximation with biased gradients. It also repairs the printed constants: Theorem 10 and Lemma 15 are false as printed (see Formalization scope), and the formal statements make the dependence on $\overline M$ explicit.

Difficulty

The obvious route treats the cycle's last-period derivative as an unbiased gradient of $C(I_\infty(S_k))$ and applies standard online convex optimization. That fails: the estimate is computed from a Markov chain started at whatever state the previous cycle left, so it is biased, and the bias decays only as the chain mixes. Controlling the bias requires an explicit mixing rate for a chain on $\mathbb R^\tau_+ \times \{0,1\}^\tau$ whose state includes the derivative process, uniformly over the levels in $[\underline M, \overline M]$ and over starting positions above $S$ . The ergodicity argument uses a coalescing demand pattern, which exists only when $\gamma(S) > 0$ ; without that condition the chain need not be ergodic. A second obstacle is that the objective $C(I_\infty(S))$ is defined as a long-run average, so its convexity and differentiability in $S$ must be established before any gradient argument applies.

Formalization scope

Everything is stated in Lean 4 with Mathlib. The inventory vector is a pair (pipeline Fin (τ-1) → ℝ, newest order first; on-hand ℝ). Lean periods are $0$ -based (Lean period $t$ is the paper's $t+1$ ); cycles are numbered from $1$ . Demand is a sequence on a probability space that is i.i.d., nonnegative, integrable, with $E[D] > 0$ and an atomless law; infinite support is $F(x) < 1$ for all $x$ ; $\tau \ge 1$ , $h, b > 0$ . The long-run cost is a limsup of Cesàro averages from the empty start (Theorem 7 shows it is a limit from every start), and $S^*$ is any minimizer over $[0,\infty)$ . The algorithm is a deterministic function of the demand path; the sample derivative is the recursion the algorithm computes, not a derivative. Integrability of every expectation follows from boundedness of the inventory and is not assumed.

Corrections, all disclosed in the items: Theorem 10 carries $\overline M$ instead of $\overline M - \underline M$ on the $C_4$ term, because the printed bound fails for $\underline M = \overline M = S^*$ , $X_{(1,1)} = 0$ , $L = 1$ , where the right side is $0$ and $\Lambda(1) = C(0) - C(I_\infty(S^*)) > 0$ . Lemma 15 carries $\overline M$ and $12\tau + 1$ . Lemma 14 keeps its printed constant; its proof appears to use the ergodicity theorem one period early. Theorem 11 is stated on an interval with the bias taken conditionally on the history. Lemmas 5 and 6 are stated for infinite support only.

A goal that bounds the regret by $\Lambda_1$ alone (costs at the steady state of $S_k$ ), or that lets the levels be any sequence in $[\underline M, \overline M]$ , is not the theorem: the regret here uses the realized inventory of the algorithm. Lean's conventions $x/0 = 0$ and $\ln$ of a nonpositive number cannot trivialize the bound, because infinite support and $\gamma(\underline M) > 0$ give $\nu \in [1/e, 1)$ . The source is the authors' working paper of February 8, 2007, whose printed page numbers equal the PDF's.

Not yet stated: Theorem 3 and Lemma 4 (ergodicity rate), Theorem 8 and Lemma 9 (bias bounds), Theorem 1 (sample derivatives). They need the joint chain $(X_t, X'_t)$ and are welcome as contributions, as are the general pieces: geometric ergodicity via coalescence, and the biased projected-gradient bound.

Selected references

W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand, working paper, 2007; Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0367
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
W. T. Huh, P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0355
G. Janakiraman, R. O. Roundy, Lost-Sales Problems with Stochastic Lead Times: Convexity Results for Base-Stock Policies, Operations Research 2004. https://doi.org/10.1287/opre.1040.0130

12 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: mikedeng1

Contact Interactions on a Lattice II: If λₖ/μ < k/(2d − 1), the Expected Size of a Contact Process Is Integrable in TimeResearch Paper

Motivation

The contact process is the basic model of an infection spreading on a graph: infected sites recover at a constant rate, and healthy sites are infected at a rate that depends on how many of their neighbours are infected. T. E. Harris introduced it in Contact Interactions on a Lattice (Ann. Probab. 2, 1974, doi:10.1214/aop/1176996493), and it became one of the central examples of the theory of interacting particle systems (Liggett, Interacting Particle Systems, 1985, Ch. VI; Liggett, Stochastic Interacting Systems, 1999, Part I). Its questions are those of epidemiology and population dynamics on a spatial grid: does a finite infection die out, and how large does it get on the way?

Harris's paper gives the first rigorous subcritical bounds. Section 7 treats two quantities for a process started from a finite set: the probability $p_\infty(\xi)$ of surviving forever, and the expected size $m_t(\xi)$ at time $t$ . This mission formalizes the second, Theorem 7.6: under an explicit condition on the rates, the expected size is integrable in time. The companion mission (Contact Interactions on a Lattice I) formalizes Theorem 7.1, extinction under the same condition.

A short timeline. Harris (1974) defined the process, proved monotonicity, subadditivity and submodularity by coupling, and gave the bounds of §7 and a survival result for large rates (§9). Holley and Liggett (Ann. Probab. 3, 1975) developed duality for such systems. Holley and Liggett's paper also proves, for a discrete-time branching process with interference, the analogue $P_F(A_n\ne\varnothing)\le E_F|A_n|\le\lambda^n|F|$ of the size bounds studied here; it is a different process, related but not reused.

Setting

Fix $d \ge 1$ and the lattice $Z_d$ of integer points $x = (x^1, \dots, x^d)$ . Sites $x, y$ are neighbours, $x \sim y$ , if $\sum_i |x^i - y^i| = 1$ ; $N_x$ is the set of the $2d$ neighbours of $x$ . A configuration is a finite set $\xi \subset Z_d$ (the set $\Xi_0$ ); $|\xi|$ is its number of points, $\xi(N_x)$ is the number of neighbours of $x$ in $\xi$ , and $x \sim \xi$ means $x \notin \xi$ and $x$ has a neighbour in $\xi$ .

The parameters are a death rate $\mu \ge 0$ and birth rates $\lambda_0 = 0, \lambda_1, \dots, \lambda_{2d} \ge 0$ . The contact process is the continuous-time Markov chain on finite configurations that, from $\xi$ , removes a point $x \in \xi$ at rate $\mu$ and adds a site $x \sim \xi$ at rate $\lambda_{\xi(N_x)}$ . Its total jump rate is

q_\xi = \mu|\xi| + \sum_{x \sim \xi} \lambda_{\xi(N_x)} .

The empty configuration is absorbing. $P_t(\xi, \eta)$ is its transition function, $r(\xi,\eta) = q_{\xi\eta}/q_\xi$ the transition matrix of its jump chain, and

m_t(\xi) = \mathscr E_\xi\, |\xi_t| = \sum_{\eta} P_t(\xi, \eta)\, |\eta|

the expected size at time $t$ . In the Lean development these are trans μ lam t ξ η, jump μ lam ξ η and meanSize μ lam t ξ, where lam k is $\lambda_k$ .

Formalization targets

Goal: Theorem 7.6 (p. 982)

If $\mu > 0$ and

\frac{\lambda_k}{\mu} < \frac{k}{2d-1}, \qquad k = 1, \dots, 2d,

then for every finite $\xi$ ,

\int_0^\infty m_t(\xi)\, dt < \infty .

Milestones

In the paper's proof order:

Lemma 4.7: $m_t(\xi) \le |\xi|\, e^{(2d\Lambda - \mu)t}$ with $\Lambda = \max_i \lambda_i$ .
Lemma 5.8, its $m_t$ half: $\lambda_k \le \min_{j \ge k} \lambda'_j$ implies $m_t \le m'_t$ .
The change of time scale: multiplying all rates by $c$ replaces $m_t$ by $m_{ct}$ .
Remark 5.5, three times. $m_t$ is increasing in $\xi$ when $\lambda_k \uparrow$ ; it is subadditive when also $\lambda_k / k \downarrow$ ; and it is submodular when $\lambda$ is concave and non-decreasing.
The first-jump equation (7.7) for a pair of neighbours, with $K = 2 + (4d-2)\lambda$ .
The bound after (7.11): $M_2(T) - M_1(T) \le 1/(1 - (2d-1)\lambda)$ .
Lemma 7.5: if $\int_0^\infty m_t(\{x\})\,dt = \infty$ , then $\int_0^\infty (m_t(\xi) - m_t(\{x\}))\,dt = \infty$ for $|\xi| \ge 2$ .

After the goal come two consequences: Lemma 4.11, $m_{t+h}(\xi) \ge e^{-\mu h} m_t(\xi)$ , and Remark 7.12, $m_t(\xi) \to 0$ .

Significance

The theorem says that the total expected infection time, summed over all sites, is finite. That is stronger than extinction (Theorem 7.1), and it quantifies how fast the process dies out on average. With Lemma 4.11 it gives $m_t(\xi) \to 0$ . Bounds on the expected size are the standard route to subcritical estimates for spatial epidemics and branching systems with interference. The milestones are also the paper's general tools. Monotonicity, subadditivity and submodularity of $m_t$ , comparison of rate sequences, and time scaling hold for every contact process and are reusable beyond this mission.

The theorem has been known since 1974, and the formalization of the contact process is new work: the platform has no machine-checked development of an interacting particle system on $Z_d$ , nor of a continuous-time chain with unbounded rates. The mission produces a formal model of the contact process from a finite set, a Lean proof of the subcritical bound, and the coupling inequalities (stated here for $m_t$ ) that any further work on the process will need.

Difficulty

The obvious argument fails. One would bound the growth rate of $|\xi_t|$ by its worst case: a site is born at rate at most $\lambda_k$ for each of at most $2d|\xi|$ boundary sites. This gives only Lemma 4.7, an exponential bound whose exponent $2d\Lambda - \mu$ is positive in most of the regime of the theorem. The factor $2d - 1$ instead of $2d$ comes from correlations: a newly born site always has an occupied neighbour, so it adds at most $2d - 1$ new boundary sites. Capturing this needs the comparison between a single site and a pair of neighbours in (7.7)–(7.11), together with submodularity, which is a coupling statement about the whole process. Lemma 7.5 then has to turn a bound on the difference $M_2 - M_1$ into a bound on $M_1$ , and the paper omits its proof.

In the formal setting the chain has unbounded rates (since $q_\xi$ grows with $|\xi|$ ), so its transition function is not a matrix exponential. Uniformization does not apply either, and every statement goes through the minimal solution of the backward equations.

Formalization scope

The chain model. The process is the countable-state chain on finite configurations that the paper itself uses from §4 on. Theorems 4.1 and 4.3 show that the infinite-volume process started in $\Xi_0$ is this chain. No process on infinite configurations and no probability space is constructed, and $P_\xi$ , $\mathscr E_\xi$ enter only through $P_t$ .
The transition function. $P_t$ is the minimal transition function of the rates (4.4)–(4.5), $P_t = \sup_n P^{(n)}_t$ , where $P^{(n)}_t$ is defined by Feller's backward recursion over at most $n$ jumps.
Finite initial sets. Statements the paper makes for all $\xi \in \Xi$ (Lemmas 4.11 and 5.8, Remark 5.5) are drafted for finite $\xi$ .
Values. $P_t$ , $p_t$ and $m_t$ take values in $[0, \infty]$ . Integrals of $m_t$ are Lebesgue integrals of $[0,\infty]$ -valued functions.
Lattice. Sites are Fin d → ℤ with the $\ell^1$ adjacency of the paper.
Standing hypotheses. Every statement carries $d \ge 1$ , $\mu \ge 0$ , $\lambda_0 = 0$ and $\lambda_k \ge 0$ for $k \le 2d$ . Conditions on $\lambda$ range over $k \le 2d$ only, since $\lambda_k$ for $k > 2d$ never enters the model. The goal adds $\mu > 0$ , which the paper's ratio $\lambda_k/\mu$ presupposes.

Several trivializing formalizations are excluded:

$m_t$ is not a real tsum, which would be $0$ when the series diverges;
the integral is not a real Bochner integral, which would be $0$ for a non-integrable function;
the rate condition does not range over all $k \in \mathbb N$ ;
$\mu > 0$ is not left implicit: in Lean $\lambda_k / 0 = 0$ , and at $\mu = 0$ the conclusion is false;
the goal is not stated for singletons only.

A complete development needs the backward equation and non-explosion for $P_t$ (Theorem 4.3, formalized in the companion mission), Fubini–Tonelli for $\sum$ and $\int$ in $[0,\infty]$ , and couplings of contact processes. The couplings are the paper's auxiliary multi-type processes (§§5–6), or an equivalent argument on the generator. Contributions are welcome at every level. The coupling lemmas and the backward and forward equations for minimal chains are the parts most reusable beyond this mission.

Selected references

T. E. Harris, Contact interactions on a lattice, Ann. Probab. 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
R. Holley, T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
T. M. Liggett, Interacting Particle Systems, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Trans. Amer. Math. Soc. 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

13 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 3: With One Markdown or Markup Allowed, Thresholds x_n < z_n Give the Optimal PolicyResearch Paper

Motivation

Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.

Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).

Setting

There are three prices $p_1 < p < p_2$ . At price $p_i$ demand is a Poisson process of intensity $\lambda_i$ , and at $p$ of intensity $\lambda$ , with

\lambda_1 > \lambda > \lambda_2, \qquad r_1 > r > r_2, \qquad r_i = p_i\lambda_i,\ r = p\lambda,

all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section $p_1$ is the lower price; the initial price is $p$ .

A seller with $n$ units and time-to-go $t$ sells at $p$ and may switch once, to $p_1$ or to $p_2$ . Write $N(\cdot)$ for the demand process at $p$ and $N_i(\cdot)$ for that at $p_i$ .

$J^i(n,t;s) = (p - p_i)E\min(n,N(s)) + p_iE\min(n, N(s) + N_i(t-s))$ is the expected revenue of switching to $p_i$ after $s$ time units.
$J(n,t;0) = \max\{J^1(n,t;0), J^2(n,t;0)\}$ is the revenue of switching at once to the better alternative, and $J(n,t;t) = pE\min(n,N(t))$ the revenue of never switching.
The optimal revenue is

J(n,t) = \sup_{\tau \in \mathcal T} E\bigl[p\min(n,N(\tau)) + J(n - N(\tau), t - \tau; 0)\bigr],

where $\mathcal T$ is the set of stopping times of the history of $N$ with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.

$G^i(n,t) = r - r_i - p_i(\lambda - \lambda_i)P(N_i(t) \ge n)$ .
$\Delta^i(n,t) = J(n,t;t) - J^i(n,t;0)$ and $\Delta(n,t) = J^1(n,t;0) - J^2(n,t;0)$ , with first positive zeros $t^i_n$ and $t_n$ .

Formalization targets

Goal: Theorem 3 (pp. 1385–1386)

Under the paper's assumption $t^1_n < t_n < t^2_n$ for every $n$ , there are strictly increasing sequences $(x_n)$ , $(z_n)$ with

x_n < t^1_n < t_n < t^2_n < z_n

such that $J(n,t) = V(n,t)$ , where $V(n,t) = J(n,t;0) + F(n,t)$ for $x_n \le t \le z_n$ and $V(n,t) = J(n,t;0)$ otherwise. The excess $F(n,\cdot)$ equals $H^1(n,\cdot)$ on $[x_n,t_n]$ and $H^2(n,\cdot)$ on $[t_n,z_n]$ . Each $H^i$ solves

\frac{\partial H}{\partial t} = -\lambda H + L^i(n,t), \qquad L^i(n,t) = G^i(n,t) + \lambda\bigl[V(n-1,t) - J^i(n-1,t;0)\bigr],

with $H^1(n,x_n) = 0$ and $H^2(n,t_n) = H^1(n,t_n)$ . The thresholds are $x_n = \inf\{t \ge 0 : L^1(n,t) = 0\}$ and $z_n = \inf\{t \ge t_n : H^2(n,t) \le 0\}$ .

Milestones

(16), p. 1385: $\partial J^i(n,t;0)/\partial t = r - \lambda[J^i(n,t;0) - J^i(n-1,t;0)] - G^i(n,t)$ .
Lemma 2, p. 1379, in both cases: the zeros of $G(n,\cdot)$ increase strictly in $n$ , and $G(n,\cdot)$ changes sign exactly once.
Lemma 3, p. 1382, in both cases: $J(n,t;t) - J(n,t;0)$ changes sign exactly once at a strictly increasing sequence $t_n$ , and is monotone beyond it.
Lemma 1, p. 1378: a verification criterion identifying $J(n,t)$ as the solution of a system of differential equations and inequalities.

Significance

Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With $m$ units left and time-to-go $u$ , the seller marks down at once when $u$ falls below $x_m$ , marks up at once when $u$ exceeds $z_m$ , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of $2n$ numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.

Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.

Difficulty

The value $J(n,t)$ is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock $n+1$ are defined through $V(n,\cdot)$ , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that $L^1(n+1,\cdot)$ again has a single sign change, which requires $V(n,\cdot) - J^1(n,\cdot;0)$ to be increasing beyond $x_n$ . One must also know that $H^2(n+1,\cdot)$ is positive up to $t^2_{n+1}$ and eventually negative, so that $z_{n+1}$ is finite, and that $z_n < z_{n+1}$ . These facts concern three different price pairs at once: $(p,p_1)$ , $(p,p_2)$ and $(p_1,p_2)$ . A direct comparison of $V$ with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on $V$ matters.

Formalization scope

Model. Demand at $p$ is the counting process of i.i.d. exponential interarrival times from the published definition QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and $N_i(t-s)$ enters only through its law: the sum $N(s) + N_i(t-s)$ is written through its Poisson $(\lambda s + \lambda_i(t-s))$ law. $\mathcal T$ is the class of real-valued stopping times $\tau$ of the σ-algebras generated by the counts $N(u)$ , $0 \le u \le s$ , with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.
Conventions. Time is time-to-go, $t \ge 0$ ; ODEs are imposed at every $t > 0$ through HasDerivAt. Threshold sequences are indexed from $n = 1$ . Every infimum is a real sInf paired with the nonemptiness of its set. $F$ , $H^1$ , $H^2$ , $V$ and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption $t^1_n < t_n < t^2_n$ is a hypothesis of the goal, as on the page.
Added hypotheses. Prices and intensities are positive, the paper's standing convention. Lemma 1 as printed is false. It is stated with the boundary condition $V(n,0) = J(n,0;0)$ , the zero-stock condition $V(0,t) = 0$ , the obstacle condition $V \ge J(\cdot;0)$ , and local Lipschitz continuity of $V$ in place of "continuous and almost everywhere differentiable". The page's proof uses all four. Lemma 2's printed "bounded" is corrected to "bounded away from zero", since $y_n \to \infty$ .
No trivialization. No statement assumes the optimality identity, the verification conditions, the derivative identity (16), or any sign-change fact as a hypothesis. A goal that defined $V$ and assumed $J = V$ , or that left the thresholds unrelated to $L^1$ and $H^2$ , would not be Theorem 3.
Infrastructure needed. Poisson tail calculus (differentiation of $E\min(n, N(t))$ in $t$ ), variation-diminishing properties of the kernel $e^{-\lambda(t-u)}$ , linear first-order ODEs, and a martingale decomposition for Poisson counting processes evaluated at bounded stopping times. Contributions of any of these, or of proofs of the milestones, are welcome.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8):1371–1391, 1995. https://doi.org/10.1287/mnsc.41.8.1371
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
S. Karlin, Total Positivity, Vol. 1, Stanford University Press, 1968.
G. Bitran and R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003. https://doi.org/10.1287/msom.5.3.203.16031

10 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 2: Markup Is Optimal Once Time-to-Go Exceeds an Increasing Threshold z_nResearch Paper

Why a promotional fare needs a switching rule

An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.

The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.

Demand, inventory, and admissible decisions

There are $n\ge1$ items and $t\ge0$ units of time-to-go. At price $p_i$ , sales requests follow a Poisson counting process $N_i$ with rate $\lambda_i$ . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has

0<p_1<p_2,\qquad 0<\lambda_2<\lambda_1,\qquad p_2\lambda_2<p_1\lambda_1.

The salvage value at the end of the horizon is zero. A fixed switch at time $s\in[0,t]$ charges $p_1$ first and $p_2$ afterwards. Its expected revenue, denoted $J(n,t;s)$ , is

J(n,t;s)=(p_1-p_2)\sum_{j=1}^n\Pr\{N_1(s)\ge j\} +p_2\sum_{j=1}^n\Pr\{N_1(s)+N_2(t-s)\ge j\}.

The two counts in the last term are independent, so their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . This is the expression in §3 of the paper. In particular, $J(n,t;0)$ is the revenue from increasing the price immediately.

An admissible switching time $\tau$ uses only the history of sales at $p_1$ ; it lies between zero and $t$ and cannot wait past stock exhaustion. The optimal value $J(n,t)$ is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.

Formalization targets

The goal is Theorem 2 on pp. 1382–1383. Define the switching function

G(n,t)=p_1\lambda_1-p_2\lambda_2 -p_2(\lambda_1-\lambda_2)\Pr\{N_2(t)\ge n\}, \qquad y_n=\inf\{u\ge0:G(n,u)=0\}.

There are thresholds $x_n,z_n$ with $y_n\le x_n<z_n$ , and $(z_n)_{n\ge1}$ is increasing. A continuation premium $F$ gives the value

J(n,t)=\begin{cases} J(n,t;0)+F(n,t),&t<z_n,\\ J(n,t;0),&t\ge z_n. \end{cases}

For $n\ge1$ , $F(n,t)=H(n,t)$ below $z_n$ and is zero at or above it; $F(0,t)=0$ . The function $H$ satisfies $H(n,0)=0$ and the differential equation $\partial_tH(n,t)=-\lambda_1H(n,t)+L(n,t)$ , where $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ . The remaining thresholds are the first nonnegative zero of $L(n,\cdot)$ and the first positive zero of $H(n,\cdot)$ :

x_n=\inf\{u\ge0:L(n,u)=0\},\qquad z_n=\inf\{u>0:H(n,u)=0\}.

The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of $G$ , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.

What the result supplies

The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for $z_n$ : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for $F$ and $H$ , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.

Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.

Where the difficulty lies

The immediate-switch comparison $G(n,t)$ has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For $n>1$ , the relevant forcing term is $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , so the sign of $G$ alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.

Formalization scope

The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as $\min(n,N_1(\tau))$ , equal almost surely to $N_1(\tau)$ for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.

Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for $y_n$ , $x_n$ , and $z_n$ is nonempty; it also keeps $u>0$ in the definition of $z_n$ , since $H(n,0)=0$ . Continuity of $H(n,\cdot)$ at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; $y_n$ is unbounded as stock grows. These choices are recorded for review in the moderation notes.

The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

A Proof of the Optimality of the Shortest Remaining Processing Time Discipline: SRPT Minimizes the Number of Jobs in System at Every Time, for Every Arrival Stream and Every ScheduleResearch Paper

Motivation

A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).

Timeline:

1966. Schrage and Miller analyse the M/G/1 queue under SRPT and state, without proof, that SRPT minimizes the number in system at every time for every arrival sequence (Schrage–Miller, 1966).
1968. Schrage publishes a letter giving a proof by an interchange argument (Schrage, 1968). This mission formalizes that letter.
1978. D. R. Smith gives a new proof of the same statement (Smith, 1978) by a different argument.

Setting

An arrival stream is a sequence of pairs $(A(n), P(n))$ , $n = 0, 1, 2, \dots$ , of real numbers: $A(n)$ is the arrival time and $P(n)$ the processing time of job $n$ . A schedule is a family of measurable functions $\delta(n, \cdot) : \mathbb R \to \{0, 1\}$ , with $\delta(n, t) = 1$ meaning that the processor works on job $n$ at time $t$ . No job is processed before it arrives ( $\delta(n, t) = 0$ for $t < A(n)$ ), and the processor works on at most one job at a time.

The remaining processing time of job $n$ at time $t$ is

S(n, t) = P(n) - \int_{A(n)}^{t} \delta(n, x)\,dx,

and its completion time is

C(n) = \min\Big\{x \ge A(n) : \int_{A(n)}^{x} \delta(n, t)\,dt \ge P(n)\Big\},

or $+\infty$ if the job never receives its processing time. The set of jobs in system at time $t$ is $\theta(t) = \{n : A(n) \le t,\ S(n, t) > 0\}$ , and $N(t)$ is its cardinality.

A schedule follows SRPT if, at every time $t$ with $\theta(t) \ne \emptyset$ , the processor works on a job $k \in \theta(t)$ with $S(k, t) \le S(j, t)$ for all $j \in \theta(t)$ . Ties may be broken arbitrarily.

Formalization targets

Goal: SRPT minimizes the number in system at every time

For every locally finite arrival stream, every SRPT schedule $\delta_s$ and every schedule $\delta$ of the same stream,

N_s(t) \le N(t) \qquad \text{for all } t \in \mathbb R.

The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.

Milestones: the steps of the letter's interchange argument

All five come from the PROOF on p. 689. They compare an original schedule $\delta_o$ with a revised schedule $\delta_r$ .

Idle case (b1). If the processor is idle on $[t, t+v]$ while job $j$ waits, processing $j$ there gives $C_r(j) < C_o(j)$ and $C_r(i) = C_o(i)$ for $i \ne j$ .
Max identity. Reassigning the capacity that two jobs $j, k$ share after time $t$ , in any way, leaves $\max\{C(k), C(j)\}$ unchanged.
SRPT minimizes the minimum. Giving that capacity first to the job with the smaller remaining time minimizes $\min[C(k), C(j)]$ .
Relation (2). If $k$ is served on $[t, t+v]$ while $j$ with $S_o(j,t) < S_o(k,t)$ waits, the SRPT reassignment gives $\min[C_r(k), C_r(j)] < \min[C_o(k), C_o(j)]$ .
Counting. Relations (1)–(3) on completion times give $N_r(y) = N_o(y) - 1$ for $C_r(j) \le y < \min[C_o(k), C_o(j)]$ , and $N_r(y) = N_o(y)$ otherwise.

Significance

The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.

Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.

Difficulty

The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.

Formalization scope

All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from $0$ , and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in $\{0,1\}$ , each δ n measurable, $\delta(n,t) = 0$ before arrival, and at most one job served at a time. The letter's $\sum_n \delta(n,t) \le 1$ is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for $S(n,t)$ , which has no setup term. Completion times take values in WithTop ℝ, with $+\infty$ for a job that never completes. A job is in system on $[A(n), C(n))$ . $N(t)$ is Set.ncard, and the goal assumes local finiteness ( $\{n : A(n) \le t\}$ is finite for every $t$ ) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every $t$ .

Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 (" $S(k,t) > S(j,t)$ for $j \in \theta(t)$ implies $\delta(k,t)=0$ ") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.

The milestones add disclosed hypotheses that the letter uses silently:

finiteness of $C_o(j)$ in the idle case;
no service on a job after it completes in the max identity;
that one of the two jobs completes under $\delta_o$ in relation (2).

The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.

A complete development needs:

continuity and monotonicity of $x \mapsto \int_{A(n)}^x \delta(n,t)\,dt$ ;
the characterization $n \in \theta(t) \iff A(n) \le t < C(n)$ ;
interval integrals of schedules modified on sets.

All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.

Selected references

L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3):687–690, 1968. https://doi.org/10.1287/opre.16.3.687
L. E. Schrage and L. W. Miller, The queue M/G/1 with the shortest remaining processing time discipline, Operations Research 14(4):670–684, 1966. https://doi.org/10.1287/opre.14.4.670
D. R. Smith, A new proof of the optimality of the shortest remaining processing time discipline, Operations Research 26(1):197–199, 1978. https://doi.org/10.1287/opre.26.1.197
J. D. C. Little, A proof for the queuing formula L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
M. Harchol-Balter, B. Schroeder, N. Bansal and M. Agrawal, Size-based scheduling to improve web performance, ACM Transactions on Computer Systems 21(2):207–233, 2003. https://doi.org/10.1145/762483.762486

7 thms3 active usersReviewed

Markov Chain Operations Research Probability·Captain: mikedeng1

Stochastic Processes Occurring in the Theory of Queues and their Analysis by the Method of the Imbedded Markov Chain: In GI/M/s, a Positive Wait Is Exponential and a Positive Queue GeometricResearch Paper

Motivation

A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).

Timeline:

Erlang (1908–1929) treated M/M/s, where the queue length is itself Markovian.
Kendall (1951) treated M/G/1 by a chain imbedded at departure epochs.
W. L. Smith (Kendall's ref. [19]) observed that for a single server, under restrictions on the input law, exponential service gives an exponential waiting time apart from an atom at zero.
Kendall (1953), this paper, treated GI/M/s for every input law and every number of servers $s$ , and showed that Smith's restrictions are unnecessary.
Foster (1953) gave the criterion for ergodicity of a denumerable chain through a summable invariant vector, which is the step Kendall's argument relies on.

Setting

Customers arrive with independent inter-arrival times of law $A$ on $[0,\infty)$ and mean $a$ , $0<a<\infty$ . There are $s\ge 1$ servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean $b$ , $0<b<\infty$ . The relative traffic intensity is $\rho=b/(sa)$ .

The state of the imbedded chain at an arrival epoch is the number $i\in\{0,1,2,\dots\}$ of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix $P=[p_{ij}]$ of eq. (8) is given in three blocks, written with the death-process probabilities $[n\mid m]=\int_0^\infty\binom{m}{n}(1-e^{-u/b})^n e^{-(m-n)u/b}\,dA(u)$ of (9)–(10), the probabilities $\{n\mid s;m\}$ of (11)–(12), and the Poisson probabilities $(n\mid s)=\int_0^\infty e^{-su/b}(su/b)^n/n!\,dA(u)$ of (13)–(14):

p_{ij}=\begin{cases}(i+1-j\mid s) & j\ge s,\ j\le i+1,\\ [\,i+1-j\mid i+1\,] & i<s,\ j<s,\ j\le i+1,\\ \{s-j\mid s;\,i-s+1\} & i\ge s,\ j<s,\\ 0 & j>i+1.\end{cases}

The key function is

F(\lambda)=\int_0^\infty e^{-(1-\lambda)su/b}\,dA(u).

The queue size met by an arrival is $Q=\max(i-s,0)$ . The waiting time $w$ is, given $i$ , the sum of $k=\max(i-s+1,0)$ independent exponential variables of mean $b/s$ .

Formalization targets

Goal: Theorem IV (p. 350)

When $\rho<1$ the chain has a limiting distribution $\pi$ , and with $\lambda$ the root of $F(\lambda)=\lambda$ in $(0,1)$ and $c=b/(s(1-\lambda))$ ,

\Pr(Q=n\mid Q>0)=(1-\lambda)\lambda^{n-1}\ (n\ge1),\qquad \Pr(w>t\mid w>0)=e^{-t/c}\ (t\ge0),

with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: $\lambda$ and $c$ are determined by $A$ , $b$ and $s$ .

Milestones

The matrix is stochastic (p. 349), and the chain is irreducible and aperiodic (p. 347).
The coefficients $(n\mid s)$ are positive, sum to one and have mean $1/\rho$ ; $F(\lambda)=\sum_n (n\mid s)\lambda^n$ ; for $\rho<1$ the equation $F(\lambda)=\lambda$ has a unique root in $(0,1)$ (p. 348–349).
For the trial vector $x=[\mu_0,\dots,\mu_{s-2},1,\lambda,\lambda^2,\dots]$ (15): the invariance equations for $j\ge s$ are equivalent to $F(\lambda)=\lambda$ ; those for $1\le j\le s-1$ determine the $\mu$ 's; the one for $j=0$ follows from the row sums (pp. 348–349).
A nonnull absolutely summable invariant vector makes the chain ergodic, and normalized it is the limiting distribution (p. 348).
Theorem I: for $\rho<1$ the chain is irreducible and ergodic, and $\pi_j=C\lambda^{j-(s-1)}$ for $j\ge s-1$ .
Theorem II: $\Pr(Q=0)=\alpha=\dfrac{\sum\mu+1+\lambda}{\sum\mu+1/(1-\lambda)}$ and $\Pr(w=0)=\beta=\dfrac{\sum\mu+1}{\sum\mu+1/(1-\lambda)}$ .
Theorem III: $E(Q)=(1-\alpha)/(1-\lambda)$ and $E(w)/b=(1-\beta)/(s(1-\lambda))$ .
Eq. (27): for M/M/s the root is $\lambda=\rho$ .

Significance

Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number $\lambda$ . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing $\lambda$ from a one-dimensional equation and the finitely many $\mu$ 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.

The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of $Q$ and $w$ from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover $s\ge2$ .

Difficulty

The obvious route is to guess the geometric tail and check it against the balance equations. For $j\ge s$ this works, but the rows $i\ge s$ of the block $\mathbf B$ involve the convolution integral (11), and the equations for $j<s$ couple the geometric tail to the boundary terms $\mu_0,\dots,\mu_{s-2}$ . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give $p^n_{ij}\to\pi_j$ . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.

Formalization scope

The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and $w$ by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are $0$ -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all $i,j$ , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by $[0,\infty)$ , integrable, mean $a$ ), and $(n\mid s)$ is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.

Trivializing formalizations are ruled out: $\lambda$ is tied to $F(\lambda)=\lambda$ on $(0,1)$ rather than free; $\pi$ is the limiting distribution of $P$ , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the $\mu$ 's of Theorems II–III are characterized by the invariance equations, never defined from $\pi$ .

A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block $\mathbf B$ , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.

Selected references

D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950, ch. 15.
W. L. Smith, On the distribution of queueing times, Proc. Cambridge Philos. Soc. 49, 449–461, 1953 (cited by Kendall as "to be published", ref. [19]).
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.

22 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: mikedeng1

Contact Interactions on a Lattice I: A Contact Process with (2d − 1)λₖ < kμ Dies Out from Every Finite Initial SetResearch Paper

Motivation

The contact process is the basic model of an infection spreading on a lattice: each infected site recovers at a constant rate, and each healthy site becomes infected at a rate that depends on how many of its neighbours are infected. It was introduced by T. E. Harris in Contact Interactions on a Lattice (Ann. Probab. 2, 1974), and it became one of the central examples of interacting particle systems, alongside the voter model and the stochastic Ising model (Liggett, Interacting Particle Systems, 1985, Ch. VI). Its main question is whether a finite infection dies out with probability one or survives forever with positive probability, and how that answer depends on the rates.

Harris's paper gives the first answers. It shows that, under natural conditions on the rates, the probability of survival is monotone, subadditive and submodular as a function of the initial set, and it uses these properties to prove a condition for certain extinction: Theorem 7.1. For the linear contact process (recovery rate $1$ , infection rate $\lambda$ per infected neighbour) the condition is $(2d-1)\lambda<1$ . Holley obtained Theorem 7.1 by different methods at about the same time (footnote 4, p. 981); Holley and Liggett (Ann. Probab. 3, 1975) later developed the duality theory of such processes.

Setting

Let $Z_d$ be the $d$ -dimensional integer lattice, $d\ge1$ . Sites $x,y$ are neighbours, $x\sim y$ , if $\sum_i|x^i-y^i|=1$ ; $N_x$ is the set of the $2d$ neighbours of $x$ . A configuration is a finite set $\xi\subset Z_d$ of infected sites; $\Xi_0$ is the set of all of them, $\xi(N_x)=|\xi\cap N_x|$ , and $x\sim\xi$ means $x\notin\xi$ and $x$ has a neighbour in $\xi$ .

The parameters are a recovery rate $\mu\ge0$ and infection rates $\lambda_0=0,\lambda_1,\dots,\lambda_{2d}\ge0$ . The contact process $\{\xi_t\}$ started from a finite set is the continuous-time Markov chain on $\Xi_0$ that leaves $\xi$ at rate

q_\xi=\mu|\xi|+\sum_{x\sim\xi}\lambda_{\xi(N_x)}\qquad(4.4)

and jumps to $\xi\setminus x$ ( $x\in\xi$ ) at rate $\mu$ and to $\xi\cup x$ ( $x\sim\xi$ ) at rate $\lambda_{\xi(N_x)}$ (4.5). The empty set is absorbing. Write $P_t(\xi,\eta)$ for its transition function, $r(\xi,\eta)=q_{\xi\eta}/q_\xi$ for the transition matrix of its imbedded jump chain, and

p_t(\xi)=P_\xi\{\xi_t\neq\varnothing\},\qquad p_\infty(\xi)=\lim_{t\to\infty}p_t(\xi),\qquad m_t(\xi)=\mathscr E_\xi|\xi_t| .

The process is increasing, subadditive or submodular if, for all $\xi,\eta$ and $t\ge0$ , respectively $p_t(\xi)\le p_t(\xi\cup\eta)$ , $p_t(\xi\cup\eta)\le p_t(\xi)+p_t(\eta)$ , or $p_t(\xi\cup\eta)+p_t(\xi\cap\eta)\le p_t(\xi)+p_t(\eta)$ ((5.2)–(5.4)).

Formalization targets

Goal: Theorem 7.1 (p. 981)

If

(2d-1)\lambda_k<k\mu,\qquad k=1,\dots,2d,

then

p_\infty(\xi)=0\qquad\text{for every finite }\xi\subset Z_d .

Milestones, in the order of the paper

Theorem 4.3 (p. 975): from a finite set the process has finitely many jumps on every $[0,t]$ ; equivalently $\sum_\eta P_t(\xi,\eta)=1$ .
(5.1) (p. 976): $p_t(\xi)$ is non-increasing in $t$ , so $p_\infty(\xi)$ is a limit.
Theorem 5.6(a) (p. 977): if $\lambda_k\uparrow$ , the process is increasing.
Theorem 5.6(b) (p. 977): if moreover $\lambda_k/k\downarrow$ , it is subadditive.
Lemma 5.8 (p. 978): if $\lambda_k\le\min_{j\ge k}\lambda'_j$ , then $p_t\le p'_t$ and $m_t\le m'_t$ .
Theorem 6.2 (p. 979): if $\{\lambda_i\}$ is concave and non-decreasing with $\lambda_0=0$ , the process is submodular.
Change of time scale (p. 981): multiplying all rates by $c>0$ replaces $P_t$ by $P_{ct}$ and leaves $p_\infty$ unchanged.
First-step display (p. 981): for a subadditive process, a singleton $\{x\}$ , and $n\ge1$ , $p_\infty(\{x\})=\sum_\eta r^{(n)}(\{x\},\eta)p_\infty(\eta)\le p_\infty(\{x\})\,\mathscr E_x|\xi_{(n)}|$ .
(7.2) (p. 981): for $\mu=1$ , $\lambda_k=k\lambda$ : $\pi_1=\frac{2d\lambda}{1+2d\lambda}\pi_2$ , where $\pi_1,\pi_2$ are $p_\infty$ of a site and of a pair of neighbours.
(7.3)–(7.4) (p. 981): $\pi_2-\pi_1=(1+(2d-1)\lambda)\sum'r(\xi,\xi\cup x)(p_\infty(\xi\cup x)-\pi_2)\le(\pi_2-\pi_1)(2d-1)\lambda$ .
Conclusion of the proof (p. 981): for $\mu=1$ , $\lambda_k=k\lambda$ , $\pi_1>0$ implies $(2d-1)\lambda\ge1$ .

Significance

Theorem 7.1 gives a computable sufficient condition for extinction that holds in every dimension and for every non-linear infection law satisfying it. For the linear process it gives the lower bound $\lambda_c\ge1/(2d-1)$ on the critical infection rate; the paper's §9 shows conversely that the process survives for large $\lambda_k/\mu$ , so the critical rate is non-trivial. The monotonicity, subadditivity and submodularity theorems of §§5–6 are the comparison tools on which much of the later theory of attractive spin systems was built, and Lemma 5.8 is the prototype of comparison between processes with ordered rates.

The results are proved in the paper, and the proof of Theorem 7.1 is half a page once §§5–6 are available. No machine-checked version of the contact process, of its comparison theorems, or of Theorem 7.1 is known to exist. A formalization produces a continuous-time Markov chain with unbounded rates and an absorbing state on a countable state space, its minimal transition function, a non-explosion criterion, first-step analysis for absorption probabilities, and coupling arguments for monotone comparison. The companion mission Contact Interactions on a Lattice II treats Theorem 7.6, the integrability of the expected size, on the same model.

Difficulty

The obvious argument is first-step analysis on singletons and pairs, (7.2) and (7.3). It fails as it stands because (7.3) involves $p_\infty$ of every three-point set $\xi\cup x$ , and no finite system of first-step equations closes; some inequality between survival probabilities of nested sets is needed, and the milestones record the one the paper uses. Submodularity, subadditivity and monotonicity are not consequences of the rates by direct computation: the paper proves each by building several contact processes on one probability space (Tables 1–4), which in a formal development means constructing couplings of chains with unbounded rates and checking that each marginal has the right law. The reduction from general $\lambda_k$ to the linear case also needs the comparison Lemma 5.8, another coupling. Finally the rates grow linearly in $|\xi|$ , so uniformization does not apply and non-explosion (Theorem 4.3) must be proved before transition probabilities are known to sum to one.

Formalization scope

The process is the countable-state chain of §4, not the Feller process on all subsets of $Z_d$ of §2: sites are Fin d → ℤ, configurations are Finsets, and $P_t$ is the minimal transition function of the rates (4.4)–(4.5), defined as the increasing limit of Feller's backward recursion. There is no measure-theoretic process object; $P_\xi$ and $\mathscr E_\xi$ enter only through $P_t$ . Consequently Theorem 4.1 ( $\Xi_0$ is stochastically closed) is built in, and every statement is made for finite initial sets, including those the page makes for arbitrary $\xi\in\Xi$ ((5.2)–(5.4), Lemma 5.8); for infinite $\xi$ the page itself notes $p_t(\xi)=1$ .

The committed conventions:

$P_t$ , $p_t$ , $p_\infty$ and $m_t$ take values in $[0,\infty]$ ; $p_t(\xi)=1-P_t(\xi,\varnothing)$ and $p_\infty(\xi)=\inf_{t\ge0}p_t(\xi)$ , so $p_\infty=0$ means absorption at $\varnothing$ and cannot be produced by loss of mass to explosion.
The rates are real; every theorem assumes $d\ge1$ , $\mu\ge0$ , $\lambda_0=0$ and $\lambda_k\ge0$ for $k\le2d$ . Conditions on $\{\lambda_k\}$ range over $k=1,\dots,2d$ (or $0,\dots,2d$ ), never over all natural numbers.
$2d-1$ is the real number $2d-1$ .
In the linear case the scalar rate is written $l$ ( $\lambda$ is reserved in Lean), $\mu=1$ and $\lambda_k=kl$ .

Trivializing formalizations are ruled out: the survival probability is not taken from an arbitrary semigroup or a uniformization (the rates are unbounded); $p_\infty$ is not a real infimum or limUnder, whose junk value $0$ would make the goal free; $\lambda$ is indexed by the number of infected, not vacant, neighbours, and $\lambda_0=0$ forbids spontaneous infection; and (7.2) is stated for every site and every neighbour, not for one fixed pair.

A complete development needs: non-explosion for chains with linearly growing rates; the Chapman–Kolmogorov and strong Markov properties of the minimal chain at jump times; lattice symmetries (translations and coordinate reflections) acting on the chain; and couplings of several contact processes realised as one chain on a product type space. The chain infrastructure and the coupling lemmas are reusable beyond this mission, in particular by its companion. Contributions to any milestone are welcome, including proofs of the milestones under the paper's hypotheses by methods other than Harris's.

Selected references

T. E. Harris, Contact interactions on a lattice, The Annals of Probability 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
R. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, The Annals of Probability 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Transactions of the AMS 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

13 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Heavy-Traffic Limits for Queues with Many Exponential Servers: The Scaled Stationary M/M/n Queue Length Converges to a Hybrid Exponential–Normal LawResearch Paper

Why many-server queues in heavy traffic

Telephone exchanges, call centers, hospital wards and cloud server pools are queues with a large number $s$ of parallel servers. For such systems two classical approximations pull in opposite directions. Holding $s$ fixed and letting the traffic intensity $\rho \to 1$ gives the conventional heavy-traffic limit, in which almost every customer waits. Letting $s$ grow with $\rho$ fixed below one gives a limit in which almost nobody waits. Real systems sit in between: a positive fraction of customers wait, and waits are short. Halfin and Whitt (Operations Research 29 (1981) 567–588) identified the scaling that produces this middle regime and the limit laws it yields. The scaling is now called the Halfin–Whitt or quality-and-efficiency-driven (QED) regime, and it underlies square-root staffing: run $n \approx R + \beta\sqrt R$ servers for an offered load of $R$ Erlangs. Borst, Mandelbaum and Reiman (Operations Research 52 (2004) 17–34) built staffing rules for large call centers on it.

Timeline. Erlang (1917) gave the delay probability of the M/M/s queue. Iglehart (1965) proved diffusion limits for M/M/s queues with the number of servers growing and the traffic intensity fixed. Halfin and Whitt (1981) proved that the delay probability has a limit strictly between 0 and 1 exactly when $(1-\rho_n)\sqrt n$ converges to a positive constant (their Proposition 1), derived the limit of the stationary queue length (Theorem 1), and extended the process-level limit to GI/M/s queues. Later work extended the regime to many-server queues with general service times and abandonment.

Setting

An M/M/s queue has Poisson arrivals at rate $\lambda > 0$ , $s \ge 1$ servers, and exponential service times with rate $\mu > 0$ . Its traffic intensity is $\rho = \lambda/(s\mu)$ . The number $Q(t)$ of customers in the system (waiting or in service) is a birth–death process on $\{0,1,2,\dots\}$ with birth rate $\lambda$ and death rate $\min(k,s)\mu$ in state $k$ . When $\rho < 1$ , $Q(t)$ converges in distribution to $Q(\infty)$ , whose law $p_k = P(Q(\infty) = k)$ is the unique probability distribution solving the balance equations of this chain. The probability of delay $\alpha = P(Q(\infty) \ge s)$ is the Erlang-C formula.

The mission studies a sequence of such queues: queue $n \ge 1$ has $s_n = n$ servers, the fixed service rate $\mu$ , and arrival rate $\lambda_n$ with $\rho_n = \lambda_n/(n\mu) < 1$ and $\lambda_n \to \infty$ . Its stationary queue length is $Q_n(\infty)$ , and the scaled queue length is

X_n = \frac{Q_n(\infty) - n}{\sqrt n}.

Throughout, $\Phi$ and $\varphi$ denote the standard normal distribution function and density, and for $\beta > 0$

\alpha(\beta) = \big[1 + \sqrt{2\pi}\,\beta\,\Phi(\beta)\,e^{\beta^2/2}\big]^{-1} = \frac{\varphi(\beta)}{\varphi(\beta) + \beta\Phi(\beta)} \in (0,1).

The standing assumption of the paper's Section 2 is the heavy-traffic condition

\lim_{n\to\infty} (1-\rho_n)\sqrt n = \beta, \qquad \beta > 0. \tag{2.2}

Formalization targets

Goal: Theorem 1

Under (2.2), with $\alpha = \alpha(\beta)$ ,

X_n \Rightarrow X, \qquad P(X \ge 0) = \alpha,\quad P(X > x \mid X \ge 0) = e^{-x\beta}\ (x \ge 0),\quad P(X \le x \mid X \le 0) = \frac{\Phi(\beta + x)}{\Phi(\beta)}\ (x \le 0).

The limit is exponential with rate $\beta$ above zero and a normal law truncated at zero below it, with masses $\alpha$ and $1-\alpha$ .

Milestones, in the order the paper proves them

The stationary law (1.1)–(1.3) of one M/M/s queue, and the identification (1.2) of $P(Q(\infty) \ge s)$ with the Erlang-C formula.
Lemma 1: recursions expressing the partial moments $\sum_{k<s} k^m p_k$ and $\sum_{k \ge s} k^m p_k$ through lower ones and $\alpha$ .
Proposition 1: $P(Q_n(\infty) \ge n) \to \alpha \in (0,1)$ if and only if (2.2) holds, and then $\alpha = \alpha(\beta)$ .
Proposition 2: for $\delta > 0$ and $(n - \delta_n)/\sqrt n \to \delta$ with $\delta_n \le n$ ,

P(Q_n(\infty) \le \delta_n \mid Q_n(\infty) \le n) \to \frac{\Phi(\beta-\delta)}{\Phi(\beta)},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \le n) \to \frac{\varphi(\beta-\delta)}{\Phi(\beta)},

and for $(\delta_n - n)/\sqrt n \to \delta$ with $\delta_n \ge n$ ,

P(Q_n(\infty) \ge \delta_n \mid Q_n(\infty) \ge n) \to e^{-\delta\beta},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \ge n) \to \beta e^{-\delta\beta}.

Corollary 1: the first four moments and the variance of $X_n$ converge to explicit functions of $\alpha$ and $\beta$ , for example $E X_n \to -\beta + \alpha/\beta$ .

Significance

Theorem 1 is the stationary half of the Halfin–Whitt regime. It turns the Erlang-C formula, a ratio of sums with $n$ terms that is opaque for large $n$ , into a two-parameter description of congestion: $\alpha$ is the fraction of customers who wait, $\beta$ is the scaled safety margin of servers, and the conditional laws above give the distribution of the number waiting and of the number of idle servers. Proposition 1 and Theorem 1 are what square-root staffing rules evaluate; Corollary 1 supplies the mean and variance used in the paper's numerical approximations.

All results of this mission are proved in the paper, by direct calculation from (1.1)–(1.3), Stirling's formula and the central limit theorem for Poisson variables. None has a machine-checked proof. Proposition 1 and the two Section 1 facts are posed on the platform as open theorems from the Gross et al. queueing textbook series; this mission adds the conditional and local limits, the weak-convergence theorem and the moment results on the same definitions, so that a closed development would give a fully checked derivation of the Halfin–Whitt limit from the balance equations.

Difficulty

The stationary law is explicit, so nothing here needs a stochastic process. The difficulty is analytic and uniform: each statement is a limit of ratios of sums of $n$ or infinitely many terms, $(n\rho_n)^k/k!$ below $n$ and a geometric tail above $n$ , in which $\rho_n \to 1$ and $n \to \infty$ at linked rates. The lower half needs a central limit theorem for Poisson laws whose parameter $n\rho_n$ moves with $n$ and is evaluated at a moving point; the local limits (2.10) and (2.12) need Stirling's formula with explicit control of $\log \rho_n$ to second order. Weak convergence then needs tightness, or a direct argument from the conditional limits, and the moment limits need uniform integrability, which the fixed- $s$ moment recursions do not give by themselves. Holding $\rho$ fixed, or taking limits in $n$ and $\rho$ one after the other, gives degenerate answers ( $\alpha = 0$ or $\alpha = 1$ ); the two limits must be taken together.

Formalization scope

The Lean development lives in the namespace HalfinWhitt81.Stationary. The law of $Q_n(\infty)$ is a sequence p n : ℕ → ℝ satisfying IsSteadyState (fun _ => lam n) (mmcDeath μ n) (p n) of the referenced definition QueueingFundamentals.BirthDeath.Balance (nonnegative, summing to one, solving the balance equations of the M/M/n chain); the Erlang-C formula and $\alpha(\beta)$ are erlangC and halfinWhittAlpha of QueueingFundamentals.BirthDeath.Erlang, and $\Phi$ , $\varphi$ are Mathlib's cdf (gaussianReal 0 1) and gaussianPDFReal 0 1. These, and the three open theorems for (1.1)–(1.3), (1.2) and Proposition 1, come from the Gross et al. (2008) series and are referenced, not restated. The related Borst–Mandelbaum–Reiman items (DimCallCenters.*.lemma_4_1, for the continuous extension of Erlang-C) state a different result and are not used.

Conventions committed to:

hypotheses on queue $n$ (rates, steady state, $\delta_n \le n$ or $\delta_n \ge n$ ) are imposed for $n \ge 1$ , and only limits are asserted; $\lambda_n \to \infty$ is kept as a hypothesis although it follows from (2.2);
the standing assumption "(2.1) or, equivalently, (2.2)" is the hypothesis (2.2) with $\beta > 0$ , and $\alpha$ is written as $\alpha(\beta)$ , equal to the limit in (2.1) by Proposition 1;
probabilities of $Q_n(\infty)$ are sums of p n (probLE, probGE, probEqInt); a conditional probability $P(A \mid B)$ with $A \subseteq B$ is the ratio $P(A)/P(B)$ ; $[x]$ is Int.floor, with $P(Q = m) = 0$ for $m < 0$ ;
$X_n$ uses $n^{-1/2}$ : the page's (2.13) prints $n^{1/2}$ , a misprint; (2.12) prints the limit $\beta e^{-\beta}$ , a misprint for $\beta e^{-\delta\beta}$ , which is what is formalized;
" $X_n \Rightarrow X$ " is stated as: there is a Borel probability measure $\nu$ on $\mathbb R$ with the three properties of Theorem 1 such that $\sum_k p_n(k)\,g((k-n)/\sqrt n) \to \int g\,d\nu$ for every bounded continuous $g$ ; the exponential clause is for $x \ge 0$ and the normal clause for $x \le 0$ ;
infinite sums whose convergence is not implied by the hypotheses (the moment series of Lemma 1 and Corollary 1) have their convergence in the conclusion.

The goal cannot be met trivially: the law of $Q_n(\infty)$ is the M/M/n steady state, not a free sequence; the limit measure is asserted to exist together with its three properties and the convergence, so no vacuous "for every $\nu$ " reading is possible; and the statement $P(X_n \ge 0) \to \alpha$ alone is Proposition 1, already posed.

A complete development needs: the closed form of the M/M/n steady state, Poisson central limit and local limit theorems with a moving parameter, Stirling's formula with error terms, a criterion for weak convergence from convergence of distribution functions, and uniform integrability for the moments. The Poisson limit theorems and the weak-convergence criterion are reusable beyond this mission. Proofs of the referenced open theorems, of individual milestones, and alternative routes to Theorem 1 (moment convergence, or the process-level limit) are all welcome.

Selected references

S. Halfin and W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3) (1981) 567–588. https://doi.org/10.1287/opre.29.3.567
R. B. Cooper, Introduction to Queueing Theory, Macmillan, 1972 (the source cited for (1.1)–(1.3)).
D. L. Iglehart, Limiting Diffusion Approximations for the Many Server Queue and the Repairman Problem, Journal of Applied Probability 2(2) (1965) 429–441.
S. Borst, A. Mandelbaum and M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1) (2004) 17–34. https://doi.org/10.1287/opre.1030.0081
D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008 (§2.4: the Erlang-C formula and the Halfin–Whitt limit).

13 thms3 active usersReviewed

Completed

Dynamical Systems Operations Research Probability·Captain: mikedeng1

Subadditive Ergodic Theory 1: Kingman's Theorem — x₀ₜ/t Converges with Probability One and in Mean to a Finite ξ with E(ξ) = γResearch Paper

Motivation

Many stochastic systems have an accumulated cost or passage time that grows with the length of an observation window. Splitting a window at an intermediate time gives an upper bound on the total, even when it does not give an equality. First-passage percolation and products of random matrices are examples discussed by Kingman (1973). A central question is whether the cost per unit time settles to a long-run rate on almost every sample path.

Hammersley and Welsh introduced subadditive stochastic processes in 1965. Kingman's 1968 theorem established the almost-sure limit for the stationary process considered here. His 1973 paper restated the result, identified the limit's expectation, and set out the process model and related formulations used in later applications. The 1973 article explicitly attributes the proof of Theorem 1, its maximal inequality, and its decomposition to the 1968 work; this mission formalizes the statements as presented in the 1973 paper.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ . For integers $0\le s<t$ , let $x_{st}:\Omega\to\mathbb R$ be a measurable random variable. Think of $x_{st}$ as the accumulated quantity over the interval from $s$ to $t$ . Condition S₁ is subadditivity: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ . The stronger equality defines an additive process.

Condition S₂ says that shifting every interval one time unit forward leaves the joint distribution of the whole family unchanged. It concerns the law of $(x_{s+1,t+1})_{s<t}$ as a single countable path. The one-dimensional statement that each $x_{st}$ has a distribution depending only on $t-s$ is called S₂′ in the paper; it does not replace S₂. Condition S₃ says that every positive-time variable $x_{0t}$ is integrable and that, for some real $A$ , its mean $g_t=E_P(x_{0t})$ satisfies $g_t\ge-At$ for all $t\ge1$ . A subadditive process satisfies S₁, S₂, and S₃.

The associated mean growth rate is $\gamma(x)=\inf_{t\ge1}g_t/t$ . The time index starts at one in this infimum because division by zero would introduce an unrelated value. S₃ gives a finite lower bound; the subadditive mean relation makes this infimum the limit of $g_t/t$ . Kingman also considers the invariant σ-field $\mathcal I$ : events determined by the entire path and unchanged by the shift $(x_{st})\mapsto(x_{s+1,t+1})$ . It records the part of the process that can remain random in the limiting rate. Source: §§1.1–1.2, pp. 883–885.

Formalization targets

Theorem 1: finite long-run rate

For every subadditive process there is an integrable real random variable $\xi$ such that

\frac{x_{0t}(\omega)}{t}\longrightarrow\xi(\omega) \quad\text{for }P\text{-almost every }\omega, \qquad \int_\Omega\left|\frac{x_{0t}}{t}-\xi\right|\,dP\longrightarrow0, \qquad E_P(\xi)=\gamma(x).

These are three distinct claims: almost-sure convergence, convergence in mean, and an identity for the limit's expectation. The limit need not be a constant. The milestone list also covers the convergence of the means, the maximal inequality (1.2.5), the decomposition (1.2.6), the measure-preserving formulation (1.3.4)–(1.3.5), and the representation through $\mathcal I$ in (1.2.4). Each statement comes from the 1973 paper, §§1.1–1.3.

Measure-preserving formulation

For a measure-preserving map $\theta:\Omega\to\Omega$ , condition Sᴱ concerns integrable functions $f_n$ with $f_{m+n}(\omega)\le f_m(\omega)+f_n(\theta^m\omega)$ for $m,n\ge1$ and a linear lower bound on their expectations. It yields an integrable $\xi$ with $f_n/n\to\xi$ almost surely and in mean. Neither invertibility nor ergodicity of $\theta$ is assumed. Source: §1.3, p. 886.

Significance

The theorem assigns a finite sample-path growth rate to an entire class of stationary subadditive systems. It also ties the average of that rate to the infimum of the normalized expected values. The equality is useful when a system's finite-window means are easier to estimate than its individual long-run paths. The invariant σ-field statement explains why a stationary system can have different rates on different paths without contradicting the mean identity. Kingman's examples show how the same framework reaches percolation and matrix products.

The result is mathematically proved, as the 1973 article states. The remaining work here is a machine-checked development of its process model and the displayed results. A published Prove2Me item, PalmQueueing.Ergodic.kingman_subadditive, is open and concerns an ergodic bijective flow with a constant possibly infinite limit; it does not supply this nonergodic finite-limit theorem or convergence in mean. The draft statements in this mission compile with proof placeholders. No machine-checked proof of these new statements is claimed.

Difficulty

Subadditivity gives bounds when intervals are joined, but it does not express $x_{0t}$ as a sum of identically distributed increments. The ordinary additive ergodic theorem therefore does not immediately give convergence for $x_{0t}/t$ . Nor does convergence of the expectations $g_t/t$ alone force convergence on individual paths or in mean. The process may also have a nonconstant limit: stationarity is a joint-law condition, not an ergodicity assumption that erases invariant information. These are the gaps the formalization must close without strengthening the hypotheses. Source: §§1.1–1.3.

Formalization scope

Lean represents $x$ as a function of two natural-number indices and a sample point, but every condition and conclusion uses only $s<t$ . S₁ and the Sᴱ cocycle inequality follow the paper's pointwise displays; random-variable equality in the decomposition is stated almost surely at each valid index pair. Measurability of each valid coordinate is explicit. S₂ compares two probability measures on the full countable path space, so equality of individual marginals cannot satisfy it. The probability measure is normalized, and S₃ requires Bochner integrability to keep every mean finite. The constant $\gamma$ is a real infimum over positive times, used only under S₃. The goal's limit is real and integrable; Kingman's separate Theorem 2 treats a possible value of $-\infty$ and belongs to another mission.

The invariant σ-field is the pullback of the path-space shift-invariant σ-field. Its measurability claim is made through an almost-everywhere equal version, since almost-sure limits are insensitive to changes on null sets. Conditional expectation uses this explicit sub-σ-field. All limits in this mission take positive integer time to infinity. The Sᴱ definition requires measure preservation but no inverse and no ergodicity. Thus neither a marginal-law substitution for S₂ nor an ergodic constant-limit specialization can trivialize the target.

A complete proof can reuse Mathlib's measure theory, conditional expectation, product measurable spaces, measure-preserving maps, and subadditive-sequence results. The two process definitions, the invariant σ-field interface, and auxiliary statements are useful to later formalizations of stationary growth models. Contributions that prove the stated results or develop general-purpose lemmas for these objects fit the mission.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6), 883–899, 1973. DOI: 10.1214/aop/1176996798.

8 thms3 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Loss Networks 1: The Primal Problem Has a Unique Optimum x_r = ν_r ∏_j (1 − B_j)^{A_jr}; the Conditions on B Are Solvable, Uniquely if rank A = J, and Biject with Dual OptimaResearch Paper

Motivation

A loss network carries calls that require capacity on one or more links. A call is accepted only when every required link has enough free circuits; otherwise it is lost. This makes the traffic on different links dependent even when calls on different routes arrive independently. Network operators need to know where capacity constraints bind and how offered traffic is converted into carried traffic. Kelly's 1991 survey develops a continuous optimization problem that identifies a characteristic flow vector and gives a linkwise description of blocking in this setting. Kelly, Loss networks (1991), §§1.2 and 2.1.

The paper begins with the equilibrium distribution of the discrete network and uses a continuous relaxation when analyzing its likely state. The resulting primal problem is useful beyond the original probability calculation because it links route flows, capacity constraints, and a convex dual. Theorem 2.8 collects the existence, uniqueness, and correspondence statements for these descriptions. This mission targets that theorem and the intermediate claims Kelly states in §2.1. Kelly (1991), pp. 327–329.

Setting

There are finitely many links $j$ and finitely many routes $r$ . Link $j$ has $C_j$ circuits, and one call on route $r$ uses $A_{jr}$ circuits there, with $A_{jr}$ a nonnegative integer. Calls request route $r$ at positive offered rate $\nu_r$ . The matrix $A$ need not be a zero–one incidence matrix: one call may use more than one circuit on a link. Kelly's fixed-routing model and its general integer matrix are described in §1.2. Kelly (1991), p. 321.

A real route-flow vector $x=(x_r)$ is primal feasible if $x_r\ge0$ for every route and $\sum_r A_{jr}x_r\le C_j$ for every link. The objective is

F(x)=\sum_r\bigl(x_r\log\nu_r-x_r\log x_r+x_r\bigr),

with $x_r\log x_r=0$ at $x_r=0$ . The primal optimum maximizes $F$ over precisely this feasible set. This is the continuous problem (2.1), rather than an optimization over the integer-valued network state. Kelly (1991), p. 327, (2.1).

A nonnegative vector $y=(y_j)$ assigns one multiplier to each link. The dual objective is

D(y)=\sum_r\nu_r\exp\!\left(-\sum_jy_jA_{jr}\right)+\sum_jy_jC_j, \qquad y_j\ge0.

A blocking vector $B=(B_j)$ has $0\le B_j<1$ . Its carried route flow is $\nu_r\prod_i(1-B_i)^{A_{ir}}$ . The conditions on $B$ say that the total carried flow through link $j$ equals $C_j$ when $B_j>0$ , and is at most $C_j$ when $B_j=0$ . The multiplier and blocking coordinates are related by $B_j=1-e^{-y_j}$ , equivalently $y_j=-\log(1-B_j)$ . These are equations (2.3), (2.6), and (2.7). Kelly (1991), p. 328.

Formalization targets

Theorem 2.8: primal optimum, blocking solutions, and dual optima

The goal first asserts that the primal problem has exactly one optimizer. Every blocking solution must describe that same optimizer:

x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}\quad\text{for every route }r.

It also asserts that a blocking solution exists, and that it is unique if $A$ has rank $J$ , the number of links. Finally, the transformations $B_j=1-e^{-y_j}$ and $y_j=-\log(1-B_j)$ give a bijection between all blocking solutions and all dual optima. The formal goal includes both directions and both inverse identities, even when the dual optimizer is not unique. Kelly (1991), p. 329, Theorem 2.8.

Claims leading to the theorem

The milestone list follows Kelly's stated progression: unique primal attainment; the Lagrangian maximum and the dual value in (2.2); feasibility and complementary slackness in (2.4)–(2.5); the substitution (2.6); dual attainment; both directions of the blocking–dual correspondence; and strict convexity plus uniqueness under full row rank. One direction of the correspondence is an existing, proved platform theorem, KellyStochasticNetworks.dual_optimum_conditions; it is referenced directly. The other direction remains a new target. Kelly (1991), pp. 327–329.

Significance

The theorem makes the carried flow uniquely determined even when several blocking vectors or dual optimizers describe it. Under full row rank, it also identifies a unique linkwise blocking vector. Its correspondence lets a statement in the flow language be translated to a statement in the multiplier language without selecting a preferred optimizer. The interpretation following Theorem 2.8 explains the linkwise condition: positive blocking occurs only on a saturated link. Kelly (1991), p. 329, discussion after Theorem 2.8.

The mathematical result was proved in the source paper. The work here is to obtain machine-checked proofs of its exact finite-dimensional statements. The published Kelly–Yudovina definition KellyStochasticNetworks.dualObjective already represents the dual formula, and its proved optimum-conditions theorem supplies one direction of the correspondence. The remaining development would give reusable facts about separable entropy objectives, nonnegative linear capacity constraints, complementary slackness, and exponential coordinate changes. Those facts can support later loss-network formalizations without changing this mission's target.

Difficulty

The boundary $x_r=0$ requires care: the objective has a continuous value there, but its logarithmic derivative does not. Thus a calculation that differentiates the objective throughout the closed nonnegative cone does not justify the printed differentiability sentence on p. 327. Dual existence is another boundary issue. A nonnegative capacity permits $C_j=0$ , while the paper's stated growth of the dual objective in every nonnegative coordinate can fail at that input. Any formal argument for the complete theorem must cover these domains accurately. Full row rank controls uniqueness of the dual coordinates; without it, the paper explicitly allows nonunique blocking solutions. Kelly (1991), pp. 327–329.

Formalization scope

Lean represents links by Fin J, routes by Fin R, $A_{jr}$ and $C_j$ by natural numbers, and $x_r$ , $y_j$ , $B_j$ , and $\nu_r$ by real numbers. The primal feasible set includes both coordinatewise nonnegativity and every link-capacity inequality. The dual optimum is minimal over the nonnegative orthant, using the published dual objective. The finite sums and products have their usual empty-index values; no hidden nonemptiness assumption is imposed. Matrix rank is taken over the reals and compared with $J$ , so the rank condition is full row rank.

The goal assumes $\nu_r>0$ and $C_j\ge1$ for every route and link. Positive rates give the logarithm in the primal objective its intended meaning. Positive capacities exclude a degeneracy in the dual-attainment and blocking parts of the theorem. The value at $x_r=0$ is the continuous extension $x_r\log x_r=0$ ; no differentiability assertion at that boundary is part of the formal target. Blocking values belong to $[0,1)$ , so the inverse logarithm is evaluated on a positive number. A flow optimum always ranges over the exact primal feasible set, and a blocking solution always ranges over the full conditions (2.7); neither can be replaced by an arbitrary vector with a convenient equation.

A complete proof may require finite-dimensional convex analysis, strict concavity of the entropy term, attainment on a closed feasible set, the dual first-order condition, and facts about exponentials, logarithms, products, and matrix rank. The definitions and theorems are kept separate so work on these pieces can be reused. Contributions proving either a milestone or a reusable supporting lemma are in scope.

Selected references

F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3), 319–378, 1991. DOI: 10.1214/aoap/1177005872.

11 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 1: Markdown Is Optimal Once Time-to-Go Falls Below a Strictly Increasing Threshold x_nResearch Paper

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$ . Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$ . A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$ . Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$ . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$ . If the price changes at deterministic time $s\in[0,t]$ , let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$ , and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$ , is a stopping time for the history of $N_1$ , and occurs before stock is exhausted almost surely. At $s=0$ , $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$ , switching immediately earns the optimal value; when $t>x_n$ , a correction $F(n,t)$ is added:

J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$ . For $n\ge1$ , set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$ . A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$ ; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$ , the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$ .

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$ . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$ , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Stochastic Systems

Missions

Stochastic Orders IV: The Increasing Convex and Increasing Concave OrdersTextbook

Comparing location and spread together

The increasing convex and increasing concave orders

Formalization targets

Goal: the submartingale-coupling characterization (Theorem 4.A.5, increasing convex case)

Companion: the supermartingale-coupling characterization (Theorem 4.A.5, increasing concave case)

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

First-Order and Stochastic Optimization Methods for Machine Learning IV: Variance-Reduced Mirror Descent for Finite-Sum ProblemsTextbook

Motivation

Setting

Formalization targets

Goal — Corollary 5.8

Supporting milestones, in attack order

Significance

Difficulty

Formalization scope

Prior art

Selected references

Stochastic Networks III: Loss Networks and the Erlang Fixed PointTextbook

Motivation

Setting

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

Supporting levels

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Setting

Formalization targets

Goal

Milestones toward and around the goal

Significance

Difficulty

Formalization scope

Selected references

Learning Unknown Service Rates in Queues 3: In Heavy Traffic Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least D(μ)(K−1) log t / (4 log log t) Up to Time (K−1)D(μ)/(4ε)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 18)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Learning Unknown Service Rates in Queues 1: Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least λ_min D(μ)(1−α)(K−1)/(8t) for Infinitely Many tResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 12)

Goal: Theorem 38 for $0<\alpha<1$