Statistics

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

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.

Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.

Motivation

A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.

Setting

A random variable $X$ with mean $\mu=\mathbb E[X]$ is sub-Gaussian with parameter $\sigma$ (Definition 2.2) if $\mathbb E[e^{\lambda(X-\mu)}]\le e^{\sigma^2\lambda^2/2}$ for all $\lambda\in\mathbb R$; it is sub-exponential with parameters $(\nu,\alpha)$ (Definition 2.7, a strictly milder condition) if the same bound holds only for $|\lambda|<1/\alpha$, with the convention $1/0=+\infty$ so that $\alpha=0$ recovers the sub-Gaussian case exactly.

A sequence $\{D_k\}_{k\ge1}$, adapted to a filtration $\{\mathcal F_k\}$, is a martingale difference sequence if each $D_k$ is $\mathcal F_k$-measurable and $\mathbb E[D_k\mid\mathcal F_{k-1}]=0$. Such sequences arise throughout statistics via the Doob martingale construction: given a function $f$ of independent variables $X_1,\dots,X_n$, setting $D_k:=\mathbb E[f(X)\mid X_1,\dots,X_k]-\mathbb E[f(X)\mid X_1,\dots,X_{k-1}]$ telescopes to $f(X)-\mathbb E[f(X)]=\sum_k D_k$, converting a deviation question about $f(X)$ into a martingale concentration question.

A function $f:\mathbb R^n\to\mathbb R$ is $L$-Lipschitz with respect to the Euclidean norm if $|f(x)-f(y)|\le L\|x-y\|_2$ for all $x,y$ (Eq. (2.38)).

Formalization targets

Goal — Theorem 2.26 (Gaussian concentration of Lipschitz functions)

Let $(X_1,\dots,X_n)$ be i.i.d. standard Gaussian and $f$ be $L$-Lipschitz with respect to the Euclidean norm. Then $f(X)-\mathbb E[f(X)]$ is sub-Gaussian with parameter at most $L$, and hence

The bound is dimension-free: it depends on $n$ only through $f$'s Lipschitz constant, not the ambient dimension itself.

Milestone — Lemma 2.27 (Gaussian interpolation identity)

For any differentiable $f$ and convex $\varphi$, $\mathbb E[\varphi(f(X)-\mathbb E[f(X)])] \le \mathbb E[\varphi(\tfrac\pi2\langle\nabla f(X),Y\rangle)]$ for $X,Y\sim N(0,I_n)$ independent — the interpolation identity Theorem 2.26's proof is built on.

Milestone — Theorem 2.19 (martingale Bernstein bound)

Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound $\mathbb E[e^{\lambda D_k}\mid\mathcal F_{k-1}]\le e^{\lambda^2\nu_k^2/2}$ for $|\lambda|<1/\alpha_k$, the sum $\sum_k D_k$ is itself sub-exponential with parameters $\big(\sqrt{\sum_k\nu_k^2},\ \max_k\alpha_k\big)$, and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.

Significance

Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field — the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform (azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz concentration is separately significant: it is the tool behind dimension-free operator-norm bounds for random matrices, concentration of the empirical spectral distribution, and much of the machinery of Chapters 5 and 6 of the same book.

Formalizing it. No faithful prior art exists on the platform for either the martingale Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz concentration" returned no hits; the existing Vershynin-book item HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused from the platform's existing, already-proved formalizations.

Difficulty

The naive approach to Theorem 2.26 — try to bound $f(X)-\mathbb E[f(X)]$ directly via a Lipschitz-type argument in $\mathbb R^n$ — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an $\varepsilon$-net of the domain) picks up a factor that grows with $n$. The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity $f(X)-\mathbb E[f(X)]$ with the linear, and hence exactly computable, Gaussian quantity $\langle\nabla f(X),Y\rangle$, at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly $n$ times while keeping track of the interplay between the two parameters $\nu_k,\alpha_k$ per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.

Formalization scope

Expectations are Bochner integrals against an explicit probability measure, with integrability required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner integral silently returns $0$ for a non-integrable function, which this mission's definitions rule out as a trivializing formalization). The sub-exponential condition's domain restriction |λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention for the degenerate sub-Gaussian case.

