Bandit Algorithms

The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant $16/\Delta_i$ is eight times the information-theoretic limit, and its worst-case rate carries a spurious $\sqrt{\log n}$. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule $f(t) = 1 + t\log^2 t$ yields the asymptotically optimal $\limsup_{n\to\infty} R_n/\log n \le \sum_{i:\Delta_i>0} 2/\Delta_i$ — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index $\hat\mu_i + \sqrt{\tfrac{4}{T_i}\log^+\!\big(\tfrac{n}{k T_i}\big)}$ achieves minimax regret $R_n \le 39\sqrt{kn} + \sum_i \Delta_i$, matching the $\Omega(\sqrt{kn})$ lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.

A learner repeatedly chooses one of $k$ slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition $R_n = \sum_i \Delta_i\,\mathbb{E}[T_i(n)]$) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound $R_n \le 3\sum_i \Delta_i + \sum_{i:\Delta_i>0} 16\log(n)/\Delta_i$ — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion $R_n \le 8\sqrt{nk\log n} + 3\sum_i \Delta_i$.

The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves $\lim_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} 2/\Delta_i$, exactly asymptotically optimal, alongside the minimax-grade $R_n \le C\sqrt{kn\log n}$. Together they explain why posterior sampling is both principled and practically dominant.

Is the $d\sqrt{n}$ regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter $\theta$ with $\|\theta\|_2^2 = d^2/(48n)$ forcing $R_n \ge \frac{d\sqrt{n}}{16\sqrt{3}}$ — the goal theorem — and the hypercube gives the same $\Omega(d\sqrt{n})$ rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant $c(\mathcal{A},\theta)$ is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.

What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial $k$-armed bandit: rewards $x_{ti} \in [0,1]$ are an arbitrary fixed matrix, the learner samples $A_t \sim P_t$, and regret is measured against $\max_i \sum_t x_{ti}$. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates $\hat X_{ti} = 1 - \mathbb{1}\{A_t = i\}(1 - X_t)/P_{ti}$, achieves $R_n \le \sqrt{2nk\log k}$ — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first $n$ rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret $O(d\sqrt n\log^{3/2} n)$ with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension $d \ge 1$ and an unknown parameter $\theta_* \in \mathbb R^d$. In round $t = 1, 2, \dots$ the learner is given a nonempty decision set $D_t \subseteq \mathbb R^d$, chooses $X_t \in D_t$, and observes the reward

There is a filtration $\{F_t\}_{t \ge 0}$ such that $X_t$ is $F_{t-1}$-measurable and $\eta_t$ is $F_t$-measurable and conditionally $R$-sub-Gaussian: $\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)$ for all $\lambda \in \mathbb R$, with $R \ge 0$ fixed.

For a regularization parameter $\lambda > 0$ let $\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\top$ and let $\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_s$ be the regularized least-squares estimate. With $\|v\|_A = \sqrt{v^\top A v}$ and a known bound $\|\theta_*\|_2 \le S$, the confidence ellipsoid is

The OFUL algorithm chooses, in round $t$, a pair $(X_t, \widetilde\theta_t)$ maximizing $\langle x, \theta \rangle$ over $D_t \times C_{t-1}$. The pseudo-regret is $R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangle$, where $\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle$.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If $\|X_t\|_2 \le L$, $\langle x, \theta_*\rangle \in [-1,1]$ for all $x \in D_t$, and $\lambda \ge \max(1, L^2)$, then for every $\delta > 0$, with probability at least $1 - \delta$,

Milestone: Theorem 1, the self-normalized bound

For any positive definite $V$, $\overline V_t = V + \sum_{s\le t}X_sX_s^\top$ and $S_t = \sum_{s \le t}\eta_sX_s$: with probability at least $1-\delta$, for all $t \ge 0$,

Milestones: Theorem 2, the confidence ellipsoids

With probability at least $1 - \delta$, $\theta_* \in C_t$ for all $t \ge 0$ (first claim). If $\|X_t\|_2 \le L$, then with probability at least $1-\delta$, for all $t$, $\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S$ (second claim, stated here for $d \ge 2$).

