Machine Learning

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

A data curator holds a database of $n$ records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class $C$ to error $\alpha$ once the database has size roughly $\log|X| \cdot \mathrm{VCDIM}(C)/(\alpha^3\epsilon)$, so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.

This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than $\mathrm{VCDIM}(C)/2$ records, every differentially private mechanism has constant error on some query of $C$. The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.

Setting

Let $X$ be a set (the data universe). An input database of size $n$ is a tuple $z = (z_1,\dots,z_n) \in X^n$. A predicate is a map $\varphi : X \to \{0,1\}$, and its counting query is

$$Q_\varphi(z) = \frac{1}{n}\,\#\{i : \varphi(z_i) = 1\}.$$

A class $C$ of predicates is identified with its class of counting queries. A finite set $S \subseteq X$ is shattered by $C$ if every function $S \to \{0,1\}$ is the restriction of some $\varphi \in C$; the VC-dimension $\mathrm{VCDIM}(C) \in \mathbb N \cup \{\infty\}$ is the supremum of the sizes of shattered sets.

A mechanism $M$ maps each input $z \in X^n$ to a probability distribution $M(z)$ on an output space $O$; an output $o$ is read through an answer map $\mathrm{ans}(o, \varphi) \in \mathbb R$. Two inputs are neighbours if they differ in exactly one entry. The mechanism is $\epsilon$-differentially private if $M(z)(E) \le e^{\epsilon} M(z')(E)$ for all neighbours $z, z'$ and all measurable events $E$. It is $(\alpha,\delta)$-useful for $C$ if for every input $z$, with probability at least $1-\delta$ over $o \sim M(z)$, every query is answered to within $\alpha$:

$$\forall \varphi \in C:\quad |\mathrm{ans}(o,\varphi) - Q_\varphi(z)| \le \alpha .$$

In the paper the output is a synthetic database $\hat D$ and $\mathrm{ans}(\hat D,\varphi) = Q_\varphi(\hat D)$.

Formalization targets

Goal: Theorem 3.11 (p. 11)

There is an absolute constant $c > 0$ such that for every universe $X$, class $C$, size $n \ge 1$ with $n \le \mathrm{VCDIM}(C)/2$, $0 \le \epsilon \le 1$ and $0 < \delta \le 1/4$: every $\epsilon$-differentially private mechanism that is $(\alpha,\delta)$-useful for $C$ on databases of size $n$ satisfies

$$\alpha \ \ge\ \frac{c}{4 + 16\epsilon}.$$

Milestones

1. Lemma 3.12. For a set $S$ of size $d$ and the family $\mathcal D_S$ of its subsets of size $d/2$, and $Q_T$ the counting query of a predicate equal to the indicator of $T$ on $S$: $Q_T(T) - Q_T(T') = |T\Delta T'|/d$ for $T, T' \in \mathcal D_S$.
2. Lemma 3.13. For an $(\alpha,\delta)$-useful mechanism, a fixed procedure recovers from $M(T)$ a set $T' \in \mathcal D_S$ with $|T'\Delta T| \le 2d\alpha$, with probability at least $1-\delta$.
3. The final inequality of the proof (p. 12), with $\delta$ kept. Under the goal's hypotheses with $0 < \delta < 1$ and any $\epsilon$:

$$(1-\delta)(1-2\alpha) \ \le\ e^{\epsilon}(\delta + 2\alpha).$$

Significance

Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension $d$, no private mechanism is accurate on databases of size below $d/2$, whatever its running time. It thereby locates the sample complexity of private query release between $\mathrm{VCDIM}(C)$ and $\mathrm{VCDIM}(C)\cdot\log|X|$ up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).

The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability $\delta$ of the two reconstructions, and keeping it shows that the conclusion requires $\delta$ below $1/(1+e^{\epsilon})$, not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.

Difficulty

The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random $T \in \mathcal D_S$, a random element $x \in T$ and a random $y \notin T$, and the swapped set $\hat T = (T\setminus\{x\})\cup\{y\}$. Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls $|T'\Delta T|$, not whether a particular element is recovered. The "probabilities" $\Pr[x \in T']$ of the printed proof mix the mechanism's randomness with the random choice of $T$, $x$, $y$, and they are not the probability of any single event under any single $M(z)$, so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability $\delta$ must be carried through both reconstructions. A proof that sets $\delta = 0$, as the printed one does, does not prove the stated theorem.

Formalization scope

