Probability

Motivation

Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point $x$ does not change for any perturbation $\delta$ in a stated set, typically an $\ell_2$ ball $\|\delta\|_2<R$. Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.

Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.

Setting

Inputs live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$; classes form a set $\mathcal Y$. A base classifier is a map $f:\mathbb R^d\to\mathcal Y$ with Borel decision regions. For a noise level $\sigma>0$, write $\mathcal N(x,\sigma^2I)$ for the isotropic Gaussian law of $x+\varepsilon$ with $\varepsilon\sim\mathcal N(0,\sigma^2I)$. The class probability of $c$ at $x$ is $\mathbb P(f(x+\varepsilon)=c)$, and the smoothed classifier is

$$g(x)=\arg\max_{c\in\mathcal Y}\ \mathbb P(f(x+\varepsilon)=c).$$

Let $\Phi$ be the standard Gaussian CDF and $\Phi^{-1}$ its inverse on $(0,1)$. A classifier $f$ is consistent with the observed class probabilities (6) for a top class $c_A$ and numbers $\underline{p_A}\ge\overline{p_B}$ if

$$\mathbb P(f(x+\varepsilon)=c_A)\ \ge\ \underline{p_A}\ \ge\ \overline{p_B}\ \ge\ \max_{c\ne c_A}\mathbb P(f(x+\varepsilon)=c).$$

The certified radius is $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$. In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces $A=\{z:\delta^T(z-x)\le\sigma\|\delta\|\Phi^{-1}(\underline{p_A})\}$ and $B=\{z:\delta^T(z-x)\ge\sigma\|\delta\|\Phi^{-1}(1-\overline{p_B})\}$ of the paper's Appendix A are setA and setB.

Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.

Formalization targets

Goal: Theorem 2 (corrected)

Assume $0<\overline{p_B}\le\underline{p_A}<1$, $\underline{p_A}+\overline{p_B}\le1$, and that some finite set $s$ of classes other than $c_A$ satisfies $1\le\underline{p_A}+|s|\,\overline{p_B}$. Then for every $\delta$ with $\|\delta\|_2>R$ there is a base classifier $f^*$ consistent with (6) and a class $c\ne c_A$ with

$$\mathbb P(f^*(x+\delta+\varepsilon)=c_A)\ <\ \mathbb P(f^*(x+\delta+\varepsilon)=c),$$

so that $g(x+\delta)\ne c_A$ under any tie-breaking. The classifier may depend on $\delta$.

The class-capacity hypothesis is a correction. As printed, with only $\underline{p_A}+\overline{p_B}\le1$, the theorem fails for two classes: with $\mathcal Y=\{c_A,c_B\}$, $\underline{p_A}=0.6$, $\overline{p_B}=0.1$ and $\sigma=\|\delta\|_2=1$, one has $R\approx0.767<1$, yet every consistent $f$ gives $c_A$ probability at least $0.9$, and Theorem 1 then certifies radius $\Phi^{-1}(0.9)\approx1.28$.

Milestones

The milestones are the steps the paper itself states, in its order: the Claims $\mathbb P(X\in A)=\underline{p_A}$ and $\mathbb P(X\in B)=\overline{p_B}$ for $X\sim\mathcal N(x,\sigma^2I)$; the disjointness of $A$ and $B$ (corrected to "null" when $\underline{p_A}+\overline{p_B}=1$); equations (13) and (14) for $Y\sim\mathcal N(x+\delta,\sigma^2I)$,

$$\mathbb P(Y\in A)=\Phi\Big(\Phi^{-1}(\underline{p_A})-\tfrac{\|\delta\|}{\sigma}\Big),\qquad \mathbb P(Y\in B)=\Phi\Big(\Phi^{-1}(\overline{p_B})+\tfrac{\|\delta\|}{\sigma}\Big);$$

the equivalence $\mathbb P(Y\in A)<\mathbb P(Y\in B)\iff\|\delta\|_2>R$; and the existence of the worst-case classifier $f^*$ satisfying (6) with equalities.

Significance

Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about $f$, the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open $\ell_2$ ball of radius $R$. It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.

The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim $A\cap B=\emptyset$ fails at $\underline{p_A}+\overline{p_B}=1$. To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.