Significance

Theorem 3 bounds the regret of OFUL by $O(d\sqrt n\log n)$ with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases $V = \lambda I$, $R = 1$, $\delta < 1$ of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence $X_t$ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix $\overline V_t$, which is itself built from the adaptively chosen actions; a bound for each fixed $t$ does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $\|x\|_A$ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed $t+1$ for $t : ℕ$, so sums over $s \le t$ are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy $R^2$) requires; this is an added hypothesis. Every "with probability at least $1-\delta$, for all $t$" is stated as an outer-measure bound $\le \delta$ on the failure event, with the time quantifier inside the event. $\det(\cdot)^{1/2}$ is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes $\langle x,\theta\rangle$ over $D_t \times C_{t-1}$, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward $\langle x^*_t, \theta_*\rangle$ is the supremum over $D_t$, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed $nL/d$ is replaced by $nL^2/d$, which is what the determinant–trace bound $\det\overline V_n \le (\lambda + nL^2/d)^d$ gives; for $L \le 1$ the corrected bound implies the printed one. The hypothesis $\lambda \ge \max(1, L^2)$ is added: for $\lambda < 1$ the printed logarithm can be negative, and the printed bound would then assert $R_n \le 0$. In the second claim of Theorem 2, $d \ge 2$ is added, because at $d = 1$ the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if $\theta_* \in C_{t-1}$ for all $t$ then $R_n \le \dots$". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same $\delta$ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on $\mathbb R^d$, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general $V$ and $R$, and reusable determinant lemmas are all welcome.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401

The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with $S$ states, $A$ actions and rewards in $[0,1]$. The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability $1-\delta$, $\hat R_n < C\,D(M)\,S\sqrt{An\log(nSA/\delta)}$, where $D(M)$ is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound $\mathbb{E}[\hat R_n] \ge C'\sqrt{DSAn}$ brackets the true complexity of tabular reinforcement learning up to $\sqrt{DS}$.

