Statistics

Motivation

The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is $\ell_1$-penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).

Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into $K$ cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).

Setting

A sample is a point $z = (z^{(y)}, z^{(x)})$ with a response $z^{(y)} \in \mathbb R$ and a feature vector $z^{(x)} \in \mathbb R^m$, so the samples live in $\mathbb R^{m+1}$. The sample space $\mathcal Z \subseteq \mathbb R^{m+1}$ is a compact set, and $\mathbb R^{m+1}$ carries the norm $\|z\|_\infty = \max(|z^{(y)}|, \max_j |z^{(x)}_j|)$. A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$.

A learning algorithm maps each training set $\mathbf s$ to a hypothesis $\mathcal A_{\mathbf s}$; with a loss $l(h, z)$, it is $(K, \epsilon(\cdot))$-robust (Definition 2, p. 396) if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$, fixed independently of the data, such that for every $\mathbf s \in \mathcal Z^n$, every training point $s \in \mathbf s$, every $z \in \mathcal Z$ and every $i$,

$$s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).$$

For a metric $\rho$ on $\mathcal Z$ and $\epsilon > 0$, a set $\hat T \subseteq \mathcal Z$ is an $\epsilon$-cover of $\mathcal Z$ if every point of $\mathcal Z$ is within distance $\le \epsilon$ of a point of $\hat T$; the covering number $\mathcal N(\epsilon, \mathcal Z, \rho)$ is the least cardinality of such a cover (Definition 1, p. 394).

For a coefficient vector $w \in \mathbb R^m$ let $\|w\|_1 = \sum_j |w_j|$. Given $c > 0$, the Lasso is

$$\min_{w} \ \frac1n \sum_{i=1}^n \big(s_i^{(y)} - w^\top s_i^{(x)}\big)^2 + c\|w\|_1, \tag{5}$$

a Lasso algorithm returns a minimizer $\mathcal A_{\mathbf s} = w$ of (5) for each $\mathbf s$, and the loss is the absolute prediction error $l(w, z) = |z^{(y)} - w^\top z^{(x)}|$. Finally $Y(\mathbf s) = \frac1n \sum_{i=1}^n [s_i^{(y)}]^2$.

Formalization targets

Goal: Example 6 (p. 404)

For every compact $\mathcal Z \subseteq \mathbb R^{m+1}$, every $c > 0$, every Lasso algorithm $\mathcal A$ and every $\gamma > 0$,

$$\mathcal A \text{ is } \Big(\mathcal N(\gamma/2, \mathcal Z, \|\cdot\|_\infty),\ \big(Y(\mathbf s)/c + 1\big)\gamma\Big)\text{-robust}.$$

The statement holds for every selection of a minimizer, since (5) need not have a unique solution.

Milestones

1. Optimality bound (proof of Lemma 3, p. 419): every Lasso solution satisfies $\|w^*\|_1 \le \frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2$.
2. Lemma 3 (p. 419): for all $z_a, z_b \in \mathbb R^{m+1}$,

$$|l(w^*(\mathbf s), z_a) - l(w^*(\mathbf s), z_b)| \le \Big[\frac{1}{nc} \sum_{i=1}^n [s_i^{(y)}]^2 + 1\Big] \|z_a - z_b\|_\infty.$$

3. Theorem 6 (p. 402): for a metric $\rho$ on $\mathcal Z$ and $\gamma > 0$, if $|l(\mathcal A_{\mathbf s}, z_1) - l(\mathcal A_{\mathbf s}, z_2)| \le \epsilon(\mathbf s)$ whenever $z_1 \in \mathbf s$ and $\rho(z_1, z_2) \le \gamma$, and $\mathcal N(\gamma/2, \mathcal Z, \rho) < \infty$, then $\mathcal A$ is $(\mathcal N(\gamma/2, \mathcal Z, \rho), \epsilon(\cdot))$-robust.

Significance

Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form $\epsilon(\mathbf s) + M\sqrt{(2K\ln 2 + 2\ln(1/\delta))/n}$ with $K$ a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.

The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the $\ell_1$/$\ell_\infty$ pairing on $\mathbb R \times \mathbb R^m$, and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.

Difficulty

The constant in the robustness level depends on the training set through $Y(\mathbf s)$, while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on $\mathbf s$ proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by $\epsilon(\mathbf s)$ and the cells must depend only on $\mathcal Z$ and $\gamma$. A cover by balls is not a partition, and the radius of the cover ($\gamma/2$) and the closeness threshold in Theorem 6 ($\gamma$) differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between $\|w\|_1$ and $\|\cdot\|_\infty$ is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.

Formalization scope

• $\mathbb R^{m+1}$ is ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly $\|\cdot\|_\infty$. $\|w\|_1$ is written out as $\sum_j |w_j|$, since the default norm on Fin m → ℝ is the sup norm; $w^\top x$ is dotProduct w x.
• The sample space is a set Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.
• The covering number is Mathlib's Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is $\mathcal Z$ itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return $0$ and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.
• A Lasso algorithm is any function A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies $c > 0$, which the paper leaves implicit. The factor $1/n$ is a real division; for $n = 0$ it is $0$ in Lean, the objective reduces to $c\|w\|_1$, and all statements remain true.
• The robustness level is $(Y(\mathbf s)/c + 1)\gamma$ in Example 6 and $\frac{1}{nc}\sum_i [s_i^{(y)}]^2 + 1$ in Lemma 3, each in its printed form.

Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. doi:10.1007/s10994-011-5268-1
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society, Series B 58(1) (1996) 267–288. doi:10.1111/j.2517-6161.1996.tb02080.x
• H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, IEEE Transactions on Information Theory 56(7) (2010) 3561–3574. doi:10.1109/TIT.2010.2048503
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. jmlr.org/papers/v2/bousquet02a

Motivation

Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.

Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).

Setting