Difficulty

Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on $\mathbb R^d$ under a linear functional $z\mapsto\delta^T z$ is the one-dimensional Gaussian with variance $\|\delta\|^2$, and $\Phi$ is a continuous strictly increasing bijection $\mathbb R\to(0,1)$ with $\Phi^{-1}(1-p)=-\Phi^{-1}(p)$. The construction of $f^*$ has a further step the paper leaves informal: the region between $A$ and $B$, of mass $1-\underline{p_A}-\overline{p_B}$, must be shared among "other classes" with none exceeding $\overline{p_B}$, which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $\mathcal N(x,\sigma^2I)$ is the pushforward of Mathlib's stdGaussian under $z\mapsto x+\sigma z$, with $\sigma>0$ a binder. $\Phi$ is cdf (gaussianReal 0 1); $\Phi^{-1}(p)$ is the generalized inverse $\inf\{t:p\le\Phi(t)\}$, which is the true inverse on $(0,1)$ and the junk value $0$ at the endpoints, so every statement that evaluates it assumes $0<p<1$; at $\overline{p_B}=0$ or $\underline{p_A}=1$ the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of $c_A$ to be a strict unique argmax.

A formalization in which the junk endpoint value of $\Phi^{-1}$ makes $R$ negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.

Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on $(0,1)$. Contributions of general Mathlib-style lemmas (the law of $\delta^T X$ for $X\sim\mathcal N(x,\sigma^2I)$, properties of $\Phi^{-1}$) are welcome.

Selected references

• J. M. Cohen, E. Rosenfeld, J. Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML 2019; arXiv:1902.02918v2. https://arxiv.org/abs/1902.02918v2
• M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, S. Jana, Certified Robustness to Adversarial Examples with Differential Privacy, IEEE S&P 2019. https://arxiv.org/abs/1802.03471
• B. Li, C. Chen, W. Wang, L. Carin, Certified Adversarial Robustness with Additive Noise, NeurIPS 2019. https://arxiv.org/abs/1809.03113
• J. Neyman, E. S. Pearson, On the Problem of the Most Efficient Tests of Statistical Hypotheses, Phil. Trans. R. Soc. A 231, 1933. https://doi.org/10.1098/rsta.1933.0009

Motivation

A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.

Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.

Timeline:

• 1960s: Y. S. Chow (Ann. Math. Statist. 37, 1966) introduces a conditional exponential-moment condition close to Azuma's property [G] in a convergence theorem for independent variables.
• 1967: Azuma proves the moment bound (2.4) for conditionally sub-Gaussian martingale differences, a law of the iterated logarithm for direct weighted sums (Theorem 2), and the strong law for reversed weighted sums (Theorem 3), the subject of this mission.

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub-$\sigma$-fields of $\mathfrak A$. A sequence $(x_n)_{n\ge1}$ of real random variables is a sequence of martingale differences if, for every $n\ge1$, $x_n$ is $\mathfrak A_n$-measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely. Theorem 3 assumes moreover $|x_n|\le1$ almost surely for every $n$.

Let $(a_n)_{n\ge1}$ be positive increasing weights: $a_n>0$ and $a_n\le a_{n+1}$. Put

$$A_n = a_1+a_2+\dots+a_n,\qquad \bar S_n = a_nx_1 + a_{n-1}x_2+\dots+a_1x_n=\sum_{j=1}^n a_{n-j+1}x_j .$$

The sums $\bar S_n$ are the reversed weighted sums. In passing from $\bar S_n$ to $\bar S_{n+1}$ every existing term changes its weight, so $(\bar S_n)$ is in general not a martingale. In the Lean development, $A_n$ is A a n, $\bar S_n(\omega)$ is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.

Formalization targets

Goal: Theorem 3, (4.9)–(4.10)

If $(x_n)$ is a sequence of martingale differences with $|x_n|\le1$ a.s., $(a_n)$ is positive and nondecreasing, and

$$\frac{a_n}{A_n}=o\Big(\frac{1}{\log\log A_n}\Big)\qquad(n\to\infty),\tag{4.9}$$

then

$$\frac{\bar S_n}{A_n}\longrightarrow0\quad\text{almost surely}.\tag{4.10}$$

Milestones

The milestones follow the paper's proof, in attack order.

1. Remark 1 (p. 358): if $|x_n|\le K_n$ a.s., then $E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\cosh(tK_n)\le\exp(t^2K_n^2/2)$ a.s.
2. The tail step of (4.16) (p. 366): for $|x_n|\le1$, real $c_1,\dots,c_N$ with $\sum c_j^2>0$ and $\lambda\ge0$,