• Databases. Inputs are Fin n → X with $n \ge 1$; the empty database is excluded because every mechanism is private on it and $Q_\varphi = 0/0$ there. In the proof, a set $T \in \mathcal D_S$ is given to the mechanism as any injective listing of its elements.
• Neighbours. The paper's "$|D\Delta D'| \le 1$" for databases of equal size is read as replacing one entry (PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading $T$ and $\hat T$ are neighbours, so the paper's factor $e^{2\epsilon}$ becomes $e^{\epsilon}$.
• Mechanisms. The output space is an arbitrary measurable space and answers are read through ans. Synthetic-data mechanisms are the special case $O =$ databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for $\varphi \in C$. Without the first, the zero measure is private; without the second, a mechanism into a trivial $\sigma$-algebra would be private and "useful".
• Ω and the range of δ. The paper writes $\alpha \ge \Omega(1/(4+16\epsilon))$ for "$0<\delta<1$ bounded away from 1 by a constant". The Lean goal quantifies one absolute constant $c > 0$ before every other binder and assumes $0 < \delta \le 1/4$. The proof gives $\alpha \ge ((1-\delta) - e^{\epsilon}\delta)/(2(1-\delta+e^{\epsilon}))$, which is positive only for $\delta < 1/(1+e^{\epsilon})$ (about $0.27$ at $\epsilon=1$). The hypotheses $\epsilon \le 1$ and $n \le \mathrm{VCDIM}(C)/2$ are the paper's, the latter written $2n \le \mathrm{VCDIM}(C)$ in $\mathbb N\cup\{\infty\}$.
• Ruled out. The statement quantifies over every mechanism satisfying the hypotheses, randomized or not, so no restriction to deterministic or constant-output mechanisms makes the bound easy. The usefulness event is weighed by a probability measure, so the zero measure cannot be "useful". The constant cannot depend on $n$, $d$, $X$ or $C$.
• Infrastructure. The development reuses the published PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and $2n \le \mathrm{VCDIM}(C)$ yields a shattered set of size exactly $2n$; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1 (2011); J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229 , https://doi.org/10.1145/2450142.2450148
• 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
• I. Dinur, K. Nissim, Revealing Information while Preserving Privacy, PODS 2003. https://doi.org/10.1145/773153.773173
• M. Bun, J. Ullman, S. Vadhan, Fingerprinting Codes and the Price of Approximate Differential Privacy, STOC 2014. https://arxiv.org/abs/1311.3158
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §8.3 (VC dimension). https://doi.org/10.1017/9781108231596

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

Motivation

A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.

Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.

Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set of players $N$, a finite strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$. A probability distribution $\psi$ on $S$ is a correlated $\varepsilon$-equilibrium if for every player $i$ and all $j,k\in S^i$

$$\sum_{s:\,s^i=j}\psi(s)\,[u^i(k,s^{-i})-u^i(s)]\le\varepsilon ;$$

a correlated equilibrium is the case $\varepsilon=0$.

The game is played at $t=1,2,\dots$, producing a history $h_t=(s_1,\dots,s_t)$. For $j,k\in S^i$ the regret of player $i$ is

$$D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}[u^i(k,s^{-i}_\tau)-u^i(s_\tau)],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}:$$

the average gain player $i$ would have had by playing $k$ every time they played $j$. Fix $\mu$ with $\mu>2M^i(m^i-1)$ for every $i$, where $M^i\ge|u^i|$ and $m^i=|S^i|$. Under regret matching (2.2), if player $i$ last played $j$, then at $t+1$ they play each $k\ne j$ with probability $R^i_t(j,k)/\mu$ and repeat $j$ with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t:s_\tau=s\}|$.

Formalization targets

Goal: the Main Theorem

Almost surely, $z_t$ converges to the set of correlated equilibria:

$$P\Big(\forall\varepsilon>0\ \exists T\ \forall t>T\ \exists\psi\ \text{correlated equilibrium with } \operatorname{dist}(z_t,\psi)<\varepsilon\Big)=1 .$$

This is convergence to a set, not to a point; the paper notes that $z_t$ need not converge.

Milestones

They follow the Appendix proof:

• the PROPOSITION (§3), a deterministic equivalence: $\limsup_t R^i_t(j,k)\le\varepsilon$ for all $i$ and $j\ne k$ iff $z_t$ converges to the set of correlated $\varepsilon$-equilibria;
• positivity of the diagonal of the transition matrix $\Pi_t$ of (2.2);
• Steps M1–M11, with the two LEMMAs used in the proofs of M4 and M7.