Let $\mathcal Z$ be a measurable sample space, $\mathcal H$ a set of hypotheses and $l : \mathcal H \times \mathcal Z \to [0, M]$ a loss, with each $l(h, \cdot)$ measurable. A training set $\mathbf s = (s_1, \dots, s_n)$ consists of $n$ i.i.d. draws from a probability measure $\mu$ on $\mathcal Z$; its empirical distribution is $\mu_{\mathrm{emp}} = \frac1n \sum_i \delta_{s_i}$. A learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$, and $\mathcal A_{\mathbf s}$ is the hypothesis learned from $\mathbf s$.

For a real random variable $X$ and a level $\beta$, the $\beta$-quantile value is

$$\mathbb Q^\beta(X) = \inf\{ c \in \mathbb R : \Pr(X \le c) \ge \beta \},$$

and, writing $Q = \mathbb Q^\beta(X)$, the $\beta$-truncated mean is

$$\mathbb T^\beta(X) = \mathbb E[X \cdot \mathbf 1(X < Q)] + \big(\beta - \Pr[X < Q]\big)\, Q,$$

where the second term vanishes when $\Pr[X = Q] = 0$. It is the contribution to $\mathbb E X$ of the leftmost $\beta$ fraction of the distribution. For a hypothesis $h$ and a measure $\nu$ on $\mathcal Z$ put $\mathcal Q(h, \beta, \nu) = \mathbb Q^\beta(l(h, z))$ and $\mathcal T(h, \beta, \nu) = \mathbb T^\beta(l(h, z))$ with $z \sim \nu$.

The algorithm is $(K, \epsilon(\cdot), \hat n(\cdot))$ pseudo robust, with $\epsilon : \mathcal Z^n \to \mathbb R$ and $\hat n : \mathcal Z^n \to \{1, \dots, n\}$, if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$, fixed in advance, such that every training set $\mathbf s$ has a subset $\hat{\mathbf s}$ of $\hat n(\mathbf s)$ samples with: whenever $s \in \hat{\mathbf s}$ and $z \in \mathcal Z$ lie in a common cell, $|l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s)$. With $\hat n \equiv n$ this is $(K, \epsilon(\cdot))$-robustness.

Formalization targets

Goal: Theorem 5 (p. 402)

Let $\lambda_0 = \sqrt{(2K \ln 2 + 2 \ln(1/\delta))/n}$ and $r(\mathbf s) = (n - \hat n(\mathbf s))/n$. If $\mathcal A$ is $(K, \epsilon(\cdot), \hat n(\cdot))$ pseudo robust, $\beta \in (0,1)$ and $\delta > 0$, then with probability at least $1 - \delta$: whenever $0 \le \beta - \lambda_0 - r(\mathbf s)$ and $\beta + \lambda_0 + r(\mathbf s) \le 1$,

$$\mathcal Q(\mathcal A_{\mathbf s}, \beta - \lambda_0 - r(\mathbf s), \mu_{\mathrm{emp}}) - \epsilon(\mathbf s) \le \mathcal Q(\mathcal A_{\mathbf s}, \beta, \mu) \le \mathcal Q(\mathcal A_{\mathbf s}, \beta + \lambda_0 + r(\mathbf s), \mu_{\mathrm{emp}}) + \epsilon(\mathbf s),$$ $$\mathcal T(\mathcal A_{\mathbf s}, \beta - \lambda_0 - r(\mathbf s), \mu_{\mathrm{emp}}) - \epsilon(\mathbf s) \le \mathcal T(\mathcal A_{\mathbf s}, \beta, \mu) \le \mathcal T(\mathcal A_{\mathbf s}, \beta + \lambda_0 + r(\mathbf s), \mu_{\mathrm{emp}}) + \epsilon(\mathbf s).$$

The constants are the paper's, and $K$, $\epsilon$, $\hat n$, $M$, $\mu$, $\delta$ and the algorithm are arbitrary.

Milestones (Appendix C)

1. Property 1 (p. 415): for a nonnegative $X$ and levels $0 \le \beta_2 \le \beta_1 \le 1$ (with $\beta_1 = 1$ only for $X$ bounded above), $\mathbb Q^{\beta_1}(X) \ge \mathbb Q^{\beta_2}(X)$ and $\mathbb T^{\beta_1}(X) \ge \mathbb T^{\beta_2}(X)$.
2. Property 2 (p. 415): if $\Pr(Y \ge a) \ge \Pr(X \ge a)$ for all $a$, then $\mathbb Q^\beta(Y) \ge \mathbb Q^\beta(X)$ and $\mathbb T^\beta(Y) \ge \mathbb T^\beta(X)$ for $\beta \in [0,1]$.
3. The event $\mathcal E$ (pp. 415–416): with $N_i$ the indices of samples in $C_i$, $\sum_i \big| |N_i|/n - \mu(C_i) \big| \le \lambda_0$ with probability at least $1 - \delta$.

Significance

The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by $\lambda_0 + (n - \hat n(\mathbf s))/n$, up to the robustness tolerance $\epsilon(\mathbf s)$. The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case $\hat n \equiv n$ is the paper's Theorem 2 (p. 400).

Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on $\mathbb R$ developed here are reusable beyond this mission.

Difficulty

The concentration step is the same as for the expected loss: on the event $\mathcal E$ the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to $n - \hat n(\mathbf s)$ samples outside $\hat{\mathbf s}$ carry no guarantee at all, so an arbitrary fraction $r(\mathbf s)$ of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level $\beta$, not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.

Formalization scope