"$X,Y\sim N(0,I_n)$ independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's HasGaussianLaw predicate together with explicit coordinatewise mean-zero and identity-covariance hypotheses, which together pin down the standard multivariate normal law, plus IndepFun. The inner product $\langle\nabla f(X),Y\rangle$ is realized as fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to $Y(\omega)$ — equal to $\langle\nabla f(X(\omega)),Y(\omega)\rangle$ by the Riesz representation of the gradient on a Hilbert space, avoiding the need to separately construct a gradient vector field.

Theorem 2.19's printed parameter pair for part (a), "$(\sum_k\nu_k^2,\alpha_*)$," is formalized as $(\sqrt{\sum_k\nu_k^2},\alpha_*)$: Definition 2.7 parametrizes the sub-exponential MGF bound by $\nu$ (with $\nu^2$ appearing in the exponent), so a literal transcription of the printed pair's first entry would silently square the effective parameter and make part (a), read literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full derivation.

Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 2.
• K. Azuma, "Weighted sums of certain dependent random variables," Tôhoku Mathematical Journal, 19:357–367, 1967.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association, 58:13–30, 1963.

Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

Motivation

Generalization bounds in statistical learning theory control the gap between the empirical and the true performance of a predictor chosen from a class $F$. Bartlett and Mendelson (JMLR 3, 2002) showed that this gap is governed by the Rademacher complexity of a loss class built from $F$, and that, unlike the VC dimension, this complexity can be estimated from data. Their bounds are useful only if the Rademacher complexity of a large class can be bounded in terms of simpler classes: voting methods take convex combinations of base classifiers, neural networks compose fixed squashing functions with linear combinations, and loss classes compose a class with a Lipschitz loss. Section 3.1 of the paper collects the elementary rules for such constructions in one statement, Theorem 12. These rules are used throughout the later literature on margin bounds, boosting, and neural-network generalization (e.g. Koltchinskii and Panchenko, Ann. Statist. 2002).

This mission formalizes those rules, as stated in the published journal article (J. Mach. Learn. Res. 3 (2002), pp. 463–482), Theorem 12 on p. 469.

Setting

Let $\mathcal X$ be a measurable space, $\mu$ a probability measure on it, and $n\ge0$ an integer. A class is a set $F$ of functions $f:\mathcal X\to\mathbb R$; no boundedness is assumed.

For a sample $x=(x_1,\dots,x_n)\in\mathcal X^n$, the empirical Rademacher complexity of $F$ (Definition 2, p. 464) is

the expectation over independent uniform random signs $\sigma_1,\dots,\sigma_n$. The Rademacher complexity is its expectation over an i.i.d. sample from $\mu$:

In the Lean development these are empiricalRademacher n F x and rademacherComplexity μ n F, both valued in $[0,\infty]$.

The constructions on classes are those of §2, p. 467: $\mathrm{conv}\,F$ is the class of convex combinations of functions from $F$; $-F=\{-f:f\in F\}$; $\mathrm{absconv}\,F$ is the class of convex combinations of functions from $F\cup-F$; $cF=\{cf:f\in F\}$; for $\phi:\mathbb R\to\mathbb R$, $\phi\circ F=\{\phi\circ f:f\in F\}$; and $\sum_{i=1}^kF_i=\{f_1+\dots+f_k:f_i\in F_i\}$.

Formalization targets

Goal: Theorem 12, parts 1–4 and 7 (p. 469)

For all classes $F,F_1,\dots,F_k,H$ of real functions:

The goal is the conjunction, each part quantified over its own classes.

Milestones

Parts 1, 3, 2 and 4 are milestones, in the order of the paper's proof. Part 7 remains a theorem item in the mission and a conjunct of the goal.

Significance

The result. Theorem 12 reduces the complexity of a constructed class to the complexities of its building blocks. Part 2 says that convex combinations come for free, which is why margin bounds for boosting depend only on the base class. Part 4 converts a complexity bound for a class into one for a Lipschitz loss composed with it, which is how the risk bounds of the paper's §2 are applied to concrete losses. Parts 1, 3 and 7 are the bookkeeping rules that combine the others; the paper uses parts 1 and 3 to show part 7 is tight.