The squared distance $\rho_t=\sum_{j\ne k}[R_t(j,k)]^2$ satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives

$$E[(t+v)^2\rho_{t+v}\mid h_t]\le t^2\rho_t+O(v^3+tv^{1/2})\qquad\text{(M8)}.$$

Along $t_n=\lfloor n^{5/3}\rfloor$ this gives $\rho_{t_n}\to0$ a.s. (M9–M10), and then $R_t(j,k)\to0$ a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.

Significance

The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.

Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.

Difficulty

The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of $\Pi_t$, which is the procedure of Theorem A, but regret matching uses a row of $\Pi_t$ instead. The cross term of the one-step recursion therefore does not vanish.

The proof has to work over blocks of $v$ periods. Within a block the players' choices are not independent given $h_t$, because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time $t$. The matrix-power estimate cannot use convergence of $\Pi_t^w$, since only the diagonal of $\Pi_t$ is known to be positive and $\Pi_t$ may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors $w^2/t$ and $w^{-1/2}$, which is why the subsequence $t_n=\lfloor n^{5/3}\rfloor$ appears.

Formalization scope

Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. $\Delta(Q)$ is Mathlib's stdSimplex. Time is 0-based: play τ is $s_{\tau+1}$, and a history is a tuple Fin t → ∀ i, S i. Regrets, $z_t$, $\Pi_t$ and $\rho_t$ are deterministic functions of a finite history. Every statement has $t\ge1$, because the Lean value at $t=0$ is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given $h_t$ assume $P[h_t]>0$. The auxiliary $\hat s$-process is encoded by its explicit law, a power of the product transition matrix. The paper's $O(\cdot)$ (footnote 34) is a constant chosen after the game, $M$ and $\mu$ and before the initial play, the probability space and the play. Distances on $\mathbb R^S$ are sup distances.

The hypotheses are exactly footnote 5's: $|u^i|\le M^i$ and $\mu>2M^i(m^i-1)$, with one $\mu$ for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than $\varepsilon$, not with a distance to a possibly empty set, so no encoding makes it vacuous.

Disclosed choices:

• the LEMMA of M7 is stated with a constant that depends only on a lower bound on the diagonal, which is what the proof gives and what M7 uses;
• the PROPOSITION states $\limsup\le\varepsilon$ as "for every $\delta>0$, eventually $\le\varepsilon+\delta$";
• the strong law assumes each $X_n$ is measurable and in $L^2$.

Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.

Selected references

• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• D. Fudenberg and D. K. Levine, Conditional Universal Consistency, Games and Economic Behavior 29 (1999), 104–130. https://doi.org/10.1006/game.1998.0705
• D. Blackwell, An Analog of the Minimax Theorem for Vector Payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Loève, Probability Theory II, 4th ed., Springer (1978), Theorem 32.1.E.

Motivation

A model trained to minimize its average loss $\mathbb E_{P_0}[\ell(\theta;X)]$ can perform poorly on subpopulations that are rare under the training distribution $P_0$. Distributionally robust optimization replaces the average loss by its worst case over all distributions $Q$ close to $P_0$ in an $f$-divergence, which upweights the tail of the loss and controls performance on every subpopulation of sufficient size. Duchi and Namkoong (arXiv:1810.08750, Ann. Statist. 49 (2021), DOI 10.1214/20-AOS2004) study this objective for the Cressie–Read family of divergences, which interpolates between the $\chi^2$-divergence and the KL-divergence and links the robust risk to $L^{k_*}$-norms of the loss.

In practice $P_0$ is unknown and the robust risk is computed on the empirical distribution $\widehat P_n$ of a sample. Whether this plug-in estimate is close to the population robust risk, and at what rate, is the question this mission formalizes. Earlier work on the same estimator (Namkoong and Duchi 2017; Duchi, Glynn and Namkoong 2021) let the radius shrink as $\rho/n$; here the radius $\rho>0$ is fixed, so the robust risk is a genuinely different functional of $P_0$ from the mean.

Setting

Let $(\mathcal X,\mathcal A)$ be a measurable space, $P_0$ a probability measure on it, $\Theta$ a parameter set and $\ell:\Theta\times\mathcal X\to\mathbb R$ a loss. Fix $k\in(1,\infty)$, write $k_*=k/(k-1)$, and fix a radius $\rho>0$.

