Statistics

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Motivation

The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative $i$ with probability proportional to $e^{z_i\theta}$, where $z_i$ is a vector of observed attributes and $\theta$ an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate $\theta$ by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.

Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.

Setting

Observations are indexed serially, $m = 0, 1, 2, \dots$, as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation $m$ offers $J_m \ge 1$ alternatives, and alternative $i$ carries a vector $z_{im} \in \mathbb R^K$ of independent variables. For a parameter $\theta \in \mathbb R^K$ the selection probabilities are

$$P_{im}(\theta) = \frac{e^{z_{im}\theta}}{\sum_{j=1}^{J_m} e^{z_{jm}\theta}}, \qquad \bar z_m(\theta) = \sum_{i} P_{im}(\theta)\, z_{im}.$$

The data are generated at a true parameter $\theta^0$: the chosen alternatives $Y_0, Y_1, \dots$ are independent random variables with $\Pr(Y_m = i) = P_{im}(\theta^0)$. The log-likelihood of the first $q$ observations is $L^q(\theta) = \sum_{m<q}\log P_{Y_m m}(\theta)$. The moment matrix of observation $m$ is

$$\Omega_m = \sum_{i} P_{im}(\theta^0)\,(z_{im}-\bar z_m)(z_{im}-\bar z_m)', \qquad \bar z_m = \bar z_m(\theta^0).$$

Axiom 7 asks that $J_m \le J_*$ and $|z_{im}| \le M$ uniformly, and that $\frac1q\sum_{m<q}\Omega_m$ converge to a positive definite matrix $\Omega$. Axiom 6, for a given sample, asks that no nonzero $\gamma$ satisfy $(z_{jm} - z_{Y_m m})\gamma \le 0$ for all observed $m$ and all $j$. A maximum likelihood estimator $\hat\theta^q$ is a measurable choice of a maximizer of $L^q$, wherever one exists.

Formalization targets

Goal: Lemma 6

$$\hat\theta^q \xrightarrow{\Pr} \theta^0 \quad\text{and}\quad \sqrt q\,\Omega^{1/2}(\hat\theta^q - \theta^0) \xrightarrow{d} N(0, I_K) \qquad (q \to \infty).$$

Milestones

1. Axiom 7 implies Axiom 5 (the full-rank condition) in all sufficiently large samples.
2. Equation (42): $P_{im}(\theta) \ge 1/(J_* e^{2M|\theta|})$.
3. Lemma 5: $\Pr(\text{Axiom 6 holds and } L^q \text{ attains its maximum}) \to 1$.
4. Equation (43): the first three derivatives of $\log P_{im}$ are bounded by $2M$, $4M^2$, $8M^3$.
5. Equation (46): each score $\nabla\log P_{Y_m m}(\theta^0)$ has mean zero.
6. Equation (47): each expected Hessian equals $-\Omega_m$.
7. Consistency of $\hat\theta^q$.
8. Equation (58): $q^{-1/2}\,\Omega^{-1/2}\sum_{m<q}\nabla\log P_{Y_m m}(\theta^0) \xrightarrow{d} N(0, I_K)$.

Significance

The result. Lemma 6 is what licenses reading $\hat\theta^q$ as approximately $N(\theta^0, q^{-1}\Omega^{-1})$, so that the diagonal of the inverse information matrix estimates the sampling variances and $q(\hat\theta^q-\theta^0)'\Omega(\hat\theta^q-\theta^0)$ is asymptotically $\chi^2_K$. Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction $\gamma$ of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.

Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization $1/q$ in (58), which must be $1/\sqrt q$, and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.

Difficulty

The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around $\theta^0$, controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances $\Omega_m$ that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin K); $z\theta$ is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.
• The paper's $N$ trials with $R_n$ repetitions are the special case of the serial indexing in which consecutive observations repeat their data; the sample size $\sum_n R_n$ is $q$.
• Axiom 7's limit (27) is taken in its serial form (48), with $P$ evaluated at $\theta^0$.
• The estimator is any measurable selection that maximizes $L^q$ whenever $L^q$ has a maximum, and is unconstrained otherwise. Requiring a maximizer for every sample would be unsatisfiable, since Axiom 6 fails with positive probability, and would make the goal vacuous; this convention rules that out.
• Consistency is TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. $\Omega^{1/2}$ is the positive semidefinite square root CFC.sqrt.
• Needed infrastructure: derivatives of log-sum-exp, a law of large numbers for bounded independent vectors, and a multivariate Lindeberg–Feller theorem. Mathlib provides the one-dimensional i.i.d. central limit theorem only. Contributions of these general results as separate theorems are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966 (Lindeberg–Feller theorem, pp. 256–258).
• C. R. Rao, Linear Statistical Inference and Its Applications, Wiley (cited by McFadden as Rao (1968), pp. 347–351, for the asymptotic $\chi^2$ test).

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

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.