Probability

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem

$$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$

On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

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

$$Y_t = \langle X_t, \theta_* \rangle + \eta_t .$$

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

$$C_t = \Big\{\theta : \|\widehat\theta_t - \theta\|_{\overline V_t} \le R\sqrt{2\log\big(\det(\overline V_t)^{1/2}\det(\lambda I)^{-1/2}/\delta\big)} + \lambda^{1/2}S\Big\}.$$

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$,

$$\forall n \ge 0, \quad R_n \le 4\sqrt{nd\log(\lambda + nL^2/d)}\Big(\lambda^{1/2}S + R\sqrt{2\log(1/\delta) + d\log(1 + nL^2/(\lambda d))}\Big).$$

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$,

$$\|S_t\|^2_{\overline V_t^{-1}} \le 2R^2\log\big(\det(\overline V_t)^{1/2}\det(V)^{-1/2}/\delta\big).$$

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

Motivation

For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp $\tfrac12 n\log n$ location and window $n$, in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.

Setting

A family of chains is a sequence $P^{(n)}$ on state spaces $V_n$ with stationary distributions $\pi_n$; all single-chain quantities acquire an index $n$. As before, $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$, $d_n(t)=\max_x\|P^{(n)t}(x,\cdot)-\pi_n\|_{TV}$, $t^{(n)}_{\mathrm{mix}}(\varepsilon)=\min\{t:d_n(t)\le\varepsilon\}$, and $t^{(n)}_{\mathrm{mix}}=t^{(n)}_{\mathrm{mix}}(1/4)$. The family has a cutoff when for every $0<\varepsilon<1$

$$\frac{t^{(n)}_{\mathrm{mix}}(\varepsilon)}{t^{(n)}_{\mathrm{mix}}(1-\varepsilon)}\;\longrightarrow\;1\qquad(n\to\infty),$$

and a cutoff at $t_n$ with window $w_n$ when $w_n=o(t_n)$ and the distance at time $t_n+\alpha w_n$ tends (in the appropriate limsup/liminf sense) to $1$ as $\alpha\to-\infty$ and to $0$ as $\alpha\to+\infty$. The separation distance from $x$ is $s_x(t)=\max_y\bigl(1-P^t(x,y)/\pi(y)\bigr)$ (Mission III), $s(t)=\max_xs_x(t)$, and a separation cutoff is defined by the same window template with $s$ in place of $d$. From Mission VII, $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ is the relaxation time; from Mission VI, $t_{\mathrm{hit}}=\max_{x,y}\mathbb E_x(\tau_y)$ and $t_{\mathrm{cov}}$ are the maximal hitting and cover times, and the pairwise distance $\bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{TV}$ is from Mission II.