The Cressie–Read function is $f_k(t)=\frac{t^k-kt+k-1}{k(k-1)}$ for $t\ge0$ and $f_k(t)=+\infty$ for $t<0$. It is convex, nonnegative and vanishes at $t=1$. The Cressie–Read divergence of $Q\ll P$ from $P$ is $D_{f_k}(Q\|P)=\mathbb E_P[f_k(dQ/dP)]$.

The robust risk at $\theta$ under $P$ is

$$\mathcal R_k(\theta;P)=\sup_{Q\ll P}\big\{\mathbb E_Q[\ell(\theta;X)]:D_{f_k}(Q\|P)\le\rho\big\} =\sup\big\{\mathbb E_P[L\,\ell(\theta;X)] : L\ge0,\ \mathbb E_P[L]=1,\ \mathbb E_P[f_k(L)]\le\rho\big\},$$

the second form writing $L=dQ/dP$ for the likelihood ratio. Let $X_1,\dots,X_n$ be i.i.d. with law $P_0$ and $\widehat P_n=\frac1n\sum_{i=1}^n\delta_{X_i}$ their empirical measure. With $c_k(\rho)=(1+k(k-1)\rho)^{1/k}$ and $Z=\ell(\theta;\cdot)$, the dual objective is

$$g_k(\eta;P)=c_k(\rho)\,\mathbb E_P\big[(Z-\eta)_+^{k_*}\big]^{1/k_*}+\eta ,\qquad\eta\in\mathbb R .$$

The Lean development uses the same names: cressieRead, robustRisk, empiricalMeasure, dualObjective, kstar, ck, in the namespace UniformDRO.Concentration.

Formalization targets

Goal: Theorem 2 (p. 20)

Assume $\ell(\theta;x)\in[0,M]$ for all $\theta,x$, with $M\ge1$. For a fixed $\theta\in\Theta$ and $t>0$, whenever $n\ge k\vee3$, with probability at least $1-2e^{-t}$,

$$\big|\mathcal R_k(\theta;\widehat P_n)-\mathcal R_k(\theta;P_0)\big|\le10\,n^{-\frac1{k_*\vee2}}\,c_k(\rho)^2M\Big(\frac{c_k(\rho)}{c_k(\rho)-1}\vee2\Big)\Big(\frac1k+\sqrt{t+2\log n}\Big).$$

The goal is stated exactly as printed, constants included.

Milestones (Appendices A.1 and C.1)

1. Lemma 3 (p. 33): the conjugate $f_k^*(s)=\frac1k((k-1)s+1)_+^{k_*}-\frac1k$.
2. Lemma 1 (p. 6): the duality $\mathcal R_k(Z;P)=\inf_{\eta}g_k(\eta;P)$.
3. Lemma 6 (p. 38): two-sided concentration of convex Lipschitz functions of bounded independent variables, referenced from an existing platform statement.
4. Lemma 7 (p. 38): $y\mapsto(\frac1n\sum_i|y_i|^{k_*})^{1/k_*}$ is $n^{-1/(2\vee k_*)}$-Lipschitz in $\|\cdot\|_2$.
5. (28) (p. 39): for fixed $\eta$, $g_k(\eta;\widehat P_n)$ is within $\sqrt{2t}\,c_k(\frac{c_k}{c_k-1}\vee2)Mn^{-1/(k_*\vee2)}$ of its mean with probability $1-2e^{-t}$.
6. Lemma 8 (p. 39): the bias bound $\mathbb E[(\frac1n\sum_i|Y_i|^{k_*})^{1/k_*}]\ge\mathbb E[|Y|^{k_*}]^{1/k_*}-\frac2k\,C\,n^{-1/(k_*\vee2)}$ (corrected, see below).
7. (30) (p. 39): for fixed $\eta$, $|g_k(\eta;\widehat P_n)-g_k(\eta;P_0)|\le\epsilon_t$ with probability $1-2e^{-t}$ (corrected).
8. Lemma 9 (p. 39): for $Z\in[0,M]$ the infimum over $\eta$ may be restricted to $[-\frac{M}{c_k-1},M]$.
9. Union bound (p. 40): $|\mathcal R_k(Z;\widehat P_n)-\mathcal R_k(Z;P_0)|\le(2c_k+3)\epsilon_{t,n}$ with probability $1-2\exp(-t+\log(\frac{c_k}{c_k-1}\frac{M}{\epsilon_{t,n}}))$.

Significance