How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: $D(\mathbb{P}_{\nu\pi}, \mathbb{P}_{\nu'\pi}) = \sum_i \mathbb{E}[T_i(n)] D(P_i, P_i')$. Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound $R_n \ge \frac{1}{27}\sqrt{(k-1)n}$ over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers $\liminf_n R_n/\log n \ge \sum_{i:\Delta_i>0} \Delta_i / d_{\inf}(P_i, \mu^*, \mathcal{M}_i)$, certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk $\delta$. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity $\mathbb E_{\boldsymbol\mu}[\tau_\delta]$, the expected number of samples a strategy takes before stopping.

Timeline of the question this mission formalizes:

• Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
• Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every $\delta$-PAC strategy (arXiv:1407.4443).
• Garivier and Kaufmann (COLT 2016) identified the exact constant $T^*(\boldsymbol\mu)$ in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as $\delta\to0$ (arXiv:1602.04589). This mission covers the upper-bound half of that paper.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$; $b$ is twice differentiable and strictly convex, and $\nu_\theta$ has mean $\dot b(\theta)$. Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence $d(\mu,\mu')$ is the Kullback–Leibler divergence between the members with means $\mu$ and $\mu'$.

A bandit model $\boldsymbol\mu=(\mu_1,\dots,\mu_K)$ assigns a member of the family to each arm. The class $\mathcal S$ consists of models with a unique optimal arm $a^*(\boldsymbol\mu)$. At each round $t=1,2,\dots$ the learner picks an arm $A_t$ as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time $\tau_\delta$ recommends an arm. $N_a(t)$ is the number of draws of arm $a$ in the first $t$ rounds and $\hat\mu_a(t)$ its empirical mean.

With $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S: a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ and $\Sigma_K$ the probability simplex, the characteristic time is

and the maximizer $w^*(\boldsymbol\mu)$ are the optimal proportions of arm draws.

Track-and-Stop combines two ingredients:

• a sampling rule that tracks the plug-in proportions $w^*(\hat{\boldsymbol\mu}(t))$ while forcing each arm to be drawn about $\sqrt t$ times: C-Tracking tracks the cumulated sum of projections of $w^*(\hat{\boldsymbol\mu}(s))$ onto $\Sigma^{\epsilon_s}_K=\{w\in\Sigma_K: w_a\ge\epsilon_s\}$, $\epsilon_s=(K^2+s)^{-1/2}/2$; D-Tracking draws an under-sampled arm when some $N_a(t)<\sqrt t-K/2$, and otherwise the arm maximizing $t\,w^*_a(\hat{\boldsymbol\mu}(t))-N_a(t)$;
• Chernoff's stopping rule, which stops at the first $t$ at which some arm $a$ beats every other arm $b$ in a generalized likelihood ratio test, $Z_{a,b}(t)>\beta(t,\delta)$, here with $\beta(t,\delta)=\log(r(t)/\delta)$.

Formalization targets

Goal: Theorem 14 (p. 13)

For $\alpha\in[1,e/2]$ and $r(t)=O(t^\alpha)$, Chernoff's stopping rule with $\beta(t,\delta)=\log(r(t)/\delta)$ combined with C-Tracking or D-Tracking satisfies

for every $\boldsymbol\mu\in\mathcal S$.

Milestones

• Lemma 15 (p. 20): greedy tracking of cumulated proportions $P(k)$ keeps $\max_i|N_i(n)-P_i(n)|\le K-1$.
• Lemma 7 (p. 7): C-Tracking ensures $N_a(t)\ge\sqrt{t+K^2}-2K$ and $\max_a|N_a(t)-\sum_{s<t}w^*_a(\hat{\boldsymbol\mu}(s))|\le K(1+\sqrt t)$.
• Lemma 8 (p. 7): D-Tracking ensures $N_a(t)\ge(\sqrt t-K/2)_+-1$, and proportions within $3(K-1)\epsilon$ of $w^*(\boldsymbol\mu)$ after a time $t_\epsilon$ that does not depend on the trajectory, once the plug-in targets are within $\epsilon$.
• Proposition 9 (p. 8): under either rule, $N_a(t)/t\to w^*_a(\boldsymbol\mu)$ almost surely.
• Lemma 18 (p. 27): an explicit $x$ with $c_1x\ge\log(c_2x^\alpha)$ for $\alpha\in[1,e/2]$.
• Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to $w^*$, $\tau_\delta<\infty$ almost surely and $\limsup_{\delta\to0}\tau_\delta/\log(1/\delta)\le\alpha T^*(\boldsymbol\mu)$ almost surely.

Significance

Theorem 1 of the same paper shows $\mathbb E_{\boldsymbol\mu}[\tau_\delta]\ge T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ for every $\delta$-PAC strategy, and $\mathrm{kl}(\delta,1-\delta)\sim\log(1/\delta)$. Theorem 14 with $\alpha=1$ therefore shows that the lower bound is attained: $T^*(\boldsymbol\mu)$ is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.

The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.

Difficulty

The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of $\tau_\delta/\log(1/\delta)$ does not control $\mathbb E[\tau_\delta]$, because on the rare events where the empirical means are far from $\boldsymbol\mu$ the stopping time may be very large. Theorem 14 needs a quantitative concentration of $\hat{\boldsymbol\mu}(t)$ on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the $\sqrt t$ lower bounds on $N_a(t)$ (the concentration step of App. D, Lemmas 19–20).

A second obstacle is the regularity of $w^*$: the tracking lemmas only transfer convergence of $\hat{\boldsymbol\mu}(t)$ to convergence of $N_a(t)/t$ through the continuity of $\boldsymbol\mu\mapsto w^*(\boldsymbol\mu)$ on $\mathcal S$, proved from the characterization of $w^*$ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near $\boldsymbol\mu$, which requires the empirical means to lie in the interior of the mean space.

Formalization scope

• Model. The exponential family is a structure $(\xi,\Theta,b)$ with $\Theta$ a nonempty open interval, each $\nu_\theta$ normalized, $b$ twice continuously differentiable and $\ddot b>0$ on $\Theta$. Openness and $\ddot b>0$ are added to the paper's "convex, twice differentiable"; strict convexity is what makes $\nu^\mu$ unique. Bandit models are parameter vectors $\theta\in\Theta^K$ with $K\ge2$; arms are indexed $0,\dots,K-1$. $\mathcal S$ is the set of parameter vectors with a unique arm of largest mean $\dot b(\theta_a)$.
• Protocol. Policies, the trajectory law $\mathbb P_{\boldsymbol\mu}$, pull counts, empirical means and $T^*(\boldsymbol\mu)$ are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). $T^*$ uses Kullback–Leibler divergences of the arm laws over the class $\mathcal S$ and takes values in $[0,\infty]$. Trajectory coordinate $t$ is round $t+1$. An arm never drawn has empirical mean $0$.
• Target map. $w^*(\hat{\boldsymbol\mu}(t))$ is undefined in the paper when $\hat{\boldsymbol\mu}(t)\notin\mathcal S$ (an unsampled arm, ties, a mean outside $\dot b(\Theta)$). Every tracking statement quantifies over every target map with values in $\Sigma_K$ that returns optimal proportions on $\mathcal S$, over every choice of $L^\infty$ projections, and over every tie-breaking, including randomized ones.
• Stopping rule. The two maxima in $Z_{a,b}(t)$ are suprema over $\Theta$ in the extended reals. $Z_{a,b}(t)>\beta$ is written without subtracting infinities. The stopping time is the first $t\ge1$ at which the test succeeds, $+\infty$ if none. "$r(t)=O(t^\alpha)$" is $r(t)\le Dt^\alpha$ for $t\ge1$; $r>0$ is added so that $\log(r(t)/\delta)$ is defined.
• Values in $[0,\infty]$. Expectations of $\tau_\delta$, the ratios and $T^*$ live in $[0,\infty]$. No statement converts them to reals, so an infinite expected stopping time is never read as $0$.
• Corrections, disclosed. Proposition 9's printed $\mathbb P_w$ is $\mathbb P_{\boldsymbol\mu}$. Lemma 18 adds $c_2/c_1^\alpha>1$ and $x>0$, without which its expressions are undefined.
• Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
• Welcome contributions. Exponential-family facts ($\dot b$ is the mean, the KL formula, concentration of empirical means); the continuity of $w^*$ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
• H. Chernoff, Sequential Design of Experiments, Ann. Math. Statist. 30(3), 1959. doi:10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 33. doi:10.1017/9781108571401

Motivation

Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces $K$ unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed $\delta$. The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.

Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant $T^*(\boldsymbol\mu)$ is exactly matched, as $\delta \to 0$, by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).