Formalizing it. The results are proved, and part 4 is due to Ledoux and Talagrand (Probability in Banach Spaces, Springer 1991, Corollary 3.17). The platform already has a one-sided contraction lemma in a different normalization (UnderstandingML.contraction_lemma, Shalev-Shwartz and Ben-David's Lemma 26.9: per-coordinate Lipschitz maps, $1/m$ normalization, no absolute value, bounded nonempty sets of vectors), referenced here as supporting material, and a convex-hull identity for Mohri et al.'s empirical complexity without absolute value. None of the five parts is formalized for Definition 2's complexity (factor $2/n$, absolute value inside the supremum, expectation over the sample, arbitrary classes). The mission provides machine-checked versions in exactly that normalization, reusable by the other missions of this paper and by any later development of Rademacher-complexity bounds.

Difficulty

Parts 1, 2, 3 and 7 are pointwise statements about finite averages of suprema, but they have to be carried through the expectation over the sample and through suprema that may be infinite. Part 2 needs the supremum of the absolute value of a linear functional over a convex hull to equal its supremum over the set, including the symmetric hull $\mathrm{conv}(F\cup-F)$.

Part 4 is the substantial one. The natural first idea, comparing $|\sum_i\sigma_i\phi(f(x_i))|$ with $L_\phi|\sum_i\sigma_i f(x_i)|$ term by term for each sign vector, fails: the inequality holds only after averaging over the signs, and only with the factor $2$ caused by the absolute value. Without the hypothesis $\phi(0)=0$ the statement fails (a constant $\phi\equiv1$ has $L_\phi=0$ but $R_n(\phi\circ F)>0$ for nonempty $F$ and $n\ge1$), so any argument must use it.

Formalization scope

Representation. Classes are Set (X → ℝ). Signs are averaged over all $2^n$ vectors Fin n → Bool (encoded $\pm1$). Complexities take values in ℝ≥0∞: a class unbounded on the sample has complexity $+\infty$, the empty class has complexity $0$, and $R_n$ is the lower Lebesgue integral against Measure.pi (fun _ : Fin n => μ) with μ a probability measure. This is the paper's meaning for arbitrary classes. A real-valued formalization would not be: a real supremum over an unbounded set and a Bochner integral of a non-integrable function both evaluate to $0$. That would make the upper bounds false for unbounded classes and every comparison trivially satisfied for others. No boundedness hypothesis is added anywhere, since Theorem 12 is about arbitrary classes. $\mathrm{conv}\,F$ is convexHull ℝ F (finite convex combinations, no closure); $\mathrm{absconv}\,F$ is convexHull ℝ (F ∪ -F); $cF$ is c • F; $|c|$ enters as ENNReal.ofReal |c|, and $0\cdot\infty=0$ makes $c=0$ consistent. The Lipschitz map in part 4 is LipschitzWith Lφ φ on all of $\mathbb R$, as printed. The classes of part 7 are indexed by Fin k and summed pointwise. At $n=0$ all complexities are $0$ and every part holds trivially, matching the page.

Added hypothesis. Part 7 (and its conjunct in the goal) assumes that each sample function $x\mapsto\hat R_n(F_i)(x)$ is almost-everywhere measurable for $\mu^{\otimes n}$. The paper does not discuss measurability. The lower integral is monotone and positively homogeneous without it, so parts 1–4 need no such hypothesis, but it is not additive, and part 7 needs additivity. The hypothesis holds whenever each $F_i$ is a countable class of measurable functions.

Omitted parts. Parts 5 and 6 of Theorem 12 are not posed. Part 5, $R_n(F+h)\le R_n(F)+\|h\|_\infty/\sqrt n$, is false as printed: its proof (p. 470) bounds $\mathbf E\sup|\sum\sigma_i(f+h)(x_i)|$ correctly but drops the factor $2/n$ of Definition 2, and the correct conclusion is $R_n(F)+2\|h\|_\infty/\sqrt n$. For $F=\{0\}$, $h\equiv1$, $n=1$ the left side is $2$ and the printed right side is $1$. Part 6 is derived from part 5. A corrected part 5 would not be the paper's statement, so neither is included. The remark after the theorem that parts 1–3 hold for the Gaussian complexity, and the others with an extra $\ln n$ factor, is also not included.

Contributions welcome. Proofs of the milestones; a proof of part 4 from the platform's one-sided contraction lemma, converted to Definition 2's normalization; and general lemmas about empiricalRademacher (finiteness on finite classes, measurability for countable classes) that the other missions of this paper can reuse.

Selected references

• P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• V. Koltchinskii and D. Panchenko, Empirical margin distributions and bounding the generalization error of combined classifiers, Annals of Statistics 30 (2002), 1–50. https://doi.org/10.1214/aos/1015362183
• S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Lemma 26.9. https://doi.org/10.1017/CBO9781107298019

Motivation

A binary classifier is judged by its misclassification probability, the chance that it mislabels a fresh example. That probability is unknown; what a learner sees is the training error, the fraction of mistakes on the sample it was trained on. A generalization bound controls the gap between the two simultaneously for every classifier in a class, so that a classifier chosen by looking at the data still has a guaranteed error. The classical bounds of Vapnik and Chervonenkis measure the class by its VC dimension, a fixed combinatorial quantity that does not depend on the data distribution, and the paper recalls evidence that such fixed complexity penalties cannot be universally effective for model selection (p. 464).

Bartlett and Mendelson's paper in the Journal of Machine Learning Research (2002) studies two data-dependent alternatives, the Rademacher and Gaussian complexities, and proves risk bounds and structural rules for them. This mission formalizes the paper's classification bound, Theorem 5(b), which replaces the VC penalty by half the Rademacher complexity of the class. The source is the published JMLR article (jmlr.org/papers/v3/bartlett02a), pp. 463–482; all page numbers below are the journal's.

Timeline. Uniform convergence of empirical frequencies with a VC-dimension rate is due to Vapnik and Chervonenkis (1971). Rademacher penalties for model selection were introduced by Koltchinskii (2001) and by Bartlett, Boucheron and Lugosi (2002), who also proved Theorem 5(a) with the maximum discrepancy. The 2002 paper proves part (b) in Appendix B (p. 480) by adapting its proof of the general risk bound, Theorem 8 (p. 467).

Setting

Let $\mathcal X$ be a measurable space and $P$ a probability distribution on $\mathcal X \times \{\pm 1\}$; a pair $(X, Y) \sim P$ is an example $X$ with label $Y$. Let $F$ be a set of $\{\pm 1\}$-valued functions on $\mathcal X$ (the classifiers), and let $(X_i, Y_i)_{i=1}^n$ be an i.i.d. sample drawn from $P^n$.

• The misclassification probability of $f \in F$ is $P(Y \ne f(X))$.
• The training error of $f$ is $\hat P_n(Y \ne f(X)) = \frac1n \#\{i : Y_i \ne f(X_i)\}$, where $\hat P_n$ is the empirical measure of the sample (p. 463).
• Let $\sigma_1, \dots, \sigma_n$ be independent uniform $\{\pm 1\}$-valued random variables, independent of the sample. The empirical Rademacher complexity of a class $G$ of real functions on $\mathcal X$ at the points $x_1, \dots, x_n$ is

and the Rademacher complexity is $R_n(G) = \mathbb E\, \hat R_n(G)(X_1, \dots, X_n)$ with $X_1, \dots, X_n$ i.i.d. (Definition 2, p. 464). Note the factor $2/n$ and the absolute value.

• In Theorem 5, $R_n(F)$ is the Rademacher complexity of $F$ itself, viewed as a class of real functions with values $\pm1$, under the marginal of $P$ on $\mathcal X$.
• With the 0–1 loss $\mathcal L(Y, f(X)) = \mathbf 1(Y \ne f(X))$, the largest gap on a sample is $\Phi = \sup_{h \in \mathcal L \circ F}(\mathbb E h - \hat{\mathbb E}_n h) = \sup_{f\in F}\big(P(Y \ne f(X)) - \hat P_n(Y \ne f(X))\big)$.

Formalization targets

Goal: Theorem 5(b), p. 465

For every $0 < \delta < 1$, with probability at least $1 - \delta$ over the sample, every $f \in F$ satisfies

The bound is uniform: the probability that some $f$ violates it is at most $\delta$.

Milestones (Appendix B, p. 480)

1. Bounded differences. Replacing one example changes $\Phi$ by at most $1/n$.
2. McDiarmid step. With probability at least $1-\delta$, every $f \in F$ satisfies

3. Symmetrization. $\mathbb E\,\Phi \le R_n(F)/2$.

Supporting platform items, referenced and not restated: McDiarmid's inequality for i.i.d. samples (StabGen.Uniform.mcdiarmid_inequality, open) and the symmetrization lemma in the normalization of Shalev-Shwartz and Ben-David (UnderstandingML.representativeness_le_rademacher, proved).

Significance

The result. Theorem 5(b) is a distribution-dependent risk bound for classification whose complexity term can be estimated from a single sample. The paper shows (Theorem 6, p. 465) that it is never much worse than the VC bound, since the empirical Rademacher complexity of a $\{\pm1\}$ class is $O(\sqrt{d/n})$ in terms of its empirical VC dimension $d$, and it can be much better. It also serves as the template for margin bounds for large-margin classifiers, kernel machines and voting methods in Section 4 of the paper.

Formalizing it. The result is proved in the paper; no machine-checked proof is known to exist. A formal proof needs McDiarmid's inequality, a symmetrization argument with a ghost sample, and the reduction of the 0–1 loss class to the classifier class through the identity $\mathbf 1(Y \ne f(X)) = (1 - Y f(X))/2$. The milestones split these, so they can be proved independently. The symmetrization milestone also corrects a printed slip (see Formalization scope).

Difficulty

The bounded-difference step and the final union of the two halves are short. The difficulty is in the symmetrization. The supremum over an uncountable class is not automatically measurable, so the expectations in the paper's chain need not exist as written; a proof must work with exactly the random variables it integrates and use only the measurability it is given. The exchange of a sample point with its ghost copy, the conditioning on the sample, and the replacement of $\sigma_i Y_i$ by $\sigma_i$ must each be justified on finite sign averages and product measures. The obvious shortcut, bounding the gap by the Rademacher complexity of the loss class $\mathcal L \circ F$, does not give the stated term: with the absolute value of Definition 2, the loss class's complexity is not $R_n(F)/2$, because $(1 - Y_i f(X_i))/2$ contributes a sign sum that does not depend on $f$.

Formalization scope

Lean conventions:

• Labels $\{\pm1\}$ are the units $\mathbb Z^\times = \{1, -1\}$, coerced to $\mathbb R$; the real class of $F$ is $\{x \mapsto (f(x) : \mathbb R)\}$. Sample indices are $0, \dots, n-1$; the sample law is the product measure $P^n$.
• The Rademacher complexities take values in $[0, \infty]$: the sign expectation is the exact average over the $2^n$ sign vectors, and the sample expectation is a lower Lebesgue integral. An unbounded class therefore has complexity $+\infty$, not a junk $0$. The goal compares values in $[0,\infty]$ with ENNReal.ofReal on the real terms.
• "With probability at least $1-\delta$, every $f$ in $F$" is encoded as: the outer $P^n$-measure of $\{S : \exists f \in F,\ \text{the bound fails}\}$ is at most $\delta$.

Hypotheses added relative to the page, each necessary or a reading of the page:

• $n \ge 1$: at $n = 0$ Lean's $2/0 = 0$ makes $R_0(F) = 0$ and the bound false.
• $0 < \delta < 1$, as in Theorem 8 (p. 467).
• Every $f \in F$ is measurable, and three random variables are measurable: the gap supremum $\Phi$, the double-sample supremum $(S, S') \mapsto \sup_f(\hat P'_n - \hat P_n)(Y \ne f(X))$, and $x \mapsto \hat R_n(F)(x)$. The paper does not discuss measurability; these are exactly the variables the proof integrates, as in the proved platform item UnderstandingML.representativeness_le_rademacher. They hold, for instance, for countable classes.
• The two intermediate milestones assume $F$ nonempty, so that the real suprema in them are genuine.

Corrected slip: the chain on p. 480 ends "$= \mathbb E \sup_f \frac1n\sum_i\sigma_i f(X_i) = R_n(F)/2$". The last equality is only "$\le$": $R_n$ carries an absolute value, and for $F = \{f\}$ the left side of that step is $0$ while $R_n(F)/2 > 0$. The symmetrization milestone states the chain's conclusion with $\le$, which is all Theorem 5(b) needs.

Not a valid formalization: a version with a real-valued supremum or Bochner integral for $R_n$ (which would read $0$ on an unbounded or non-integrable class and make the bound false or free), one that drops the absolute value or uses the $1/n$ normalization, or one that measures $R_n$ of the loss class instead of $F$. Theorem 5(a) (maximum discrepancy, due to Bartlett, Boucheron and Lugosi) is not part of this mission.

Contributions welcome: proofs of the three milestones and the goal; the general McDiarmid inequality (the referenced open item); and reusable lemmas on measurable suprema of classifier families.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
• V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47(5) (2001) 1902–1914. https://doi.org/10.1109/18.930926
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16 (1971) 264–280. https://doi.org/10.1137/1116025

Motivation

A learning algorithm picks a predictor $f$ from a class $F$ after looking at $n$ training examples, and the quantity of interest is its expected loss on a fresh example. Since $f$ depends on the data, its training error is a biased estimate of that loss, and a risk bound quantifies the bias uniformly over the class: with high probability, every $f \in F$ has expected loss at most an observable sample average plus a complexity penalty. Classical penalties (VC dimension, covering numbers, fat-shattering dimension) are fixed in advance; data-dependent penalties such as the Rademacher complexity can be estimated from the sample itself and adapt to the distribution, which matters for model selection by complexity regularization.

Bartlett and Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002, jmlr.org), state such a bound in a general decision-theoretic setting (Theorem 8, p. 467): the loss is any $[0,1]$-valued function of an outcome and an action, and the sample average is taken of a dominating cost $\phi \ge \mathcal L$, which may be Lipschitz and hence amenable to the structural results of the paper's §3 even when $\mathcal L$ is a discontinuous $0$–$1$ loss. Multiclass classification with error-correcting output codes is the paper's example. The ingredients — McDiarmid's inequality (McDiarmid, 1989) and symmetrization — are standard; the paper combines them for this setting with a centred cost class. The source is the published JMLR article (pp. 463–482); all page numbers below are its printed pages.