• The Lean namespace is XuMannorRobust.Quantile. $\mathcal Z$ is a type with a measurable space structure, $\mathcal H$ an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).
• "With probability at least $1 - \delta$" is encoded as: the outer measure of the set of training sets on which the claim fails is at most $\delta$. No measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$ is needed.
• Added measurability. The paper ignores measurability; the formalization requires each $l(h,\cdot)$ and each cell $C_i$ to be measurable.
• Corrected Definition 3. The paper prints the second branch of the truncated mean as $\big(\beta - \Pr[X < Q]\big)/\Pr[X = Q] \cdot Q$. That contradicts its own worked example on p. 399, where the $0.63$-truncated mean of a uniform law on $c_1 < \dots < c_{10}$ is $0.1(\sum_{i \le 6} c_i + 0.3 c_7)$, and its verbal description. The formalization drops the division, as the example requires; with the printed formula $\mathbb T^\beta$ would not even be monotone in $\beta$.
• $\mathbb Q^\beta$ and $\mathbb T^\beta$ are defined on the law of the random variable, a measure on $\mathbb R$. Lean returns $0$ for the infimum of an empty set or of a set unbounded below, so $\mathbb Q^0 = 0$ (the paper's value is $-\infty$). This never helps: $\mathcal Q(\mathcal A_{\mathbf s}, \beta, \mu) \ge 0$ and $\epsilon(\mathbf s) \ge 0$, so the goal's inequalities remain meaningful at level $0$. The goal keeps every level in $[0,1]$ through the paper's side condition, which depends on $\hat n(\mathbf s)$ and is therefore placed inside the probability event as a premise. The codomain $\{1, \dots, n\}$ of $\hat n$ is part of the definition: with $\hat n(\mathbf s) = 0$ nothing would constrain $\epsilon(\mathbf s)$.
• The partition is fixed before the training set; the good subset $\hat{\mathbf s}$ may depend on $\mathbf s$ and is a set of indices. Choosing the partition after $\mathbf s$ would make pseudo robustness trivial and is ruled out.
• Properties 1 and 2 are stated for nonnegative laws and levels in $[0,1]$. The level $1$ is admitted only for a variable bounded above (for property 2, the dominating one). For an unbounded variable, $\mathbb Q^1$ is $+\infty$ in the paper, where the inequality is trivial, and a junk $0$ in Lean. Property 3 of Appendix C (p. 415) is misprinted (with the constraint $\sum \alpha_i \le \beta$ the minimum is $0$) and is not formalized.
• Needed infrastructure: the Bretagnolle–Huber–Carol inequality for multinomial frequencies (van der Vaart and Wellner 1996, Prop. A.6.6) (or a direct concentration argument), and elementary order properties of lower quantile values and truncated means of laws on $\mathbb R$. Contributions of these as separate lemmas are welcome.

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86(3):391–423, 2012. https://doi.org/10.1007/s10994-011-5268-1
• R. Koenker and G. Bassett, Regression Quantiles, Econometrica 46(1):33–50, 1978. https://doi.org/10.2307/1913643
• P. J. Huber, Robust Statistics, Wiley, 1981. https://doi.org/10.1002/0471725250
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2

Motivation

Most generalization guarantees in statistical learning theory bound the gap between training error and expected error through a complexity measure of the hypothesis class: VC dimension, Rademacher complexity, covering numbers. Such bounds are sufficient conditions, and they say little about why a particular algorithm, run on a particular data stream, does or does not generalize. Xu and Mannor (Mach Learn 86 (2012) 391–423) proposed algorithmic robustness as an alternative: an algorithm is robust if a test sample "close to" a training sample incurs a loss close to that training sample's loss. Their first results show that robustness implies generalization (Theorem 1 of the paper, the subject of the first mission in this series).

Section 8 of the paper asks the converse question: is some form of robustness also necessary? The answer is Theorem 8. For a learning method trained on a fixed, growing sequence of samples, generalization is equivalent to a weaker property, weak robustness. The authors present this as evidence that robustness is "an essential property of successful learning", and contrast it with the characterization of learnability by stability (Remark 5 of the paper, citing Shalev-Shwartz et al. 2009; journal version JMLR 11 (2010)): learnability is uniform over all distributions, whereas the generalization studied here is for one distribution and one training sequence.

Setting

Let $\mathcal Z$ be a measurable space of samples, drawn from an unknown probability measure $\mu$. Let $\mathcal H$ be a set of hypotheses and $l : \mathcal H \times \mathcal Z \to \mathbb R$ a loss with $0 \le l(h, z) \le M$ for all $h, z$ (the paper's standing assumption, Sect. 1.1).

• The expected loss of $h$ is $\mathcal L(h) = \mathbb E_{z \sim \mu}\, l(h, z)$ (expectedLoss).
• The average loss of $h$ on an $n$-sample set $\mathbf t(n) = (t_1, \dots, t_n)$ is $L(h, \mathbf t(n)) = \frac1n \sum_{i=1}^n l(h, t_i)$ (avgLoss).
• A learning method $\mathcal A = \{\mathcal A^n\}_{n \in \mathbb N}$ is a sequence of maps $\mathcal A^n : \mathcal Z^n \to \mathcal H$; $\mathcal A_{\mathbf s(n)}$ is the hypothesis learned from $\mathbf s(n)$.
• A training sequence $\mathbf s^* = (s^*_1, s^*_2, \dots)$ is fixed and deterministic, and $\mathbf s^*(n)$ denotes its first $n$ elements (firstN).
• A test sample $\mathbf t(n)$ consists of $n$ i.i.d. draws from $\mu$; $\Pr$ always refers to $\mathbf t(n) \sim \mu^n$.

The method generalizes w.r.t. $\mathbf s^*$ (Definition 8) if

$$\lim_{n\to\infty} \big| \mathcal L(\mathcal A_{\mathbf s^*(n)}) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n)) \big| = 0.$$

It is weakly robust w.r.t. $\mathbf s^*$ (Definition 9) if there are sets $\mathcal D_n \subseteq \mathcal Z^n$ with $\Pr(\mathbf t(n) \in \mathcal D_n) \to 1$ and

$$\lim_{n\to\infty} \Big\{ \max_{\hat{\mathbf s}(n) \in \mathcal D_n} \big| L(\mathcal A_{\mathbf s^*(n)}, \hat{\mathbf s}(n)) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n)) \big| \Big\} = 0. \qquad (6)$$

A set $\mathcal D_n$ can be read as a family of perturbed copies of the training set that carries almost all of the probability of the test sample.

Formalization targets

Goal: Theorem 8 (p. 409)

$$\mathcal A \text{ generalizes w.r.t. } \mathbf s^* \iff \mathcal A \text{ is weakly robust w.r.t. } \mathbf s^*,$$