The concrete chains: the lazy biased walk on $\{0,\dots,n\}$ holds with probability $\tfrac12$ and otherwise steps up with probability $p>\tfrac12$, down with probability $1-p$ (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on $\{0,1\}^n$. The lamplighter chain $G^\ast$ over a graph $G$ has states (lamp configuration in $\{0,1\}^{V}$, lamplighter position in $V$); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on $G$, and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.

Formalization targets

Goal

Theorem 18.3: the lazy hypercube walk has a cutoff at $\tfrac12\,n\log n$ with window $n$ — the family's total variation distance undergoes its full collapse in a window of size $\Theta(n)$ around $\tfrac12 n\log n$.

Milestones

• Lemma 18.1 — cutoff is equivalent to the step-function limit: $d_n(\lfloor c\,t^{(n)}_{\mathrm{mix}}\rfloor)\to1$ for every $c<1$ and $\to0$ for every $c>1$.
• Theorem 18.2 — the lazy biased walk on $\{0,\dots,n\}$ with bias $\beta=p-\tfrac12>0$ has a cutoff at $\beta^{-1}n$ with window $\sqrt n$.
• Proposition 18.4 (the product condition) — for a reversible family with $t^{(n)}_{\mathrm{mix}}\to\infty$, if $t^{(n)}_{\mathrm{mix}}\le C\,t^{(n)}_{\mathrm{rel}}$ for a fixed constant $C$, the family has no cutoff: $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ is necessary.
• Theorem 18.8 — the lazy hypercube walk has a separation cutoff at $n\log n$ with window $n$ — at twice the total-variation cutoff time.
• Lemma 19.3 (Aldous–Diaconis) — the separation–total-variation relation $s(2t)\le1-\bigl(1-\bar d(t)\bigr)^2$ for reversible chains.
• Theorem 19.1 — for lamplighter chains over a growing family of connected graphs, $t_{\mathrm{rel}}(G_n^\ast)\asymp t_{\mathrm{hit}}(G_n)$: the relaxation time is comparable, with universal constants, to the maximal hitting time of the base walk.
• Theorem 19.2 — likewise $t_{\mathrm{mix}}(G_n^\ast)\asymp t_{\mathrm{cov}}(G_n)$: the lamplighter's mixing time is governed by the base walk's cover time.

Significance

The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the $\tfrac12 n\log n$ location with window $n$ is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.

Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.

Difficulty

The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ($\lambda_j=1-j/n$ with multiplicity $\binom nj$, via Mission VII's spectral representation) and the $\ell^2$ bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time $\tfrac12 n\log n+\alpha n$). Proposition 18.4 converts an eigenfunction with eigenvalue near $1$ into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over $n$, limits in the window parameter $\alpha$) exercises the filter library in earnest.

Formalization scope

Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over $n$ composed with limits in the real parameter $\alpha$ (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants $c_1,c_2$ and the threshold $N$ are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times $t$.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• D. Aldous, P. Diaconis, Shuffling cards and stopping times, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821
• P. Diaconis, The cutoff phenomenon in finite Markov chains, Proc. Natl. Acad. Sci. USA 93 (1996). https://doi.org/10.1073/pnas.93.4.1659
• Y. Peres, D. Revelle, Mixing times for random walks on finite lamplighter groups, Electron. J. Probab. 9 (2004). https://doi.org/10.1214/EJP.v9-198

Motivation

Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$; $\|\mu-\nu\|_{TV}=\max_{A}|\mu(A)-\nu(A)|$, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ as in the earlier missions; $\pi_{\min}=\min_x\pi(x)$. The chain is lazy when $P(x,x)\ge\tfrac12$ at every state.

A martingale adapted to the chain is a family $M_t$ of functions of the trajectory up to time $t$ such that the conditional expectation of $M_{t+1}$, given the trajectory so far, equals $M_t$ — for a finite chain, a pointwise finite-sum identity. A stopping time $\tau$ is a $\{0,1\}$-valued stopping rule in the sense of Mission III: whether to stop at time $t$ depends only on the trajectory up to $t$.

From Mission IV: the edge measure is $Q(x,y)=\pi(x)P(x,y)$, with $Q(S,y)=\sum_{x\in S}Q(x,y)$, and the bottleneck constant $\Phi_\star$ is the minimum over sets $S$ with $0<\pi(S)\le\tfrac12$ of $\Phi(S)=Q(S,S^c)/\pi(S)$. The evolving-set process is the Markov chain on subsets of $V$ in which, from the current set $S$, one draws $u$ uniform on $(0,1]$ and passes to the superlevel set

$$S'=\Bigl\{y\;:\;\frac{Q(S,y)}{\pi(y)}\ge u\Bigr\}$$

— states currently receiving a large share of the flow out of $S$ are likely to join, states receiving little are likely to leave.

Formalization targets

Goal

Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —

$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\frac{2}{\Phi_\star^{2}}\,\log\!\Bigl(\frac{1}{\varepsilon\,\pi_{\min}}\Bigr).$$

Milestones

• Corollary 17.7, the Optional Stopping Theorem — if $M$ is a martingale adapted to the chain, bounded uniformly by a constant, and $\tau$ is an almost surely finite stopping time, then $\mathbb E_x(M_\tau)=M_0(x)$: stopping a fair game at a fair time wins nothing.
• Lemma 17.12 — the evolving-set process, started from the singleton $\{x\}$, recovers the chain: $P^t(x,y)=\dfrac{\pi(y)}{\pi(x)}\,\mathbb P_{\{x\}}\{y\in S_t\}$.
• Lemma 17.13 — for the evolving-set process, the stationary mass $\pi(S_t)$ of the current set is a martingale.
• Theorem 17.17 — return probabilities of the lazy random walk on a graph of maximum degree $\Delta$: $\bigl|P^t(x,x)-\pi(x)\bigr|\le\sqrt2\,\Delta^{5/2}/\sqrt t$, an application of the evolving-set machinery.

Significance

The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound $t_{\mathrm{mix}}\lesssim\Phi_\star^{-2}\log(1/\pi_{\min})$ of Mission VII, but it needs no reversibility, and its proof technique — controlling the root $\sqrt{\pi(S_t)}$ as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.

Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.

Difficulty

The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series $\sum_t\mathbb P\{\tau=t\}\,M_t$ must be shown summable and equal to $M_0$ by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from $S$ to $T$ is the length of the set of $u\in(0,1]$ whose superlevel set is exactly $T$, which the formalization encodes by explicit upper and lower thresholds (a min over $T$ and a max over $T^c$ of the clipped ratios $Q(S,y)/\pi(y)$); establishing that these lengths sum to one over $T$, and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on $\sqrt{\pi(S_t)}$: laziness keeps the thresholds in $[\tfrac12,1]$, an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of $\mathbb E\sqrt{\pi(S_t)\bigl(1-\pi(S_t)\bigr)}$, and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.

Formalization scope

Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by $\prod P(\omega_i,\omega_{i+1})$, with expectations over the stopping time as tsums in $t$ (non-summable families sum to $0$; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to $1$). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume $\pi$ positive and $P$ lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with $\pi(x)=\deg(x)/2|E|$ written out. Real-valued bounds on the natural-valued $t_{\mathrm{mix}}$ are direct inequalities on the cast, with no hidden rounding.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• B. Morris, Y. Peres, Evolving sets, mixing and heat kernel bounds, Probab. Theory Related Fields 133 (2005). https://doi.org/10.1007/s00440-005-0434-7
• D. Williams, Probability with Martingales, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9780511813658

Motivation

The Ising model is statistical mechanics' fruit fly: spins $\pm1$ on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature $\beta$ — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small $\beta$) the dynamics mixes in $O(n\log n)$ steps on any bounded-degree graph; on the complete graph the same dynamics passes, as $\beta$ crosses an explicit threshold, from $O(n\log n)$ mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.

Setting

Spin configurations on a finite graph $G$ with vertex set of size $n$ and maximum degree $\Delta$ are functions $\sigma$ assigning $\pm1$ to each vertex (encoded over Booleans, $\mathrm{true}\mapsto+1$). The Ising model at inverse temperature $\beta>0$ is the Gibbs distribution

$$\pi(\sigma)\;=\;\frac{e^{\,\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)}}{Z(\beta)},$$

each edge counted once, $Z(\beta)$ the normalizing partition function. The Glauber dynamics for $\pi$ picks a uniform vertex and re-samples its spin from $\pi$ conditioned on all other spins — concretely, the new spin at $v$ is $+1$ with probability $\bigl(1+\tanh(\beta S)\bigr)/2$ where $S$ is the sum of the neighbouring spins.

The yardsticks are as in the earlier missions: $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance, $d(t)=\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}$, and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$. From Mission VII: an eigenvalue of a chain is a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$; $\lambda_2$ is the largest eigenvalue $\ne1$, the spectral gap is $\gamma=1-\lambda_2$, $\lambda_\star$ the largest $|\lambda|$ over eigenvalues $\ne1$, and the relaxation time is $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$.

Formalization targets

Goal

Theorem 15.1, the high-temperature fast-mixing theorem: if $\Delta\tanh\beta<1$ then the Glauber dynamics on any graph satisfies

$$t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{n\,\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\Delta\tanh\beta}\Bigr\rceil,$$

together with its refinement for graphs with all degrees even, where the condition relaxes to $(\Delta/2)\tanh(2\beta)<1$.

Milestones

• Lemma 15.2 (the tanh lemma) — the elementary inequalities about $x\mapsto\tanh(\beta(x+1))-\tanh(\beta(x-1))$ (symmetry, monotonicity, the bounds by $2\tanh\beta$ and, at odd integers, by $\tanh 2\beta$) that drive the one-site coupling contraction.
• Theorem 15.3 — the dynamical phase transition on the complete graph at $\beta=\alpha/n$: (i) for $\alpha<1$, $t_{\mathrm{mix}}(\varepsilon)\le n(\log n+\log(1/\varepsilon))/(1-\alpha)$; (ii) for $\alpha>1$, there are $r(\alpha),C>0$ with $t_{\mathrm{mix}}\ge C\,e^{r n}$ — split here into a fast half and a slow half.
• Theorem 15.4 — on the $n$-cycle, at every $\beta>0$, mixing is $n\log n$ up to explicit constants: $(1+o(1))\,\frac{n\log n}{2c_O(\beta)}\le t_{\mathrm{mix}}(\varepsilon)\le(1+o(1))\,\frac{n\log n}{c_O(\beta)}$ with $c_O(\beta)=1-\tanh(2\beta)$.
• Theorem 15.6 (Kenyon–Mossel–Peres) — on the rooted $b$-ary tree of depth $k$ with $n_k$ vertices, the relaxation time is polynomial at every temperature: $t_{\mathrm{rel}}\le n_k^{\,c_T(\beta,b)}$ with $c_T(\beta,b)=2\beta(3b+1)/\log b+1$.
• Proposition 15.7 — removing $r$ edges changes the spectral gap of the Glauber dynamics by at most a factor $e^{2\beta(\Delta+2r)}$.
• Theorem 15.9 — the block-dynamics comparison: if blocks $V_1,\dots,V_b$ cover the vertex set, each of size at most $M$, each vertex in at most $M_\star$ blocks, then the spectral gap $\gamma_B$ of the block dynamics and the gap $\gamma$ of the single-site dynamics satisfy $\gamma_B\le M^2M_\star\,(4e^{2\beta\Delta})^{M+1}\,\gamma$.

Significance

The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.

Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their $\tanh$ closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.

Difficulty

The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate $1-\bigl(1-\Delta\tanh\beta\bigr)/n$, and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space $\{\pm1\}^V$ has size $2^n$, so all "polynomial" bounds are polynomial in $n$, not in the size of the state space.

Formalization scope

The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the $\tanh$ closed form is a provable lemma, not a definition. Asymptotic statements ($o(1)$, "for sufficiently large $n$") are rendered with explicit $\exists N,\forall n\ge N$ quantifiers and a free precision parameter $\delta$; the phase-transition constants $r(\alpha),C$ are existentially quantified. The tree is encoded as words of length $\le k$ over an alphabet of size $b$; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• C. Kenyon, E. Mossel, Y. Peres, Glauber dynamics on trees and hyperbolic graphs, FOCS 2001. https://doi.org/10.1109/SFCS.2001.959934
• D. A. Levin, M. J. Luczak, Y. Peres, Glauber dynamics for the mean-field Ising model: cut-off, critical power law, and metastability, Probab. Theory Related Fields 146 (2010). https://doi.org/10.1007/s00440-008-0189-z
• F. Martinelli, Lectures on Glauber dynamics for discrete spin models, Lectures on Probability Theory and Statistics (Saint-Flour XXVII), Springer, 1999. https://doi.org/10.1007/978-3-540-48115-7_2

Motivation

How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the $L$-reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").

Setting

All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position $0$ on top. Random transpositions have increment distribution $\mu(\mathrm{id})=1/n$, $\mu(\text{transposition})=2/n^2$. The lazy adjacent-transposition walk puts mass $1/2$ on the identity and $1/[2(n-1)]$ on each $(i\ i{+}1)$. One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled $0$ to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The $L$-reversal chain on circular arrangements indexed by $\mathbb Z_n$ picks a position $i$ and a length $k<L$ uniformly and reverses the segment $[i,i+k]$.

Formalization targets

Goal

$$t_{\mathrm{mix}}\;\le\;(2+o(1))\,n\log n$$

for random transpositions on $n$ cards (Corollary 8.10), formalized as: for every $\delta>0$ there is $N$ with $t_{\mathrm{mix}}\le(2+\delta)n\log n$ for all $n\ge N$.

Milestones

Proposition 8.11 (random transpositions lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\frac{n-1}{2}\log\bigl(\frac{(1-\varepsilon)n}{6}\bigr)$, via fixed points); Proposition 8.13 (riffle shuffle: $t_{\mathrm{mix}}\le 2\log_2(4n/3)+1$); Proposition 8.14 (riffle shuffle: $t_{\mathrm{mix}}(\varepsilon)\ge(1-\delta)\log_2 n$ for large $n$, by the counting bound of Mission IV); the random adjacent transpositions upper bound $t_{\mathrm{mix}}(\varepsilon)\le 2n^3\log_2 n$ for large $n$ (§16.1.2, display (16.4)) and lower bound $t_{\mathrm{mix}}\ge n^2(n-1)/16$ (§16.1.3, by following a single card); and Proposition 16.2 (the $L$-reversal chain with $L<n/2$ satisfies $d\bigl((1-\varepsilon)\frac n2\log n\bigr)\to1$, via conserved adjacencies).

Significance

The results. Random transpositions at $\frac12 n \log n$ (the constant $2$ here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at $\frac32\log_2 n$ are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for $n=52$. The adjacent-transposition walk at order $n^3\log n$ is the basic example where geometry (diameter $\binom n2$) forces polynomial mixing. The $L$-reversal lower bound is the quantitative starting point of the biological application.

Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.

Difficulty

Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra $\log n$ factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after $t$ transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after $t$ inverse shuffles the deck is a uniform stable sort of $t$-bit labels, and mixing reduces to the birthday problem for $2^t$ labels; formalizing "distinct labels imply uniform order" is the crux. The $L$-reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.

Formalization scope

All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular $L$-reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements ($o(1)$, "for sufficiently large $n$") are spelled out with explicit $\forall\delta\,\exists N$ quantifiers; upper bounds carry a $+1$ where integer rounding requires it. The $L$-reversal family takes the length function $L(n)$ as a hypothesis-carrying parameter with $1\le L(n)<n/2$, and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to $1$).

Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• P. Diaconis, M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981). https://doi.org/10.1007/BF00535487
• D. Bayer, P. Diaconis, Trailing the dovetail shuffle to its lair, Ann. Appl. Probab. 2 (1992). https://doi.org/10.1214/aoap/1177005705
• R. Durrett, Shuffling chromosomes, J. Theoret. Probab. 16 (2003). https://doi.org/10.1023/A:1024940217006

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

$$T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}\ \inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\ \sum_{a=1}^K w_a\,d(\mu_a,\lambda_a),$$

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

$$\limsup_{\delta\to0}\frac{\mathbb E_{\boldsymbol\mu}[\tau_\delta]}{\log(1/\delta)}\le\alpha\,T^*(\boldsymbol\mu)$$

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):

$$T^*(\boldsymbol\mu)^{-1} = \sup_{w \in \Sigma_K}\ \inf_{\boldsymbol\lambda \in \mathrm{Alt}(\boldsymbol\mu)} \sum_{a=1}^K w_a\, d(\mu_a, \lambda_a).$$

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$,

$$\mathbb E_{\boldsymbol\mu}[\tau] \ \ge\ T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta, 1 - \delta).$$

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)$,

$$\sum_{a=1}^K d(\mu_a, \lambda_a)\, \mathbb E_{\boldsymbol\mu}[N_a(\tau)] \ \ge\ \mathrm{kl}(\delta, 1 - \delta).$$

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