Statistics

Motivation

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

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

Setting

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

Table 1 gives four generators used here:

$$\phi_v(t)=|t-1|,\qquad \phi_h(t)=(\sqrt t-1)^2,\qquad \phi_{\mathrm{kl}}(t)=t\log t-t+1,\qquad \phi_j(t)=(t-1)\log t.$$

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

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

$$\mathcal P^\phi(P_0;\varepsilon) =\{P\in\mathfrak M(\Xi,\mathcal F):\mathfrak D^\phi(P,P_0)\le\varepsilon\}.$$

Formalization targets

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

$$\frac14\bigl(\mathfrak D^{\phi_v}(P,P_0)\bigr)^2 \le\mathfrak D^{\phi_h}(P,P_0) \le\mathfrak D^{\phi_{\mathrm{kl}}}(P,P_0) \le\mathfrak D^{\phi_j}(P,P_0).$$

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

$$\mathcal P^{\phi_j}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_{\mathrm{kl}}}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_h}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_v}(P_0;2\sqrt\varepsilon).$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Every generalization bound presented so far in this series is for classification, where the error of a prediction is binary (correct or not). Regression asks a different question: predictions are real-valued, and error is measured by the magnitude of the deviation from the true label, via a loss function L. Chapter 11 develops generalization theory for bounded regression, showing that the same two complexity measures used for classification — Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or a reduction to classification via level-set thresholding (pseudo-dimension route).

Setting

A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible); R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2 develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in its first (predicted-value) argument, the Rademacher complexity of the loss-composed family G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent, purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a pseudo-dimension generalization bound by reducing regression to a family of classification problems (one per threshold t), using the tail-integral identity Eq. 11.5.

Formalization targets

Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).

Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).

Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).

Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).

Significance

Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show "how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction — combined via a new observation (Proposition 11.2) specific to loss-composed families, not a restatement of either. Theorem 11.8 is the chapter's second, structurally independent technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a VC-dimension-style growth-function argument), but the reduction itself — regression to a continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq. (11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall content either: GET /theorems?q=generalization%20bound%20regression and GET /theorems?q=pseudo-dimension both return zero hits.

Difficulty

Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz constant taken in the first argument of L only — the predicted value h(x_i), holding the true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style classification bound (Corollary 3.19) to the family of thresholded classifiers — whose VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim definition by relabeling, would misrepresent this chapter's genuinely different (real-valued, threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.

Formalization scope

Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter being stated for real-valued scores and labels. EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather than the sign-function form of Definition 11.4 directly, since the two coincide except at a measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem 11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only, per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any of the four theorems.

Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation of the general theorem for a specific loss family, not a separate numbered theorem); Theorem 11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces, background/illustration rather than the chapter's general machinery — drafting only these examples instead of the general Theorem 11.8 would be this chapter's trivializing formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof (an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear regression, kernel ridge regression, SVR, Lasso and their online variants), which is applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 11 (§11.1-11.2).
• D. Haussler, "Decision theoretic generalizations of the PAC model for neural net and other learning applications," Information and Computation 100(1), 1992 (pseudo-dimension's origin).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (the tail-integral identity Eq. 11.5's classical antecedent).

Motivation

Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is $\tilde O(\sqrt{T\sum_k T_k})$, and a lower bound showing that no policy, even one told the periods, does better than $\Omega(\sqrt{T\max_k T_k})$. This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.