for every probability measure $\mu$, every loss measurable in $z$ with values in $[0, M]$, every learning method $\mathcal A$ and every training sequence $\mathbf s^*$.

Milestones

1. First equality of the proof (p. 410). For $n \ge 1$ and every $h$, $\mathbb E_{\mathbf t(n)} L(h, \mathbf t(n)) = \mathcal L(h)$.
2. Sufficiency display (p. 410). If $\Pr(\mathbf t(n) \notin \mathcal D) \le \delta$ and $|L(h, \hat{\mathbf s}) - L(h, \mathbf s)| \le \epsilon$ on $\mathcal D$, then

$$\big|\mathcal L(h) - L(h, \mathbf s)\big| \le \delta M + \epsilon.$$

3. Lemma 2 (p. 410). If $\mathcal A$ is not weakly robust w.r.t. $\mathbf s^*$, there are $\epsilon^*, \delta^* > 0$ with

$$\Pr\big(|L(\mathcal A_{\mathbf s^*(n)}, \mathbf t(n)) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))| \ge \epsilon^*\big) \ge \delta^* \quad\text{for infinitely many } n. \qquad (8)$$

4. Eq. (9) (p. 411). $L(\mathcal A_{\mathbf s^*(n)}, \mathbf t(n)) - \mathcal L(\mathcal A_{\mathbf s^*(n)}) \to 0$ in probability.

Milestones 1–2 give the sufficiency direction; milestones 3–4 give necessity.

Significance

Theorem 8 is a characterization, not a bound. The sufficiency half says a quantitative robustness property yields generalization. The necessity half says every method that generalizes along a sequence is weakly robust along it, so no generalization argument can avoid something of this shape. The paper remarks that $(K, \epsilon)$-robustness for every $\epsilon$ implies weak robustness, which places Theorem 1's condition inside this characterization. Corollary 6, the almost-sure version (generalization with probability 1 iff almost-sure weak robustness), follows from Theorem 8 applied sequence by sequence.

The result is proved in the paper; no machine-checked proof of it is known. This mission contributes a formal statement of Definitions 8 and 9 in Lean, the two directions of the proof as reusable finite-$n$ and asymptotic lemmas, and a place to formalize the bounded-loss law of large numbers for a hypothesis that changes with $n$ (Eq. (9)), which Mathlib states for a fixed random variable.

Difficulty

The sufficiency direction is a direct estimate once the expectation of the average test loss is identified with the expected loss; the formal work is in handling the product measure $\mu^n$ and a set $\mathcal D_n$ that need not be measurable.

The necessity direction is where care is needed. Eq. (9) is not the weak law of large numbers for a fixed function: the hypothesis $\mathcal A_{\mathbf s^*(n)}$ changes with $n$, so the concentration must be uniform in the hypothesis, which holds only because the loss is uniformly bounded. Lemma 2 negates a statement with an existential over sequences of sets and a limit; the naive reading "for each $\epsilon, \delta$ some $\mathcal D_n$ works eventually" does not by itself produce a single sequence $\mathcal D_n$ satisfying (6) with one limit.

Formalization scope

• $\mathcal Z$ is a type with a MeasurableSpace, $\mu$ a Measure with IsProbabilityMeasure, $\mathcal H$ an arbitrary type. The learning method is A : (n : ℕ) → (Fin n → Z) → H, the training sequence sStar : ℕ → Z, and $\mathbf t(n) \sim$ Measure.pi (fun _ : Fin n => μ). Indices start at $0$.
• The loss bound $0 \le l \le M$ is a hypothesis of every theorem. Measurability of $l(h, \cdot)$ is added; the paper explicitly ignores measurability. Expectations are Bochner integrals, well defined here because the loss is bounded and measurable.
• Probabilities and their limits live in $[0, \infty]$ (ℝ≥0∞). The sets $\mathcal D_n$ need not be measurable; their probability is the outer measure. "For infinitely many $n$" is ∃ᶠ n in atTop.
• Eq. (6) is encoded without a supremum: weak robustness asks for sets $D_n$ and reals $\eta_n \to 0$ with $|L(\mathcal A_{\mathbf s^*(n)}, \hat{\mathbf s}) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))| \le \eta_n$ for all $n$ and all $\hat{\mathbf s} \in D_n$. This avoids Lean's junk value $\sup \emptyset = 0$; since $\Pr(\mathbf t(n) \in D_n) \to 1$ forces $D_n$ to be nonempty for all large $n$, the bound form is equivalent to the paper's reading.
• Only part 1 of Definitions 8 and 9 is formalized. Corollary 6 is out of scope.
• The goal is not trivial in either direction: a constant method on a one-point space satisfies both sides, and a constant method whose hypothesis has training average $1$ and expected loss $1/2$ along a fixed sequence fails both, so neither side is vacuous or always true.
• Needed infrastructure: integrals over Measure.pi of coordinate functions, a Chebyshev or Hoeffding bound for averages of bounded i.i.d. variables uniform over a family of functions, and a diagonal-sequence construction. The uniform concentration lemma is reusable beyond this mission. Proofs of the milestones, and alternative routes to Eq. (9), are welcome.

Selected references

• Huan Xu, Shie Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
• Shai Shalev-Shwartz, Ohad Shamir, Nathan Srebro, Karthik Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://www.jmlr.org/papers/v11/shalev-shwartz10a.html
• Wassily Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Why algorithmic robustness

A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.

Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.

Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.

Setting

Throughout, $\mathcal Z$ is a measurable space of samples and $\mathcal H$ is an arbitrary set of hypotheses. A loss $l : \mathcal H \times \mathcal Z \to \mathbb R$ satisfies $0 \le l(h,z) \le M$ for a constant $M$. A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$, and a learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$, written $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

For a probability measure $\mu$ on $\mathcal Z$, the expected error and the training error of the learned hypothesis are

$$\mathcal L(\mathcal A_{\mathbf s}) = \mathbb E_{z\sim\mu}\, l(\mathcal A_{\mathbf s}, z), \qquad l_{\mathrm{emp}}(\mathcal A_{\mathbf s}) = \frac1n \sum_{i=1}^n l(\mathcal A_{\mathbf s}, s_i).$$

