Bandit Algorithms

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

Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is $\tilde O(\sqrt{T\sum_k T_k})$, and a lower bound showing that no policy, even one told the periods, does better than $\Omega(\sqrt{T\max_k T_k})$. This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.

Lower bounds of this kind fix what is achievable. For the stationary $K$-armed bandit, the minimax regret is of order $\sqrt{TK}$ (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces $\sum_k T_k$ "effective arms" (arm $k$ at each phase of its cycle), which suggests the rate $\sqrt{T\sum_k T_k}$. The paper proves the weaker but general bound $\sqrt{T\max_k T_k}/(32e)$, which matches the upper bound up to a factor $\sqrt K$ and logarithms.

Setting

There are $K \ge 2$ arms and epochs $t = 1, \dots, T$. An instance $\nu$ is a family of mean rewards $\mu_{k,t}$. If arm $k$ is pulled at epoch $t$, the reward is drawn from the Gaussian law $\mathcal N(\mu_{k,t}, 1)$, independently of the past given the arm.

A sequence $f$ has minimum period $p \ge 1$ if $f(t+p) = f(t)$ for all $t \ge 1$ and no smaller positive integer has this property.

A policy $\pi$ chooses the arm $\pi_t$ at epoch $t$ at random, from a distribution that depends on the previous arms and rewards. Its expected regret on $\nu$ is display (1) of the paper:

$$\mathbb E_\nu[R^\pi_T] = \sum_{t=1}^T\Big(\max_k \mu_{k,t} - \mathbb E[\mu_{\pi_t,t}]\Big).$$

Three classes of instances appear, all with unit-variance Gaussian rewards and means in $[0,1]$ (Assumption 1):

1. $\mathcal E_1$: every arm is stationary;
2. $\mathcal E_2(T_1)$: the first arm's mean has minimum period $T_1$, the other arms are stationary;
3. $\mathcal E_3(T_1,\dots,T_K)$: arm $k$'s mean has minimum period $T_k$.

The proof compares instances through the metric (B-48),

$$\mathcal M(\nu_1,\nu_2) = \Big(\sum_{k=1}^K\sum_{p=1}^{T_k}\big(\mu^{(\nu_1)}_{k,p} - \mu^{(\nu_2)}_{k,p}\big)^2\Big)^{1/2}.$$

The periods satisfy Assumption 3 with the parameters (7): with $n = \lfloor\sqrt{T/K}\rfloor$ and $g = \lceil\sqrt n\rceil$, $T > 4K$, $g \ge 2$ and $T_k < n/(2g)$ for every $k$.

Formalization targets

Goal: Theorem 3 (p. 24)

For every policy $\pi$ there is $\nu \in \mathcal E_3(T_1,\dots,T_K)$ with

$$\mathbb E_\nu[R^\pi_T] \ge \frac{1}{32e}\sqrt{T\max_k T_k}.$$

Milestones

1. Lemma 12 (p. 23). Stationary Gaussian bandits whose arms other than the first have known mean $1/2$: every policy has regret at least $\sqrt T/(8\sqrt2 e)$ on some choice of $\mu_1 \in [0,1]$.
2. Lemma 13 (p. 23). One periodic arm: every policy has regret at least $\sqrt{TT_1}/(16e)$ on some instance of $\mathcal E_2(T_1)$ whose other arms have mean $1/2$.
3. Fact 1 (proof of Theorem 3, p. 48). $\mathcal E_3$ is dense in $\mathcal E_2 \cup \mathcal E_3$ under $\mathcal M$: an instance of $\mathcal E_2(T_1)$ can be perturbed on the arms other than the first into an instance of $\mathcal E_3(T_1,\dots,T_K)$ at $\mathcal M$-distance less than any $\delta > 0$.
4. Fact 2 (proof of Theorem 3, p. 48). The regret $f_\pi(\nu) = \mathbb E_\nu[R^\pi_T]$ is continuous in $\nu$ on $\mathcal E_2 \cup \mathcal E_3$ for $\mathcal M$, uniformly in $\pi$.

Significance

Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like $\sqrt{T\max_k T_k}$, not like $\sqrt{TK}$. Together with the paper's upper bound $\tilde O(\sqrt{T\sum_k T_k})$ and the inequality $\sqrt{T\max_k T_k} \ge \sqrt{T\sum_k T_k}/\sqrt K$, it shows the two-stage policy is near-optimal when $K$ is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.

The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.

Difficulty

The two-point argument of Lemma 12 is standard, but its constant needs $\Delta = \sqrt{1/(2T)} < 1/2$, so small horizons must be handled separately. Lemma 13 decomposes the problem into $T_1$ phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon $\lfloor T/T_1\rfloor$, with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly $T_1$ (all phases may coincide), so a perturbation is needed to land in $\mathcal E_2(T_1)$; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a $T$-round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.

Formalization scope

• Arms are Fin K, 0-based: the paper's first arm is index $0$. Epochs are 1-based natural numbers; history coordinate $i$ is epoch $i+1$. Values of the means at $t = 0$ are ignored.
• A policy is the platform's BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, $T\mu^* - \mathbb E[\sum_t X_t]$, which equals (1) for Gaussian arms; the other statements use (1) directly.
• Assumption 1 is stated on epochs $1,\dots,T$. Minimum periods are exact.
• Every lower bound has the order "for every policy there is an instance", with the instance in the class, so the policy may depend on $K$, $T$ and the periods; this is the paper's "policy that knows $T_k$". The supremum over the class is replaced by an attained instance, which is the stronger form.
• Added hypotheses, all disclosed: $K \ge 2$ (with one arm the regret is $0$); $T_k \ge 1$ (the paper's $T_k \in \mathbb N^+$); in Lemmas 12 and 13, the means of the arms other than the first are $1/2$, which is how "a policy that knows $\mu_k$ for $k \ge 2$" is read (with arbitrary known values the printed lemmas fail). Assumption 3 with (7) is the standing assumption of Appendix B.4.
• A statement with the quantifiers in the order "there is an instance for every policy", without the $[0,1]$ clause, or without exact minimum periods, would be false or trivial; none of these is the target.

Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, Operations Research, 2025; arXiv:2005.08088v4, 2021. https://arxiv.org/abs/2005.08088v4
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375

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

Motivation

In contextual dynamic pricing a seller posts a price for each arriving customer, observes only whether the customer buys, and must learn the demand from these binary responses while selling. The problem arises in e-commerce, insurance and consumer lending, where every customer comes with features (product attributes, customer characteristics) that shift the willingness to pay. Most regret analyses assume either that the noise distribution of the valuation is known up to a parameter, or that it belongs to a parametric family. Luo, Sun and Liu (arXiv:2109.07340, Mathematics of Operations Research, 2024) drop that assumption: the valuation is linear in the features plus a noise with an unknown distribution, and they give a policy, DIP, whose regret is bounded without parametric knowledge of the noise.

This mission formalizes the paper's main upper bound, Theorem 1, together with the chain of lemmas and propositions of its proof. The source is the arXiv v2 preprint (6 March 2023); all proofs are in its Appendix A.

Setting

At each period $t = 1, 2, \dots$ a customer arrives with a covariate $x_t \in \mathcal X \subseteq \mathbb R^{d_0}$, where $\|x\|_\infty \le 1$ on $\mathcal X$. The customer's valuation is $v_t = x_t^\top\theta_0 + z_t$, with an unknown parameter $\theta_0$, $\|\theta_0\|_1 \le W$ for a known $W$, and market noises $z_t$ drawn i.i.d. from an unknown CDF $F$. The seller posts a price $p_t \in (0, p_{\max})$ and observes $y_t = \mathbf 1\{v_t \ge p_t\}$; the revenue is $p_ty_t$. The expected revenue of price $p$ at linear value $q = x^\top\theta_0$ is

$$f_q(p) = p\bigl(1 - F(p - q)\bigr).$$

The clairvoyant price $p^*(x)$ maximizes $f_{x^\top\theta_0}$ over $p > 0$ and is assumed to lie in $(0, p_{\max})$. The regret of period $t$ is $r_t = f_{x_t^\top\theta_0}(p^*(x_t)) - f_{x_t^\top\theta_0}(p_t)$, and $R_T = \sum_{t=1}^T r_t$.

Two assumptions are made on $F$. Assumption 1: $F$ is $L$-Lipschitz. Assumption 2: there is a constant $C_A$ with $f_q(p^*(x)) - f_q(p) \le C_A(p^*(x) - p)^2$ for all $x \in \mathcal X$, $q = x^\top\theta_0$ and $p \in [0, p_{\max}]$.

The DIP policy (Algorithm 4) splits time into episodes of lengths $\ell_1 = \alpha_1$ and $\ell_k = 2^{k-2}\ell_2$, $\ell_2 = \alpha_2$, for $k \ge 2$. In episode $k \ge 2$ it takes an estimate $\hat\theta_{k-1}$ computed from episode $k-1$ (Inner Algorithm A), cuts $G(\hat\theta) = [-\|\hat\theta\|_1, p_{\max} + \|\hat\theta\|_1]$ into $d_k = C_d\lceil(2^{k-2}\ell_2)^{1/6}\rceil$ equal pieces with midpoints $m_j$, and runs a UCB rule (Inner Algorithm B) over the candidate prices $m_j + x_t^\top\hat\theta \in (0, p_{\max})$. The UCB step is analysed as a perturbed linear bandit (PLB): rewards $Z_t = \langle\xi_t, A_t\rangle + \eta_t$ whose parameters satisfy $\|\xi_s - \xi_t\|_\infty \le C_p$. The algorithm M-LinUCB (Algorithm 5) is optimistic linear UCB with forced exploration of new coordinates.

Formalization targets

Goal: Theorem 1 with the $\tilde O$ pinned

For every model satisfying the standing assumptions and Assumptions 1–2, every DIP configuration with $p_{\max} + 2W < C_d\,p_{\max}$ and $\lambda > 0$, there is $C > 0$ such that every run of DIP satisfies, for all $T \ge 2$,

$$\mathbb E(R_T) \le C\,T^{2/3}\log T + 4p_{\max}L\sum_{k=2}^{n}2^{k-2}\ell_2\,\mathbb E\|\hat\theta_{k-1} - \theta_0\|_1,$$

where $n = n(T, \alpha_1, \alpha_2)$ is the number of episodes. The printed statement reads $\tilde O(T^{2/3})$; the single logarithm is what the proof gives.

Milestones

In the order of the proof: Lemma 1 (the pricing problem of one episode is a PLB with perturbation $2L\|\hat\theta - \theta_0\|_1$); Lemma 2 (M-LinUCB on that PLB is Inner Algorithm B); Lemmas S1–S5 (weighted averages, the elliptical potential lemma, the shadow parameter, the self-normalized bound, a confidence ellipsoid); Lemma 3 (M-LinUCB on a PLB has regret $\tilde O(d\sqrt{T_0}) + 2a_{\max}C_pT_0$ with high probability); Proposition 4 (the discrete-part regret of one episode); Lemma S6 (the confidence term in $\sqrt d\log T_0$ form); Proposition 3 (the total regret of one episode, $\mathbb E(R_{T_0}) \le C'_3\log(C'_2T_0)T_0^{2/3} + 4p_{\max}L\|\hat\theta - \theta_0\|_1T_0$). Lemmas S2 and S4 are already proved on the platform and are referenced.

Significance

The bound separates the cost of learning the unknown noise distribution, $T^{2/3}$ up to a logarithm, from the cost of estimating $\theta_0$, which enters only through the $\ell_1$ estimation errors. Any estimator with a known error rate therefore gives an explicit regret rate for DIP: if $\mathbb E\|\hat\theta_k - \theta_0\|_1 = O(\ell_k^{-\alpha})$ with $0 < \alpha \le 1/2$, the regret is $\tilde O(T^{2/3 \vee (1-\alpha)})$ (p. 19). The rate of the paper's logistic-regression estimator on adaptively collected data is not established; the authors study it by simulation. Lemma 3 is a regret bound for linear bandits with bounded parameter drift that is linear in the drift and $\tilde O(d\sqrt{T_0})$ otherwise, which the authors note is of independent interest.

The results are proved in the paper, not formalized. The two textbook lemmas the paper quotes, the elliptical potential lemma (S2) and the self-normalized bound (S4), are already proved on the platform; the paper's own results (Lemma 3, the PLB reduction, the episode analysis and Theorem 1) have no machine-checked proof. Faithfulness checks during drafting found printed slips that the formal statements correct and disclose: the unsquared norm in Lemma S2, the finite UCB of an unpulled arm in display (2), and a missing nonemptiness condition for the candidate price sets.

Difficulty

The obvious argument treats each episode as a linear bandit around the central parameter $\xi^* = (1 - F(m_j))_j$ and invokes the standard optimistic regret bound. That fails because the parameter $\xi_t$ moves with the covariate $x_t$ through the estimation error $x_t^\top(\hat\theta - \theta_0)$; the ridge estimate then tracks no fixed vector, and a general misspecified-bandit bound pays an extra factor $\sqrt d$ in the drift term (Remark 5, p. 21), which destroys the $T^{2/3}$ rate once $d$ grows with the horizon. A second difficulty is bookkeeping: the per-episode bound must hold uniformly over the random estimate $\hat\theta_{k-1}$, over the growing discretization $d_k$, and over the truncated last episode, before the episodes are summed.

Formalization scope

Periods are 1-based; arm indices are Fin d, 0-based. Norms are written out: $\|v\|_1 = \sum_i|v_i|$, $\|v\|_\infty$ coordinatewise. The probability space carries a filtration $\mathcal G$; covariates and prices are $\mathcal G_{t-1}$-measurable (adaptive or adversarial covariates and randomized prices are allowed), and $z_t$ has CDF $F$ and is independent of $\mathcal G_{t-1}$. Conditional sub-Gaussianity is Mathlib's HasCondSubgaussianMGF, which needs a standard Borel sample space. Expectations are lower Lebesgue integrals of nonnegative regrets. "With probability at least $1 - \delta$" means a measurable event of probability at least $1 - \delta$ on which the bound holds.

The standing assumptions are $\|\theta_0\|_1 \le W$, $p_{\max} > 0$, $\|x\|_\infty \le 1$ on $\mathcal X$, and $p^*(x) \in (0, p_{\max})$ maximizing the revenue over $p > 0$. Hypotheses added to the printed statements: $p_{\max} + 2\|\hat\theta\|_1 < d\,p_{\max}$ (resp. $p_{\max} + 2W < C_d\,p_{\max}$), which makes every candidate price set nonempty; $\|\hat\theta\|_1 \le W$ in Proposition 3; $\delta \in (0,1)$ in Lemma 3; finite action sets; a nonempty index set in Lemma S1. Algorithm 3 is read with forced exploration of unpulled arms, as Lemma 2 fixes. Inner Algorithm A is any measurable estimator of the previous episode's data with values in $\{\|\theta\|_1 \le W\}$; the paper's logistic regression with projection is one instance. Algorithms are run predicates that hold for every tie-breaking rule. The constants of Theorem 1, Proposition 3 and Lemma S6 are chosen before the processes, the estimate, $d$ and the horizon.

The formalization cannot be satisfied trivially: expectations are integrals of nonnegative quantities, so no non-integrability default applies; the run predicates are satisfiable (a sorry-free check accompanies the drafts); LinUCB is a closed form whose maximality over the confidence ellipsoid is itself a milestone, not a real supremum; and the noise CDF is pinned by $\mathbb P(z_t \le c) = F(c)$.

A complete development needs the PLB analysis (Lemmas S3, S5, 3), which is reusable for any linear bandit with one-sparse actions, and the conditional Hoeffding step for Lemma 1, for which a platform theorem exists. Proofs of any milestone, and reusable lemmas on ridge estimates with diagonal designs, are welcome.

Selected references

• Y. Luo, W. W. Sun, Y. Liu, Distribution-Free Contextual Dynamic Pricing, Mathematics of Operations Research, 2024; arXiv:2109.07340v2. https://arxiv.org/abs/2109.07340 , https://doi.org/10.1287/moor.2023.1369
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (Lemma 19.4, Theorem 20.4). https://doi.org/10.1017/9781108571401
• Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS, 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• R. Kleinberg, T. Leighton, The Value of Knowing a Demand Curve: Bounds on Regret for Online Posted-Price Auctions, FOCS, 2003. https://doi.org/10.1109/SFCS.2003.1238232

Motivation

Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.

Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.

Setting

A bandit problem with $K$ arms is a family $\underline\nu=(\nu_a)_{a=1,\dots,K}$ of probability distributions on $\mathbb R$, each with a finite expectation. A strategy $\psi$ plays for $T$ rounds. In round $t+1$ it picks an arm $A_{t+1}$ as a measurable function of $I_t=(U_0,Y_1,U_1,\dots,Y_t,U_t)$, where the $U_t$ are independent uniforms on $[0,1]$. It then observes a reward $Y_{t+1}$ drawn from $\nu_{A_{t+1}}$ and a fresh independent uniform $U_{t+1}$. The strategy together with the problem determines the law $\mathbb P_{\underline\nu}$ of $I_T$; $\mathbb E_{\underline\nu}$ is its expectation. The number of draws of arm $a$ is

$$N_{\psi,a}(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}.$$

$\mathrm{KL}(P,Q)\in[0,+\infty]$ is the Kullback–Leibler divergence between two probability measures: $\int\ln\frac{\mathrm dP}{\mathrm dQ}\,\mathrm dP$ when $P$ is absolutely continuous with respect to $Q$ and the integral exists, and $+\infty$ otherwise. The binary divergence $\mathrm{kl}(p,q)$, for $p,q\in[0,1]$, is the Kullback–Leibler divergence between the Bernoulli distributions of parameters $p$ and $q$. For $q\in(0,1)$ it is given by (5):

$$\mathrm{kl}(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}.$$

It equals $+\infty$ for $q\in\{0,1\}$ and $p\ne q$.

The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on $I_t$; fullHistoryMeasure ν ψ T is the law of $I_T$, fullPullCount ψ a is $N_{\psi,a}(T)$, and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for $\mathrm{kl}(p,q)$.

Formalization targets

Goal: the fundamental inequality (6), p. 6

For every strategy $\psi$, every pair of bandit problems $\underline\nu,\underline\nu'$, every horizon $T$, and every $\sigma(I_T)$-measurable statistic $Z$ with values in $[0,1]$:

$$\sum_{a=1}^K\mathbb E_{\underline\nu}\big[N_{\psi,a}(T)\big]\,\mathrm{KL}(\nu_a,\nu'_a)\ \ge\ \mathrm{kl}\big(\mathbb E_{\underline\nu}[Z],\ \mathbb E_{\underline\nu'}[Z]\big),$$