Lower bounds of this kind fix what is achievable. For the stationary $K$-armed bandit, the minimax regret is of order $\sqrt{TK}$ (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces $\sum_k T_k$ "effective arms" (arm $k$ at each phase of its cycle), which suggests the rate $\sqrt{T\sum_k T_k}$. The paper proves the weaker but general bound $\sqrt{T\max_k T_k}/(32e)$, which matches the upper bound up to a factor $\sqrt K$ and logarithms.

Setting

There are $K \ge 2$ arms and epochs $t = 1, \dots, T$. An instance $\nu$ is a family of mean rewards $\mu_{k,t}$. If arm $k$ is pulled at epoch $t$, the reward is drawn from the Gaussian law $\mathcal N(\mu_{k,t}, 1)$, independently of the past given the arm.

A sequence $f$ has minimum period $p \ge 1$ if $f(t+p) = f(t)$ for all $t \ge 1$ and no smaller positive integer has this property.

A policy $\pi$ chooses the arm $\pi_t$ at epoch $t$ at random, from a distribution that depends on the previous arms and rewards. Its expected regret on $\nu$ is display (1) of the paper:

$$\mathbb E_\nu[R^\pi_T] = \sum_{t=1}^T\Big(\max_k \mu_{k,t} - \mathbb E[\mu_{\pi_t,t}]\Big).$$

Three classes of instances appear, all with unit-variance Gaussian rewards and means in $[0,1]$ (Assumption 1):

1. $\mathcal E_1$: every arm is stationary;
2. $\mathcal E_2(T_1)$: the first arm's mean has minimum period $T_1$, the other arms are stationary;
3. $\mathcal E_3(T_1,\dots,T_K)$: arm $k$'s mean has minimum period $T_k$.

The proof compares instances through the metric (B-48),

$$\mathcal M(\nu_1,\nu_2) = \Big(\sum_{k=1}^K\sum_{p=1}^{T_k}\big(\mu^{(\nu_1)}_{k,p} - \mu^{(\nu_2)}_{k,p}\big)^2\Big)^{1/2}.$$

The periods satisfy Assumption 3 with the parameters (7): with $n = \lfloor\sqrt{T/K}\rfloor$ and $g = \lceil\sqrt n\rceil$, $T > 4K$, $g \ge 2$ and $T_k < n/(2g)$ for every $k$.

Formalization targets

Goal: Theorem 3 (p. 24)

For every policy $\pi$ there is $\nu \in \mathcal E_3(T_1,\dots,T_K)$ with

$$\mathbb E_\nu[R^\pi_T] \ge \frac{1}{32e}\sqrt{T\max_k T_k}.$$

Milestones

1. Lemma 12 (p. 23). Stationary Gaussian bandits whose arms other than the first have known mean $1/2$: every policy has regret at least $\sqrt T/(8\sqrt2 e)$ on some choice of $\mu_1 \in [0,1]$.
2. Lemma 13 (p. 23). One periodic arm: every policy has regret at least $\sqrt{TT_1}/(16e)$ on some instance of $\mathcal E_2(T_1)$ whose other arms have mean $1/2$.
3. Fact 1 (proof of Theorem 3, p. 48). $\mathcal E_3$ is dense in $\mathcal E_2 \cup \mathcal E_3$ under $\mathcal M$: an instance of $\mathcal E_2(T_1)$ can be perturbed on the arms other than the first into an instance of $\mathcal E_3(T_1,\dots,T_K)$ at $\mathcal M$-distance less than any $\delta > 0$.
4. Fact 2 (proof of Theorem 3, p. 48). The regret $f_\pi(\nu) = \mathbb E_\nu[R^\pi_T]$ is continuous in $\nu$ on $\mathcal E_2 \cup \mathcal E_3$ for $\mathcal M$, uniformly in $\pi$.

Significance

Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like $\sqrt{T\max_k T_k}$, not like $\sqrt{TK}$. Together with the paper's upper bound $\tilde O(\sqrt{T\sum_k T_k})$ and the inequality $\sqrt{T\max_k T_k} \ge \sqrt{T\sum_k T_k}/\sqrt K$, it shows the two-stage policy is near-optimal when $K$ is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.

The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.

Difficulty

The two-point argument of Lemma 12 is standard, but its constant needs $\Delta = \sqrt{1/(2T)} < 1/2$, so small horizons must be handled separately. Lemma 13 decomposes the problem into $T_1$ phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon $\lfloor T/T_1\rfloor$, with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly $T_1$ (all phases may coincide), so a perturbation is needed to land in $\mathcal E_2(T_1)$; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a $T$-round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.

Formalization scope

• Arms are Fin K, 0-based: the paper's first arm is index $0$. Epochs are 1-based natural numbers; history coordinate $i$ is epoch $i+1$. Values of the means at $t = 0$ are ignored.
• A policy is the platform's BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, $T\mu^* - \mathbb E[\sum_t X_t]$, which equals (1) for Gaussian arms; the other statements use (1) directly.
• Assumption 1 is stated on epochs $1,\dots,T$. Minimum periods are exact.
• Every lower bound has the order "for every policy there is an instance", with the instance in the class, so the policy may depend on $K$, $T$ and the periods; this is the paper's "policy that knows $T_k$". The supremum over the class is replaced by an attained instance, which is the stronger form.
• Added hypotheses, all disclosed: $K \ge 2$ (with one arm the regret is $0$); $T_k \ge 1$ (the paper's $T_k \in \mathbb N^+$); in Lemmas 12 and 13, the means of the arms other than the first are $1/2$, which is how "a policy that knows $\mu_k$ for $k \ge 2$" is read (with arbitrary known values the printed lemmas fail). Assumption 3 with (7) is the standing assumption of Appendix B.4.
• A statement with the quantifiers in the order "there is an instance for every policy", without the $[0,1]$ clause, or without exact minimum periods, would be false or trivial; none of these is the target.

Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, Operations Research, 2025; arXiv:2005.08088v4, 2021. https://arxiv.org/abs/2005.08088v4
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375

Motivation

Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.

Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.

Setting

A bandit problem with $K$ arms is a family $\underline\nu=(\nu_a)_{a=1,\dots,K}$ of probability distributions on $\mathbb R$, each with a finite expectation. A strategy $\psi$ plays for $T$ rounds. In round $t+1$ it picks an arm $A_{t+1}$ as a measurable function of $I_t=(U_0,Y_1,U_1,\dots,Y_t,U_t)$, where the $U_t$ are independent uniforms on $[0,1]$. It then observes a reward $Y_{t+1}$ drawn from $\nu_{A_{t+1}}$ and a fresh independent uniform $U_{t+1}$. The strategy together with the problem determines the law $\mathbb P_{\underline\nu}$ of $I_T$; $\mathbb E_{\underline\nu}$ is its expectation. The number of draws of arm $a$ is

$$N_{\psi,a}(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}.$$

$\mathrm{KL}(P,Q)\in[0,+\infty]$ is the Kullback–Leibler divergence between two probability measures: $\int\ln\frac{\mathrm dP}{\mathrm dQ}\,\mathrm dP$ when $P$ is absolutely continuous with respect to $Q$ and the integral exists, and $+\infty$ otherwise. The binary divergence $\mathrm{kl}(p,q)$, for $p,q\in[0,1]$, is the Kullback–Leibler divergence between the Bernoulli distributions of parameters $p$ and $q$. For $q\in(0,1)$ it is given by (5):

$$\mathrm{kl}(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}.$$

It equals $+\infty$ for $q\in\{0,1\}$ and $p\ne q$.

The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on $I_t$; fullHistoryMeasure ν ψ T is the law of $I_T$, fullPullCount ψ a is $N_{\psi,a}(T)$, and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for $\mathrm{kl}(p,q)$.

Formalization targets

Goal: the fundamental inequality (6), p. 6

For every strategy $\psi$, every pair of bandit problems $\underline\nu,\underline\nu'$, every horizon $T$, and every $\sigma(I_T)$-measurable statistic $Z$ with values in $[0,1]$:

$$\sum_{a=1}^K\mathbb E_{\underline\nu}\big[N_{\psi,a}(T)\big]\,\mathrm{KL}(\nu_a,\nu'_a)\ \ge\ \mathrm{kl}\big(\mathbb E_{\underline\nu}[Z],\ \mathbb E_{\underline\nu'}[Z]\big),$$

in $[0,+\infty]$, with $0\cdot(+\infty)=0$. The arm laws have the finite expectations required in §1.1; their divergences may be infinite.

Milestones, in the order of the proof (§2.1, pp. 7–8)

1. (9), p. 7: the one-round chain rule. Under finite arm divergences, the divergence between the observed-history laws after round $t+1$ is the divergence after round $t$ plus $\mathbb E_{\underline\nu}\big[\sum_a\mathrm{KL}(\nu_a,\nu'_a)\,\mathbb I\{A_{t+1}=a\}\big]$. The observed-history kernel version is proved on the platform.
2. Equality in (8), p. 7: $\sum_a\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a,\nu'_a)=\mathrm{KL}(\mathbb P_{\underline\nu}^{I_T},\mathbb P_{\underline\nu'}^{I_T})$. The platform has the observed-history kernel version under finite arm divergences; relating it to the full information law is part of the goal's work.
3. Lemma 1, first display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)=\mathrm{KL}(\mathbb P_1\otimes\lambda,\mathbb P_2\otimes\lambda)$, with $\lambda$ the Lebesgue measure on $[0,1]$.
4. Lemma 1, second display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}\big((\mathbb P_1\otimes\lambda)(E),(\mathbb P_2\otimes\lambda)(E)\big)$ for every measurable $E\subseteq\Gamma\times[0,1]$.
5. Lemma 1, last display, p. 8: $(\mathbb P\otimes\lambda)\{(\gamma,x):x\le Z(\gamma)\}=\mathbb E[Z]$.
6. Lemma 1, p. 8: for probability measures $\mathbb P_1,\mathbb P_2$ on any measurable space and any measurable $Z$ with values in $[0,1]$, $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}(\mathbb E_1[Z],\mathbb E_2[Z])$.