Setting

Let $\mathcal X$ be an input space, $\mathcal Y$ an output space and $\mathcal A$ an action space with a distinguished action $0 \in \mathcal A$, each a measurable space. A probability measure $P$ on $\mathcal X \times \mathcal Y$ generates independent examples $(X_1, Y_1), \dots, (X_n, Y_n)$, and $(X, Y)$ is a fresh draw from $P$.

• A loss is $\mathcal L : \mathcal Y \times \mathcal A \to [0,1]$; a cost $\phi : \mathcal Y \times \mathcal A \to [0,1]$ dominates it if $\phi(y,a) \ge \mathcal L(y,a)$ for all $y, a$.
• $F$ is a class of maps $\mathcal X \to \mathcal A$; the expected loss of $f$ is $\mathbf E\mathcal L(Y, f(X)) = \int \mathcal L(y, f(x))\, dP(x,y)$.
• The empirical mean of $h : \mathcal X \times \mathcal Y \to \mathbb R$ is $\hat{\mathbf E}_n h = \frac1n\sum_{i=1}^n h(X_i, Y_i)$.
• The centred cost class is $\tilde\phi\circ F = \{(x,y) \mapsto \phi(y, f(x)) - \phi(y, 0) : f \in F\}$.
• For a class $G$ of real functions on a space $\mathcal Z$ and a sample $z_1, \dots, z_n$, the empirical Rademacher complexity is