$$P\Big\{\sum_{j=1}^Nc_jx_j>\lambda\Big\}\le\exp\Big(-\frac{\lambda^2}{2\sum_{j=1}^Nc_j^2}\Big).$$

3. The blocks (4.11)–(4.14) (pp. 364–365): for every $\varepsilon>0$ there are indices $n_1<n_2<\cdots$ with $A_{n_1}>2(3+\varepsilon)/(6+\varepsilon)$, $a_n/A_n<\varepsilon/(6+\varepsilon)$ and $a_n\log\log A_n/A_n<\varepsilon^2/64$ for $n>n_1$, and $A_{n_{k-1}}<A_{n_k}\le(1+\varepsilon/3)A_{n_{k-1}}<A_{n_k+1}$.
4. The maximal inequality (4.15) (p. 365): if $A_{N_1}\le(1+\varepsilon/3)A_{N_0}$ with $1\le N_0<N_1$, then

$$2P\{\bar S_{N_1}>(\varepsilon/2)A_{N_0}\}\ge P\Big\{\max_{N_0<n\le N_1}\bar S_n>\varepsilon A_{N_0}\Big\}.$$

5. Block growth (p. 366): (4.11), (4.12) and (4.14) give $A_{n_k}>(2(3+\varepsilon)/(6+\varepsilon))^{k-1}$.

Significance

The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition $a_n^2/\sum_{j\le n}a_j^2\to0$ of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an $o(1/\log\log A_n)$ share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.

Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.

Difficulty

The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: $(\bar S_n)$ is not a martingale, because each new step reweights all earlier terms. The maximum of $\bar S_n$ over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants $\varepsilon/(6+\varepsilon)$, $\varepsilon^2/64$ and $1+\varepsilon/3$ have to be chosen to fit together.

Formalization scope

Conventions committed to in Lean:

• Indices start at $1$: sums run over Finset.Icc 1 n, and $a_0$, $x_0$ are never used. Every hypothesis on $a$ and $x$ is quantified over $n\ge1$.
• The filtration is a Mathlib Filtration ℕ. Its first $\sigma$-field plays the role of $\mathfrak A_0$ and is arbitrary rather than trivial; the paper's $\mathfrak A_0=\{\emptyset,\Omega\}$ is a special case, so the formal statements are at least as general.
• "Positive increasing" is read as $a_n>0$ and $a_n\le a_{n+1}$ (nondecreasing), the weaker hypothesis.
• (4.9) is stated literally as a little-$o$ relation (IsLittleO along atTop). $A_n\to\infty$ is not a hypothesis, since it follows from positivity and monotonicity.
• The conclusion is convergence of the real sequence $\bar S_n(\omega)/A_n$ to $0$ for almost every $\omega$, which contains both the upper and the lower tail; a statement giving only $\limsup\le0$ is not the goal. No real-valued limsup is used anywhere.
• Probabilities are real-valued (μ.real); conditional expectations are Mathlib's μ[f | ℱ n].

A formalization of the goal that replaces $\bar S_n$ by the direct sums $a_1x_1+\dots+a_nx_n$, drops the monotonicity of the weights, or strengthens (4.9) to $a_n/A_n=o(1/\log A_n)$ or to $a_n^2/\sum_{j\le n}a_j^2\to0$ states a different theorem and does not count.

A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. https://doi.org/10.2748/tmj/1178243286
• Y. S. Chow, Some convergence theorems for independent random variables, Annals of Mathematical Statistics 37 (1966), 1482–1493.
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

Motivation

Thompson Sampling is the oldest heuristic for the multi-armed bandit problem: proposed by Thompson in 1933, it plays each arm with the posterior probability that the arm is the best one. It is simple to implement, performs well empirically (Chapelle and Li, NIPS 2011), and has been used in production systems such as click-through-rate prediction for search advertising. For a long time, however, no finite-time regret guarantee was known for it: the analyses available before 2012 gave only $o(T)$ regret.

Agrawal and Goyal (arXiv:1111.1797, COLT 2012) gave the first logarithmic bounds on the expected regret of Thompson Sampling. This mission formalizes their bound for the general case of $N$ arms (their Theorem 2). A companion mission of the same series formalizes their two-armed bound (Theorem 1), whose proof is independent.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least of order $\sum_i \frac{\Delta_i}{D(\mu_i\|\mu_1)}\ln T$. Auer, Cesa-Bianchi and Fischer (2002) showed that UCB1 achieves $O(\sum_i \ln T/\Delta_i)$ in finite time. Agrawal and Goyal (2012) proved $O((\sum_a 1/\Delta_a^2)^2\ln T)$ for Thompson Sampling with $N$ arms; Kaufmann, Korda and Munos (2012) and Agrawal and Goyal (2013) later proved the asymptotically optimal constant for Bernoulli rewards.