in $[0,+\infty]$, with $0\cdot(+\infty)=0$. The arm laws have the finite expectations required in §1.1; their divergences may be infinite.

Milestones, in the order of the proof (§2.1, pp. 7–8)

1. (9), p. 7: the one-round chain rule. Under finite arm divergences, the divergence between the observed-history laws after round $t+1$ is the divergence after round $t$ plus $\mathbb E_{\underline\nu}\big[\sum_a\mathrm{KL}(\nu_a,\nu'_a)\,\mathbb I\{A_{t+1}=a\}\big]$. The observed-history kernel version is proved on the platform.
2. Equality in (8), p. 7: $\sum_a\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a,\nu'_a)=\mathrm{KL}(\mathbb P_{\underline\nu}^{I_T},\mathbb P_{\underline\nu'}^{I_T})$. The platform has the observed-history kernel version under finite arm divergences; relating it to the full information law is part of the goal's work.
3. Lemma 1, first display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)=\mathrm{KL}(\mathbb P_1\otimes\lambda,\mathbb P_2\otimes\lambda)$, with $\lambda$ the Lebesgue measure on $[0,1]$.
4. Lemma 1, second display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}\big((\mathbb P_1\otimes\lambda)(E),(\mathbb P_2\otimes\lambda)(E)\big)$ for every measurable $E\subseteq\Gamma\times[0,1]$.
5. Lemma 1, last display, p. 8: $(\mathbb P\otimes\lambda)\{(\gamma,x):x\le Z(\gamma)\}=\mathbb E[Z]$.
6. Lemma 1, p. 8: for probability measures $\mathbb P_1,\mathbb P_2$ on any measurable space and any measurable $Z$ with values in $[0,1]$, $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}(\mathbb E_1[Z],\mathbb E_2[Z])$.

