Stochastic Systems

Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$. They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$. Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$, finite for $\theta\ge0$:

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).$$

Increments after time $s$ are independent of $\mathcal F_s$. Initial capital $x$ is added to $X$. The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$, and either $\sigma>0$, $\int_{(-1,0)}|y|\,\nu(dy)=\infty$, or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$. The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$. The strategy is admissible ($L\in\Pi$) if no lump sum exceeds the current reserves. Its value is

$$v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),$$

with discount rate $q>0$. For $C\in[0,\infty]$, $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$.

The $q$-scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$. It is extended by $W=0$ on $(-\infty,0)$. The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$, paying $(x-a)^+$ at time $0$. The paper computes its value

$$v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),$$

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$, read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$. The generator is

$$\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).$$

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$, or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$. Then $c^*<\infty$ and:

$$\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);$$ $$\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.$$

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

• Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$, $x\in[0,a]$.
• Lemma 2(i) (p. 15): $c^*<\infty$.
• Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$, $a\ge0$.
• Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$.
• Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$.
• Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$.

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$, and optimality over all strategies reduces to one inequality on $(c^*,\infty)$. It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$, Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$. The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$. Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$. Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$. The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$. The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$: it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

• Admissibility. The paper requires $L_{t+}-L_t<U_t$. The formalization uses $\le$, because the paper's own strategy of paying out everything at once needs it.
• Barrier level (5.2). Printed over $a>0$ and "all $x$", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$, and otherwise $c^*=\infty$.
• Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$. In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$, and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$.
• Proposition 4(i) is stated for initial capital $x\le C$. Beyond $C$, $w$ is unconstrained and the printed claim fails.
• Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$.

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

• Lévy processes and their Laplace exponents;
• scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$;
• reflected processes;
• Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
• M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
• R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

The multiarmed bandit problem asks how a gambler should allocate successive plays among $n$ independent projects, each of which changes state only when it is played, so as to maximize the expected total-discounted reward. Gittins and Jones (1974) showed that it is optimal to play, at every epoch, a project of greatest Gittins index, a number computed from that project alone. The result underlies job scheduling on a single machine, sequential clinical trials and many stochastic resource-allocation models.

Weber (1992) gave a short proof of the index theorem through prevailing charges, and used the same idea to prove a result that was new: the optimal value is a submodular function of the set of projects that are available. Submodularity of the value says that the marginal worth of an extra project shrinks as more projects are on hand. Two consequences appear in the paper: for statistically identical projects started in a common state, the optimal value is concave in their number; and a bound of Tsitsiklis (1986) for a problem with a retirement option is a special case.

Timeline. Gittins and Jones (1974): the index theorem, by an interchange argument (book-length treatment in Gittins (1989)). Whittle (1980): a proof through a retirement option. Varaiya, Walrand and Buyukkoc (1985): the interchange argument in a general setting. Tsitsiklis (1986): a short proof of the index theorem, including the bound $V(S)\le V(\{i,1\})+V(S\setminus\{i\})-M$ for a retirement bandit. Weber (1992): the prevailing-charge proof and the submodularity of the value (Theorem 4).

Setting

There are $n$ bandits $j\in\{1,\dots,n\}$. Bandit $j$ is a Markov chain on a state space $S$ with transition kernel $P$; at each epoch $t=0,1,2,\dots$ the gambler plays one bandit $j(t)$, receives the reward $r(x_{j(t)}(t))$, the played bandit moves one step of its chain and the others stay where they are. Rewards are nonnegative and uniformly bounded, and $0<\beta<1$ is the discount factor. The initial states $x(0)=x$ are fixed. A policy chooses $j(t)$ from the history; its value is $V_\pi(x)=\mathbb E_\pi\big[\sum_{t\ge0}\beta^t r(x_{j(t)}(t))\big]$.

For a set of bandits $I\subseteq\{1,\dots,n\}$, the restricted problem $P(I)$ is the same game played with the bandits of $I$ only, each started in its state in $x$, and