Setting

A stochastic $N$-armed bandit has arms $1,\dots,N$. Arm $i$, when played, yields a random reward drawn from a fixed distribution $\nu_i$ supported in $[0,1]$, with mean $\mu_i$; rewards of an arm are i.i.d. and independent of the other arms. Arm $1$ is assumed to be the unique optimal arm, $\mu_1>\mu_i$ for $i\ne1$, and $\Delta_i=\mu_1-\mu_i>0$ is the gap of arm $i$.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a count $S_i$ of successes and $F_i$ of failures, both starting at $0$. In each round $t$ it draws $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$ independently for every arm, plays $i(t)=\arg\max_i\theta_i(t)$, observes a reward $\tilde r_t\sim\nu_{i(t)}$, performs a Bernoulli trial with success probability $\tilde r_t$, and increments $S_{i(t)}$ on success and $F_{i(t)}$ on failure.

The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu^*-\mu_{i(t)})\Big],\qquad \mu^*=\max_i\mu_i,$$

the expectation being over the rewards, the Bernoulli trials and the posterior samples.

The proof works with the reward stacks $Z_{i,m}$: the outcome of the $m$-th Bernoulli trial of arm $i$, all independent. Then $s(j)=\sum_{m\le j}Z_{1,m}$, the number of successes in the first $j$ plays of arm $1$, is a $\mathrm{Binomial}(j,\mu_1)$ random variable. The other objects of the proof are the threshold $L_i=24\ln T/\Delta_i^2$, the saturated set $C(t)$ of suboptimal arms with at least $L_i$ plays before round $t$, the intervals $I_j$ between the $j$-th and $(j+1)$-th plays of arm $1$, and the counts $\gamma_j$ and $V_j^{\ell,a}$ defined in §4.

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $N\ge2$, every instance as above and every horizon $T\ge2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\sum_{a=2}^N\frac{1}{\Delta_a^2}\Big)^2\ln T .$$

$C$ does not depend on $N$, on the reward distributions or on $T$.

Milestones

1. Lemma 4: with $E(t)$ the event that every saturated arm's sample lies within $\Delta_i/2$ of its mean, $\Pr(E(t))\ge1-4(N-1)/T^2$, also conditionally on $s(j)=s$.
2. Lemma 5 (Eq. (7)): the expected regret from saturated arms inside $I_j$ is at most $\mathbb E\big[\mathbb E[\gamma_j+1\mid s(j)]\sum_a\Delta_a\mathbb E[\min\{X(j,s(j),\mu_a+\Delta_a/2),T\}\mid s(j)]\big]$.
3. Lemma 1: $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$, where $X(j,s,y)$ counts the trials before an independent $\mathrm{Beta}(s+1,j-s+1)$ sample exceeds $y$.
4. Lemma 3: a three-case bound on $\mathbb E[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]]$ in terms of the Bernoulli KL divergence $D$ between $y$ and $\mu_1$.

Significance

The result. Theorem 2 shows that Thompson Sampling, a randomized Bayesian heuristic, achieves regret logarithmic in the horizon for any number of arms with bounded rewards, matching the order in $T$ of the Lai–Robbins lower bound. Its dependence on the gaps, $(\sum_a\Delta_a^{-2})^2$, is worse than UCB1's; the paper's own Remark 1 and later work improve it. The proof introduced the device of bounding the waiting time between plays of the optimal arm through geometric variables with Beta-cdf parameters (Lemmas 1 and 3), which reappears in later analyses of Thompson Sampling.

Formalizing it. The theorem is proved on paper; it has not been machine-checked. Bandit theory in Lean (bandit environments, regret, UCB-type analyses) is still young, and no Beta–Bernoulli Thompson Sampling result is formalized. The mission produces a Lean model of Algorithm 2 for general $[0,1]$ rewards with the paper's stack coupling, the §4 bookkeeping of saturated arms and intervals, and the paper's lemmas as separate targets.

Difficulty

