Bandit Algorithms

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

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

Why bandit feedback matters

In online learning with bandit feedback, the learner chooses one action and sees only that action's loss. This is the information pattern of sequential trials in which testing one option does not reveal the outcomes of the others. The learner must keep its cumulative loss close to that of a good fixed action while learning which actions are good. A full-information method can update from every arm's loss each round; here the unseen losses have to be handled through the observations the learner actually receives. Chapter 9 of Orabona's text develops this distinction for multi-armed bandits.

Two environments are treated in the chapter. With an oblivious adversary, all losses are fixed before play, although the learner does not know them. With a stochastic environment, each arm has a fixed loss distribution and new losses are drawn across rounds. An algorithm with a guarantee in both environments does not need to be told which generated its data. Theorem 9.17 gives such a pair of guarantees for the FTRL version of Tsallis-INF, using the precise constants stated in the pinned version of the book.

Arms, losses, and the algorithm

There are $d$ arms and $T$ rounds, numbered $1,\ldots,T$. In round $t$, the learner forms a probability vector $x_t=(x_{t,1},\ldots,x_{t,d})$ on the simplex $\Delta^{d-1}$, draws an arm $A_t$ with probability $x_{t,i}$ of choosing $i$, and observes only $g_{t,A_t}$. The loss $g_{t,i}$ of an unchosen arm is not revealed. For an oblivious adversary, the entire table $(g_{t,i})$ is deterministic and the expectation is over the learner's draws.

Algorithm 9.6 uses the importance-weighted estimate $\widetilde g_{t,i}=g_{t,i}/x_{t,i}$ if $A_t=i$, and $0$ otherwise. Its Tsallis-INF FTRL prediction minimizes, over $x\in\Delta^{d-1}$,

$$\left\langle\sum_{s=1}^{t-1}\widetilde g_s,x\right\rangle -4L_\infty\sqrt t\sum_{i=1}^{d}\sqrt{x_i}.$$

The minimizer has positive coordinates. Thus each denominator $x_{t,i}$ used by the estimator is positive. In the stochastic environment, arm $i$ has mean $\mu_i$; if $j$ is a best arm, its gap is $\Delta_i=\mu_i-\mu_j$. The pull count $S_{T,i}$ is the number of rounds through $T$ in which arm $i$ is selected. Stochastic pseudo-regret compares the learner's expected loss with $T\mu_j$, the expected loss of always playing the best arm.

Formalization targets

The mission's main theorem is the adversarial claim of Theorem 9.17, p. 165. For every fixed comparator arm $k$ and losses in $[0,L_\infty]$,

$$\mathbb E\!\left[\sum_{t=1}^{T}(g_{t,A_t}-g_{t,k})\right] \le 32L_\infty\sqrt{(d-1)T}.$$

Taking $k$ to be the best arm in the fixed loss table yields the stated adversarial regret bound. The companion item formalizes the second claim of the same theorem: if the losses are stochastic with a unique best arm and $T\ge1$, then

$$\mathrm{P\!\operatorname{-}Regret}_T \le256L_\infty^2\sum_{i:\Delta_i\ne0}\frac{1+\ln T}{\Delta_i}.$$

The milestone list contains the chapter's pseudo-regret decomposition (Lemma 9.10), its sub-Gaussian sample-mean bound (Corollary 9.9, reused from an existing formal statement), and the probability-sensitive Tsallis-INF inequality (9.8). These are distinct mathematical claims rather than alternate names for the final bound.

What the result provides

The adversarial bound grows like $\sqrt{T}$ and remains valid for any fixed bounded loss table. The stochastic bound instead measures the difficulty of distinguishing arms through the positive gaps $\Delta_i$ and grows logarithmically with the horizon for fixed gaps. Both refer to the same FTRL update and the same importance-weighted estimator. The finite-horizon constants $32$ and $256$ are part of the target, not unspecified factors hidden in asymptotic notation.

Both claims are proved in the book. The work here is to give their hypotheses, random experiment, and algorithm a machine-checkable Lean interface, then formalize the known arguments. At this drafting stage the theorem bodies are open Lean problems; a successful build checks that their statements are well formed, not that the regret bounds have been proved. The resulting finite-history bandit protocol and stochastic pseudo-regret definitions can also support other loss-based bandit algorithms. The existing formalized sub-Gaussian tail bound can be reused for concentration results elsewhere in the chapter.