with $\sigma_1, \dots, \sigma_n$ independent uniform signs, and the Rademacher complexity is $R_n(G) = \mathbf E\hat R_n(G)$, the expectation over an i.i.d. sample (Definition 2, p. 464). The factor is $2/n$ and the absolute value is inside the supremum.

In Lean these are RadGauss.RiskBound.empiricalRademacher, rademacherComplexity, empMean, supDev (the uniform deviation $\sup_{h \in G}(\mathbf Eh - \hat{\mathbf E}_nh)$), doubleSupDev and phiTildeComp.

Formalization targets

Goal: Theorem 8 (p. 467)

For every integer $n \ge 1$ and every $0 < \delta < 1$, with probability at least $1-\delta$ over the sample, every $f \in F$ satisfies

The event is uniform over $F$. The constant $\sqrt 8$ is the printed one.

Milestones (the steps of the paper's proof)

1. Theorem 9 (McDiarmid's inequality), p. 467: for independent, not necessarily identically distributed $X_i$ and $f$ with bounded differences $c_i$,

2. Bounded differences, p. 467: replacing one example changes $\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$ by at most $2/n$.
3. Concentration, p. 467: with probability at least $1 - \delta/2$,

4. Combined bound, p. 468: with probability at least $1-\delta$, for all $f \in F$,

5. Symmetrization, p. 468:

The platform's Proved UnderstandingML.representativeness_le_rademacher (Shalev-Shwartz and Ben-David, Lemma 26.2) is included as a supporting reference: it is the middle inequality of milestone 5 in the $1/n$, absolute-value-free normalization.

Significance

Theorem 8 bounds the expected loss of any predictor in the class, including one selected by the data, by quantities the learner can compute or estimate: the empirical cost and the Rademacher complexity of the centred cost class, which concentrates around its empirical version. Combined with the paper's structural results (§3: contraction by Lipschitz maps, convex hulls, sums), it yields margin bounds for voting methods, neural networks and kernel machines (§4) from complexities of simple base classes. Centring by $\phi(y,0)$ matters: with the absolute value inside the supremum, $R_n(\phi\circ F)$ can exceed $R_n(\tilde\phi\circ F)$ by order $1/\sqrt n$ even for a single function.

The result is proved in the paper. As far as the platform's catalog shows, it has no machine-checked proof in this normalization; McDiarmid's inequality in the non-identically distributed form, the $2/n$ bounded-difference step and the absolute-value Rademacher symmetrization with factor $2/n$ are not on the platform. A Lean proof would give a reusable risk-bound template for any loss dominated by a bounded cost.

Difficulty

The obvious argument — bound $\mathbf E\phi(Y,f(X)) - \hat{\mathbf E}_n\phi(Y,f(X))$ for a fixed $f$ by Hoeffding's inequality — does not survive the choice of $f$ after seeing the data: the deviation must be controlled uniformly over $F$, and $F$ is typically infinite. The supremum over $F$ is a single random variable, but its expectation is not obviously small, and relating it to the Rademacher complexity requires a ghost sample and a sign-swap symmetry of the product measure. In a formal development, the supremum of an uncountable family is not automatically measurable; the expectations the argument manipulates must be genuine, not lower integrals, which is why the statements carry explicit measurability hypotheses. McDiarmid's inequality itself, for independent but not identically distributed coordinates, is a martingale-difference concentration argument that is not in Mathlib in this form.

Formalization scope

• Sample and law. A sample is S : Fin n → X × Y, its law the product Measure.pi (fun _ => P). "With probability at least $1-\delta$, every $f \in F$ satisfies …" is encoded by bounding the (outer) measure of $\{S \mid \exists f \in F,\ \neg\,\text{bound}\}$ by $\delta$, with $0 < \delta < 1$.
• Complexities in $[0,\infty]$. $\hat R_n$ is an average over all $2^n$ sign vectors (Fin n → Bool, true $= +1$) of $[0,\infty]$-valued suprema; $R_n$ is its Lebesgue integral. The goal is stated in $[0,\infty]$, with the real terms embedded by ENNReal.ofReal (all are nonnegative). A real supremum or a Bochner integral would silently return $0$ on an unbounded class or a non-integrable integrand, making the bound trivially false or vacuous; this is ruled out by the choice of codomain.
• Added hypotheses, all implicit in the paper. $n \ge 1$ (at $n = 0$ Lean's $1/0 = 0$ makes the bound read $\mathbf E\mathcal L \le 0$, which is false); measurability of $\mathcal L$, $\phi$ and every $f \in F$; a distinguished action $0$ ([Zero A]).
• Measurability guard. The goal and milestones 3–5 assume measurability of exactly the random variables the proof integrates: the uniform deviation $S \mapsto \sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$, the empirical Rademacher complexity $S \mapsto \hat R_n(\tilde\phi\circ F)$, and the double-sample deviation $(S,S') \mapsto \sup_h(\frac1n\sum_i h(S'_i) - \hat{\mathbf E}_nh)$. These hold, for example, for countable $F$; the same guard is used by UnderstandingML.representativeness_le_rademacher.
• No printed slip was found in the statements formalized here. In Theorem 9, if every $c_i = 0$ the printed exponent has a zero denominator; Lean reads it as $0$ and the bound as $1$, which is true.
• Not formalized: the paper's Theorem 10 and the applications; this mission covers Definition 2 and §2 up to the end of the proof of Theorem 8.

Contributions welcome: a proof of McDiarmid's inequality for Measure.pi (reusable well beyond this mission), the ghost-sample symmetrization with the sign-swap invariance of $P^n \otimes P^n$, and the final assembly.

Selected references

• P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, London Math. Soc. Lecture Note Series 141, Cambridge University Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26. https://doi.org/10.1017/CBO9781107298019
• V. Koltchinskii and D. Panchenko, Empirical margin distributions and bounding the generalization error of combined classifiers, Annals of Statistics 30 (2002), 1–50. https://doi.org/10.1214/aos/1015362183

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