Two difficulties are specific to the $N$-armed analysis. First, the arm that competes with arm $1$ changes over time: the set of saturated arms grows, and which saturated arm is "best" depends on the history, so the waiting time between plays of arm $1$ cannot be compared with a single geometric variable as in the two-armed case. Second, the number $\gamma_j$ of rounds at which arm $1$'s sample is large but arm $1$ is not played is not independent of the counts $V_j^{\ell,a}$: both depend on the same posterior samples, and Lemma 5 needs a careful conditioning on the history to separate them. The obvious union bound over arms, treating each suboptimal arm as in the two-armed proof, fails because it ignores the interruptions by unsaturated arms, whose number is the source of the squared sum in the bound.

Formalization scope

• Probability space. Algorithm 2 is realized on a product of three independent i.i.d. tables: Beta draws indexed by (arm, round, successes, failures), rewards indexed by (arm, round) and uniform variables indexed by (arm, round); the Bernoulli trial of a round succeeds when the played arm's uniform variable is below its reward. The law of the run is that of Algorithm 2, which runs for every round $t=1,2,\dots$. $s(j)$ is the number of successful trials among the first $j$ plays of arm $1$ in this infinite run (possibly after the horizon $T$), so it is a $\mathrm{Binomial}(j,\mu_1)$ random variable for every $j$, as the paper's independent $Z_{1,m}$ make it. Ties in the arg max (probability $0$) go to the smallest index.
• Indexing. Arms are Fin N, and Lean arm 0 is the paper's arm $1$. Rounds are $0,\dots,T-1$; Lean round $t$ is the paper's round $t+1$. Sums over $a=2,\dots,N$ are sums over $a\ne0$.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, which has no junk value for non-integrable functions. Conditional expectations given $s(j)$ are written as finite sums over the values of $s(j)$.
• The $O(\cdot)$. The paper writes $O(\cdot)$ in the sense of its footnote 1 ($f(n)\le c\,g(n)$ for $n\ge n_0$). The goal states it with one universal constant $C$, quantified before $N$, the instance and $T$, for every $T\ge2$. The explicit constants printed in App. D are not formalized: expanding the paper's Eq. (21) gives terms $288(N-1)(\ln T)\sum_a\Delta_a^{-2}$ and $48(N-1)^2$ where the paper prints $288(\ln T)\sum_i\Delta_i^{-2}$, and Eq. (22) drops a factor $\ln T$ in its $192/\Delta_a^2$ term. The $O(\cdot)$ claim does not depend on these slips; a statement pinned to the printed numerals might be false.
• Ruled out. A constant depending on $N$, on the means or on $T$; a fixed number of arms; Bernoulli rewards only; or any algorithm other than Algorithm 2 would each make the goal a different and weaker theorem. The statement quantifies over all $N\ge2$ and all reward distributions on $[0,1]$.
• Not included. Eq. (8), the bound $\sum_{j}\mathbb E[\gamma_j\mid s(j)]\le\sum_uL_u+4(N-1)$ "for all instantiations", is not a milestone: each term is conditioned on a different $s(j)$, and the pointwise reading does not follow from the argument given. Remark 1 (an alternate bound) and App. A (several optimal arms) are not part of this mission.
• Contributions welcome: Beta–Binomial identities, geometric waiting times, Hoeffding bounds for binomial cdfs, and the stopping-time arguments behind Lemma 5. Lemma 1 and Lemma 3 are shared with the two-armed mission of this series.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3, 2012. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.1093/biomet/25.3-4.285
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling
• E. Kaufmann, N. Korda and R. Munos, Thompson Sampling: an asymptotically optimal finite-time analysis, ALT 2012. https://arxiv.org/abs/1205.4217
• S. Agrawal and N. Goyal, Further optimal regret bounds for Thompson Sampling, AISTATS 2013. https://arxiv.org/abs/1209.3353

Motivation

Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row $n$ to be chosen anew makes an almost-sure statement about all large $n$ different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and $\log n$.

The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$. Let $x_1,x_2,\ldots$ be real measurable random variables. They form a bounded multiplicative system with unit bounds if $|x_k|\le1$ almost surely for every $k\ge1$, and

$$E\!\left[\prod_{k\in S}x_k\right]=0 \quad\text{for every nonempty finite }S\subseteq\{1,2,\ldots\}.$$

The indices in $S$ are distinct. Taking a singleton shows $E[x_k]=0$; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so $x_0$ is outside the mathematical sequence. Azuma, p. 357, property [M].