Significance

The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem $\underline\nu'$ and a statistic $Z$, usually $Z=N_{\psi,a}(T)/T$. The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound $\liminf_T\mathbb E[N_{\psi,a}(T)]/\ln T\ge 1/\mathcal K_{\inf}$ for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while $T$ is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.

The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.

Difficulty

Two points need care. First, Lemma 1 is stated for an arbitrary $[0,1]$-valued $Z$. The data-processing inequality only gives it directly for indicators of events, and pushing $\mathbb P_j$ forward by $Z$ gives a law on $[0,1]$, not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When $\mathrm{KL}(\nu_a,\nu'_a)=+\infty$ for an arm that is drawn with positive probability, the left side is $+\infty$ and there is nothing to prove. When such an arm is never drawn, its term is $0\cdot(+\infty)=0$. The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.

Formalization scope

• Arms are Fin K, indexed from $0$. The horizon $T$ is a natural number; at $T=0$ both sides are $0$. For $K=0$ no policy exists, so $K\ge1$ needs no hypothesis.
• Strategies are FullStrategy K, measurable functions of the paper's $I_t$. The same strategy runs under $\underline\nu$ and $\underline\nu'$. The local history law includes every auxiliary uniform, so $Z$ may depend on any of them.
• Both bandit problems satisfy Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.
• The binary divergence is the $[0,+\infty]$-valued Kullback–Leibler divergence of two Bernoulli laws, klBer, never a real formula. A real formula would return a finite junk value at $q\in\{0,1\}$, where (5) is $+\infty$, and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to $q\in(0,1)$, would be a weaker theorem and is not the target.
• In Lemma 1 and its displays, the "distributions" are probability measures on an arbitrary measurable space. $\lambda$ is the volume on Mathlib's unitInterval. $Z$ is real-valued and measurable, with values in $[0,1]$.
• Builds on the published definitions StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019; arXiv:1602.07182v3. https://arxiv.org/abs/1602.07182v3, https://doi.org/10.1287/moor.2017.0928
• 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. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17, 1996. https://doi.org/10.1006/aama.1996.0007
• E. Kaufmann, O. Cappé, A. Garivier, On the complexity of best-arm identification in multi-armed bandit models, Journal of Machine Learning Research 17, 2016. https://jmlr.org/papers/v17/kaufman16a.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. 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 multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.

J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.

Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.

Setting

A bandit process $D$ is a Markov chain $x(0), x(1), \dots$ on a measurable state space $\Theta$ with transition kernel $P$. Applying the continuation control at process time $t$ earns the discounted reward $a^t R(x(t))$, with $0<a<1$, and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time $\tau$ of the chain (possibly infinite) write

$$R_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^tR(x(t))\,\Big|\,x(0)=x\Big\},\qquad W_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^t\,\Big|\,x(0)=x\Big\}.$$