Significance

The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem $\underline\nu'$ and a statistic $Z$, usually $Z=N_{\psi,a}(T)/T$. The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound $\liminf_T\mathbb E[N_{\psi,a}(T)]/\ln T\ge 1/\mathcal K_{\inf}$ for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while $T$ is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.

The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.

Difficulty

Two points need care. First, Lemma 1 is stated for an arbitrary $[0,1]$-valued $Z$. The data-processing inequality only gives it directly for indicators of events, and pushing $\mathbb P_j$ forward by $Z$ gives a law on $[0,1]$, not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When $\mathrm{KL}(\nu_a,\nu'_a)=+\infty$ for an arm that is drawn with positive probability, the left side is $+\infty$ and there is nothing to prove. When such an arm is never drawn, its term is $0\cdot(+\infty)=0$. The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.

Formalization scope

• Arms are Fin K, indexed from $0$. The horizon $T$ is a natural number; at $T=0$ both sides are $0$. For $K=0$ no policy exists, so $K\ge1$ needs no hypothesis.
• Strategies are FullStrategy K, measurable functions of the paper's $I_t$. The same strategy runs under $\underline\nu$ and $\underline\nu'$. The local history law includes every auxiliary uniform, so $Z$ may depend on any of them.
• Both bandit problems satisfy Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.
• The binary divergence is the $[0,+\infty]$-valued Kullback–Leibler divergence of two Bernoulli laws, klBer, never a real formula. A real formula would return a finite junk value at $q\in\{0,1\}$, where (5) is $+\infty$, and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to $q\in(0,1)$, would be a weaker theorem and is not the target.
• In Lemma 1 and its displays, the "distributions" are probability measures on an arbitrary measurable space. $\lambda$ is the volume on Mathlib's unitInterval. $Z$ is real-valued and measurable, with values in $[0,1]$.
• Builds on the published definitions StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019; arXiv:1602.07182v3. https://arxiv.org/abs/1602.07182v3, https://doi.org/10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17, 1996. https://doi.org/10.1006/aama.1996.0007
• E. Kaufmann, O. Cappé, A. Garivier, On the complexity of best-arm identification in multi-armed bandit models, Journal of Machine Learning Research 17, 2016. https://jmlr.org/papers/v17/kaufman16a.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$. Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$, and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$, so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$-divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$. This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$, $n\ge1$, an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

• The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$.
• The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$, and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$.
• The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$, and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
• A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$.
• The localization inequality (20) asks that, for all $r\ge0$,

$$\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],$$

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$.

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$. With probability at least $1-4e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .$$

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