Definition 2 (p. 396). For $K \in \mathbb N$ and $\epsilon(\cdot) : \mathcal Z^n \to \mathbb R$, the algorithm $\mathcal A$ is $(K, \epsilon(\cdot))$-robust if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$ such that for every $\mathbf s \in \mathcal Z^n$,

$$\forall s \in \mathbf s,\ \forall z \in \mathcal Z,\ \forall i:\quad s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).$$

The partition is chosen once, before the training set. Only the tolerance $\epsilon(\mathbf s)$ may depend on $\mathbf s$.

For a partition $C_1,\dots,C_K$, the cell count $|N_i|$ is the number of training points in $C_i$. The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.

Formalization targets

Goal: Theorem 1 (p. 396)

Let $\mathcal A$ be $(K,\epsilon(\cdot))$-robust and let $\mathbf s$ consist of $n \ge 1$ i.i.d. draws from $\mu$. Then for every $\delta > 0$, with probability at least $1-\delta$,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

The constants are the paper's and are kept as printed. $K$, $\epsilon(\cdot)$, $M$, $n$, $\delta$, $\mu$ and the algorithm are all universally quantified.

Milestones (proof of Theorem 1, pp. 396–397)

1. Bretagnolle–Huber–Carol inequality for the multinomial vector of cell counts. For every $\lambda \ge 0$,

$$\Pr\Big\{\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \ge \lambda\Big\} \le 2^K \exp\Big(\frac{-n\lambda^2}{2}\Big).$$

2. Eq. (3). With probability at least $1-\delta$,

$$\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \le \sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

3. Eq. (4). For a partition witnessing robustness and for every training set $\mathbf s$, deterministically,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big|.$$

Significance

Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:

• Corollary 1: an adaptive number of cells;
• Corollaries 2 and 3: covering-number instances;
• Theorem 4: a pseudo-robust version;
• the Markovian case.

Its complexity term depends only on the number of cells $K$, not on any capacity measure of $\mathcal H$. This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, $K$ is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.

Theorem 1 is a published result with a short proof. What a formalization adds:

• a machine-checked statement of the robustness notion, pinning down which quantifier comes first;
• a formal proof of the multinomial concentration step, which the paper takes from van der Vaart and Wellner rather than proving;
• a reusable interface for the covering-number examples.

A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.

Difficulty

The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of $\mu$-measure zero, where the conditional expectation in the paper's chain is undefined.

The main obstacle is the probabilistic step. The quantity $\sum_i ||N_i|/n - \mu(C_i)|$ is an $\ell_1$ deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the $K$ coordinates gives a bound whose deviation level grows linearly in $K$. That is not $2^K e^{-n\lambda^2/2}$, and it does not give the constant $\sqrt{2K\ln 2}$ of Theorem 1. The difficulty is to obtain the exact exponential rate $2^K e^{-n\lambda^2/2}$ for the $\ell_1$ deviation as a whole, with no loss in the constant.

Formalization scope

Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and $\mu(C_i)$ enters as a real number.

"With probability at least $1-\delta$" is encoded as an upper bound $\delta$ on the outer measure, under $\mu^n$, of the set of training sets where the inequality fails. This needs no measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

The paper ignores measurability. The formalization restores it: every $l(h,\cdot)$ is measurable and every cell is a measurable set. Together with $0 \le l \le M$ this makes the expected error a genuine expectation.

The theorems assume $n \ge 1$. The Bretagnolle–Huber–Carol step assumes $\lambda \ge 0$, because the printed inequality is false for $\lambda < 0$. No upper bound on $\delta$ is imposed: for $\delta > 2^K$ the radicand is negative, the square root evaluates to $0$, and the statements remain true.

Two trivializing readings of Definition 2 are ruled out:

• The partition may not depend on the training set. In IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a $\{0,1\}$-valued loss would be $(2,0)$-robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.
• The tolerance may not depend on the test point, and the condition is required for every $z \in \mathcal Z$, not only for $z$ equal to a training point.

Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2
• 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
• H. Xu, C. Caramanis and S. Mannor, Robustness and Regularization of Support Vector Machines, Journal of Machine Learning Research 10 (2009) 1485–1510. https://www.jmlr.org/papers/v10/xu09b.html
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Markov chain Monte Carlo (MCMC) estimates an expectation $\int f\,d\pi$ by the average of $f$ along a Markov chain whose invariant distribution is $\pi$. Many chains share the same $\pi$: every Metropolis–Hastings acceptance rule that satisfies detailed balance, every mixture of such kernels, every choice of proposal. Practitioners need a criterion for preferring one of them. The standard yardstick is the asymptotic variance of the ergodic average, the constant in the Markov chain central limit theorem. A smaller asymptotic variance means fewer iterations for the same Monte Carlo error.

Peskun (1973) compared chains on a finite state space through a partial order on transition matrices: if one reversible matrix moves off the diagonal at least as much as another, entry by entry, its asymptotic variances are no larger, for every function. That result justifies the Metropolis–Hastings acceptance probability as the best possible among reversible acceptance rules. It covers only finite state spaces, while MCMC is used almost exclusively on continuous or mixed ones.

Tierney (1998) extended Peskun's theorem to general state spaces, using the spectral approach of Kipnis and Varadhan (1986) for reversible chains. The theorem is the one usually cited when an MCMC paper argues that one sampler dominates another; Mira (2001) surveys orderings built on it.

Setting

Let $(E, \mathcal E)$ be a measurable space in which singletons are measurable, and let $\pi$ be a probability measure on $E$. A Markov kernel $H$ assigns to each $x \in E$ a probability measure $H(x, \cdot)$, measurably in $x$. It acts on functions by $(Hf)(x) = \int f(y)\,H(x,dy)$. The measure $\pi$ is invariant for $H$ if $\int H(x, A)\,\pi(dx) = \pi(A)$ for every $A \in \mathcal E$. The kernel $H$ is reversible with respect to $\pi$ (satisfies detailed balance) if

$$\pi(dx)\,H(x,dy) = \pi(dy)\,H(y,dx),$$