The dynamic allocation index of $D$ in state $x$ is the largest reward per unit of discounted time obtainable by continuing for at least one step:

$$\nu(D,x)=\sup_{\tau>0}\nu_\tau(D,x),\qquad \nu_\tau(D,x)=\frac{R_\tau(D,x)}{W_\tau(D,x)}. \tag{2}$$

A simple family of alternative bandit processes consists of $k$ bandit processes. At each stage $n=0,1,2,\dots$ a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.

The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x ($\nu_\tau$), gittinsIndex P r α x ($\nu$), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first $n$ stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with $a$ written α and $R$ written r.

Formalization targets

Goal: the DAI Theorem (Section 3, p. 154)

For every policy $\pi$ and initial state vector $x$,

$$V_\pi(x)=\sup_{\pi'}V_{\pi'}(x)\iff \forall n,\ \text{a.s. under the play of }\pi\text{ from }x:\ \ \pi_n\Big(\big\{i:\nu(x_i(n))=\max_j\nu(x_j(n))\big\}\Big)=1 .$$

Milestones

1. Section 4, Lemma (p. 154). For $\Theta_0=\{y:\nu(D,y)<\nu(D,x)\}$ and $\tau$ the first $t\ge1$ with $x(t)\in\Theta_0$,

$$\nu_\tau(D,x)=\nu(D,x).$$