Setting

A canonical one-parameter exponential family is given by a reference measure $\xi$ on $\mathbb R$, an open interval $\Theta \subset \mathbb R$ and a function $b$, twice continuously differentiable on $\Theta$ with $\ddot b > 0$, such that the laws $\nu_\theta$ with density $\exp(\theta x - b(\theta))$ with respect to $\xi$ are probability measures for $\theta \in \Theta$. The mean of $\nu_\theta$ is $\dot b(\theta)$. Bernoulli laws and Gaussian laws of known variance are examples.

A bandit model is a vector $\theta = (\theta_1, \dots, \theta_K) \in \Theta^K$; arm $a$ returns i.i.d. rewards with law $\nu_{\theta_a}$ and mean $\mu_a = \dot b(\theta_a)$. Arm $a^*(\boldsymbol\mu)$ is the unique optimal arm if $\mu_{a^*} > \mu_a$ for every $a \ne a^*$. Let $\mathcal S$ be any set of bandit models of the family each having a unique optimal arm, and put $\mathrm{Alt}(\boldsymbol\mu) = \{\boldsymbol\lambda \in \mathcal S : a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)\}$.

A strategy consists of a sampling rule $\pi$ (the arm $A_t$ drawn at round $t$ depends, possibly with extra randomization, on the first $t - 1$ observations), a stopping time $\tau$ of the natural filtration $\mathcal F_t = \sigma(A_1, X_1, \dots, A_t, X_t)$, and an $\mathcal F_\tau$-measurable decision $\hat a_\tau$. It is $\delta$-PAC on $\mathcal S$ if for every $\boldsymbol\mu \in \mathcal S$, $\mathbb P_{\boldsymbol\mu}(\tau < \infty) = 1$ and $\mathbb P_{\boldsymbol\mu}(\hat a_\tau \ne a^*(\boldsymbol\mu)) \le \delta$. $N_a(t)$ is the number of draws of arm $a$ among the first $t$ rounds.