that is, $\int_A H(x,B)\,\pi(dx) = \int_B H(x,A)\,\pi(dx)$ for all $A, B \in \mathcal E$. Reversibility implies invariance.

Write $\langle f, g\rangle = \int fg\,d\pi$, $L^2(\pi)$ for the square-integrable functions and $L^2_0(\pi) = \{g \in L^2(\pi) : \int g\,d\pi = 0\}$.

Off-diagonal domination. For kernels $P_1, P_2$, $P_1 \succeq P_2$ (OffDiagDominates π P₁ P₂) if for $\pi$-almost every $x$,

$$P_1(x, A\setminus\{x\}) \ge P_2(x, A \setminus\{x\}) \quad\text{for all } A \in \mathcal E.$$

So from almost every state $P_1$ moves to every region at least as readily as $P_2$, and the kernels differ only in the probability of staying put.

The chain and its asymptotic variance. For a Markov kernel $H$, let $X_0, X_1, \dots$ be the Markov chain with initial distribution $\pi$ and transition kernel $H$ (chainMeasure π H, a measure on paths $\mathbb N \to E$). For $f \in L^2_0(\pi)$ put $S_n = \sum_{i=1}^n f(X_i)$ (pathSum f n) and

$$v(f, H) = \lim_{n \to \infty} \frac1n \operatorname{Var}_H(S_n) \in [0, \infty].$$

The lag inner products are $\langle f, H^k f\rangle = \int f(x) \int f(y)\,H^k(x,dy)\,\pi(dx)$ (lagInner π H f k), and for $0 \le \lambda < 1$ the regularized variance is $v_\lambda(f,H) = \langle f,f\rangle + 2 \sum_{k\ge1} \lambda^k \langle f, H^k f\rangle$ (vLam π H f lam).

Formalization targets

Goal: Theorem 4 (p. 5)

Let $P_1, P_2$ be Markov kernels reversible with respect to $\pi$, $f \in L^2_0(\pi)$, and $P_1 \succeq P_2$. Then both asymptotic variances exist in $[0,\infty]$ and

$$v(f, P_1) \le v(f, P_2).$$

No rate, constant or regularity of the kernels is fixed. The statement is the ordering itself, valid for every reversible pair and every $f \in L^2_0(\pi)$.

Milestones, in attack order

1. Lemma 3 (p. 5): if $P_1, P_2$ have invariant distribution $\pi$ and $P_1 \succeq P_2$, then $P_2 - P_1$ is a positive operator on $L^2(\pi)$:

$$\iint f(x)f(y)\,\bigl(P_2(x,dy) - P_1(x,dy)\bigr)\,\pi(dx) \ge 0 \qquad (f \in L^2(\pi)).$$

2. A reversible kernel is a self-adjoint contraction on $L^2_0(\pi)$ (p. 5): $\langle Hf, g\rangle = \langle f, Hg\rangle$ and $\|Hf\| \le \|f\|$.
3. Finite-$n$ variance identity (p. 5), for $n \ge 1$:

$$\frac1n \operatorname{Var}_H(S_n) = \langle f,f\rangle + 2\sum_{i=1}^n \frac{n-i}{n}\,\langle f, H^i f\rangle.$$

4. Existence of $v(f,H)$ in $[0,\infty]$ (p. 6).
5. $v_\lambda(f,H) \to v(f,H)$ as $\lambda \uparrow 1$, finite or infinite (p. 6).
6. $v_\lambda(f,P_1) \le v_\lambda(f,P_2)$ for $0 \le \lambda < 1$ when $P_1 \succeq P_2$ (p. 6).

Significance

The result. Theorem 4 turns a pointwise, one-step comparison of kernels, which is easy to check, into a comparison of the quantity that governs Monte Carlo error. Its main consequence, drawn in §3 of the paper, is that the Metropolis–Hastings acceptance probability $\alpha_{MH}(x,y) = \min\{1, r(y,x)\}$ gives the maximal kernel in the off-diagonal order among reversible Metropolis–Hastings kernels with a given proposal. It is therefore optimal in asymptotic variance, on arbitrary state spaces. Proposition 5 of the same paper (a separate mission in this series) combines with it to show that a single Metropolis–Hastings kernel built on a mixture proposal beats the mixture of the component kernels. Later orderings of samplers (Mira 2001; Andrieu and Livingstone 2021) take this theorem as their base case.

Formalizing it. The theorem has been proved since 1998. No machine-checked version exists for general state spaces, and none of its milestones is on the platform. The formalization produces reusable infrastructure: the asymptotic variance of a stationary chain as an extended-real limit on Mathlib's Ionescu–Tulcea path measure, the $L^2$ facts for reversible kernels (self-adjointness, contraction, the covariance formula for path sums), and the positivity of $P_2 - P_1$ under off-diagonal domination. Each of these is used again in any formal treatment of MCMC efficiency or the Markov chain central limit theorem.

Difficulty

The direct approach compares the two finite-$n$ variances. This fails, and not just technically: the paper exhibits two doubly stochastic, symmetric $4\times4$ matrices with $P_1 \succeq P_2$ for which the variance of $f(X_0)+f(X_1)+f(X_2)$ is 15.4 under $P_1$ and 14.8 under $P_2$ (p. 7). Off-diagonal domination orders the lag-one covariances, but higher-order correlations "need not be ordered" (p. 5). The ordering appears only in the limit, and only for reversible kernels. The comparison must pass through an object that sees all lags at once and is monotone along the segment $P_1 + \beta(P_2 - P_1)$, and that object involves resolvents of operators on $L^2_0(\pi)$. The limit may be infinite, so every comparison must be made in $[0,\infty]$. Mathlib has neither the spectral measure of a self-adjoint operator nor the Kipnis–Varadhan theory.

Formalization scope