The result. Theorem 2 shows that the plug-in robust risk is a consistent estimator of the population robust risk for a fixed divergence radius, at rate $n^{-1/(k_*\vee2)}$ up to a $\sqrt{\log n}$ factor; Theorem 3 of the same paper shows this rate cannot be improved in general. Through a covering argument it yields uniform bounds over a model class (Corollaries 1–2, p. 20) and hence guarantees for the plug-in minimizer $\widehat\theta_n$: the robust risk of the learned model is close to the best achievable robust risk. The rate degrades as $k\downarrow1$, quantifying the statistical price of protecting against larger distribution shifts.

Formalizing it. The result is proved on paper; no machine-checked version exists. A formal proof requires a measure-theoretic duality theorem for $f$-divergence balls (Lemma 1), convex concentration for product measures (Lemma 6, posed on the platform and not yet proved), and a moment bias bound (Lemma 8). Formalization already exposed two slips in the printed proof, both corrected in the milestones without changing Theorem 2.

Difficulty

The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so concentration cannot be read off any single empirical average. The argument goes through the dual: Lemma 1 reduces the robust risk to a one-dimensional infimum of $g_k$, which is a Lipschitz function of the data only for $\eta$ in a bounded interval (Lemma 9), and only up to a bias, because $g_k(\eta;\widehat P_n)$ is a nonlinear (norm-like) function of an empirical mean. Neither half is routine: the duality for general $P$ requires the closed form of $f_k^*$ and an attained infimum over $\lambda\ge0$, and the bias bound (Lemma 8) needs a careful case split at $k_*=2$. The naive approach — concentrating $\mathbb E_{\widehat P_n}[L\,Z]$ for a fixed $L$ — fails because the optimal $L$ depends on the sample.

Formalization scope

• The robust risk is defined in the likelihood-ratio form (3): a real supremum over measurable $L\ge0$ with $\mathbb E_P[L]=1$, $\mathbb E_P[LZ]$ integrable, and the divergence constraint written as a lower Lebesgue integral of $f_k(L)\ge0$, so ratios of infinite divergence are excluded. Every statement about it assumes a bounded loss (or $Z\in L^{k_*}(P)$ in Lemma 1), which makes the value set nonempty and bounded above. The published conjugate PhiDivRobust.Counterpart.conj is reused for Lemma 3.
• The sample is a point of $\mathcal X^n$ under the product measure $P_0^{\otimes n}$; $\widehat P_n=\frac1n\sum_i\delta_{X_i}$; failure events are bounded in outer measure. Real powers are Real.rpow; Euclidean distances on $\mathbb R^n$ are written out as $\sqrt{\sum_i(y_i-y_i')^2}$, since the default norm on Fin n → ℝ is the sup norm.
• Standing assumptions of Section 4 (p. 19), carried as hypotheses: $k\in(1,\infty)$, $\ell\in[0,M]$ with $M\ge1$. Added and disclosed: measurability of the loss, $n\ge1$ where the page leaves it implicit, $\mathbb E_P|Z|^{k_*}<\infty$ in Lemma 1 (otherwise both sides are $+\infty$), and integrability of $|Y|^{2k_*}$ in Lemma 8.
• Corrections of the print. Lemma 8's term $\frac2k\sqrt C\,n^{-1/(k_*\vee2)}$ is false (the hypothesis makes $C$ scale like $Y$; a three-point counterexample is in the statement) and is posed with $C$ in place of $\sqrt C$, written $2\frac{k_*-1}{k_*}C$. Display (30)'s probability $1-2e^{-2t}$ is posed as $1-2e^{-t}$, which is what (28) and a deterministic bias bound give. Theorem 2 is posed as printed; neither correction affects it.
• A trivializing formalization is ruled out: the robust risk is not a junk sSup (the loss is bounded, so the value set is nonempty and bounded), the divergence constraint cannot be met by non-integrable ratios, and the goal mentions only $\mathcal R_k$, $n$, $k$, $\rho$, $M$ and $t$, not the proof's auxiliary objects.
• Reusable beyond this mission: Lemma 1 (Cressie–Read duality), Lemma 7, Lemma 8, and the convex concentration inequality. Proofs of any milestone, and of Lemma 6 on its own platform page, are welcome.

Selected references

• J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization, Ann. Statist. 49(3), 2021. arXiv:1810.08750v6. https://arxiv.org/abs/1810.08750 — https://doi.org/10.1214/20-AOS2004
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg and G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• H. Namkoong and J. C. Duchi, Variance-based Regularization with Convex Objectives, NeurIPS 2017. https://arxiv.org/abs/1610.02581
• J. C. Duchi, P. W. Glynn and H. Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, Math. Oper. Res. 46(3), 2021. https://arxiv.org/abs/1610.03425