Write $d(\mu_a, \lambda_a) = \mathrm{KL}(\nu_{\theta_a}, \nu_{\lambda_a})$ for the divergence between two arm laws, $\mathrm{kl}(x, y) = x\log\frac{x}{y} + (1 - x)\log\frac{1 - x}{1 - y}$, and $\Sigma_K$ for the probability simplex on the $K$ arms. The characteristic time is defined by eq. (1):

Formalization targets

Goal: Theorem 1 (p. 3)

For $\delta \in (0, 1/2]$, every $\delta$-PAC strategy on $\mathcal S$ and every $\boldsymbol\mu \in \mathcal S$,

The statement fixes no constant beyond those of the paper, and it holds for every $\delta$, not only in the limit.

Milestone: eq. (2) (p. 4)

For every $\boldsymbol\lambda \in \mathcal S$ with $a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)$,

This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.

Significance

Theorem 1 identifies $T^*(\boldsymbol\mu)$ as the exact problem-dependent complexity of fixed-confidence best arm identification: since $\mathrm{kl}(\delta, 1 - \delta) \sim \log(1/\delta)$, it gives $\liminf_{\delta \to 0} \mathbb E_{\boldsymbol\mu}[\tau_\delta]/\log(1/\delta) \ge T^*(\boldsymbol\mu)$, and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer $w^*(\boldsymbol\mu)$ of eq. (1) (mission II).

Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant $\log(1/(4\delta))$; for $\delta \le 1/2$, $\mathrm{kl}(\delta, 1 - \delta) \ge \log(1/(2.4\delta)) > \log(1/(4\delta))$, so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.

Difficulty

The obvious proof applies the finite-horizon divergence decomposition $\mathrm{KL}(\mathbb P^n_{\boldsymbol\mu}, \mathbb P^n_{\boldsymbol\lambda}) = \sum_a \mathbb E_{\boldsymbol\mu}[N_a(n)]\,d(\mu_a, \lambda_a)$ at a deterministic horizon $n$. That fails here: $\tau$ is random and unbounded, the decision is $\mathcal F_\tau$-measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into $\mathrm{kl}(\delta, 1 - \delta)$, is the central difficulty. A second, smaller difficulty is to identify the paper's divergence $d$ and its means $\dot b(\theta)$ with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.

Formalization scope

Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); $\mathrm{kl}$ is the platform's bernoulliRelativeEntropy and $N_a(t)$ is trajPullCount. Conventions:

• arms are Fin K, 0-based (the paper's arm $a$ is index $a - 1$); trajectory coordinate $t$ is round $t + 1$;
• $\Theta$ is a nonempty open interval and $\ddot b > 0$ on $\Theta$ (added: the paper says $b$ is convex and twice differentiable; strict convexity is what makes "the unique distribution with mean $\mu$" meaningful); the paper's $d$ is written as the KL divergence of the arm laws (its first equality on p. 3), and the unique optimal arm is defined through the parameter means $\dot b(\theta_a)$;
• $\mathcal S$ is an arbitrary set of models with a unique optimal arm, not the specific set the paper fixes from p. 4 on;
• $\delta$-PAC keeps both halves of the paper's definition (almost-sure stopping and error at most $\delta$);
• $T^*(\boldsymbol\mu)$, divergences and expectations of $\tau$ take values in $[0, \infty]$, never truncated to reals; $T^* = 0$ when $\mathrm{Alt}(\boldsymbol\mu) = \emptyset$ and $T^* = \infty$ when the supremum in eq. (1) is $0$;
• $\delta \le 1/2$ is added. The paper states $\delta \in (0, 1)$, but the theorem and eq. (2) are false for $\delta \in (1/2, 1)$: with two unit-variance Gaussian arms, drawing arm 1 once and naming arm 1 exactly when the fractional part of the reward is below $1/2$ is $0.9$-PAC, while $T^*(\boldsymbol\mu) \to \infty$ as the two means merge. At $\delta = 1/2$ the bound is $0$.

A statement with $\log(1/(4\delta))$ in place of $\mathrm{kl}(\delta, 1 - \delta)$, or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates $\mathbb E[\tau]$ or $T^*$ to real numbers.

Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an $\mathcal F_\tau$-measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of $\nu_\theta$ $= \dot b(\theta)$" and "KL of two family members $= b(\theta') - b(\theta) - \dot b(\theta)(\theta' - \theta)$", and $\mathbb E[\tau] = \sum_a \mathbb E[N_a(\tau)]$. All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, Journal of Machine Learning Research 17(1), 2016. https://arxiv.org/abs/1407.4443
• T. L. Graves, T. L. Lai, Asymptotically Efficient Adaptive Choice of Control Laws in Controlled Markov Chains, SIAM Journal on Control and Optimization 35(3), 1997. https://doi.org/10.1137/S0363012994275440
• S. Mannor, J. N. Tsitsiklis, The Sample Complexity of Exploration in the Multi-Armed Bandit Problem, Journal of Machine Learning Research 5, 2004. https://www.jmlr.org/papers/v5/mannor04b.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

Motivation

The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of $d$ actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.

The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time $t$ (or with a horizon $n$ fixed in advance), and its guarantee is on the expected regret, which grows like $\log n$. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.

Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the $d$-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB($\delta$), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least $1-\delta$. This mission formalizes that section.

Setting

There are $d \ge 1$ arms with unknown means $\mu_1, \dots, \mu_d \in \mathbb R$. Write $\mu_* = \max_{1 \le i \le d} \mu_i$ for the best mean and $\Delta_i = \mu_* - \mu_i \ge 0$ for the gap of arm $i$.

Randomness lives on a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_t)_{t \ge 0}$. In round $t = 1, 2, \dots$ the learner plays an arm $I_t$ that is $\mathcal F_{t-1}$-measurable and receives the reward $\mu_{I_t} + \eta_t$. The noise $\eta_t$ is $\mathcal F_t$-measurable and conditionally 1-sub-Gaussian:

The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.

After $t$ rounds, $N_{i,t}$ is the number of plays of arm $i$ and $\overline X_{i,t}$ is the average reward received from it. For a confidence level $\delta > 0$ the confidence width is

with $c_{i,t} = +\infty$ when $N_{i,t} = 0$. UCB($\delta$) plays, in round $t$, an arm that maximizes $\overline X_{i,t-1} + c_{i,t-1}$; in particular every arm is played once before any comparison is made. The pseudo-regret after $n$ rounds is

This is the linear bandit of the paper with the standard basis of $\mathbb R^d$ as decision set and $\theta_* = \mu$.

Formalization targets

Goal: Theorem 7 (constant regret of UCB($\delta$))

For every $\delta > 0$, with probability at least $1-\delta$, for all $n \ge 0$ simultaneously,

The right-hand side depends only on the gaps, $d$ and $\delta$.

Milestone: Lemma 6 (confidence intervals)

For any adapted choice of arms (not only UCB($\delta$)) and every $\delta > 0$, with probability at least $1-\delta$,

Significance

The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability $1-\delta$ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability $\delta$ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.

Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for $V = \lambda I$ and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.

Difficulty

Two points separate this from textbook UCB analyses. First, the number of samples $N_{i,t}$ of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of $t$: a union bound over all $t$ costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale $\sum_s \eta_s \mathbf 1\{I_s = i\}$. Second, the regret statement is uniform in $n$ with constants depending on the gaps; converting a condition of the form "$c(N) \ge \Delta_i/2$" into an explicit bound on $N$ requires solving an inequality in which $N$ appears both polynomially and inside a logarithm, and the explicit constants $3$ and $16$ must come out of that step.

Formalization scope

The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.

• Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, $\mu_*$ is ⨆ i, μ i (the maximum over a nonempty finite type).
• Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index $0$ are unused.
• The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
• "With probability at least $1-\delta$, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most $\delta$. For $\delta \ge 1$ the statements are trivially true, as in the paper.
• The rule (4) is read with the statistics of rounds $1, \dots, t-1$, because the printed $\overline X_{i,t}$, $c_{i,t}$ already count round $t$. An unplayed arm, whose width is $+\infty$ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
• The printed Theorem 7 has no quantifier on $n$; it is formalized in the uniform-in-$n$ form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
• Lean's division by zero makes $\overline X_{i,t}$ and $c_{i,t}$ equal to $0$ when $N_{i,t} = 0$. Lemma 6 therefore excludes $N_{i,t} = 0$ explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with $\Delta_i > 0$, so its divisions are well defined.

A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.

Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case ($d = 1$, $\lambda = 1$, $A_s = \mathbf 1\{I_s = i\}$, $\overline V_t = 1 + N_{i,t}$), a union bound over arms, and elementary inequalities inverting $N \mapsto \frac{1+N}{N^2}(1 + 2\log(d\sqrt{1+N}/\delta))$. Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• 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
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation tradeoff using variance estimates in multi-armed bandits, Theoretical Computer Science 410, 2009. https://doi.org/10.1016/j.tcs.2009.01.016

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit $\gamma \downarrow 0$; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are $n$ jobs with service times $s_i > 0$ and weights $c_i$, and $m$ identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time $C_i$ of a job is the total service time of the jobs on its machine up to and including it; the flow time is $\sum_i C_i$ and the weighted flow time $\sum_i c_i C_i$. The load of a machine is the total service time assigned to it, and $\delta_j$ is its excess over the average $S/m$. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of $n$ boxes, in box $i$ with probability $p_i$. A search of box $i$ costs $c_i$ and finds the object with probability $q_i$ if it is there. A search policy is a sequence of boxes; after $N_i$ unsuccessful searches of box $i$ the posterior probability that the object is there is proportional to $p_i(1-q_i)^{N_i}$, and the search index of the box is $p'_i q_i/c_i$, the current probability of finding the object per unit cost. The expected cost of a policy is $\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]$.

Two discount factors. Bandit process $A$ (state space $S_A$, kernel $P_A$, reward $r_A$) discounts at rate $a$ and $B$ at rate $b$; a reward obtained at time $t$ is worth $a^t$ or $b^t$ times its face value according to which process produced it. The cross indices are $\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]$ and $\nu_{BA}(y)$ with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as $\mathbb{E}\int_0^\tau b^t\,dt$ and compares $\nu_{AB}(x)$ with $\nu_{BA}(y)$ at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union $S_A \oplus S_B$.

Formalization targets

Goal: Theorem 3.6

For prior probabilities $p_i \ge 0$ summing to one, detection probabilities $0 < q_i \le 1$ and costs $c_i > 0$, a search policy is optimal if and only if at every step it searches a box of maximal current index $p'_i q_i / c_i$:

Milestones

Theorem 3.3, as the identity $\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)$ when $c_i = \kappa s_i$; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time $t$, $A$ when $a^t \nu_{AB}(x) > b^t \nu_{BA}(y)$ and $B$ when $a^t \nu_{AB}(x) < b^t \nu_{BA}(y)$ attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on $m$ machines and that the optimal schedules are exactly those placing the $r$-th block of $m$ longest jobs at level $r$ from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time $t$ weighs the indices by $a^t$ and $b^t$, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying $0.18$ ($a = 0.9$) and $1$ ($b = 0.5$) are best played $B, B, B$ and then $A$ forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as $\sum_i \ell_i s_i$ with $\ell_i$ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in $[0, \infty]$ of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, $p_i(1-q_i)^{N_i} q_i/c_i$, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an $A$-state by $P_A$ and a $B$-state by $P_B$; the payoff is the round-by-round series $\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])$, absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: $m \ge 1$, service times positive; $p_i \ge 0$, $\sum p_i = 1$, $0 < q_i \le 1$, $c_i > 0$; countable state spaces, bounded rewards, $a, b \in (0,1)$.

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by $a^t$, $b^t$. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
• D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
• J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
• K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
• P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.