The state space is {E : Type*} [MeasurableSpace E] with [MeasurableSingletonClass E] wherever off-diagonal domination appears. This is an assumption the paper leaves implicit: $A \setminus \{x\}$ must be an event. $\pi$ is a probability measure and all kernels are Markov kernels. Reversibility is Mathlib's Kernel.IsReversible, invariance is Kernel.Invariant. The function $f$ is measurable with MemLp f 2 π and, for $L^2_0$, ∫ f ∂π = 0; measurability picks a representative of the $L^2$ class and costs nothing. The chain is Kernel.trajMeasure started from $\pi$. The sum runs over $X_1,\dots,X_n$, not $X_0$. Variances are Mathlib's evariance in $[0,\infty]$, and $v(f,H)$ is a Tendsto limit in ℝ≥0∞, so an infinite asymptotic variance is represented. The goal asserts the existence of both limits rather than assuming it, so it cannot hold vacuously. Neither it nor any milestone specializes to finite $E$, to Metropolis–Hastings kernels, or to a chain started from a point. Lemma 3 assumes invariance only, and the theorem requires reversibility, as printed.

Two statements depart in form from the page. The finite-$n$ variance identity and $v_\lambda$ are written through the moments $\langle f, H^k f\rangle$ (a Neumann series) instead of through the spectral measure $e_{f,H}$ and the resolvent $(I-\lambda H)^{-1}$. The two forms agree for a self-adjoint contraction, and this is noted in each item. The paper's appeal to the spectral theorem and to Kipnis and Varadhan (1986) is not restated as an item: a complete development needs it, or an equivalent argument, as part of the proof. Proofs of any milestone, and reusable lemmas on the path measure (stationarity and the marginal laws of $(X_i, X_j)$), are welcome.

Selected references

• L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, Ann. Appl. Probab. 8(1), 1–9, 1998. https://doi.org/10.1214/aoap/1027961031
• P. H. Peskun, Optimum Monte-Carlo sampling using Markov chains, Biometrika 60(3), 607–612, 1973. https://doi.org/10.1093/biomet/60.3.607
• C. Kipnis and S. R. S. Varadhan, Central limit theorem for additive functionals of reversible Markov processes and applications to simple exclusions, Comm. Math. Phys. 104, 1–19, 1986. https://doi.org/10.1007/BF01210789
• A. Mira, Ordering and improving the performance of Monte Carlo Markov chains, Statist. Sci. 16(4), 340–350, 2001. https://doi.org/10.1214/ss/1015346318
• C. Andrieu and S. Livingstone, Peskun–Tierney ordering for Markovian Monte Carlo: beyond the reversible scenario, Ann. Statist. 49(4), 1958–1981, 2021. https://doi.org/10.1214/20-AOS2008

Motivation

The Metropolis–Hastings algorithm (Metropolis et al. 1953; Hastings 1970) is the basic construction of Markov chain Monte Carlo. It turns a target probability distribution $\pi$, known only up to a constant, into a Markov chain that has $\pi$ as its invariant distribution. Bayesian computation depends on it, and a sampler is usually designed by proving one property: reversibility, or detailed balance, with respect to $\pi$.

For discrete state spaces, or when every measure involved has a density with respect to a common reference measure, the condition on the acceptance probability is the familiar $\pi(x)q(x,y)\alpha(x,y)=\pi(y)q(y,x)\alpha(y,x)$. Samplers used in practice often do not fit this setting: deterministic involutive proposals, mixtures of proposals with different supports, and Green's dimension-changing moves for model selection (Green 1995) have no common density. Each of these was treated separately in the literature. Tierney (1998) gives one necessary and sufficient condition that covers all of them, on an arbitrary measurable state space. This mission formalizes that condition.

Setting

Let $(E,\mathcal E)$ be a measurable space, with no topological or countability assumption. Let $\pi$ be a probability measure on $E$, the target. Let $Q(x,dy)$ be a Markov transition kernel on $E$, the proposal, and let $\alpha:E\times E\to[0,1]$ be a measurable function, the acceptance probability. From the current state $x$, a candidate $y$ is drawn from $Q(x,\cdot)$ and accepted with probability $\alpha(x,y)$; otherwise the chain stays at $x$. The resulting Metropolis–Hastings kernel (mhKernel Q α) is

$$P(x,dy)=Q(x,dy)\,\alpha(x,y)+\delta_x(dy)\int\bigl(1-\alpha(x,u)\bigr)\,Q(x,du).\tag{1}$$

A kernel $P$ satisfies detailed balance with respect to $\pi$ if the two measures $\pi(dx)P(x,dy)$ and $\pi(dy)P(y,dx)$ on $\mathcal E\otimes\mathcal E$ are equal (Eq. (2)). Equivalently, $\int_A P(x,B)\,\pi(dx)=\int_B P(x,A)\,\pi(dx)$ for all measurable $A,B$, which is Mathlib's Kernel.IsReversible P π.

Put $\mu(dx,dy)=\pi(dx)Q(x,dy)$ (π ⊗ₘ Q), and let $\mu^T(dx,dy)=\mu(dy,dx)$ be its image under the swap $(x,y)\mapsto(y,x)$. A symmetric split (IsSymmetricSplit) is a measurable set $R\subseteq E\times E$ with $(x,y)\in R\iff(y,x)\in R$, such that $\mu$ and $\mu^T$ are mutually absolutely continuous on $R$ and mutually singular on its complement $R^c$. Informally, $R$ consists of the pairs between which the proposal can move in both directions. A ratio version (IsRatioVersion) is a measurable $r:E\times E\to(0,\infty)$ that is a density of $\mu_R$ (the restriction of $\mu$ to $R$) with respect to $\mu^T_R$, and satisfies $r(x,y)=1/r(y,x)$ at every point.

Formalization targets

Goal: Theorem 2 (p. 3)

For every $\pi$, $Q$, $\alpha$ as above and every symmetric split $R$ and ratio version $r$ for $\mu=\pi\otimes Q$:

$$P\ \text{satisfies detailed balance w.r.t. }\pi\iff \begin{cases}\text{(i)}\ \ \alpha=0\quad\mu\text{-a.e. on }R^c,\\[2pt] \text{(ii)}\ \alpha(x,y)\,r(x,y)=\alpha(y,x)\quad\mu\text{-a.e. on }R.\end{cases}$$