For each $n\ge1$, choose real coefficients $a_{n1},\ldots,a_{nn}$. There is no relation required between different rows. Define the weighted sum $T_n$ and its weight norm $B_n$ by

$$T_n=\sum_{k=1}^{n}a_{nk}x_k, \qquad B_n=\left(\sum_{k=1}^{n}a_{nk}^{2}\right)^{1/2}.$$

Both definitions use the source's 1-based indices. A row of zero weights has $B_n=0$ and $T_n=0$ almost surely; such rows remain within the theorem. Azuma, p. 359, §3.

Formalization targets

The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,

$$\limsup_{n\to\infty} \frac{|T_n|}{\sqrt{2B_n^2\log n}}\le1 \qquad P\text{-almost surely}.$$

The normalizing constant is exactly $2$, and the upper bound is exactly $1$. The mission does not assume that $B_n$ grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each $\delta>0$, almost every outcome eventually satisfies $|T_n|\le(1+\delta)\sqrt{2B_n^2\log n}$. This includes zero-weight rows without assigning a meaning to a real quotient $0/0$.

The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor $2$, and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real $b_1,\ldots,b_n$ and $t\in\mathbb R$,

$$E\exp\!\left(t\sum_{k=1}^{n}b_kx_k\right) \le \exp\!\left(\frac{t^2}{2}\sum_{k=1}^{n}b_k^2\right).$$

The paper prints (2.2) with a missing factor $b_{nk}$ in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when $b_{nk}=2$ and $x_k=t=1$. Azuma, pp. 357–360.

Significance

Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.

The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.

Difficulty

The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with $n$: bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with $B_n=0$ require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.

Formalization scope

The Lean development represents the probability law by a measure $\mu$ with IsProbabilityMeasure μ, and a random sequence by $x:\mathbb N\to\Omega\to\mathbb R$. It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type $\mathbb N\to\mathbb N\to\mathbb R$, and only entries with $1\le k\le n$ contribute.

The norm $B_n$ is the nonnegative real square root of the sum of squared weights. Real.log is zero at $n=0$ and $n=1$ in Lean, but the target is eventually quantified, so its asymptotic content concerns large $n$. The exponential estimate is stated for $n\ge1$. If $B_n=0$, Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.

The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.

Selected references

• Kazuo Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. DOI: 10.2748/tmj/1178243286.

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$, the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$, and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$. The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$, and write $d\theta$ for integration against $\nu$. A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$, and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$.

The algorithm outputs a density $g$ with respect to $\nu$: a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$. $F$ denotes the set of all densities. A density is scored by the averaged loss

$$\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),$$

the expected loss of a randomized predictor that draws $h_\theta$ from $g$. The relative entropy of $g$ to $g'$ is

$$K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],$$

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$, a parameter $\lambda > 0$, and a training set $S = (z_1, \dots, z_m)$. The algorithm returns a minimizer over $F$ of

$$R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).$$

For an index $i$, the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$, and $f^{\setminus i}$ denotes one of its minimizers over $F$.

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$,

$$|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.$$

Milestones

1. $M$-admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$.
2. Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$.
3. Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$-admissible loss,

$$d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.$$

4. Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$.
5. $L^1$ displacement bound (proof of Theorem 24):

$$\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.$$

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$. The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$, which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$. Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

• Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
• The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
• $K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
• The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
• Corrected reading of the algorithm on $S^{\setminus i}$. The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$, the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$.
• Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$, which is used.
• Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$, for $f_0, g' > 0$, finite $K(g, f_0)$, $K(g', f_0)$, and integrable $g \ln(g'/f_0)$.

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173

Motivation

A learning algorithm is judged by its generalization error: the expected loss of the hypothesis it outputs on a fresh example. That quantity depends on an unknown distribution, so it is estimated from the training data, by the empirical error (the average loss on the training set) or the leave-one-out error (the average loss on each training point of the hypothesis trained without it). Classical learning theory controls the gap between these estimates and the true error uniformly over a hypothesis class, through its VC dimension or covering numbers. Such bounds say nothing useful about algorithms that search very large or infinite-dimensional spaces, such as support vector machines and regularization networks in a reproducing kernel Hilbert space.

Bousquet and Elisseeff (JMLR 2 (2002) 499–526) replaced the capacity of the class by a property of the algorithm, its stability: how much its output changes when one training example is removed. Their exponential bound for uniformly stable algorithms is the starting point of the stability approach to generalization, which was later used for stochastic gradient descent (Hardt, Recht and Singer, 2016) and differential privacy, and sharpened by Feldman and Vondrák (2019) and Bousquet, Klochkov and Zhivotovskiy (2020).

Timeline. Rogers and Wagner (1978) and Devroye and Wagner (1979) bounded the leave-one-out error of local rules such as k-nearest neighbours through their stability. McDiarmid (1989) proved the bounded-differences inequality. Lugosi and Pawlak (1994) combined it with smoothed error estimates. Kearns and Ron (1999) named hypothesis and error stability and related them to the VC dimension. Bousquet and Elisseeff (2002) introduced uniform stability and proved the exponential bounds this mission formalizes.

Setting

Let $Z = X \times Y$ be a measurable space of labelled examples with an unknown probability distribution $D$. A training set $S = (z_1, \dots, z_m)$ is drawn from $D^m$. A learning algorithm $A$ maps a training set to a hypothesis $A_S : X \to Y'$. It is deterministic and symmetric: it depends on the training set only as a multiset, so it is a function Multiset (X × Y) → (X → Y'), defined for training sets of every size. For a cost $c$, the loss of a hypothesis $f$ at $z = (x, y)$ is $\ell(f, z) = c(f(x), y)$.