Where the proof is difficult

The learner observes only one coordinate, while regret is measured against losses across all arms. The importance-weighted estimate corrects the missing observations in expectation, but its size can grow when a selected arm has small probability. Consequently, a bound based only on a uniform estimate of its magnitude loses the probability dependence needed for the theorem's constants. The stochastic claim adds another difficulty: the learner's choices depend on past observed losses, so a current loss must be related to a random pull count without letting the choice depend on that current loss.

There are two tempting but invalid shortcuts. Permitting $x_t$ to inspect $g_t$ would change the bandit protocol, and taking an expectation under an arbitrary path measure would no longer describe the arm draws of Algorithm 9.6. The formal statements tie each prediction to its FTRL objective and each path probability to the predictions made along that history.

Formalization scope

Arms are Fin d; the main theorem permits $d=1$, where both its regret and bound are zero. Rounds retain the book's $1,\ldots,T$ indexing. A finite path has a dummy coordinate zero, fixed to an arbitrary anchor arm; this coordinate is never played or scored. The adversarial losses are a fixed table, selected before any draw. A path has probability equal to the product of the algorithm's conditional arm probabilities, and regret against a fixed arm is a finite weighted sum over paths. The FTRL run predicate requires simplex membership, strict positivity, minimization against every simplex point, and dependence only on past arm choices. The last two properties specify the intended update on every possible history.

The stochastic model first samples a loss table from a probability measure and then draws an arm path conditionally using the same Algorithm 9.6. Current-round loss vectors are independent across rounds, while coordinates within one round need not be independent. Each arm has the same mean in every round. The policy is a measurable function of the observed history (past arms and their losses); its expected loss is explicitly integrable. Loss bounds are imposed on every outcome in the chosen sample space, which can be taken as the support of bounded distributions. The stochastic statement adds $T\ge1$ to make the logarithmic formula's domain explicit, and the unique-best-arm assumption ensures every denominator $\Delta_i$ in the displayed sum is positive. Lemma 9.10 also spells out the integrability of its means and pull counts.

The development needs finite probability laws, real integrals, simplex geometry, and properties of the square-root regularizer. The independent tail bound for sample means is already available as a referenced theorem. Contributions that establish existence and interiority of the FTRL minimizer, the normalization of the path law, or the stated regret inequalities fit this scope. A choice rule that sees the current loss, a path law unrelated to $x_t$, or a zero integrability default does not satisfy the intended bandit model.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 9, pp. 151–169. arXiv

Motivation

Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a $d$-dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret $\tilde O(\sqrt{d^3H^3T})$, with no dependence on the number of states or actions (Theorem 3.1).

Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only $\zeta$-approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in $\zeta T$. This mission formalizes that result. A companion mission formalizes Theorem 3.1.

Setting

An episodic MDP has a measurable state space $\mathcal S$, a finite action set $\mathcal A$, a horizon $H$, and for each step $h\in[H]$ a transition kernel $\mathbb P_h(\cdot\mid x,a)$ and a reward $r_h:\mathcal S\times\mathcal A\to[0,1]$. A policy $\pi$ chooses an action $\pi(x,h)$ at state $x$ and step $h$. Its value functions satisfy the Bellman equation

$$Q^\pi_h(x,a)=r_h(x,a)+\int V^\pi_{h+1}\,\mathrm d\mathbb P_h(\cdot\mid x,a),\qquad V^\pi_h(x)=Q^\pi_h(x,\pi(x,h)),\qquad V^\pi_{H+1}=0,$$

and $V^\star_h(x)=\max_aQ^\star_h(x,a)$ is the optimal value, with $Q^\star$ defined by the same recursion.

A feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ with $\|\phi\|\le1$ makes the MDP $\zeta$-approximately linear (Assumption B) if for every step $h$ there are signed measures $\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ on $\mathcal S$ and a vector $\theta_h$ with

$$\big\|\mathbb P_h(\cdot\mid x,a)-\langle\phi(x,a),\mu_h(\cdot)\rangle\big\|_{\mathrm{TV}}\le\zeta,\qquad|r_h(x,a)-\langle\phi(x,a),\theta_h\rangle|\le\zeta$$

for all $(x,a)$, together with the normalization $\|\theta_h\|\le\sqrt d$ and a $\sqrt d$ bound on the masses of $\mu_h$. At $\zeta=0$ this is a linear MDP.

