Machine Learning

Motivation

In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution $P$ and judged by its risk under that same $P$. In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at $P$ by the worst risk over a neighbourhood of $P$. When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).

Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual $1/\sqrt n$ rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.

Setting

The instance space $\mathcal Z$ is a Polish metric space with metric $d_{\mathcal Z}$ and Borel $\sigma$-algebra; fix $p\ge1$. For Borel probability measures $P,Q$ on $\mathcal Z$, the $p$-Wasserstein distance is

$$W_p(P,Q)=\Bigl(\inf_{M}\ \mathbf E_M[d^p_{\mathcal Z}(Z,Z')]\Bigr)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho>0$, $B^W_{\varrho,p}(P)=\{Q:W_p(P,Q)\le\varrho\}$ is the Wasserstein ball around $P$.

A hypothesis is a function $f:\mathcal Z\to\mathbb R$, read as a loss; a hypothesis class is a set $\mathcal F$ of them. The risk of $f$ under $Q$ is $R(Q,f)=\int f\,dQ$. The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f),\qquad R^*_{\varrho,p}(P,\mathcal F)=\inf_{f\in\mathcal F}R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n\sim P$ with empirical distribution $P_n=\frac1n\sum_i\delta_{Z_i}$, the local minimax ERM is

$$\hat f\in\arg\min_{f\in\mathcal F}R_{\varrho,p}(P_n,f).$$

The standing assumptions are:

• Assumption 1. $\mathcal Z$ is bounded: $\mathrm{diam}(\mathcal Z)=\sup_{z,z'}d_{\mathcal Z}(z,z')<\infty$.
• Assumption 2. Every $f\in\mathcal F$ is upper semicontinuous with $0\le f(z)\le M$.
• Assumption 4. Some $f_0\in\mathcal F$ satisfies $f_0(z)\le C_0\,d^p_{\mathcal Z}(z,z_0)$ for all $z$, for some $C_0\ge0$ and $z_0\in\mathcal Z$.

The complexity of $\mathcal F$ is measured by the entropy integral $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$, where $\mathcal N$ is the covering number of $\mathcal F$ in the uniform norm.

Formalization targets

Goal: Theorem 3, display (11)

Under Assumptions 1, 2 and 4, for every $\delta\in(0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f)-R^*_{\varrho,p}(P,\mathcal F)\le\frac{48\,\mathfrak C(\mathcal F)}{\sqrt n}+\frac{24\,C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}\Bigl(1+\Bigl(\frac{\mathrm{diam}(\mathcal Z)}{\varrho}\Bigr)^p\Bigr)+3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones

1. Proposition 4 (Gao–Kleywegt strong duality): $R_{\varrho,p}(Q,f)=\min_{\lambda\ge0}\{\lambda\varrho^p+\mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$ with $\varphi_{\lambda,f}(z)=\sup_{z'}\{f(z')-\lambda d^p_{\mathcal Z}(z,z')\}$, in the bounded setting.
2. Lemma 2: the optimal dual multiplier of a minimiser of $R_{\varrho,p}(Q,\cdot)$ lies in $\Lambda=[0,\,C_0 2^{p-1}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)]$.
3. (C.2): for an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le\int\varphi_{\lambda^*,f^*}\,d(P_n-P)$.
4. (C.3): $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)\le\sup_{\varphi\in\Phi}\int\varphi\,d(P-P_n)$, with $\Phi=\{\varphi_{\lambda,f}:\lambda\in\Lambda,f\in\mathcal F\}$.
5. (C.4): with probability at least $1-\delta/2$, the left side of (C.3) is at most $2\mathfrak R_n(\Phi)+M\sqrt{2\log(2/\delta)/n}$, where $\mathfrak R_n$ is the expected Rademacher average.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le M\sqrt{\log(2/\delta)/(2n)}$.
7. Lemma 5: $\mathfrak R_n(\Phi)\le\frac{24}{\sqrt n}\mathfrak C(\mathcal F)+\frac{12C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)$.

The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.

Significance

The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when $p>1$: a function with $\sup_{z,z'}(f(z')-f(z))/d^p_{\mathcal Z}(z,z')<\infty$ is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as $\varrho$ grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).

Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.

Difficulty

The obvious argument decomposes the excess risk through $f^*$ and bounds $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)$ by a uniform deviation over $\mathcal F$. That step fails: $R_{\varrho,p}(\cdot,f)$ is a supremum over a ball of measures, not an expectation, so it is not an empirical process in $f$. Passing to the dual makes it one, but the dual multiplier $\hat\lambda$ depends on the sample and has no a priori bound, so the class $\{\varphi_{\lambda,f}\}$ over all $\lambda\ge0$ is too large. Without uniform smoothness of $\mathcal F$ there is no obvious a priori bound on $\hat\lambda$, and the entropy of the resulting two-parameter class must still be controlled at rate $1/\sqrt n$. Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and $\mathrm{diam}(\mathcal Z)$ is Metric.diam Set.univ. Throughout, $p\ge1$ and $\varrho>0$ (the paper's standing choice, p. 3).
• The Wasserstein distance and ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's $\mathcal P_p(\mathcal Z)$ ball.
• Local risks, $\varphi_{\lambda,f}$, $\Lambda$, $\Phi$ and $\mathfrak R_n$ are real-valued suprema and infima, used only for classes bounded in $[0,M]$, where they are finite.
• The sample is a point of $\mathcal Z^n$ under $P^{\otimes n}$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$; this equals the probability when the set is measurable and is stronger otherwise.
• The ERM is a sample-indexed function $\hat f$ with hypotheses $\hat f(\omega)\in\mathcal F$ and minimality of $R_{\varrho,p}(P_n,\cdot)$. These hypotheses presuppose that an empirical minimiser exists, as (7) does. No measurability of $\hat f$ is assumed.
• The covering number is internal (centres in $\mathcal F$). $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$, and every bound containing it assumes $\mathfrak C(\mathcal F)<\infty$: otherwise the paper's bound is $+\infty$, while its conversion to a real number would be $0$.
• Proposition 4 is stated for bounded upper semicontinuous $f$ on bounded $\mathcal Z$, the only case the paper uses. The printed statement covers every usc $f$ and every $Q\in\mathcal P_p(\mathcal Z)$.
• (C.2) and (C.5) assume an achiever $f^*$, as printed; the goal does not.

The following formalizations would trivialize the goal and are ruled out: a bound for each fixed $f\in\mathcal F$ in place of $R^*_{\varrho,p}(P,\mathcal F)$; an $\hat f$ defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite $\mathfrak C(\mathcal F)$.

The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.

Selected references

• J. Lee, M. Raginsky, Minimax statistical learning with Wasserstein distances, NeurIPS 2018; arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• A. Sinha, H. Namkoong, J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1, 1967. https://doi.org/10.1016/0022-1236(67)90017-1

Motivation

In statistical learning a hypothesis $f$ is chosen from a class $\mathcal F$ using $n$ samples drawn from an unknown distribution $P$, and its quality is measured by the risk $R(P,f) = \mathbf E_P[f(Z)]$. When the distribution at deployment time may differ from the one that generated the data (domain drift, adversarial perturbation, model misspecification), a natural replacement is the worst-case risk over a neighbourhood of $P$. Distributionally robust optimization with Wasserstein neighbourhoods takes these neighbourhoods to be balls in an optimal-transport distance, which compare distributions through the geometry of the instance space instead of through likelihood ratios. Wasserstein balls also contain distributions with support different from that of $P$, which divergence balls do not.

J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances (NeurIPS 2018, arXiv:1705.07815), give generalization guarantees for the empirical version of this procedure, the local minimax ERM. Their analysis rests on the strong duality theorem of Gao and Kleywegt (arXiv:1604.02199), which turns the supremum over a Wasserstein ball into a minimization over one real multiplier $\lambda \ge 0$. This mission formalizes their Theorem 2, the excess-risk bound for a class of uniformly Lipschitz hypotheses, together with the steps of its proof. The source is the arXiv v2 preprint, which contains the NeurIPS camera-ready text and the supplementary appendices.

Setting

The instance space $\mathcal Z$ is a Polish space (complete separable metric space) with metric $d_{\mathcal Z}$, and it is bounded: $\operatorname{diam}(\mathcal Z) = \sup_{z,z'} d_{\mathcal Z}(z,z') < \infty$ (Assumption 1). Fix $p \ge 1$. The $p$-Wasserstein distance between Borel probability measures is

$$W_p(P,Q) = \Big(\inf_{M} \mathbf E_M\big[d^p_{\mathcal Z}(Z,Z')\big]\Big)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho > 0$ the ball is $B^W_{\varrho,p}(P) = \{Q : W_p(P,Q) \le \varrho\}$.

The hypothesis class $\mathcal F$ consists of upper semicontinuous functions $f : \mathcal Z \to \mathbb R$ with $0 \le f \le M$ (Assumption 2). The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f) = \sup_{Q \in B^W_{\varrho,p}(P)} R(Q,f), \qquad R^*_{\varrho,p}(P,\mathcal F) = \inf_{f \in \mathcal F} R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n$ from $P$ with empirical distribution $P_n = \frac1n\sum_i \delta_{Z_i}$, the local minimax ERM is $\hat f \in \arg\min_{f \in \mathcal F} R_{\varrho,p}(P_n,f)$.

Assumption 3 asks that every $f \in \mathcal F$ be $L$-Lipschitz with one constant $L$: $f(z') - f(z) \le L\,d_{\mathcal Z}(z',z)$. The complexity of $\mathcal F$ is measured by the entropy integral

$$\mathfrak C(\mathcal F) = \int_0^\infty \sqrt{\log \mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du,$$

where $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ is the covering number of $\mathcal F$ in the uniform metric. The dual integrand of Gao–Kleywegt duality is $\varphi_{\lambda,f}(z) = \sup_{z'}\{f(z') - \lambda d^p_{\mathcal Z}(z,z')\}$.

Formalization targets

Goal: Theorem 2 (10)

Under Assumptions 1–3, for every $\delta \in (0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f) - R^*_{\varrho,p}(P,\mathcal F) \le \frac{48\,\mathfrak C(\mathcal F)}{\sqrt n} + \frac{48 L\cdot\operatorname{diam}(\mathcal Z)^p}{\sqrt n\cdot\varrho^{p-1}} + 3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones, in the order the proof uses them

1. Proposition 4 (8): $R_{\varrho,p}(Q,f) = \min_{\lambda\ge0}\{\lambda\varrho^p + \mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$.
2. Lemma 1: the optimal dual multiplier satisfies $\tilde\lambda \le L\varrho^{-(p-1)}$.
3. (C.2): $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le \int \varphi_{\lambda^*,f^*}\,d(P_n - P)$ for an achiever $f^*$.
4. (C.3) with $\Lambda = [0, L\varrho^{-(p-1)}]$ and $\Phi = \{\varphi_{\lambda,f} : \lambda \in \Lambda, f \in \mathcal F\}$: $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le \sup_{\varphi\in\Phi}\int\varphi\,d(P - P_n)$.
5. (C.4): with probability at least $1-\delta/2$, $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le 2\mathfrak R_n(\Phi) + M\sqrt{2\log(2/\delta)/n}$.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le M\sqrt{\log(2/\delta)/(2n)}$.
7. The Rademacher bound of Appendix C.3: $\mathfrak R_n(\Phi) \le \frac{24}{\sqrt n}\mathfrak C(\mathcal F) + \frac{24L\operatorname{diam}(\mathcal Z)^p}{\sqrt n\,\varrho^{p-1}}$.

Significance

Theorem 2 says that robust ERM over a uniformly Lipschitz class is nearly optimal for the robust risk at the unknown distribution, with excess of order $1/\sqrt n$ and explicit constants. The dependence on $\varrho$ enters only through $\varrho^{-(p-1)}$; at $p = 1$ the bound does not depend on $\varrho$ and recovers the usual rate of ordinary ERM. The paper derives Corollaries 1 and 2 (regression with a Lipschitz link, and Gaussian-kernel classes) and the domain-adaptation bound of Theorem 4 from it. Lemma 1, which confines the dual multiplier to a fixed interval, is also used outside the theorem: Remark 3 proposes it as the search range for the fixed-$\lambda$ adversarial training of Sinha et al.

The result is proved in the paper; to our knowledge none of it has been machine-checked. What this mission adds is a verified version of a complete distributionally robust generalization argument: Gao–Kleywegt strong duality on a bounded Polish space, the multiplier bound, symmetrization and bounded differences for a class indexed by a function and a real parameter, and a Dudley entropy bound for that joint class. The paper's appendix states the Rademacher bound with a stray constant $C_0$ that belongs to a different assumption (Assumption 4); the milestone states the bound without it, which is what the proof gives and what the constant $48L$ of (10) needs.

Difficulty

The obvious route bounds $\sup_{f}|R_{\varrho,p}(P,f) - R_{\varrho,p}(P_n,f)|$ uniformly over $\mathcal F$. That needs uniform control of the dual multiplier for every $f$ and every empirical distribution, and without it the class $\{\varphi_{\lambda,f}\}$ is indexed by an unbounded $\lambda$, so its complexity is infinite. Lemma 1 resolves this only for the minimizers, which is why the argument is organized around $\hat f$ and an achiever $f^*$ rather than a uniform bound.

The formal difficulties are separate. Strong duality with attainment of the minimum is a measure-theoretic theorem about couplings on a Polish space (existence of optimal couplings, measurable selection of near-maximizers), none of which is in Mathlib for Wasserstein balls. The supremum over $\Phi$ must be shown measurable before its expectation means anything. Dudley's chaining bound over a separable, infinite index set is also missing from Mathlib in the form needed here. Finally, the theorem does not assume that $R^*_{\varrho,p}(P,\mathcal F)$ is attained, while the paper's proof uses an achiever $f^*$, so a complete proof needs an approximation argument that the paper does not write out.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances, and Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵). $\operatorname{diam}(\mathcal Z)$ is Metric.diam univ.
• $W_p$ and the ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall. Membership in $\mathcal P_p(\mathcal Z)$ is automatic on a bounded space.
• The standing assumptions $p \ge 1$ and $\varrho > 0$ are binders of every item.
• Risks, the dual integrand $\varphi_{\lambda,f}$ and the Rademacher average are real suprema, infima and Bochner integrals. Under the binders each is over a nonempty set that is bounded on the relevant side, and each integrand is bounded and measurable.
• The covering number is the internal one (centres in $\mathcal F$), valued in $\mathbb N\cup\{\infty\}$, and $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$. Every item whose bound contains $\mathfrak C(\mathcal F)$ assumes $\mathfrak C(\mathcal F) < \infty$ and uses its real value. This is a disclosed pin: otherwise the bound is $+\infty$.
• Assumption 3 is ∀ f ∈ ℱ, ∀ z z', f z' - f z ≤ L * dist z' z, with one $L$ quantified before $\mathcal F$, and $0 \le L$ is a disclosed pin.
• The sample is ω : Fin n → 𝒵 with law Measure.pi (fun _ => P), and $n \ge 1$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$, for $0 < \delta < 1$.
• The ERM is a sample-indexed selection $\hat f$ with membership and minimality hypotheses, never Classical.choose. Such a selection exists exactly when empirical minimizers exist, which display (7) presupposes.
• "min" over $\lambda$ in Proposition 4 includes attainment, and the argmins of Lemma 1 and (C.2) are minimality hypotheses.

Trivializing formalizations are ruled out:

• Assumption 3 is not written with $L$ chosen after $f$, and $L \ge 0$ is not omitted.
• The stray $C_0$ is not in the Lean.
• The goal is about $R^*_{\varrho,p}(P,\mathcal F)$, not about a fixed competitor $f$.
• No probability is converted with toReal, and an infinite $\mathfrak C(\mathcal F)$ is never converted to $0$.

A complete development needs:

• Gao–Kleywegt duality for bounded upper semicontinuous losses;
• McDiarmid's and Hoeffding's inequalities on product measures;
• symmetrization;
• Dudley's entropy integral bound for sub-Gaussian processes indexed by a separable pseudometric space.

The last three are reusable well beyond this mission. Contributions of any of these as stand-alone results are welcome, as are proofs of the milestones.

Selected references

• J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances, Advances in Neural Information Processing Systems 31 (NeurIPS 2018); arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao and A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199
• A. Sinha, H. Namkoong and J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014. https://doi.org/10.1007/978-3-642-54075-2

Motivation

Training data describe one probability distribution, while a deployed prediction rule may be evaluated under a nearby distribution. Distributionally robust learning measures a rule by its worst expected loss over a specified set of nearby laws. This changes the question from how well the rule fits the observed sample to how well it performs when probability mass can move. Wasserstein distance supplies a geometric notion of “nearby”: moving mass farther across the instance space costs more. The setting is relevant to the domain drift discussed by Lee and Raginsky and to Wasserstein robust optimization as developed by Mohajerin Esfahani and Kuhn.

Theorem 1 of Lee and Raginsky's 2018 paper gives a finite-sample answer. It controls the local worst-case risk at the true population law using quantities computed from the empirical law, and also controls the empirical local worst-case risk using population quantities. Both assertions are simultaneous over the entire loss class. This mission concerns exactly those two probability inequalities and the displayed claims in Appendix C.1 that support them. The source is the pinned arXiv:1705.07815v2 preprint, containing the NeurIPS 2018 paper and its supplementary appendix.

Setting

The instance space $\mathcal Z$ is a bounded Polish metric space with distance $d_{\mathcal Z}$. A probability measure $P$ generates $n\ge1$ independent observations $Z_1,\ldots,Z_n$. Their empirical distribution is $P_n=n^{-1}\sum_{i=1}^n\delta_{Z_i}$. A loss $f:\mathcal Z\to\mathbb R$ has risk $R(Q,f)=\int f\,dQ$ under a probability law $Q$. The class $\mathcal F$ consists of upper semicontinuous losses satisfying $0\le f(z)\le M$ for every $f\in\mathcal F$ and $z\in\mathcal Z$, as in Assumption 2 of the paper.

For $p\ge1$, the $p$-Wasserstein distance $W_p(Q,P)$ is the least $p$th-power transport cost over couplings of $Q$ and $P$, raised to the power $1/p$. The Wasserstein ball $B^W_{\varrho,p}(P)$ consists of probability laws $Q$ with $W_p(Q,P)\le\varrho$, where $\varrho>0$. The local worst-case risk is

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f).$$

The dual expression uses the envelope $\varphi_{\lambda,f}(z)=\sup_{z'\in\mathcal Z}\{f(z')-\lambda d_{\mathcal Z}(z,z')^p\}$ for $\lambda\ge0$. To measure the size of $\mathcal F$, let $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ be its uniform-metric covering number at radius $u$. The entropy integral is $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$. These symbols match the local Lean setting and the source's notation.

Formalization targets

Theorem 1: two data-dependent risk bounds

For every $t>0$, the mission goal is the conjunction of the paper's two displays:

$$\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_{P_n}\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2},$$ $$\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P_n,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_P\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2}.$$

The seven milestones preserve displayed claims from Appendix C.1: the deterministic comparison through the supremum deviation $X_\lambda$, its concentration and symmetrization bounds, the entropy-integral estimate with constant $24$, the fixed-$\lambda$ probability bound, and the integer-grid union and comparison with real multipliers. They are statements from the author's argument, ordered by their appearance. The goal retains both directions of the published theorem and every printed constant.

Significance

The first bound provides a sample-dependent certificate for the worst-case population loss of every member of $\mathcal F$ at once. The second compares the robust empirical quantity with a population envelope. Together they make it possible to assess what a local Wasserstein ambiguity set buys in finite samples, rather than relying only on asymptotic convergence. The complexity term depends on the geometry of the loss class through its covering numbers, following a line of empirical-process bounds also seen in Bartlett and Mendelson's study of Rademacher complexity. Lee and Raginsky emphasize that this class complexity can reflect hypotheses outside the support of the data-generating law.

The mathematical theorem is proved in the 2018 paper; the particular declarations in this mission remain open Lean goals. A complete formal development would connect probability inequalities for supremum processes to the published Wasserstein distance and ball, make the entropy integral and its measurability consequences explicit, and verify both directions of the final bound. The reusable output includes a precise internal uniform covering number and a finite-sample Rademacher process for metric-space loss classes.

Difficulty

A fixed multiplier $\lambda$ is easier to control than the infimum over all $\lambda\ge0$. A pointwise concentration bound alone does not produce a simultaneous statement over an uncountable multiplier set. The source's final formula contains a logarithmic multiplier penalty, and retaining its coefficient $M$ and the probability factor $2$ requires accounting for that parameter range exactly. Independently, the supremum over an arbitrary loss class is a genuine random variable only with enough regularity. The boundedness of individual losses does not by itself settle the measurability of their unrestricted supremum.

The envelope $\varphi_{\lambda,f}$ also mixes the metric geometry with empirical-process complexity. Estimating a class of envelopes must remain tied to the covering properties of the original class $\mathcal F$. Replacing the envelope class by a finite hand-picked subclass or assuming the desired concentration inequality as a new hypothesis would change the theorem being formalized.

Formalization scope

Lean uses a metric space with its Borel measurable structure and a Polish-space instance, together with boundedness of the whole carrier. The Wasserstein distance and ball are imported from the published WassersteinLinOpt.Ball definitions. Because the carrier is bounded, every probability measure has a finite $p$th moment, matching the source's $\mathcal P_p(\mathcal Z)$. The ball is a subtype of probability measures; its supremum is taken only over feasible laws. Sample outcomes are functions Fin n → 𝒵, and the product measure gives their independent common law. The empirical law is a normalized finite sum of Dirac masses, while $\mathbb E_{P_n}$ is written as its equal finite average.

The paper does not specify whether covering centres must lie in $\mathcal F$. This formalization uses the internal covering number, whose centres do; its value is at least the external covering number. The entropy integral is extended nonnegative and is required to be finite in statements that convert it to a real number. This disclosed restriction avoids the default conversion of $+\infty$ to zero and supports the separability needed for expected suprema. Milestones using $X_\lambda$ also require $\mathcal F$ to be nonempty, so a real supremum never acquires the empty-family default value. The empty-class case of Theorem 1 remains valid because its failure events are empty.

The source writes minima over nonnegative real multipliers and positive integers. The Lean statements use bounded-below real infima; for the final bound, the appendix's comparison holds at every multiplier, so this reading is at least as strong as the printed minimum. All radii are positive, $p\ge1$, $n\ge1$, and $t>0$ where it appears. Failure probabilities use outer measure of the sample event directly, with no conversion through toReal. The goal never quantifies over arbitrary distributions outside the Wasserstein ball, and expectations of supremum processes are guarded by the finite-entropy hypothesis. Contributions are welcome on the concentration, symmetrization, covering-number, and transport-risk interfaces as well as the goal itself.

Selected references

• Jaeho Lee and Maxim Raginsky, Minimax Statistical Learning with Wasserstein Distances, Advances in Neural Information Processing Systems 31, 2018. arXiv:1705.07815v2.
• Peyman Mohajerin Esfahani and Daniel Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: Performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. DOI:10.1007/s10107-017-1172-1.
• Peter L. Bartlett and Shahar Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. JMLR paper.

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At each step it keeps an exponential moving average $m$ of stochastic gradients and an exponential moving average $v$ of their squared coordinates, corrects both for their initialization at zero (the bias correction), and moves the iterate by $-\gamma\,\hat m/(\varepsilon+\sqrt{\hat v})$ coordinatewise.

Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size $\gamma\to0$ with $1-\alpha\sim a\gamma$ and $1-\beta\sim b\gamma$, the interpolated iterates follow a non-autonomous ordinary differential equation. Their Theorem 3.2 shows that the trajectory of this ODE approaches the critical set of the objective. That leaves open whether the trajectory settles at a single critical point, and how fast. For gradient-like systems the classical answer goes through the Łojasiewicz gradient inequality (Łojasiewicz, 1963, for real-analytic functions), and the dissipative-systems framework of Haraux and Jendoubi (2015) turns such an inequality into convergence with a rate. This mission formalizes the paper's Theorem 3.4, which brings that conclusion to the continuous-time Adam dynamics.

Timeline.

• 1963: Łojasiewicz proves the gradient inequality for real-analytic functions and derives convergence of bounded gradient-flow trajectories.
• 2009: Attouch and Bolte show convergence of the proximal algorithm under the Łojasiewicz property, with rates according to the exponent.
• 2014: Bolte, Sabach and Teboulle prove the same kind of result for proximal alternating linearized minimization.
• 2015: Haraux and Jendoubi collect the continuous-time theory for dissipative autonomous systems.
• 2018–2021: Barakat and Bianchi prove the result for the Adam ODE, which is non-autonomous and has a singular field at $t=0$.

Setting

Let $F:\mathbb R^d\to\mathbb R$ be continuously differentiable with locally Lipschitz gradient $\nabla F$, and let $S:\mathbb R^d\to\mathbb R^d$ be locally Lipschitz. In the paper $F(x)=\mathbb E f(x,\xi)$ and $S(x)=\mathbb E\,\nabla f(x,\xi)^{\odot2}$. Its §7 uses only the two properties above, and so does this mission. Assume $F$ is coercive ($F(x)\to+\infty$ as $\|x\|\to\infty$) and $S(x)>0$ coordinatewise for every $x$. Fix constants $a,b,\varepsilon>0$ with $b\le 4a$.

The state is $z=(x,m,v)\in\mathcal Z=\mathbb R^d\times\mathbb R^d\times\mathbb R^d$, and all vector operations are coordinatewise. The Adam field (3.3) is, for $t>0$,

$$h(t,z)=\Big(-\frac{(1-e^{-at})^{-1}m}{\varepsilon+\sqrt{(1-e^{-bt})^{-1}v}},\ a(\nabla F(x)-m),\ b(S(x)-v)\Big),$$

and (ODE) is $\dot z(t)=h(t,z(t))$. A global solution with initial condition $(x_0,0,0)$ is a continuous $z:[0,+\infty)\to\mathbb R^d\times\mathbb R^d\times[0,+\infty)^d$ that is continuously differentiable on $(0,+\infty)$, satisfies (ODE) for every $t>0$, and has $z(0)=(x_0,0,0)$. The critical set is $\mathcal S=\{x:\nabla F(x)=0\}$.

A number $\theta$ is a Łojasiewicz exponent of $F$ at $x^*$ if there are $c>0$ and $\sigma>0$ with

$$\|\nabla F(x)\|\ \ge\ c\,|F(x)-F(x^*)|^{1-\theta}\qquad\text{whenever }\|x-x^*\|\le\sigma. \tag{3.7}$$

Assumption 3.3 (the Łojasiewicz property) requires an exponent $\theta\in(0,\tfrac12]$ at every $x^*\in\mathcal S$. It holds for real-analytic and semialgebraic $F$.

The proof uses the Lyapunov function $V(t,z)=F(x)+\tfrac12\sum_i m_i^2/U_i(t,v)$, where $U_i(t,v)=a(1-e^{-at})(\varepsilon+\sqrt{v_i/(1-e^{-bt})})$ (3.4)–(3.5). It also uses its perturbation $\tilde W_\delta(t,z)=V(t,z)-\delta\langle\nabla F(x),m\rangle+\delta\|S(x)-v\|^2$ (7.11) and $w_\delta(t)=\tilde W_\delta(t,z(t))$.

Formalization targets

Goal: Theorem 3.4

Assume Assumption 3.3 and that $F(\mathcal S)$ has empty interior in $\mathbb R$. Let $z=(x,m,v)$ be a global solution with initial condition $(x_0,0,0)$. Then there is $x^*\in\mathcal S$ with $x(t)\to x^*$ as $t\to\infty$. Moreover, if $\theta\in(0,\tfrac12]$ is a Łojasiewicz exponent of $F$ at $x^*$, then

$$\|x(t)-x^*\|\le C\,t^{-\frac{\theta}{1-2\theta}}\quad(t>0)\ \text{ if }0<\theta<\tfrac12,\qquad \|x(t)-x^*\|\le C\,e^{-\delta t}\quad(t\ge0)\ \text{ if }\theta=\tfrac12,$$

for a constant $C>0$ (and, in the second case, some $\delta>0$) depending on the trajectory, $x^*$ and $\theta$ but not on $t$.

Milestones

The milestones follow the proof in §7.4:

• the decrease of $V$ along the non-autonomous field (Lemma 7.5, $V$ part);
• convergence to the critical set (Theorem 3.2, restated here);
• the upper bound (7.12) on $w_\delta$ by the four residual terms $|F(x)|$, $\|m\|^2$, $\|\nabla F(x)\|^2$, $\|S(x)-v\|^2$;
• the absolute continuity of $w_\delta$ and the derivative bound (7.13);
• the differential inequality $\dot w_\delta\le-c_4\,w_\delta^{2(1-\theta)}$ of step iv), after the limit value of $F(x(t))$ is normalised to $0$.

Significance

Theorem 3.2 only places the limit points of the trajectory in $\mathcal S$. When $\mathcal S$ contains a continuum of critical points, the trajectory could in principle drift along it forever. Theorem 3.4 excludes this under the Łojasiewicz property. It shows that continuous-time Adam has finite length and converges to one critical point, and it makes the speed explicit. The speed is polynomial with exponent $\theta/(1-2\theta)$ in general and exponential when $\theta=\tfrac12$, which holds for instance at a nondegenerate critical point. The theorem places continuous-time Adam in the same class as gradient flow, heavy-ball dynamics and proximal methods.

The result is proved in the paper (§7.4, with the final integration delegated to arguments of Haraux and Jendoubi). It has not, to current knowledge, been machine-checked. The mission produces a formal proof, together with formal statements of the Lyapunov estimates (7.12)–(7.13) for the Adam ODE. The Łojasiewicz-rate step is reusable for other perturbed gradient-like systems.

Difficulty

The standard Łojasiewicz argument for gradient flow uses $F$ itself as the Lyapunov function, whose derivative is $-\|\nabla F\|^2$. For the Adam ODE neither $F$ nor $V$ works. $V$ decreases only at the rate $\|m\|^2$, which says nothing about $\|\nabla F(x)\|$ when the momentum is small. The system is also non-autonomous, with a field that is singular at $t=0$ and only locally Lipschitz in $z$. As a result $w_\delta$ is only absolutely continuous, so all derivative inequalities hold only almost everywhere. A further obstacle is that the Łojasiewicz inequality at a single critical point does not by itself control the trajectory: the limit set is a connected compact subset of $\mathcal S$, and the inequality has to be made uniform on a neighbourhood of it. Finally, the rate has to be stated for an arbitrary exponent at the limit point, not only for the uniform exponent the argument produces.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and $\mathcal Z$ is the product E × E × E, whose Mathlib norm is the maximum of the three Euclidean norms. This does not change any statement here, which concern $x$, $m$, $v$ separately. $F$ and $S$ are abstract, under the hypotheses of §7 (ContDiff ℝ 1 F, LocallyLipschitz (gradient F), LocallyLipschitz S, $S>0$ coordinatewise, coercivity as Tendsto F (cocompact _) atTop). Under Assumption 2.2 the paper's $F$ and $S$ satisfy these, so the statements imply the printed ones. A solution is a map ℝ → E × E × E constrained only on $[0,\infty)$. The field uses $|v|$ in place of $v$ (the paper's extension, p. 12) and is never evaluated at $t=0$. Statements are made for every global solution; there is exactly one (Theorem 3.1, a separate mission).

The polynomial bound is stated for $t>0$, because Lean's real power gives $0^{-r}=0$ while the paper's right-hand side is $+\infty$ at $t=0$. The constant $C$ is quantified before $t$. A version with $C$ chosen after $t$, or one that assumes $x(t)$ converges, would be trivial and is not the theorem. (7.13) states absolute continuity of $w_\delta$ on every $[1,T]$ together with the almost-everywhere derivative bound, since an almost-everywhere bound alone says nothing about $w_\delta$.

A complete development needs the Lyapunov calculus of §7.1, compactness of the trajectory, the limit-set theory behind Theorem 3.2, the uniformisation of the Łojasiewicz inequality on a compact connected set of critical points, and the Haraux–Jendoubi integration lemmas. Contributions to the last two are reusable beyond this mission and are welcome, as are proofs of the individual milestones.

Selected references

• A. Barakat and P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263v4
• D. P. Kingma and J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, CNRS, 1963, pp. 87–89.
• A. Haraux and M. A. Jendoubi, The Convergence Problem for Dissipative Autonomous Systems, SpringerBriefs in Mathematics, 2015. https://doi.org/10.1007/978-3-319-23407-6
• H. Attouch and J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116, 2009, pp. 5–16. https://doi.org/10.1007/s10107-007-0133-5
• J. Bolte, S. Sabach and M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146, 2014, pp. 459–494. https://doi.org/10.1007/s10107-013-0701-9

Motivation

The Lasso is the standard estimator for high-dimensional linear regression: from $n$ noisy linear measurements of an unknown vector $\beta^*\in\mathbb R^p$, with $p$ possibly much larger than $n$, it minimizes the empirical squared error plus an $\ell_1$ penalty. Its theoretical guarantees are usually stated as sparsity oracle inequalities: the prediction error of the Lasso is bounded by the best trade-off, over all candidate vectors $\beta$, between the approximation error of $\beta$ and a term proportional to the number of nonzero components of $\beta$.

Before this paper, such inequalities for the Lasso carried a leading constant strictly larger than $1$ in front of the approximation error. The inequalities of Bunea, Tsybakov and Wegkamp (EJS 2007) and of Bickel, Ritov and Tsybakov (Ann. Statist. 2009, Theorem 6.1) have this form, and the paper notes that sharpness "was not achieved in the previous work on the Lasso" (p. 24). A leading constant larger than $1$ means the bound is not informative when the true regression function is far from every sparse linear combination: the inequality then only says that the Lasso is within a constant factor of the best approximation.

Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study nuclear-norm penalized estimation of low-rank matrices in the trace regression model. Their general oracle inequality for a linear subspace of matrices (Theorem 2) has leading constant $1$. Restricted to diagonal matrices with a fixed design, the trace regression model becomes ordinary linear regression and the estimator becomes the Lasso. Section 5.4 of the paper draws the consequence: a sharp (leading constant $1$) sparsity oracle inequality for the Lasso with Gaussian noise, Theorem 14. This mission formalizes that theorem. The source is the arXiv preprint arXiv:1011.6256v4.

Setting

Fix integers $n\ge1$ and $p\ge2$ and fixed vectors $x_1,\dots,x_n\in\mathbb R^p$, the rows of the design matrix $\mathbb X=(x_1,\dots,x_n)^\top\in\mathbb R^{n\times p}$. The diagonal elements of the Gram matrix $\frac1n\mathbb X^\top\mathbb X$ are assumed not larger than $1$. The observations are

$$Y_i = x_i^\top\beta^*+\xi_i,\qquad i=1,\dots,n,$$

with $\xi_1,\dots,\xi_n$ independent $\mathcal N(0,\sigma^2)$ random variables, $\sigma>0$.

For $z\in\mathbb R^d$, $|z|_1=\sum_j|z(j)|$, $|z|_2=(\sum_jz(j)^2)^{1/2}$ and $|z|_\infty=\max_j|z(j)|$. For $J\subseteq\{1,\dots,p\}$, $u_J$ agrees with $u$ on $J$ and vanishes on $J^c$. The support of $\beta$ is $J(\beta)=\{j:\beta(j)\neq0\}$ and the sparsity $M(\beta)$ is its cardinality.

Given $\lambda>0$, a Lasso estimator is any minimizer

$$\hat\beta^\lambda\in\arg\min_{\beta\in\mathbb R^p}\Big\{\frac1n\sum_{i=1}^n(Y_i-x_i^\top\beta)^2+\lambda|\beta|_1\Big\}.$$

The restricted constant at $\beta$, with $J=J(\beta)$ and $c_0\ge0$, is

$$\mu_{c_0}(\beta)=\inf\Big\{\mu'>0:\ |u_J|_2\le\mu'\,n^{-1/2}|\mathbb Xu|_2\ \text{ for all } u\in\mathbb R^p \text{ with } |u_{J^c}|_1\le c_0|u_J|_1\Big\},$$

equal to $+\infty$ when the set is empty, and $\mu(\beta)=\mu_5(\beta)$. It is the inverse of a restricted eigenvalue computed at the single support $J(\beta)$; the paper obtains it from its matrix quantity $\mu_{c_0}(A)$ for $A=\operatorname{diag}\beta$. Finally $\mathbf M=\frac1n\sum_i\xi_ix_i$ is the noise vector.

Formalization targets

Goal: Theorem 14 (p. 25)

Let $\lambda=C\sigma\sqrt{\log p/n}$ with $C=3b\sqrt2$, $b\ge1$. With probability at least $1-\frac{1}{p^{b^2-1}\sqrt{\pi\log p}}$,

$$\frac1n|\mathbb X(\hat\beta^\lambda-\beta^*)|_2^2\le\inf_{\beta\in\mathbb R^p}\Big\{\frac1n|\mathbb X(\beta-\beta^*)|_2^2+C^2\sigma^2\frac{\mu^2(\beta)M(\beta)\log p}{n}\Big\}.$$

The event is uniform over all $\beta$, and the statement holds for every Lasso minimizer.

Milestones

1. The cone step ((2.20)–(2.22), p. 11, diagonal case): if $\lambda\ge3\|\mathbf M\|_\infty$ and $\langle\hat\beta-\beta^*,\hat\beta-\beta\rangle_{L_2(\Pi)}>0$, then $|(\hat\beta-\beta)_{J^c}|_1\le5|(\hat\beta-\beta)_J|_1$ for $J=J(\beta)$.
2. Theorem 2 for the Lasso (p. 11 with pp. 11–12, 24–26): deterministically, if $\lambda\ge3\|\mathbf M\|_\infty$,

$$\frac1n|\mathbb X(\hat\beta^\lambda-\beta^*)|_2^2\le\inf_{\beta}\Big[\frac1n|\mathbb X(\beta-\beta^*)|_2^2+\lambda^2\mu^2(\beta)M(\beta)\Big].$$

3. The Gaussian tail bound (proof of Theorem 14, p. 25): $P(|N|>z)\le\sqrt{2/\pi}\,e^{-z^2/2}/z$ for $N\sim\mathcal N(0,1)$, $z>0$.
4. The noise bound (proof of Theorem 14, p. 25): with probability at least $1-\frac{1}{p^{b^2-1}\sqrt{\pi\log p}}$, $\|\mathbf M\|_\infty\le b\sigma\sqrt{2\log p/n}$.

Significance

Theorem 14 gives an oracle inequality for the Lasso whose leading constant is exactly $1$. As a consequence (Corollary 4 of the paper), under the restricted eigenvalue condition RE$(s,5)$ of Bickel, Ritov and Tsybakov the Lasso's prediction error is at most the best $s$-sparse approximation error plus $C^2\sigma^2M(\beta)\log p/(n\kappa^2(s,5))$, which improves the non-sharp inequality of that paper. The bound also shows that the matrix-valued argument of the paper, written for nuclear-norm penalization, specializes cleanly to the vector case; the same argument underlies the matrix completion results of the other missions of this series.

The result is proved in the paper. As far as a search of the platform shows, no formal proof of a sharp oracle inequality for the Lasso exists; the platform has the non-sharp Bickel–Ritov–Tsybakov inequality as an open statement (LassoDantzig.Oracle.theorem_6_1). This mission produces a machine-checked version of the deterministic inequality, of the Gaussian concentration step, and of their combination, with the restricted constant defined exactly as in the paper.

Difficulty

The deterministic part is where the obvious argument fails. The usual Lasso analysis compares the objective at $\hat\beta$ and at a candidate $\beta$, controls the noise cross term, and rearranges; every version of that argument in the earlier literature loses a multiplicative factor in front of the approximation error $\frac1n|\mathbb X(\beta-\beta^*)|_2^2$, and the factor cannot be pushed to $1$ by tuning constants. The sharp bound has to come from a finer use of the optimality of $\hat\beta$, and the cone constant $5$ in $\mu(\beta)=\mu_5(\beta)$ is tied to the threshold $\lambda\ge3\|\mathbf M\|_\infty$. Formally, optimality conditions for a nonsmooth convex function on $\mathbb R^p$ (the subdifferential of $|\cdot|_1$) are infrastructure that has to be in place.

The probabilistic part needs the distribution of a linear combination of independent Gaussians, a Mills-ratio tail bound that is not in Mathlib, and a union bound over $p$ coordinates, with the exact constants of the paper.

Formalization scope

Vectors are functions Fin p → ℝ, and the design is given by its rows x i : Fin p → ℝ. All statements are in vector form, as the paper itself writes Section 5.4; no matrix library is needed. The Lasso is an argmin predicate, and statements hold for every minimizer; in the goal, $\hat\beta$ is a function of the outcome that is a minimizer at every outcome, and no measurability of $\hat\beta$ is assumed (the bad event is bounded in outer measure).

The restricted constant is formalized through its witnesses: the theorems hold for every $\mu'$ in the set whose infimum is $\mu(\beta)$. This is equivalent to the infimum, because the bounds are continuous and increasing in $\mu'$. A real-valued infimum would be $0$ on an empty set and would make the oracle inequality false, so it is deliberately not used. The infimum over $\beta$ is stated as "for every $\beta$", inside the event.

Hypotheses added relative to the page, each disclosed in the item's Formalization Note: $p\ge2$ (for $p=1$, $\log p=0$ and the printed probability divides by zero), $n\ge1$, $\sigma>0$, and measurability of the noise variables. $\lambda>0$ is the paper's standing assumption. The condition $\lambda\ge3\|\mathbf M\|_\infty$ is written coordinatewise. In the deterministic milestones the noise is a fixed vector and $\mathbf M=\frac1n\sum_i\xi_ix_i$, which is the paper's $\mathbf M$ for a fixed design and centred noise. No printed slip affects these statements. The constant $C=3b\sqrt2$ is kept as printed.

A trivializing formalization would assume the event $\|\mathbf M\|_\infty\le b\sigma\sqrt{2\log p/n}$ in the goal, or use a real infimum for $\mu(\beta)$; both are ruled out. Contributions of reusable infrastructure are welcome: the Gaussian tail bound, the law of a weighted sum of independent Gaussians, and the subdifferential of the $\ell_1$ norm.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4 (2016); Ann. Statist. 39(5), 2011. https://arxiv.org/abs/1011.6256
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 2009. https://doi.org/10.1214/08-AOS620
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 2007. https://doi.org/10.1214/07-EJS008
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Statist. Soc. B 58(1), 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

Motivation

In the local model of differential privacy, no trusted curator holds the data: each individual randomizes their own record before handing it to the analyst. This is the model of randomized response in survey statistics and of the privacy-preserving telemetry deployed by large software vendors. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090), asked which learning tasks remain possible in this model. Their answer (§5) is that local algorithms are exactly as powerful as statistical query (SQ) algorithms in the sense of Kearns (J. ACM 1998), up to polynomial factors. This mission formalizes one direction of that equivalence: every local algorithm run on i.i.d. data can be simulated by an SQ algorithm.

This is the fourth of five missions on the paper. Mission III formalizes the converse direction (Theorem 5.7). All theorem numbers refer to arXiv:0803.0924v3.

Setting

A database is $z=(z_1,\dots,z_n)\in D^n$. Here its entries are drawn i.i.d. from a probability distribution $P$ on $D$.

• An $\varepsilon$-local randomizer (Definition 5.1) is a randomized map $R:D\to W$ to a discrete set $W$ such that $\Pr[R(u)=w]\le e^{\varepsilon}\Pr[R(u')=w]$ for all $u,u'\in D$ and $w\in W$.
• An $\varepsilon$-local algorithm $A$ making $t$ queries (Definitions 5.2, 5.3) sees the database only through an LR oracle. At its $k$-th call it names an index $i_k$ and an $\varepsilon_k$-local randomizer $R_k$, both possibly depending on its earlier answers, and receives a fresh sample of $R_k(z_{i_k})$. For each index $i$ the budgets of the calls on $i$ sum to at most $\varepsilon$. $A$ is noninteractive if its calls do not depend on earlier answers. Its output is a function of the $t$ answers. Its output distribution is taken over $z\sim P^n$ and the randomizers' coins.
• An SQ oracle for $P$ (Definition 5.4) answers a query $(g,\tau)$, with $g:D\to[-1,1]$ and tolerance $\tau$, with any number $v$ such that $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. It may choose its answers adversarially and adaptively.
• An SQ algorithm $B$ (Definition 5.5) accesses $P$ only through such an oracle. It may use its own coins, and the number of queries it makes may be random and unbounded.
• The statistical difference of two distributions on a discrete space (p. 8) is $\max_S|\mu(S)-\nu(S)|$.

Formalization targets

Goal: Lemma 5.8 (p. 21)

There is an absolute constant $C$ such that for every $\varepsilon$-local algorithm $A$ making $t$ queries there is an SQ algorithm $B$ with the following properties against every distribution $P$ and every valid oracle:

$$\tau=\frac{\beta}{3e^{2\varepsilon}t},\qquad \mathbb E[\#\text{queries of }B]\le C\,t\,e^{\varepsilon},\qquad \mathrm{SD}\bigl(B,\ A(z),\ z\sim P^n\bigr)\le\beta .$$

The constant $C$ is the paper's $O(\cdot)$. The tolerance is the proof's own choice.

Milestones

1. Display (5) (p. 22): a single query estimates $p(w)=\Pr_{z_i\sim P}[R(z_i)=w]$ within a factor $1\pm\beta/(3t)$, whatever valid answer the oracle gives.
2. One rejection-sampling iteration (p. 23): every iteration terminates with probability at least $\frac{1-\varphi}{1+\varphi}e^{-\varepsilon}$. Conditioned on terminating, it outputs $w$ with probability in $(1\pm3\varphi)p(w)$.
3. The interactive estimate (p. 24): two queries estimate the conditional probability of the next answer given earlier answers on the same entry, within a factor $1\pm3e^{2\varepsilon}\tau$.
4. Claim 5.9 (p. 22): the noninteractive case, with the explicit bound $2t\,e^{\varepsilon}$ on the expected number of queries.

Significance

The result. Lemma 5.8, combined with Theorem 5.7, shows that a concept class is learnable by a locally private algorithm if and only if it is learnable with statistical queries (Theorem 5.14). Every SQ lower bound therefore becomes a lower bound for local privacy. For instance, parity functions are privately learnable by a centralized algorithm (Theorem 4.4) but not by a local one, because parities need exponentially many statistical queries (Corollary 5.15, which also uses the SQ lower bound of Blum et al., STOC 1994).

Formalizing it. The result is proved on paper. As far as we know it has no machine-checked proof. The paper's proof is a few paragraphs and leaves the model implicit: what an SQ algorithm with a random number of queries is, how an adversarial oracle interacts with it, and in what sense the per-randomizer errors add up over $t$ adaptively chosen randomizers. The formal statement makes each of these explicit. The milestones isolate the estimates the proof uses, so they can be proved independently of the composition argument.

Difficulty

The estimates in the milestones are elementary inequalities. The difficulty is in the goal. First, the oracle's answers, and therefore the estimates $\tilde p(w)$, change from iteration to iteration, so the simulated distribution is not a fixed rejection sampler: the output law must be controlled iteration by iteration against an adversary. Second, the SQ algorithm has no bound on its number of steps. Its output law is a limit over an unbounded run, and its query count is an expectation that is finite only because every iteration terminates with probability bounded away from zero. Third, in the interactive case the randomizers applied to one entry are correlated through the entry. The simulation must sample from the conditional law given earlier answers on that entry, while the errors of all $t$ steps combine along adaptively chosen histories.

Formalization scope

• Local randomizers have discrete output: R u : PMF W. The simulation uses the point probabilities $\Pr[R(z_i)=w]$. Every map $u\mapsto\Pr[R(u)=w]$ is required to be measurable.
• A local algorithm makes exactly $t$ calls. Its index, randomizer and budget at call $k$ are functions of the earlier answers. The budget is required along every answer sequence. Its own coins are calls to $0$-local randomizers.
• An SQ algorithm is a state machine with a random start, random transitions depending on the answer, and an output on stopping. Its output law is a sub-probability mass function. Its expected query count lies in $[0,\infty]$ and counts every query, including those in rejected iterations.
• The oracle is an arbitrary deterministic function of the whole state trajectory, constrained only by Definition 5.4. The conclusions must hold for every valid oracle, not for the exact-mean oracle alone.
• $B$ is quantified before $P$ and sees $P$ only through answers, and every query of $B$ is a measurable $[-1,1]$-valued function with tolerance exactly $\beta/(3e^{2\varepsilon}t)$. Without these two constraints the statement would be trivial: $B$ could hard-code $P$, or rescale a query to shrink its effective tolerance.
• The constant $C$ is quantified outside every other object.
• The implicit hypotheses $\varepsilon>0$ (the queries divide by $e^{\varepsilon}-e^{-\varepsilon}$), $0<\beta\le1$ and $t\ge1$ (so that $\varphi=\beta/(3t)\le1/3$ and $\tau$ is defined) are stated. The paper's reference input $\mathbf 0$ is an arbitrary point $u_0\in D$.
• Claim 5.9 states "$t\cdot e^{\varepsilon}$ queries". Its proof gives at most $2t\,e^{\varepsilon}$, which is the bound stated.
• The paper's refinement "noninteractive $A$ yields nonadaptive $B$" is not formalized. The simulation decides from each answer whether to stop, and so which randomizer the next query belongs to. It therefore does not prepare its queries before receiving answers in the sense of Definition 5.5. The goal is the adaptive statement for all local algorithms, which contains the noninteractive case. Claim 5.10, whose statement coincides with this goal, is represented by its estimate (milestone 3) rather than restated.
• The statistical difference is valued in $[0,\infty]$, which avoids junk values of a real supremum.

Reusable beyond this mission: the SQ-algorithm state machine with expected query count, the statistical difference of sub-probability mass functions, and the model of interactive local algorithms. Welcome contributions include proofs of the estimate milestones, a general lemma bounding the statistical difference of sequentially composed approximate samplers, and the termination and expected-runtime analysis of rejection sampling with varying acceptance probabilities.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826; cited from arXiv:0803.0924v3. https://arxiv.org/abs/0803.0924 · https://doi.org/10.1137/090756090
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/10.1145/293347.293351
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly learning DNF and characterizing statistical query learning using Fourier analysis, STOC 1994, 253–262. https://doi.org/10.1145/195058.195147
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• S. L. Warner, Randomized response: a survey technique for eliminating evasive answer bias, J. Amer. Statist. Assoc. 60 (1965) 63–69. https://doi.org/10.1080/01621459.1965.10480775