Given $S$, write $S^{\setminus i}$ for $S$ with its $i$-th example removed, and $S^i$ for $S$ with $z_i$ replaced by an independent draw $z_i' \sim D$. The three errors are

$$R = \mathbb E_{z \sim D}[\ell(A_S, z)], \qquad R_{\mathrm{emp}} = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}} = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).$$

An algorithm has uniform stability $\beta$ at sample size $m$ (Definition 6) if for every $S \in Z^m$, every $i$ and every $z \in Z$,

$$|\ell(A_S, z) - \ell(A_{S^{\setminus i}}, z)| \le \beta .$$

As a function of the sample size this constant is written $\beta_m$.

Formalization targets

Goal: Theorem 12

If $A$ has uniform stability $\beta$ and $0 \le \ell(A_S, z) \le M$ for all $z$ and all training sets $S$, then for every $m \ge 1$ and $\delta \in (0,1)$, each of the following holds, separately, with probability at least $1 - \delta$ over $S \sim D^m$:

$$R \le R_{\mathrm{emp}} + 2\beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}, \qquad (11)$$ $$R \le R_{\mathrm{loo}} + \beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}. \qquad (12)$$

Milestones

1. McDiarmid's inequality (Theorem 2): for measurable $F : Z^m \to \mathbb R$ with $|F(S) - F(S^i)| \le c_i$, $P_S[F - \mathbb E_S F \ge \epsilon] \le e^{-2\epsilon^2/\sum_i c_i^2}$.
2. Uniform stability $\beta$ implies $|\ell(A_S, z) - \ell(A_{S^i}, z)| \le 2\beta$ (p. 504).
3. Lemma 7: the bias identities for $\mathbb E_S[R - R_{\mathrm{emp}}]$, $\mathbb E_S[R(A,S^{\setminus i}) - R_{\mathrm{loo}}]$ and $\mathbb E_S[R - R_{\mathrm{loo}}]$.
4. $R - R_{\mathrm{emp}}$ and $R - R_{\mathrm{loo}}$ have bounded differences $c_i = 4\beta + M/m$.
5. $\mathbb E_S[R - R_{\mathrm{emp}}] \le 2\beta$ and $\mathbb E_S[R - R_{\mathrm{loo}}] \le \beta$.
6. The tail bounds $P_S[R - R_{\mathrm{emp}} > \epsilon + 2\beta] \le \exp(-2m\epsilon^2/(4m\beta+M)^2)$ and the leave-one-out analogue.

Significance

When $\beta = O(1/m)$ both bounds are $O(1/\sqrt m)$, with constants that do not depend on any capacity of the hypothesis space. Later sections of the paper show that Tikhonov regularization in a reproducing kernel Hilbert space has $\beta = O(1/(\lambda m))$, so the theorem gives generalization bounds for support vector regression, kernel ridge regression and, through a smoothed loss, soft-margin classification. The theorem is also the template for later stability bounds: the decomposition into a bias term controlled by stability and a deviation term controlled by a concentration inequality recurs throughout the literature.

The result has been proved since 2002, and replace-one variants appear in textbooks (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Theorem 14.2; Shalev-Shwartz and Ben-David, Chapter 13). On Prove2Me the replace-one textbook version is not formalized, and Mathlib at the platform's environment has no McDiarmid inequality. This mission asks for a machine-checked proof of the paper's remove-one version with its exact constants, and a reusable McDiarmid inequality with per-coordinate constants.