2. The "if" half of the DAI Theorem. A policy that selects a process of maximal index on every history is optimal: the published BanditAlgorithm.gittins_index_theorem, already Proved.
3. Section 4, Corollary 1 (p. 155). For the $M$-horizon index $\nu^M(D,x)=\sup_{0<\tau\le M}\nu_\tau(D,x)$ (5), the rule that stops at the first $t\in\{1,\dots,M-1\}$ with $\nu^{M-t}(D,x(t))<\nu^M(D,x)$, and at $M$ otherwise, attains $\nu^M(D,x)$.

Significance

The result. The DAI Theorem replaces a dynamic program on the product of $k$ state spaces by $k$ one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.

Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.

Difficulty

The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if $\{y:\nu(D,y)<\nu(D,x)\}$ is measurable; the arguments of the countable case, which treat each state separately, do not transfer.

Formalization scope

All objects are the published discounted $k$-armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from $0$, stopping times are $\mathbb N\cup\{\infty\}$-valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times $\tau\ge1$. The explicit readings committed to are:

• "Optimal" means attaining $\sup_{\pi'}V_{\pi'}(x)$ from the given initial state vector, over all randomized history-dependent policies; this supremum is finite because the values are bounded uniformly in the policy under the integrability hypothesis.
• "At each stage … almost always" means: for every stage $n$, almost surely under the law of the first $n$ stages of $\pi$ from $x$, the selection kernel puts mass one on the processes of maximal current index. Requiring the index rule on every history would make "only if" false.
• "The supremum of the total expected reward is finite" (p. 151) is read as $E_x\sum_t a^t|R(x(t))|<\infty$ for every state $x$.
• "$\nu(D,\cdot)$ is an $\mathcal X$-measurable function" (p. 151) is an explicit hypothesis of the Lemma and of the goal; the measurability of every $\nu^m(D,\cdot)$ is a hypothesis of Corollary 1.
• "The supremum is attained by setting $\Theta_0$" means that the first hitting time of $\Theta_0$ from time $1$ on is a positive stopping time whose ratio equals the index.
• The state space is standard Borel (the paper asks only for measurable singletons), and all processes share one kernel and one reward function; a family of different processes is encoded on the disjoint union of their state spaces.

A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time $1$, so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.

Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for $k$-armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.

Selected references

• J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• 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, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
• 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. N. Tsitsiklis, A short proof of the Gittins index theorem, Ann. Appl. Probab. 4(1), 194–199, 1994. https://doi.org/10.1214/aoap/1177005207
• 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 C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401