$$\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};$$

and the uniform bound (22): with probability at least $1-2e^{-t}$, for all $f\in\mathcal F$,

$$\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .$$

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$, faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$. Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$, which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$. The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$, which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$, $\rho\ge0$). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$; empirical means and variances are normalized by $1/n$. The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$. Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$, (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

• (22) is stated with probability $1-2e^{-t}$; the paper prints $1-e^{-t}$, and its proof (p. 41) concludes $1-2e^{-t}$.
• (23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$; the proof adds two fixed-$f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$).
• Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$, as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$), under Theorem 4's standing hypothesis $M\ge1$.
• Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

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
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.

Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.

Setting

Let $f:\mathbb R\to\mathbb R$ be a target density: positive, $C^2$, integrating to one, with $f'/f$ Lipschitz, and satisfying the moment conditions (A1) $\mathbb E_f[(f'/f)^8]<\infty$ and (A2) $\mathbb E_f[(f''/f)^4]<\infty$. Here $\mathbb E_f[g(X)]=\int g(x)f(x)\,dx$. In dimension $n\ge2$ the target is the product density $\pi_n(x)=\prod_{i=1}^n f(x_i)$ on $\mathbb R^n$.

Fix a scale $l>0$ and set $\sigma_n^2=l^2/(n-1)$. The random walk Metropolis chain $X^n=(X^n_0,X^n_1,\dots)$ moves as follows. From $X^n_{m-1}$ it proposes $Y\sim N(X^n_{m-1},\sigma_n^2I_n)$. It sets $X^n_m=Y$ with probability $\alpha(X^n_{m-1},Y)=1\wedge\pi_n(Y)/\pi_n(X^n_{m-1})$, and $X^n_m=X^n_{m-1}$ otherwise. The chain starts from $\pi_n$, which is stationary for it. The speeded-up first coordinate is $U^n_t=X^n_{\lfloor nt\rfloor,1}$ for $t\ge0$.