$$V(I)=\sup_\pi V_\pi\quad\text{over the policies of }P(I),\qquad V(\emptyset)=0 .$$

The fair charge $\gamma(y)$ of a state $y$ is the largest ratio of expected discounted reward to expected discounted time over stopping times $\tau\ge1$ of a single bandit started at $y$ (Weber's (4)). On a fixed realisation, where bandit $j$ passes through states $\omega_j(0)=x_j,\omega_j(1),\dots$ on its successive plays, the prevailing charge after $k$ plays is $\gamma_{jk}=\min_{0\le v\le k}\gamma(\omega_j(v))$, a nonincreasing sequence. $U_t(I)$ is the sum of the first $t$ terms of the interleaving of the sequences $(\gamma_{jk})_{k\ge0}$, $j\in I$, into nonincreasing order.

Formalization targets

Goal: Theorem 4, eq. (9)

$$V(I\cap J)+V(I\cup J)\le V(I)+V(J)\qquad\text{for all }I,J\subseteq\{1,\dots,n\}.$$

This holds for arbitrary bandits (no identical-bandit hypothesis) under the standing assumptions of the paper's Section 1.

Milestones on the path

1. Eq. (10): for nonincreasing nonnegative sequences and every $t\ge0$, $U_t(I\cap J)+U_t(I\cup J)\le U_t(I)+U_t(J)$. A deterministic inequality.
2. The representation used in the last line of the proof:

$$V(I)=\mathbb E\Big[\sum_{t\ge0}\beta^t\big(U_{t+1}(I)-U_t(I)\big)\Big],$$

the expectation over independent realisations of the bandits' state sequences.

Consequences stated in the paper

3. Identical bandits started in a common state: $m\mapsto V$ of the $m$-bandit problem is nondecreasing and concave.
4. Tsitsiklis's bound: if bandit $b$ always pays $(1-\beta)M$, then $V(S)\le V(\{i,b\})+V(S\setminus\{i\})-M$ for $i\ne b$.

Significance

Submodularity of the value is a structural fact about the bandit problem that the index theorem alone does not give: the index theorem identifies an optimal policy for a fixed set of projects, while (9) compares optimal values across sets. It yields diminishing returns from adding projects, the concavity of the value in the number of identical projects, and Tsitsiklis's retirement bound, which separates one project from the rest. Bounds of this kind are used when choosing which projects to make available before allocation begins.

Theorem 1 of the paper, the optimality of the Gittins index policy, is already on Prove2Me as BanditAlgorithm.gittins_index_theorem (Proved, Shuze Chen), together with the discounted Markov bandit model and the Gittins index (GittinsIndex, Shuze Chen) and a finite-horizon form of the prevailing-charge coupling (BanditAlgorithm.gittins_finite_prevailing_charge_eq_stack_coupling_value, Harry_Xu). This mission builds on those items. Theorem 4, inequality (10) and the infinite-horizon representation of $V(I)$ have no machine-checked proof that we know of. The other two missions of this series formalize Weber's Theorem 2 (mission 1, a suboptimality bound by prevailing charges) and Theorem 3 (mission 2, a suboptimality bound by index gaps); this mission does not depend on them.

Difficulty

Inequality (10) concerns sums of largest terms of merged sequences; it fails without nonnegativity when $I$ and $J$ are disjoint, and a proof must use both the monotonicity of each sequence and the sign of the terms. The representation of $V(I)$ requires the fair-game property of prevailing charges in infinite horizon: that the optimal policy of $P(I)$ collects in expectation exactly the discounted charges it pays, and that, on a common probability space of independent bandit trajectories, the charges paid by the optimal policy are the nonincreasing interleaving. The finite-horizon coupling is on the platform; passing to infinite horizon, identifying the interleaving with the play of an index policy, and handling ties and measurability are the remaining work. Finally, (10) is an undiscounted, pathwise statement while (9) compares discounted expectations, so the two must be connected through series of increments of $U_t$ and an exchange of expectation and series.

Formalization scope

The model is the published BanditAlgorithm discounted Markov bandit: one standard Borel state space $S$, one kernel $P$ and one measurable reward $r$ shared by all bandits; bandits with different dynamics are encoded by a disjoint union of state spaces. $r$ is the mean reward. The value of a policy is the series of per-round expected rewards (markovBanditDiscountedValue), equal to the expectation of the discounted sum for bounded rewards. The fair charge $\gamma$ is the published gittinsIndex.

Explicit readings of the paper's phrases:

• "the restriction of the problem to bandits in $I$": the $|I|$-armed game whose arms are the bandits of $I$ in increasing order, started at their states in $x$ (restrictedValue), with $V(\emptyset)=0$ set explicitly;
• "the maximal expected total-discounted reward": the supremum over all history-dependent randomized policies;
• "a fixed realisation of the states through which bandit $j$ evolves": a point of the product of independent Markov chain laws Measure.pi (fun j => markovChainMeasure P (x j));
• "interleaving into nonincreasing order … summing the first $t$ elements": partialInterleavedSum, the maximum over allocations of $t$ plays of the sum of initial segments, equal to the interleaving sum for nonincreasing sequences, with $U_t(\emptyset)=0$; the sequences start at $k=0$ (the printed $\{\gamma_{jk}\}_{k=1}^\infty$ is a misprint);
• "multiplying (10) by $\beta^t$, summing": the discounted charge is $\sum_t\beta^t(U_{t+1}-U_t)$, the increments of $U_t$;
• "rewards are nonnegative and uniformly bounded", $0<\beta<1$: binders of every probabilistic statement, together with StandardBorelSpace S and Measurable r;
• "concave increasing": nondecreasing and with nonincreasing increments, including $n=0$;
• "bandit 1 always pays $(1-\beta)M$": an absorbing initial state with reward $(1-\beta)M$.

Trivializing formalizations are ruled out: $V(\emptyset)$ and $U_t(\emptyset)$ are defined as $0$ rather than obtained from a supremum over an empty type, the supremum defining $V(I)$ is over a nonempty family bounded by $C/(1-\beta)$, $U_t$ is a maximum over a finite nonempty set, and the hypotheses are satisfiable (checked on a one-bandit instance).

A complete development needs: the infinite-horizon prevailing-charge identity for index policies, measurability of the charge stacks (the measurability of gittinsIndex is on the platform), and a combinatorial lemma on merges of nonincreasing sequences. Inequality (10) and the merge lemmas are reusable beyond bandits, for sums of largest elements and weighted rank functions of uniform matroids.

Selected references

• R. Weber, On the Gittins index for multiarmed bandits, Ann. Appl. Probab. 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 241–266, 1974.
• J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, Wiley, 1989.
• P. Whittle, Multiarmed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42, 143–149, 1980.
• P. Varaiya, J. Walrand, C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30, 426–439, 1985.
• J. N. Tsitsiklis, A lemma on the multiarmed bandit problem, IEEE Trans. Automat. Control 31, 576–577, 1986.
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

Motivation

The multiarmed bandit problem asks how to allocate a single resource, one play per period, among several alternative projects whose states evolve only while they are worked on. It models the scheduling of jobs on one machine, the sequencing of research projects, and the design of sequential clinical trials. Gittins and Jones (1974) showed that the problem with discounted rewards is solved by an index policy: compute for every project a number depending only on that project's current state, and always work on a project of greatest index. Weber's paper (Ann. Appl. Probab. 2 (1992)) gives a short proof of this theorem through fair and prevailing charges, and uses the same accounting to derive bounds on how much any other policy loses.

In practice the optimal policy is often not the one used: indices may be expensive to compute, or a simpler heuristic may be preferred. A bound on the loss of an arbitrary policy, computable along that policy's own trajectory, tells a practitioner how far from optimal the chosen heuristic is. This mission formalizes the first such bound of the paper, Theorem 2, which Weber attributes to Glazebrook (1990).

Timeline. Gittins and Jones (1974) and Gittins (1979) proved optimality of the index policy by an interchange argument. Whittle (1980) gave a proof through a retirement option. Glazebrook (1982) bounded the suboptimality of a policy in terms of Gittins indices only; Glazebrook (1990) gave the sharper bound stated here as Theorem 2. Weber (1992) rederived it from the prevailing-charge accounting and added the index-gap bound (Theorem 3) and the submodularity of the optimal value (Theorem 4).

Setting

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

$$V_\pi(x) = \mathbb{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 per-play charge at which a gambler holding a single bandit in state $y$, free to stop at any time, would only just break even. Equivalently it is the largest ratio of expected discounted reward to expected discounted time over stopping times $\tau \ge 1$. Weber's Gittins index is $G(y) = \gamma(y)/(1-\beta)$. The prevailing charge of bandit $i$ at time $t$ is the least fair charge seen so far on that bandit, $\min_{0\le s\le t}\gamma(x_i(s))$. A Gittins policy $\pi^*$ plays at each epoch a bandit of greatest index; Theorem 1 of the paper says it is optimal.

Formalization targets

Goal: Theorem 2, inequality (6)

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

$$V_{\pi^*}(x) - V_\pi(x) \le (1-\beta)\,\mathbb{E}_\pi\Big[\sum_{t=0}^\infty \beta^t\Big(\max_i \min_{0\le s\le t} G_i(x_i(s)) - \frac{R_{j(t)}(x_{j(t)}(t))}{1-\beta}\Big) \,\Big|\, x(0)=x\Big].$$

Milestones

1. Eq. (5), from Remark 1: for every policy, $V_\pi(x) \le \mathbb{E}_\pi\big[\sum_t \beta^t \min_{0\le s\le t}\gamma_{j(t)}(x_{j(t)}(s))\big]$.
2. The greatest prevailing charge on a fixed realisation (p. 1028): along any fixed realisation of the bandits' state sequences, the greatest prevailing charge at time $t$ under any policy is at least its value under the Gittins policy.
3. The bound is achieved by the Gittins policy (proof of Theorem 1): $V_{\pi^*}(x) = \mathbb{E}_{\pi^*}\big[\sum_t \beta^t \max_i \min_{0\le s\le t}\gamma(x_i(s))\big]$.

Significance

The result. Inequality (6) bounds the loss of an arbitrary policy by a quantity observed along that policy's own trajectory: at each epoch, how far the reward collected falls below the greatest prevailing charge. A policy that plays a bandit of greatest prevailing charge whenever possible and collects its charge as reward loses nothing, which recovers Theorem 1. The bound is the basis of Glazebrook's analysis of near-optimal heuristics for bandit and stochastic-scheduling problems, and of the index-gap bound (7) of Theorem 3, which is the second mission of this series.

Formalizing it. Theorem 1 of the paper (optimality of the Gittins policy) is already formalized and proved on Prove2Me as BanditAlgorithm.gittins_index_theorem (Shuze Chen, following Lattimore and Szepesvári, Theorem 35.9), together with the finite-horizon prevailing-charge accounting and the charge-stack interleaving lemmas (Harry_Xu). Theorem 2 itself has no machine-checked proof. This mission produces the infinite-horizon forms of the charge accounting, (5) and its equality case for the Gittins policy, and the realisation-wise comparison of greatest prevailing charges, and combines them into (6). Missions 2 (Theorem 3, the index-gap bound) and 3 (Theorem 4, submodularity of the optimal value) of this series state the paper's other results on the same model; none of the three relies on the others.

Difficulty

The paper's proof is one sentence: combine (5) with the realisation-wise observation. The two pieces live on different probability spaces. Inequality (5) and the equality for the Gittins policy are expectations under the law of each policy's own history, while the comparison of greatest prevailing charges is made on a fixed realisation of each bandit's state sequence. Transferring the deterministic comparison into an inequality between expectations under two different policies needs a coupling under which every policy sees the same per-bandit state sequences, so that the prevailing-charge stacks are the same random objects under $\pi$ and $\pi^*$. The naive approach, comparing the two laws round by round, fails: the round-$t$ histories of $\pi$ and $\pi^*$ have different distributions, and no pointwise inequality holds between them. The infinite-horizon statements also require controlling the terminal retirement potential, which vanishes only in the discounted limit.

Formalization scope

The development uses the published BanditAlgorithm model (GittinsIndex, GittinsTerminalPotential, GittinsPrevailingChargeValue, GittinsChargeInterleaving). Conventions committed to:

• Weber's $n$ bandits with separate state spaces are one state space $S$ with one kernel $P$ and reward $r$ (take the disjoint union). $S$ is a standard Borel space and $r$ is measurable: regularity the paper leaves implicit.
• $r$ is the conditional mean of Weber's random reward $R_j(x_j(t))$; only the mean enters (1), (5) and (6).
• The standing assumptions of Section 1, "rewards are nonnegative and uniformly bounded" and $0<\beta<1$, are hypotheses of the goal and of milestones 1 and 3.
• Every $\mathbb{E}_\pi[\sum_t \beta^t(\cdot)]$ is written as $\sum_t \beta^t\,\mathbb{E}_\pi[\cdot]$, the convention of the published value $V_\pi$; these agree for bounded rewards.
• Time starts at $0$. At round $t$ the integrand is evaluated on the history of the first $t$ rounds together with the current state vector $x(t)$, so every $\min_{0\le s\le t}$ includes the current state.
• $\gamma$ is the published gittinsIndex (the ratio (4)); $G = \gamma/(1-\beta)$ is a new definition weberIndex. The goal uses $G$ and the factor $1-\beta$, as in (6); milestones 1 and 3 use $\gamma$, as the paper does.
• "$\pi^*$ is the optimal (Gittins) policy" is any policy satisfying the published IsGittinsIndexPolicy (with probability one it plays an arm of greatest index, ties arbitrary). The goal does not assume such a policy exists; a one-armed instance shows the hypotheses can be met.
• "On a fixed realisation" (milestone 2) is encoded deterministically: arbitrary nonincreasing sequences $H_i$ as the prevailing-charge stacks, any action sequence as a policy, and any greedy interleaving as the Gittins policy.
• $\max_i$ is a supremum over $\mathrm{Fin}\,k$; at $k=0$ no policy exists.

Replacing $G$ by $\gamma$ in (6) would weaken the bound by the factor $1-\beta$, and dropping the boundedness of rewards would let the published value be a junk $0$; neither is the paper's statement, and both are ruled out by the conventions above.

Contributions welcome: the infinite-horizon limits of the published finite accounting, a coupling of all policies on independent per-bandit state sequences, and the deterministic comparison of greatest exposed charges, which is reusable for any interleaving argument on nonincreasing sequences.

Selected references

• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
• K. D. Glazebrook, Procedures for the evaluation of strategies for resource allocation in a stochastic environment, Journal of Applied Probability 27(1), 215–220, 1990.
• K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19(3), 716–722, 1982.
• 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
• T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

Motivation

The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.

Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.

Setting

Let $f:\mathbb R\to\mathbb R$ be a target density: positive, $C^2$, integrating to one, with $f'/f$ Lipschitz, and satisfying the moment conditions (A1) $\mathbb E_f[(f'/f)^8]<\infty$ and (A2) $\mathbb E_f[(f''/f)^4]<\infty$. Here $\mathbb E_f[g(X)]=\int g(x)f(x)\,dx$. In dimension $n\ge2$ the target is the product density $\pi_n(x)=\prod_{i=1}^n f(x_i)$ on $\mathbb R^n$.