Difficulty

The deterministic steps (the bias identity and the bounded-differences estimates) are short on paper. The central difficulty is McDiarmid's inequality itself: it needs a martingale argument along the coordinates of a product measure, or an equivalent tensorization of conditional sub-Gaussian bounds, with the Doob martingale $\mathbb E[F \mid z_1, \dots, z_k]$ expressed through partial integration over Measure.pi. Hoeffding's inequality for sums, which Mathlib has, does not apply directly: $R - R_{\mathrm{emp}}$ is not a sum of independent terms. A second, bookkeeping difficulty is Lemma 7: the identities rest on exchanging $z_i$ with $z_i'$ and on the symmetry of $A$, which in Lean means measure-preserving coordinate permutations of $D^m \otimes D$ and multiset equalities such as $S^{i\,\setminus i} = S^{\setminus i}$.

Formalization scope

Conventions committed to by the Lean statements:

• An algorithm is a function of a multiset; this is how symmetry is encoded. Samples are Fin m → X × Y, and $S^i$ is Function.update.
• The law of $S$ is Measure.pi (fun _ => D) with D a probability measure; $z_i'$ and $z$ are independent draws, integrated against the product (Measure.pi fun _ => D).prod D.
• The paper's standing assumption that all functions are measurable is one hypothesis: $(S, z) \mapsto \ell(A_S, z)$ is measurable for every sample size. With the bound $0 \le \ell(A_T, z) \le M$ for training sets $T$ of every size, every expectation is a genuine integral, so no bound can hold because a non-integrable expectation defaults to $0$.
• Uniform stability quantifies over every sample, every index and every point, not almost every one.
• "With probability at least $1 - \delta$" means the $D^m$-measure of the failure set is at most $\delta$. The two bounds (11) and (12) are separate statements, joined by a conjunction; they are not claimed for one joint event.
• The paper assumes $\beta_m$ is non-increasing in $m$ and bounds $\beta_{m-1}$ by $\beta_m$ (p. 504). The leave-one-out bound (12) and its milestones carry the explicit hypothesis of uniform stability $\beta$ at size $m-1$; the empirical bound (11) does not.
• McDiarmid's inequality sums $c_i^2$ over $i = 1, \dots, m$; the paper's printed upper index $n$ is a slip.
• When a displayed tail bound has a zero denominator, its formal statement uses the limiting bound $0$. In McDiarmid's inequality this is the constant-function case; in the stability tails the loss is identically zero.

The stability notion is the paper's remove-one notion. A formalization with replace-one stability would prove a different theorem with different constants, and the published FoundationsML_Stability_UniformlyStable (replace-one) is therefore not used.

The development needs the published loss, empirical-error and generalization-error definitions from Foundations of Machine Learning, a McDiarmid inequality on product measures (reusable for any bounded-differences argument), and the coordinate-exchange lemmas for Measure.pi behind Lemma 7. Contributions of a general McDiarmid inequality, of exchangeability lemmas for product measures, and of proofs of any milestone are welcome.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989) 148–188. https://doi.org/10.1017/CBO9781107359949.008
• L. Devroye and T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Trans. Inform. Theory 25 (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087
• M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11 (1999) 1427–1453. https://doi.org/10.1162/089976699300016304
• M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240
• V. Feldman and J. Vondrák, High probability generalization bounds for uniformly stable algorithms with nearly optimal rate, COLT 2019. https://arxiv.org/abs/1902.10710
• O. Bousquet, Y. Klochkov and N. Zhivotovskiy, Sharper bounds for uniformly stable algorithms, COLT 2020. https://arxiv.org/abs/1910.07833
• M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$. The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$. These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$; the terminal value is $V_{H+1}^\pi=0$. The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$, the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$, observes transitions during the episode, and updates counts for the next episode. Its regret is

$$\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).$$

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$, and $N_k(x,a)=\sum_yN_k(x,a,y)$. When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$. Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$, and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$. The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$.

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$, write $L=\ln(5HSAT/\delta)$. The target is the exact bad-event form of the printed high-probability bound:

$$\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.$$

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$, $A$, and $H$. The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$. At $N'_{k,h+1}(y)=0$, Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$, while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$. For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

• M. G. Azar, I. Osband, and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Preprint.