Let $\Phi$ be the standard normal distribution function, and define the roughness $I=\mathbb E_f[(f'(X)/f(X))^2]$. The speed and the limiting acceptance rate are

$$h(l)=2l^2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big),\qquad a(l)=2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big).$$

The Langevin generator is $GV(x)=h(l)\big[\tfrac12V''(x)+\tfrac12(\log f)'(x)V'(x)\big]$. It generates the Langevin diffusion $dU_t=h(l)^{1/2}dB_t+h(l)\frac{f'(U_t)}{2f(U_t)}dt$.

Formalization targets

Goal: Theorem 1.1

As $n\to\infty$,

$$U^n\Rightarrow U,$$

where $\Rightarrow$ denotes weak convergence in the Skorokhod topology, $U_0$ has density $f$, and $U$ is the Langevin diffusion with speed $h(l)$. The limit is asserted to exist. No constants appear in the statement beyond those the model defines.

Milestones: the proof

1. Lemma 2.1. The stationary chain stays in the sets $F_n=\{|R_n-I|<n^{-1/8}\}\cap\{|S_n-I|<n^{-1/8}\}$ up to time $t$ with probability tending to one. Here $R_n$ and $S_n$ are the empirical averages of $((\log f)')^2$ and $-(\log f)''$ over coordinates $2,\dots,n$.
2. Proposition 2.2. $|1\wedge e^x-1\wedge e^y|\le|x-y|$.
3. Lemma 2.3. $\sup_{x\in F_n}\mathbb E|W_n|\to0$, where $W_n$ is the second-order part of the log acceptance ratio.
4. Proposition 2.4. $\mathbb E[1\wedge e^A]=\Phi(\mu/\sigma)+e^{\mu+\sigma^2/2}\Phi(-\sigma-\mu/\sigma)$ for $A\sim N(\mu,\sigma^2)$.
5. Lemma 2.5. $\limsup_n\sup_{x_1}n|\mathbb E[V(Y_1)-V(x_1)]|<\infty$ for $V\in C_c^\infty$.
6. Lemma 2.6. The discrete generator $G_nV(x)=n\,\mathbb E[(V(Y)-V(x))\alpha(x,Y)]$ converges to $GV$ uniformly on $F_n$, for $V\in C_c^\infty$ a function of the first coordinate (stated with bounded $(\log f)'''$, the assumption its proof uses).

Milestones: the optimal-scaling corollary

7. Corollary 1.2 (i). $a_n(l)=\iint\pi_n(x)\alpha(x,y)q_n(x,y)\,dx\,dy\to a(l)$.
8. Corollary 1.2 (ii). $h$ is maximised at $\hat l=2.38/\sqrt I$, with $a(\hat l)=0.23$ and $h(\hat l)=1.3/I$, to the printed precision.

Significance

Theorem 1.1 shows that, run for $n$ times as many steps, the chain in dimension $n$ looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number $h(l)$. Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the $2.38/\sqrt I$ scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.

The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on $\mathbb R^n$ as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.

Difficulty

The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of $n-1$ terms of size $1/n$. That sum does not concentrate uniformly over the state space, since the coordinates $2,\dots,n$ are arbitrary. The expansion is controlled only on the sets $F_n$, where the empirical averages $R_n$ and $S_n$ are close to $I$. The limit therefore holds only after showing that the chain rarely leaves $F_n$ over a time horizon of $nt$ steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over $nt$ steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.

Formalization scope

All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.

• Vectors are Fin n → ℝ, and the paper's first coordinate $x_1$ is index 0. Its coordinates $2,\dots,n$ are the indices i ≠ 0.
• $\sigma_n^2=l^2/(n-1)$ is computed in $\mathbb R$. All statements concern $n\ge2$ or large $n$.
• $l>0$ is assumed. The paper leaves it implicit, but $h(-l)\ne h(l)$.
• "$f$ is a density" is read as $\int f=1$. The moment conditions are read as integrability of $(f'/f)^8f$ and $(f''/f)^4f$. The standing assumption "$f'/f$ is Lipschitz" (p. 111) is carried by every statement.
• The chain is built as a random mapping on an explicit probability space: $x_0\sim\pi_n$, with i.i.d. standard normal innovations and uniform acceptance variables. Theorem 1.1's initial condition (components i.i.d. $f$, shared across dimensions) is read as "the $n$-th chain starts from $\pi_n$", since weak convergence depends only on the law of each $U^n$.
• "$U$ satisfies the Langevin SDE" is read as "the law of $U$ solves the martingale problem for $G$ on $C_c^\infty$, with continuous paths and initial law $f(x)\,dx$". This is equivalent by Ethier–Kurtz (1986), Ch. 5, Prop. 3.1 and Thm 3.3, and follows the platform definition EthierKurtz_IsContinuousDiffusionLaw.
• "$U^n\Rightarrow U$" is read as the existence of an almost-sure coupling in which càdlàg copies of the $U^n$ converge to a continuous Langevin path uniformly on compact time intervals. For a continuous limit this is equivalent to weak convergence in $D_{\mathbb R}[0,\infty)$, by Skorokhod's representation theorem and Ethier–Kurtz Ch. 3, Thm 1.8, Prop. 5.3 and Prop. 7.1. It follows the platform encoding of Ethier–Kurtz Theorem 7.4.1.
• "$\sup\to0$" and "$\limsup\sup<\infty$" are stated as eventual uniform bounds. This avoids real suprema, whose value on an unbounded set is a default.
• In Lemma 2.6, "as $d\to\infty$" is a misprint for $n\to\infty$, and "$2f(Ut)$" in (1.2) is read as $2f(U_t)$.
• Corollary 1.2 (ii) is stated for an arbitrary constant $I>0$. "To two decimal places" is read as explicit rounding intervals: $1.3$ is read to one decimal, and all maximisers over $l>0$ are covered.

The goal cannot be satisfied trivially. The limit law $Q$ must exist, and it must be a probability measure whose initial marginal is $f(x)\,dx$, so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths $U^n$, not an arbitrary process with the same one-time marginals.

The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds $\sup_z|(\log f)'''(z)|$, which Theorem 1.1 does not assume, and under $C^2$ alone the uniform convergence over $F_n$ claimed by Lemma 2.6 fails (narrow spikes of $(\log f)''$ far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while $R_n$ and $S_n$ stay close to $I$). Lemma 2.6 is therefore stated with the proof's own assumption, $f\in C^3$ with $(\log f)'''$ bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.

A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.

Selected references

• G. O. Roberts, A. Gelman, W. R. Gilks, Weak convergence and optimal scaling of random walk Metropolis algorithms, Ann. Appl. Probab. 7(1), 110–120, 1997. https://doi.org/10.1214/aoap/1034625254
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• A. Gelman, G. O. Roberts, W. R. Gilks, Efficient Metropolis jumping rules, Bayesian Statistics 5, Oxford University Press, 599–607, 1996.
• G. O. Roberts, J. S. Rosenthal, Optimal scaling for various Metropolis–Hastings algorithms, Statistical Science 16(4), 351–367, 2001. https://doi.org/10.1214/ss/1015346320

Motivation

Every generalization bound in chapters 2-5 is for binary classification. Most real-world classification problems have more than two classes, and the number of classes can itself be in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the margin-based generalization theory of chapter 5 (SVMs) to this multi-class, mono-label setting, using the same Rademacher-complexity machinery as chunk 03-rademacher-vc, but with a new combinatorial ingredient — bounding the Rademacher complexity of a family built by taking a pointwise maximum over several hypothesis sets — needed because a multi-class prediction is itself an argmax over per-class scores.

Setting

A multi-class hypothesis is a scoring function $h:X\times Y\to\mathbb R$ with $Y=\{1,\dots,k\}$ (mono-label case); the predicted label is $\arg\max_y h(x,y)$, and the margin $\rho_h(x,y)=h(x,y)-\max_{y'\ne y}h(x,y')$ (p. 215) is negative exactly when $h$ misclassifies $(x,y)$. The empirical margin loss $\hat R_{S,\rho}(h)$ (Eq. 9.5) uses the same margin-loss function $\Phi_\rho$ (Definition 5.5) as chunk 05-svm, restated locally here. $\Pi_1(H) = \{x\mapsto h(x,y):y\in Y,h\in H\}$ (p. 217) projects a multi-class hypothesis set onto ordinary real-valued functions on $X$ — the object the chapter's Rademacher-complexity bound actually controls, since $H\subseteq\mathbb R^{X\times Y}$ has no norm of its own without such a projection. Lemma 9.1 is a purely combinatorial tool: the empirical Rademacher complexity of a family built by taking the pointwise max over $l$ hypothesis sets is bounded by the sum of their individual empirical Rademacher complexities — used to control the argmax structure of a multi-class prediction. Theorem 9.2 combines this with chunk 03's Rademacher-complexity generalization machinery (Theorem 3.3) to give the chapter's margin bound. Proposition 9.3 and Corollary 9.4 specialize this to kernel-based hypotheses, where each class has its own weight vector in a reproducing kernel Hilbert space and the $k$ weight vectors are jointly constrained by an $L^p$-type group norm $\|W\|_{H,p}\le\Lambda$.

Formalization targets

Lemma 9.1 (milestone). For $F_1,\dots,F_l$ hypothesis sets in $\mathbb R^X$, $l\ge1$, and $G=\{\max\{h_1,\dots,h_l\}:h_i\in F_i\}$: $\hat R_S(G)\le\sum_{j=1}^l\hat R_S(F_j)$.

Theorem 9.2 — the mission's goal. For $H\subseteq\mathbb R^{X\times Y}$, $Y=\{1,\dots,k\}$, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac{4k}\rho R_m(\Pi_1(H)) + \sqrt{\tfrac{\log(1/\delta)} {2m}}.$$

Proposition 9.3 (milestone). For a PDS kernel $K$ with feature map $\Phi$ and $K(x,x)\le r^2$: $R_m(\Pi_1(H_{K,p})) \le \sqrt{r^2\Lambda^2/m}$.

Corollary 9.4 (milestone). Under Proposition 9.3's hypotheses, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H_{K,p}$: $R(h) \le \hat R_{S,\rho}(h) + 4k\sqrt{r^2\Lambda^2/\rho^2/m} + \sqrt{\log(1/\delta)/(2m)}$.

Significance

Theorem 9.2 is the multi-class generalization of chunk 05-svm's Theorem 5.8, and its proof is the chapter's genuine new technique rather than a restatement: it needs a $k$-way application of Lemma 9.1 (once for the argmax structure of the margin, once summing over the $k$ possible labels), which is exactly where the $4k$ factor comes from. Corollary 9.4 is the direct theoretical basis for the multi-class SVM algorithm the chapter derives next (§9.3.1): the displayed dual optimization problem literally minimizes the right-hand side of the corollary's bound. No prior art exists on the platform: GET /theorems?q=multi-class%20classification returns zero hits, and chunk 03's Rademacher-complexity machinery (needed by the proof route) is a draft, not reusable, per the "drafts cannot import drafts" rule.

Difficulty

Lemma 9.1's proof is a genuine two-function argument (max as $\tfrac12(h_1+h_2+|h_1-h_2|)$, Talagrand's lemma applied to $|\cdot|$) generalized to $l$ functions by induction, not a one-line consequence of chunk 03's single-hypothesis-set bound. Theorem 9.2's own proof (PDF pp. 234-236) is the chapter's most involved: it introduces an auxiliary margin function $\rho_{\theta,h}$ with a free parameter $\theta$ later fixed to $2\rho$, splits the resulting Rademacher complexity into a "diagonal" term (bounded via a further one-hot decomposition across the $k$ classes, giving the first factor of $k$) and a "off-diagonal" term bounded via Lemma 9.1 (giving the second factor, folded into the same $4k$ constant). A formalization that stated Theorem 9.2 for $H$ itself rather than $\Pi_1(H)$, or that treated $k$ as an unrelated free constant rather than the actual number of classes, would misstate the theorem — precisely the pitfall BRIEF.md names for this chapter. Proposition 9.3's proof is a clean Cauchy-Schwarz/Jensen argument in the RKHS but needs the $L^p$-group-norm hypothesis class $H_{K,p}$ stated with its exact footnote definition (PDF p. 236), not a simplified $p=2$ special case.

Formalization scope

GeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's MultiClass namespace (the last two identical in content to chunk 03-rademacher-vc's own copies); MarginLossFunction restates chunk 05-svm's Definition 5.5 (the same function, needed here for this chapter's own EmpiricalMarginLoss); IsPDS restates chunk 06-kernels's PDS-kernel definition. All are duplicated rather than imported since a draft item cannot import another chunk's draft module, and none of 03, 05, 06 is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. GeneralizationError is formalized via the book's own established equivalence "$h$ misclassifies $(x,y)$ iff $\rho_h(x,y)\le0$" (the form Theorem 9.2's own proof displays and works with), rather than via an explicit argmax classifier construction — checked as faithful, not a weakening, since it is exactly the quantity the chapter's proof bounds. MarginFunction's ⨆_{y'≠y} is a real supremum rather than a Finset.sup', avoiding a nonempty-finset side proof at definition time; every consuming theorem supplies 2 ≤ k (Y = Fin k) to guard it against trap 5. MaxFamily's index type is Fintype+Nonempty rather than a Finset-cardinality parameter l, a harmless generalization matching "l ≥ 1 hypothesis sets" via Nonempty. IsPDS's feature map Φ and its defining property K(x,y) = ⟪Φ(x),Φ(y)⟫ are supplied as hypotheses to the two kernel theorems rather than as a separate "feature mapping associated to a kernel" definition — the book itself treats this as a given correspondence, not a construction. No numerical constant is altered: 4k/ρ and log(1/δ) in Theorem 9.2, r²Λ²/m in Proposition 9.3, and 4k and r²Λ²/ρ²/m in Corollary 9.4 are exactly as displayed.

Not formalized: §9.1's discussion of the multi-label case (Eq. 9.2/9.3, the Hamming-distance risk) and Eq. 9.4 (empirical Hamming error) — background for a case this chapter's own generalization-bound section (§9.2) does not cover (the mono-label case only); the multi-class SVM primal/dual optimization problems (§9.3.1, an algorithm derived from Corollary 9.4, not a generalization-theoretic theorem); AdaBoost.MH (§9.3.2, a boosting algorithm, analyzed via a convex-surrogate argument rather than the Rademacher-complexity route this mission formalizes); and the uniform-over-$\rho$ extension mentioned at the end of the Theorem 9.2 proof (an unnumbered remark referencing Theorem 5.9's technique from a different chapter, not restated here). Drafting only the algorithmic consequences (the multi-class SVM's optimization problem) in place of the generalization bounds themselves would be this chapter's trivializing formalization.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 9.
• V. Koltchinskii, D. Panchenko, "Empirical margin distributions and bounding the generalization error of combined classifiers," Annals of Statistics 30(1), 2002 (Lemma 9.1's technique).
• K. Crammer, Y. Singer, "On the algorithmic implementation of multiclass kernel-based vector machines," JMLR 2, 2001 (the multi-class SVM algorithm §9.3.1 derives).