Fix a scale $l>0$ and set $\sigma_n^2=l^2/(n-1)$. The random walk Metropolis chain $X^n=(X^n_0,X^n_1,\dots)$ moves as follows. From $X^n_{m-1}$ it proposes $Y\sim N(X^n_{m-1},\sigma_n^2I_n)$. It sets $X^n_m=Y$ with probability $\alpha(X^n_{m-1},Y)=1\wedge\pi_n(Y)/\pi_n(X^n_{m-1})$, and $X^n_m=X^n_{m-1}$ otherwise. The chain starts from $\pi_n$, which is stationary for it. The speeded-up first coordinate is $U^n_t=X^n_{\lfloor nt\rfloor,1}$ for $t\ge0$.

Let $\Phi$ be the standard normal distribution function, and define the roughness $I=\mathbb E_f[(f'(X)/f(X))^2]$. The speed and the limiting acceptance rate are

$$h(l)=2l^2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big),\qquad a(l)=2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big).$$

The Langevin generator is $GV(x)=h(l)\big[\tfrac12V''(x)+\tfrac12(\log f)'(x)V'(x)\big]$. It generates the Langevin diffusion $dU_t=h(l)^{1/2}dB_t+h(l)\frac{f'(U_t)}{2f(U_t)}dt$.

Formalization targets

Goal: Theorem 1.1

As $n\to\infty$,

$$U^n\Rightarrow U,$$

where $\Rightarrow$ denotes weak convergence in the Skorokhod topology, $U_0$ has density $f$, and $U$ is the Langevin diffusion with speed $h(l)$. The limit is asserted to exist. No constants appear in the statement beyond those the model defines.

Milestones: the proof

1. Lemma 2.1. The stationary chain stays in the sets $F_n=\{|R_n-I|<n^{-1/8}\}\cap\{|S_n-I|<n^{-1/8}\}$ up to time $t$ with probability tending to one. Here $R_n$ and $S_n$ are the empirical averages of $((\log f)')^2$ and $-(\log f)''$ over coordinates $2,\dots,n$.
2. Proposition 2.2. $|1\wedge e^x-1\wedge e^y|\le|x-y|$.
3. Lemma 2.3. $\sup_{x\in F_n}\mathbb E|W_n|\to0$, where $W_n$ is the second-order part of the log acceptance ratio.
4. Proposition 2.4. $\mathbb E[1\wedge e^A]=\Phi(\mu/\sigma)+e^{\mu+\sigma^2/2}\Phi(-\sigma-\mu/\sigma)$ for $A\sim N(\mu,\sigma^2)$.
5. Lemma 2.5. $\limsup_n\sup_{x_1}n|\mathbb E[V(Y_1)-V(x_1)]|<\infty$ for $V\in C_c^\infty$.
6. Lemma 2.6. The discrete generator $G_nV(x)=n\,\mathbb E[(V(Y)-V(x))\alpha(x,Y)]$ converges to $GV$ uniformly on $F_n$, for $V\in C_c^\infty$ a function of the first coordinate (stated with bounded $(\log f)'''$, the assumption its proof uses).

Milestones: the optimal-scaling corollary

7. Corollary 1.2 (i). $a_n(l)=\iint\pi_n(x)\alpha(x,y)q_n(x,y)\,dx\,dy\to a(l)$.
8. Corollary 1.2 (ii). $h$ is maximised at $\hat l=2.38/\sqrt I$, with $a(\hat l)=0.23$ and $h(\hat l)=1.3/I$, to the printed precision.

Significance

Theorem 1.1 shows that, run for $n$ times as many steps, the chain in dimension $n$ looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number $h(l)$. Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the $2.38/\sqrt I$ scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.

The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on $\mathbb R^n$ as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.

Difficulty

The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of $n-1$ terms of size $1/n$. That sum does not concentrate uniformly over the state space, since the coordinates $2,\dots,n$ are arbitrary. The expansion is controlled only on the sets $F_n$, where the empirical averages $R_n$ and $S_n$ are close to $I$. The limit therefore holds only after showing that the chain rarely leaves $F_n$ over a time horizon of $nt$ steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over $nt$ steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.

Formalization scope

All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.

• Vectors are Fin n → ℝ, and the paper's first coordinate $x_1$ is index 0. Its coordinates $2,\dots,n$ are the indices i ≠ 0.
• $\sigma_n^2=l^2/(n-1)$ is computed in $\mathbb R$. All statements concern $n\ge2$ or large $n$.
• $l>0$ is assumed. The paper leaves it implicit, but $h(-l)\ne h(l)$.
• "$f$ is a density" is read as $\int f=1$. The moment conditions are read as integrability of $(f'/f)^8f$ and $(f''/f)^4f$. The standing assumption "$f'/f$ is Lipschitz" (p. 111) is carried by every statement.
• The chain is built as a random mapping on an explicit probability space: $x_0\sim\pi_n$, with i.i.d. standard normal innovations and uniform acceptance variables. Theorem 1.1's initial condition (components i.i.d. $f$, shared across dimensions) is read as "the $n$-th chain starts from $\pi_n$", since weak convergence depends only on the law of each $U^n$.
• "$U$ satisfies the Langevin SDE" is read as "the law of $U$ solves the martingale problem for $G$ on $C_c^\infty$, with continuous paths and initial law $f(x)\,dx$". This is equivalent by Ethier–Kurtz (1986), Ch. 5, Prop. 3.1 and Thm 3.3, and follows the platform definition EthierKurtz_IsContinuousDiffusionLaw.
• "$U^n\Rightarrow U$" is read as the existence of an almost-sure coupling in which càdlàg copies of the $U^n$ converge to a continuous Langevin path uniformly on compact time intervals. For a continuous limit this is equivalent to weak convergence in $D_{\mathbb R}[0,\infty)$, by Skorokhod's representation theorem and Ethier–Kurtz Ch. 3, Thm 1.8, Prop. 5.3 and Prop. 7.1. It follows the platform encoding of Ethier–Kurtz Theorem 7.4.1.
• "$\sup\to0$" and "$\limsup\sup<\infty$" are stated as eventual uniform bounds. This avoids real suprema, whose value on an unbounded set is a default.
• In Lemma 2.6, "as $d\to\infty$" is a misprint for $n\to\infty$, and "$2f(Ut)$" in (1.2) is read as $2f(U_t)$.
• Corollary 1.2 (ii) is stated for an arbitrary constant $I>0$. "To two decimal places" is read as explicit rounding intervals: $1.3$ is read to one decimal, and all maximisers over $l>0$ are covered.

The goal cannot be satisfied trivially. The limit law $Q$ must exist, and it must be a probability measure whose initial marginal is $f(x)\,dx$, so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths $U^n$, not an arbitrary process with the same one-time marginals.

The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds $\sup_z|(\log f)'''(z)|$, which Theorem 1.1 does not assume, and under $C^2$ alone the uniform convergence over $F_n$ claimed by Lemma 2.6 fails (narrow spikes of $(\log f)''$ far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while $R_n$ and $S_n$ stay close to $I$). Lemma 2.6 is therefore stated with the proof's own assumption, $f\in C^3$ with $(\log f)'''$ bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.

A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.

Selected references

• G. O. Roberts, A. Gelman, W. R. Gilks, Weak convergence and optimal scaling of random walk Metropolis algorithms, Ann. Appl. Probab. 7(1), 110–120, 1997. https://doi.org/10.1214/aoap/1034625254
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• A. Gelman, G. O. Roberts, W. R. Gilks, Efficient Metropolis jumping rules, Bayesian Statistics 5, Oxford University Press, 599–607, 1996.
• G. O. Roberts, J. S. Rosenthal, Optimal scaling for various Metropolis–Hastings algorithms, Statistical Science 16(4), 351–367, 2001. https://doi.org/10.1214/ss/1015346320

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.

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

1. Lemma 18 (Bretagnolle–Huber, p. 37), referenced from the platform.
2. 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)}$.
3. 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)$.
4. 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