LSVI-UCB (Algorithm 1) plays $K$ episodes. In episode $k$, with data $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ from earlier episodes, it computes backwards from $Q^k_{H+1}\equiv0$

$$\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I,\qquad w^k_h=(\Lambda^k_h)^{-1}\sum_{\tau<k}\phi^\tau_h\big[r_h(x^\tau_h,a^\tau_h)+\max_aQ^k_{h+1}(x^\tau_{h+1},a)\big],$$ $$Q^k_h(x,a)=\min\big\{\langle w^k_h,\phi(x,a)\rangle+\beta_k\|\phi(x,a)\|_{(\Lambda^k_h)^{-1}},\,H\big\},$$

and then acts greedily, $a^k_h=\arg\max_aQ^k_h(x^k_h,a)$. An adversary may choose each initial state $x^k_1$. The regret after $K$ episodes is

$$\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],$$

where $\pi_k$ is the greedy policy of episode $k$. Throughout, $T=KH$ and $\iota=\log(2dT/p)$.

Formalization targets

Goal: Theorem 3.2

There are absolute constants $c,C>0$ such that for every $\zeta$-approximately linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta_k=c\,(d\sqrt\iota+\zeta\sqrt{kd})H$, with probability at least $1-p$,

$$\mathrm{Regret}(K)\le C\Big(\sqrt{d^3H^3T\iota^2}+\zeta dHT\sqrt\iota\Big).$$

The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.

Milestones

The milestones follow Appendix C: the approximate linearity of $Q^\pi$ (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).

Significance

Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order $\zeta dHT\sqrt\iota$, linear in $T$ because of the bias of linear approximation and negligible when $\zeta\lesssim1/\sqrt T$. The paper also converts it into a PAC guarantee with an additive $\tilde O(\zeta dH^2)$ error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.

The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At $\zeta=0$ the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.

Difficulty

The central difficulty is that the regression targets $r_h+V^k_{h+1}(x^\tau_{h+1})$ depend on the data through $V^k_{h+1}$, which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on $\beta_k$; that is why the constant $C$ must be independent of $c_\beta$ and $c_\beta$ is chosen afterwards. Under misspecification a second error appears: the deviations $r_h-\langle\phi,\theta_h\rangle$ and $(\mathbb P_h-\langle\phi,\mu_h\rangle)V$ are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the $\zeta\sqrt{kd}$ term in $\beta_k$. Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).

Formalization scope

• Indices are 1-based, as on the page; values and estimates are $0$ outside $1\le h\le H$.
• Values: $V^\pi$ and $V^\star$ are defined by the Bellman recursions (1) and (2), not by $\sup_\pi$.
• Measurability: the state space is a bare measurable space. Features $\phi(\cdot,a)$ are assumed measurable, and lemmas about a policy $\pi$ assume it measurable, so that every integral is meaningful.
• Actions: $\mathcal A$ is finite and nonempty. Argmax ties are broken towards the least action of a fixed linear order on $\mathcal A$.
• Interaction: the run is a process adapted to an arbitrary filtration, with actions given by Algorithm 1 and the next-state law holding conditionally on the past. The initial states are only required to be adapted.
• Probability statements: "with probability $1-p$" is "the bad set has (outer) measure at most $p$".
• Constants: $c$ and $C$ are quantified before all types, dimensions, horizons, $\zeta$, $p$ and runs. The hypotheses $d,H,K\ge1$ and $0\le\zeta\le1$ are stated.
• Assumption B measures the TV distance by the total variation norm $|\nu|(\mathcal S)$. The page's normalization $\|\mu_h(\mathcal S)\|\le\sqrt d$ is replaced by the same bound on the vector of total variations $(|\mu_h^{(i)}|(\mathcal S))_i$, because Lemma C.2 is false under the printed form; the replacement implies the printed condition and holds for tabular MDPs.
• Lemma C.7 carries the $+4H\zeta$ term that its own proof derives; the printed statement omits it. Theorem 3.2 is unaffected.

Lemmas C.3 and C.5 are formalized as printed. Their proofs use $\sup_x|V^k_{h+1}(x)|\le H$, which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.

A formalization in which the goal assumes the event $\mathfrak E$, the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.

Selected references

• C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
• 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
• L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019; arXiv:1902.04779. https://arxiv.org/abs/1902.04779

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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