The paper phrases the left side as condition (4), $\mu(dx,dy)\alpha(x,y)=\mu^T(dx,dy)\alpha(y,x)$, which its text identifies with (2) for the kernel (1). The goal states it for the kernel itself.

Milestones

1. Proposition 1 (p. 2). For every $\sigma$-finite measure $\mu$ on $E\times E$: a symmetric split $R$ exists; any two symmetric splits differ by a set null for both $\mu$ and $\mu^T$; and every symmetric split admits a ratio version.
2. §2, Eqs. (2)–(3) (p. 2). The kernel (1) satisfies (2) if and only if

$$\pi(dx)Q(x,dy)\alpha(x,y)=\pi(dy)Q(y,dx)\alpha(y,x),\tag{3}$$

that is, the rejection mass on the diagonal does not affect reversibility.

Companion item

§2, special case 1 (pp. 3–4). If $\pi(dx)=\pi(x)\nu(dx)$ and $Q(x,dy)=q(x,y)\nu(dy)$ for a $\sigma$-finite $\nu$, then $R=\{\pi(x)q(x,y)>0,\ \pi(y)q(y,x)>0\}$ is a symmetric split, $r=\pi(x)q(x,y)/(\pi(y)q(y,x))$ is a density of $\mu_R$ with respect to $\mu^T_R$, and detailed balance is equivalent to the two conditions holding $\nu\times\nu$-almost everywhere.

Significance

Theorem 2 lets reversibility be checked in the same way for every Metropolis–Hastings variant: compute $R$ and $r$ for the proposal, then verify (i) and (ii). The paper derives from it the reversibility of the standard acceptance probability $\alpha_{MH}=\min\{1,r(y,x)\}$ on $R$ (and $0$ off $R$), and the three special cases of §2 are instances. Together with Mathlib's Kernel.IsReversible.invariant, it yields that $\pi$ is invariant for the sampler. This is the correctness statement of every MCMC method built on the Metropolis–Hastings kernel. Missions II and III of this series (Peskun ordering; mixture proposals) take reversible Metropolis–Hastings kernels as their objects.

The result is proved in the paper. The mission adds a machine-checked proof at the paper's full generality: no densities, no dominating measure, no countability of $\mathcal E$. The platform currently has only finite-state statements (MarkovMixing.metropolis_stationary, a sufficiency direction on a Fintype state space with a matrix proposal), so neither the general kernel nor the converse direction is formalized there.

Difficulty

The obvious argument works with densities: write both sides of (3) as densities with respect to one reference measure and compare them pointwise. On a general space no such reference is given for $\mu$ and $\mu^T$ together, and even $\mu+\mu^T$ yields densities only up to null sets. Pointwise comparison of densities is therefore not available, and the statement mixes three kinds of almost-everywhere claim ($\mu$-a.e., $\mu^T$-a.e., and a.e. for the restrictions to $R$ and $R^c$). The Lean statement also has to hold for every version of $R$ and $r$, not one convenient choice. Milestone 2 has its own content: the diagonal part of $P$ is a measure concentrated on the diagonal, which need not be a measurable set, and its symmetry has to be shown without that measurability.

Formalization scope

• Space. {E : Type*} [MeasurableSpace E] with nothing else: no measurable singletons, no topology, no countable generation. π : Measure E with [IsProbabilityMeasure π] and Q : Kernel E E with [IsMarkovKernel Q].
• Acceptance probability. α : E × E → ℝ≥0∞ with the hypotheses Measurable α and ∀ p, α p ≤ 1, which is the paper's measurable $\alpha:E\times E\to[0,1]$. The kernel is Q.withDensity (fun x y => α (x, y)) + Kernel.withDensity Kernel.id (fun x _ => ∫⁻ u, (1 - α (x, u)) ∂(Q x)). The measurability hypothesis rules out the junk zero kernel that Kernel.withDensity returns for a non-measurable density.
• Detailed balance is Kernel.IsReversible. It agrees with the measure identity (2) because rectangles determine a finite measure on $\mathcal E\otimes\mathcal E$.
• (i) and (ii) are almost-everywhere statements for the restrictions of $\mu$ to $R^c$ and to $R$ respectively; neither is required pointwise. Condition (ii) off $R$ would be false in general.
• $R$ and $r$ are universally quantified in the goal. A formalization that fixes one specific Radon–Nikodym derivative, or drops the everywhere conditions $0<r<\infty$, $r(x,y)=1/r(y,x)$, proves a different statement. Proposition 1's existence clause shows that the goal's hypotheses can be met, so the goal is not vacuous. A sorry-free check in the workspace confirms this for $Q=\pi$ with $R=E\times E$, $r\equiv1$.
• Added hypothesis. The companion item assumes $\nu$ is $\sigma$-finite, which the paper leaves implicit in "$\nu\times\nu$-almost all".
• Infrastructure. The definitions IsSymmetricSplit and IsRatioVersion (a symmetric Lebesgue-type decomposition of a measure against its transpose) are reusable for any reversibility argument on product spaces. Lemmas on Measure.map Prod.swap of compProd and withDensity, and on the symmetry of measures carried by the diagonal, are also welcome contributions.

Selected references

• L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, Ann. Appl. Probab. 8(1) (1998) 1–9. https://doi.org/10.1214/aoap/1027961031
• N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, E. Teller, Equation of State Calculations by Fast Computing Machines, J. Chem. Phys. 21 (1953) 1087–1092. https://doi.org/10.1063/1.1699114
• W. K. Hastings, Monte Carlo Sampling Methods Using Markov Chains and Their Applications, Biometrika 57 (1970) 97–109. https://doi.org/10.1093/biomet/57.1.97
• L. Tierney, Markov Chains for Exploring Posterior Distributions, Ann. Statist. 22 (1994) 1701–1762. https://doi.org/10.1214/aos/1176325750
• P. J. Green, Reversible Jump Markov Chain Monte Carlo Computation and Bayesian Model Determination, Biometrika 82 (1995) 711–732. https://doi.org/10.1093/biomet/82.4.711