Probability

Motivation

Algorithmic stability asks how much the output of a learning algorithm changes when its training sample is perturbed. Since Devroye and Wagner (IEEE Trans. Inf. Theory 1979) it has served as a route to generalization bounds that does not go through the complexity of the hypothesis class. Bousquet and Elisseeff (JMLR 2002) popularised uniform stability, and Mukherjee, Niyogi, Poggio and Rifkin (Adv. Comput. Math. 2006) showed that for empirical risk minimisation in supervised learning, a leave-one-out type of stability is necessary and sufficient for consistency.

Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) study stability in Vapnik's General Learning Setting, where uniform convergence can fail even though the problem is learnable. In Appendix A.2 they compare replace-one and leave-one-out (LOO) stability. For an empirical risk minimiser they prove that LOO stability is equivalent to consistency and to generalization, provided each property holds with one rate for all distributions (Theorem 31, p. 2667). This mission formalizes that theorem and the lemmas of Section 5.3 on which its proof rests.

Timeline:

• 1979, Devroye–Wagner: leave-one-out estimates for local rules.
• 2002, Bousquet–Elisseeff: uniform stability implies generalization.
• 2002, Kutin–Niyogi (UAI 2002): a taxonomy of stability notions.
• 2006, Mukherjee et al.: LOO stability characterises consistency of ERM in supervised learning.
• 2010, Shalev-Shwartz et al.: in the General Learning Setting, for ERMs, LOO stability, universal consistency and universal generalization are equivalent (Theorem 31). Universally consistent AERMs need not be LOO stable (Example 6).

Setting

A learning problem consists of an instance space $\mathcal Z$ with a $\sigma$-algebra, a nonempty hypothesis class $\mathcal H$, and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$. For a probability measure $\mathcal D$ on $\mathcal Z$:

• the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$ and the optimal risk is $F^*=\inf_{h}F(h)$;
• for a sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$ of $m$ i.i.d. draws, the empirical risk is $F_S(h)=\frac1m\sum_{i}f(h;z_i)$, and $F_S(\hat h_S)=\inf_hF_S(h)$ denotes the minimal empirical risk;
• a learning rule $A$ maps each sample of size $m\ge1$ to a hypothesis $A(S)$. It is an ERM if $F_S(A(S))=F_S(\hat h_S)$ for every sample. It is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\mathrm{erm}}(m)$;
• $A$ is consistent with rate $\varepsilon$ if $\mathbb E_{S\sim\mathcal D^m}[F(A(S))-F^*]\le\varepsilon(m)$. It generalizes with rate $\varepsilon$ if $\mathbb E[|F(A(S))-F_S(A(S))|]\le\varepsilon(m)$, and it on-average generalizes if $|\mathbb E[F(A(S))-F_S(A(S))]|\le\varepsilon(m)$;
• writing $S^{\setminus i}$ for $S$ with $z_i$ removed, $A$ is LOO stable with rate $\varepsilon$ (Definition 29) if

$$\frac1m\sum_{i=1}^m\mathbb E_{S\sim\mathcal D^m}\Big[\big|f(A(S^{\setminus i});z_i)-f(A(S);z_i)\big|\Big]\le\varepsilon(m).$$

A rate is a sequence $\varepsilon(m)$ that is non-increasing and tends to $0$. A property holds universally if it holds under every $\mathcal D$ with one and the same rate.

Formalization targets

Goal: Theorem 31

For an ERM $A$:

$$A\ \text{universally LOO stable}\iff A\ \text{universally consistent}\iff A\ \text{universally generalizes}.$$

The statement has no rates. Each side asserts that some rate exists and serves every distribution.

Milestones

In the order the proof uses them:

1. Utility Lemma 12: $\mathbb E|X-\mathbb EX|\le B/\sqrt m$ for the mean $X$ of $m$ i.i.d. variables bounded by $B$.
2. Utility Lemma 13: $X\le Y$ a.s. implies $\mathbb E|X|\le|\mathbb EX|+2\mathbb E|Y|$.
3. Lemma 14: an AERM that on-average generalizes with rate $\varepsilon_{\mathrm{oag}}$ generalizes with rate $\varepsilon_{\mathrm{oag}}+2\varepsilon_{\mathrm{erm}}+2B/\sqrt m$.
4. Lemma 15: under the same hypotheses the rule is consistent with rate $\varepsilon_{\mathrm{oag}}+\varepsilon_{\mathrm{erm}}$.
5. Lemma 16 (Main Converse Lemma): in a learnable problem, $\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\mathrm{cons}}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$.
6. Lemma 17: Eq. (12), together with an AERM that is consistent, gives generalization with rate $\varepsilon_{\mathrm{emp}}+\varepsilon_{\mathrm{erm}}+\varepsilon_{\mathrm{cons}}$.
7. First display of the proof of Theorem 31: a generalizing ERM is LOO stable with rate $\varepsilon_{\mathrm{gen}}(m-1)$.
8. Second display: a LOO stable ERM on-average generalizes on samples of size $m-1$ with rate $\varepsilon_{\mathrm{stable}}(m)+2B/m$.

Significance

Theorem 31 shows that for exact ERMs, LOO stability is not only sufficient but necessary for consistency. It transfers the supervised-learning characterisation of Mukherjee et al. to the General Learning Setting, where uniform convergence is no longer available as an intermediate. The hypothesis is sharp in one direction: Example 6 of the paper gives a universally consistent AERM that is not LOO stable. The equivalence therefore depends on exact minimisation, and an asymptotic minimiser does not suffice.

The lemmas are useful on their own. Lemmas 14 and 15 are the standard bridges between on-average generalization, generalization and consistency. Lemma 16 says that the minimal empirical risk estimates $F^*$ consistently in every learnable problem, even when no ERM learns. Lemma 16 also underlies Theorem 7, the paper's main characterisation of learnability, which is the subject of mission I of this series.

The results are proved in the paper. As far as is known they have not been formalized in any proof assistant. The platform has the textbook side of this framework (Shalev-Shwartz and Ben-David, Understanding Machine Learning, Chapter 13). Those statements are in $\mathbb R^d$ and use a replace-one stability notion; they do not cover leave-one-out stability or the General Learning Setting.

Difficulty

The implications between stability and generalization change the sample size: $S^{\setminus i}$ has $m-1$ points, so a statement about the rule at size $m$ has to be compared with the rule at size $m-1$ under the marginal law of the reduced sample. The step from universal consistency to generalization needs Lemma 16. That lemma estimates $F^*$ from a sample on which the ERM itself may be inconsistent, and it is the only place where universality of the consistency rate is used. Per-distribution consistency of an ERM does not imply generalization (Example 1 of the paper). An argument that fixes $\mathcal D$ throughout therefore cannot succeed.

Formalization scope

Samples are tuples $S:\mathrm{Fin}\,m\to\mathcal Z$ with law Measure.pi (the i.i.d. product), and $S^{\setminus i}$ is Fin.removeNth i S. A learning rule is a family $A_m:\mathcal Z^m\to\mathcal H$. Its value at $m=0$ is never used, and LOO stability is required only for $m\ge2$. $F_S(\hat h_S)$ is the infimum $\inf_hF_S(h)$ and no minimiser is chosen. An ERM is a rule attaining this infimum at every sample. A rate is non-increasing on $m\ge1$ and tends to $0$. Universal properties are stated as "there exists $\varepsilon$ with IsRate ε such that for every probability measure $\mathcal D$ …", with the rate chosen before the distribution. The bound $B$ is any bound on $|f|$; the paper's $B$ is $\sup|f|$, and all its rates increase with $B$.

Measurability is not discussed in the paper. The formalization assumes that each $f(h;\cdot)$ is measurable and that the rule is measurable in the sense that $(S,z)\mapsto f(A_m(S);z)$ is jointly measurable. Lemmas 14–17 also assume that $S\mapsto\inf_hF_S(h)$ is measurable. For a measurable ERM this holds automatically, so Theorem 31 makes no such assumption. Without these assumptions Lean's integral of a non-measurable function is $0$ and every rate bound would hold trivially. For the same reason Utility Lemma 13 assumes $X,Y$ integrable. The ERM hypothesis of the goal must not be weakened to an AERM: the statement would then be false (Example 6).

One statement corrects the printed text. In the second display of the proof of Theorem 31 (p. 2668), the chain adds $2B/m$ and then drops it. The milestone states the bound the argument proves, $\varepsilon_{\mathrm{stable}}(m)+2B/m$. The rate-free Theorem 31 is unaffected.

The development needs product measures, independence and variance bounds, all available in Mathlib, and the marginals of Measure.pi under removal of a coordinate. The definitions of risks, rules and stability notions can be reused by other stability results. Proofs of any milestone are welcome, and so are alternative proofs of the goal.

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
• S. Kutin, P. Niyogi, Almost-everywhere algorithmic stability and generalization error, UAI 2002. https://arxiv.org/abs/1301.0579
• L. Devroye, T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087

Motivation

Statistical learning theory asks when a rule that sees only an i.i.d. sample $z_1,\dots,z_m$ from an unknown distribution $D$ can return a hypothesis whose expected loss is close to the best possible. In supervised classification the classical answer is uniform convergence: learnability holds exactly when empirical risks converge to expected risks uniformly over the hypothesis class, and then empirical risk minimization (ERM) learns. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) showed that in Vapnik's broader General Learning Setting this picture breaks down. Their motivating example is stochastic convex optimization in a Hilbert space: minimizing an expected convex, Lipschitz objective over a bounded convex set from samples. This problem underlies regularized linear prediction, kernel methods and online-to-batch conversions, and the paper shows (§4.1) that in infinite dimension uniform convergence can fail and the plain empirical minimizer can fail to converge, while the problem is still learnable.

This mission formalizes the positive half of that example: Tikhonov-regularized ERM learns every such problem, with an explicit bound holding with probability $1-\delta$ (Theorem 3, p. 2644), through the stability of strongly convex empirical minimization (Theorem 2).

Setting

Let $Z$ be a measurable space of instances and $E$ a real Hilbert space. A stochastic convex optimization problem consists of a nonempty, closed, convex, bounded set $\mathcal H\subseteq E$ and an objective $f:E\times Z\to\mathbb R$ such that for every $z$ the map $h\mapsto f(h;z)$ is convex and $L$-Lipschitz on $\mathcal H$, each $f(h;\cdot)$ is measurable, and $|f(h;z)|\le C$ on $\mathcal H\times Z$. For a distribution $D$ on $Z$ define the risk and optimal risk

$$F(h)=\mathbb E_{z\sim D}[f(h;z)],\qquad F^*=\inf_{h\in\mathcal H}F(h),$$

and for a sample $S=(z_1,\dots,z_m)\sim D^m$ the empirical risk $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$. A function $g$ is $\lambda$-strongly convex on $\mathcal H$ if $g-\frac\lambda2\|\cdot\|^2$ is convex there. The regularized empirical minimizer is

$$\hat h_\lambda\in\operatorname*{arg\,min}_{h\in\mathcal H}\Big(F_S(h)+\frac\lambda2\|h\|^2\Big).\tag{5}$$

For the general part, a learning rule $A$ maps samples to hypotheses; it is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-\inf_hF_S(h)]\le\varepsilon_{\mathrm{erm}}(m)$, consistent with rate $\varepsilon_{\mathrm{cons}}$ if $\mathbb E[F(A(S))-F^*]\le\varepsilon_{\mathrm{cons}}(m)$, and uniform-RO stable with rate $\varepsilon_{\mathrm{stable}}$ if replacing any one sample point changes the loss at any test point by at most $\varepsilon_{\mathrm{stable}}(m)$ on average over the replaced index (Definition 4).

Formalization targets

Goal: Theorem 3

If $\|h\|\le B$ on $\mathcal H$, $L,B>0$, $\delta\in(0,1)$, $m\ge1$ and $\lambda=\sqrt{16L^2/(\delta B^2m)}$, then with probability at least $1-\delta$ over $S\sim D^m$

$$F(\hat h_\lambda)-F^*\ \le\ 4\sqrt{\frac{L^2B^2}{\delta m}}\Big(1+\frac8{\delta m}\Big).$$

The constants are the paper's.

Milestones, in the order the proof uses them

1. Quadratic growth at a minimizer of a $\lambda$-strongly convex $g$: $g(h')-g(h)\ge\frac\lambda2\|h'-h\|^2$ (§4.2, p. 2644).
2. Eq. (6): if $f(\cdot;z)$ is $\lambda$-strongly convex and $L$-Lipschitz, empirical minimizers of $S$ and of $S^{(i)}$ satisfy $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$ for all $z$ (p. 2645).
3. Theorem 8: a uniform- or average-RO stable AERM is consistent with rate $\varepsilon_{\mathrm{stable}}+\varepsilon_{\mathrm{erm}}$ and generalizes with rate $\varepsilon_{\mathrm{stable}}+2\varepsilon_{\mathrm{erm}}+2C/\sqrt m$ (p. 2649).
4. $\mathbb E_{S\sim D^m}[F(\hat h_S)-F^*]\le 4L^2/(\lambda m)$ for the strongly convex empirical minimizer (p. 2645).
5. Theorem 2: with probability $1-\delta$, $F(\hat h_S)-F^*\le 4L^2/(\delta\lambda m)$ (p. 2644).
6. Theorem 2 applied to $r(h;z)=\frac\lambda2\|h\|^2+f(h;z)$: with probability $1-\delta$, $\frac\lambda2\|\hat h_\lambda\|^2+F(\hat h_\lambda)\le\inf_h\big(\frac\lambda2\|h\|^2+F(h)\big)+4(L+\lambda B)^2/(\delta\lambda m)$ (p. 2645).

Significance

The result. Theorem 3 shows that every convex, Lipschitz, bounded stochastic optimization problem over a bounded subset of a Hilbert space is learnable at rate $O(LB/\sqrt{\delta m})$, with no dimension dependence and no uniform convergence. Together with the counterexamples of §4.1 it separates learnability from uniform convergence and from ERM, and it motivates the paper's general characterization: a problem is learnable if and only if it admits a uniform-RO stable asymptotic empirical risk minimizer (Theorem 7). Theorem 8 is the sufficiency half of that characterization and is reused wherever stability arguments give generalization bounds.

Formalizing it. The results are proved in the paper; to our knowledge none has a machine-checked proof. The closest platform material is the textbook treatment in Understanding Machine Learning, chapter 13 (Shalev-Shwartz and Ben-David): Corollary 13.9 (UnderstandingML.convex_lipschitz_bounded_learnable), Corollary 13.6 (rlm_lipschitz_stable) and Lemma 13.5 (strongly_convex_lemma). Those are stated in $\mathbb R^d$, bound the risk in expectation, use the regularizer $\lambda\|w\|^2$ over all of $\mathbb R^d$, and have different constants; the present mission works in an arbitrary Hilbert space, over a constraint set $\mathcal H$, with high-probability bounds and the paper's constants. Its definitions of learning rules, AERM, consistency and replace-one stability in the General Learning Setting are reusable by the other missions of this series.

Difficulty

The obvious route, bounding $\sup_{h\in\mathcal H}|F(h)-F_S(h)|$, is unavailable: §4.1 exhibits problems of exactly this type in which that supremum stays bounded away from zero for every sample size. Any successful argument therefore has to rely on a property of the learning rule rather than of the class $\mathcal H$, and the plain empirical minimizer does not have it: §4.1 shows it can stay a constant away from $F^*$ at every sample size. A second difficulty is purely formal: the regularization parameter $\lambda$ depends on $\delta$ and $m$, so the regularized minimizer changes with them, and all expectations involve a data-dependent hypothesis in a possibly non-separable Hilbert space, where measurability is not automatic.

Formalization scope

Lean conventions, fixed for every item:

• $E$ is a real inner product space with CompleteSpace E, never assumed finite-dimensional; $\mathcal H$ is Hset : Set E, and all infima, suprema, strong convexity and Lipschitz conditions are taken on Hset only. $F^*$ is ⨅ h : Hset, F h.
• Samples are Fin m → Z, $D^m$ is Measure.pi, $S^{(i)}$ is Function.update S i z', and $m\ge1$ throughout.
• The paper's standing loss bound $|f|\le B$ (p. 2637) is named $C$, because Theorem 3 uses $B$ for the norm bound $\|h\|\le B$. $L>0$ and $B>0$ are implicit in Theorem 3's choice of $\lambda$ and are stated.
• Strong convexity is Mathlib's StrongConvexOn Hset λ, which is the paper's definition.
• Minimizers are selections $S\mapsto\hat h_S\in\mathcal H$ satisfying the minimization property; the theorems hold for every such selection, hence for the minimizer, which is unique by strong convexity.
• Measurability, not discussed in the paper, is the series' single standing convention: each $f(h;\cdot)$ is measurable and the selection makes $(S,z)\mapsto f(\hat h_S;z)$ jointly measurable; for Theorem 8, the rule is measurable in the same sense and $S\mapsto\inf_hF_S(h)$ is measurable.
• "With probability at least $1-\delta$" is the bound $D^m\{\text{failure}\}\le\delta$ with $0<\delta<1$.

No statement of the paper is corrected: all printed constants were checked against the proofs and are reproduced exactly.

A formalization in which the expected excess risk is a Bochner integral of a non-measurable or non-integrable function, or in which $F^*$ is an infimum over all of $E$ or over an unbounded family, would make the bounds trivially true; the measurability hypotheses, the bound $|f|\le C$ and the infimum over the nonempty set $\mathcal H$ rule this out.

Contributions welcome: proofs of the milestones in order, and in particular a reusable replace-one identity $\mathbb E[F_S(A(S))]=\frac1m\sum_i\mathbb E[f(A(S^{(i)});z'_i)]$ under Measure.pi, and Markov's inequality in the form used for high-probability bounds.

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Stochastic Convex Optimization, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/018.pdf
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, chapter 13. https://doi.org/10.1017/CBO9781107298019
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

Motivation

Classifiers trained to high standard accuracy on image benchmarks can be made to fail by perturbations of the input that are small in the $\ell_\infty$ norm (Szegedy et al., 2014; Goodfellow et al., 2015). Adversarial training reaches high robust accuracy on the training set, but on CIFAR10 the robust accuracy on held-out data is much lower than on the training set (Madry et al., 2018). That is, robust generalization fails.

Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this is a statistical phenomenon: does learning a robust classifier need more samples than learning an accurate one, even in the simplest distributional model? This mission formalizes their answer for a mixture of two Gaussians. In that model, with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma \le c\, d^{1/4}$, a single sample suffices for standard generalization (their Theorem 4). Robust generalization, by contrast, needs a number of samples that grows polynomially with the dimension, for every learning algorithm.

Setting

Write $\mathbb R^d$ for the feature space and $\{\pm 1\}$ for the labels.

• The $\ell_\infty$ perturbation set of radius $\varepsilon$ around $x$ is $\mathcal B_\infty^\varepsilon(x) = \{x' \in \mathbb R^d : \|x' - x\|_\infty \le \varepsilon\}$.
• For $\theta \in \mathbb R^d$ and $\sigma > 0$, the $(\theta, \sigma)$-Gaussian model $P_{\theta,\sigma}$ is the law of $(x, y)$ obtained by drawing $y$ uniformly from $\{\pm1\}$ and then $x \sim \mathcal N(y\theta, \sigma^2 I)$ (Definition 1). Here $\sigma$ is a standard deviation.
• The $\ell_\infty^\varepsilon$-robust classification error of a classifier $f : \mathbb R^d \to \{\pm1\}$ under a distribution $P$ is $\mathbb P_{(x,y) \sim P}[\exists\, x' \in \mathcal B_\infty^\varepsilon(x) : f(x') \ne y]$ (Definitions 2–3). With $\varepsilon = 0$ it is the ordinary classification error.
• A learning algorithm $g_n$ maps $n$ labelled samples $S \in (\mathbb R^d \times \{\pm 1\})^n$ to a classifier $f_n = g_n(S)$.
• The expected robust error $\Xi$ of $g_n$ is the robust error of $g_n(S)$ under $P_{\theta,\sigma}$, averaged over $S \sim P_{\theta,\sigma}^{\otimes n}$ and then over a prior $\theta \sim \mathcal N(0, I)$. The learner sees $S$ but not $\theta$.

Formalization targets

Goal: Corollary 23 (p. 30)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$n \le \frac{\varepsilon^2\sigma^2}{8\log d} \quad\Longrightarrow\quad \Xi \ \ge\ \Big(1 - \frac1d\Big)\frac12 .$$

Theorem 11 (p. 28)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$\Xi \ \ge\ \frac12\, \mathbb P_{v \sim \mathcal N(0, I)}\Big[\sqrt{\tfrac{n}{\sigma^2+n}}\,\|v\|_\infty \le \varepsilon\Big].$$

Intermediate statements (milestones)

1. Eq. (2). Given $n$ samples $z_i \sim \mathcal N(\theta, \sigma^2 I)$, the posterior of $\theta \sim \mathcal N(0, I)$ is $\mathcal N(\mu', \Sigma')$ with $\mu' = (\sigma^2+n)^{-1}\sum_i z_i$ and $\Sigma' = \frac{\sigma^2}{\sigma^2+n} I$. The expectations over $\theta$ and over the samples may therefore be exchanged.
2. Eq. (3). Averaging $P_{\theta,\sigma}$ over $\theta \sim \mathcal N(m, s^2 I)$ gives $P_{m, \sqrt{s^2+\sigma^2}}$.
3. The bound on $\Psi$. If $\|m\|_\infty \le \varepsilon$, every classifier has $\ell_\infty^\varepsilon$-robust error at least $\frac12$ under $P_{m,s}$.
4. The law of $\bar z$. The sample mean $\bar z$ of the $z_i$ is marginally $\mathcal N(0, (1+\sigma^2/n) I)$.
5. Maximum of $d$ Gaussians. $\mathbb P_{v\sim\mathcal N(0,I_d)}[\|v\|_\infty \le 2\sqrt{2\log d}] \ge 1 - 1/d$.

Corollary 23 is the goal because it is the statement the paper advertises: its main-text Theorem 6 is Corollary 23 with $\sigma = c_1 d^{1/4}$.

Significance

In the same model with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma$ of order $d^{1/4}$, a single sample suffices to reach standard error below 1% (Theorem 4 of the paper), and on the order of $\varepsilon^2\sqrt d$ samples suffice for robust error below 1% when $\varepsilon$ is below a small constant (Theorem 5; Corollary 22, formalized in mission 3 of this series). Corollary 23 shows that, up to the logarithmic factor, no learner can do better. Robust generalization then needs $\varepsilon^2 \sqrt d / \log d$ times as many samples as standard generalization. The gap is information-theoretic: it concerns every algorithm, not a particular training procedure or model class. The authors present this as a candidate explanation for the robust-generalization gap observed on CIFAR10. The ½ is tight: a constant classifier attains it.

The paper's proof is complete and short. As far as a search of the platform shows, none of its statements has been formalized. A machine-checked version requires multivariate Gaussian conjugacy, Gaussian convolution identities, the outer-measure robust event, and a union bound for the maximum of Gaussians. The Gaussian conjugacy and convolution facts are standard and appear throughout Bayesian statistics. As of this Mathlib version they are not available for stdGaussian on EuclideanSpace.

Difficulty

The obvious attempt fixes $\theta$ and bounds the robust error for each $\theta$. That fails: a learner may ignore the data and output the Bayes-optimal robust classifier for one fixed $\theta$, so for each $\theta$ some learner does well. The lower bound holds only on average over the prior on $\theta$. The classifier $f_n$ depends on the samples, and the samples depend on $\theta$, so the classifier and the test distribution are correlated through $\theta$. A second obstacle is measure-theoretic. The robust error of a classifier is the probability of an $\ell_\infty$-thickening of an arbitrary set $\{f \ne y\}$. Such a set need not be Borel, and it must be bounded below with no structure on the classifier beyond what the learner provides. The same statement with the $\ell_2$ ball is a different theorem.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra; $\mathcal N(0, I)$ is Mathlib's stdGaussian; $\mathcal N(m, s^2 I)$ is its image under $v \mapsto m + s v$, so every Gaussian parameter in the development is a standard deviation.
• The $\ell_\infty$ ball is written coordinatewise ($|x'_i - x_i| \le \varepsilon$ for all $i$), because the ambient norm is $\ell_2$. $\|v\|_\infty \le r$ is written the same way.
• Labels are Bool, with true for $+1$. A classifier is ℝ^d → Bool, and a learning algorithm is (Fin n → ℝ^d × Bool) → ℝ^d → Bool.
• A model is a measure on $\mathbb R^d \times$ Bool; $n$ samples form the product measure Measure.pi.
• The robust event need not be Borel. Its probability is the outer measure, which is its probability under the completion. The expectations are lower Lebesgue integrals.
• Theorem 11 and Corollary 23 assume the learner is jointly measurable in (samples, input). This is the only condition on it. $\log$ is the natural logarithm. With Lean's conventions $\log 0 = \log 1 = 0$ and $x/0 = 0$, the goal's hypothesis forces $n = 0$ for $d \le 1$, where the statement is still true.
• The paper writes the posterior mean as $\frac{n}{\sigma^2+n}\bar z$, with "$\bar z = \sum_i z_i$" on p. 28. The formalization uses $(\sigma^2+n)^{-1}\sum_i z_i$, which is the posterior mean. It agrees with the paper when $\bar z$ is read as the sample mean, as it is on p. 30.

A formalization that fixes $\theta$ instead of averaging over the prior, that restricts the learner (to linear classifiers, or to classifiers that do not depend on the data), that uses the $\ell_2$ ball, or that assumes the posterior formula as a hypothesis states a different theorem. These are ruled out by the definitions file.

Needed infrastructure: the multivariate Gaussian conjugacy and convolution identities for stdGaussian pushforwards, translation invariance of outer measure under Gaussian shifts, and a sub-Gaussian tail bound for one coordinate. The Gaussian identities are reusable well beyond this mission. Contributions of general Gaussian lemmas, stated for stdGaussian on any finite-dimensional inner product space, are welcome. Related platform work: missions 2–4 of this series formalize the Bernoulli-model lower bound and the two upper bounds of the same paper.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2, 2018. https://arxiv.org/abs/1804.11285
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 5.8). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Firms that sell new products (consoles, books, films) often take preorders before release. A preorder serves two purposes at once. It lets the firm charge early adopters a different price from later buyers, a form of price discrimination, and the number of preorders is advance demand information: an early signal of how large regular-season demand will be. Li and Zhang (MSOM 15(1), 2013) ask whether better advance information always helps a seller who runs a preorder, when consumers are strategic and anticipate the seller's stocking decision. Their answer is no. The second-period stocking decision improves, but the preorder price can fall. Whether the net effect is positive depends on the low-type margin and the size of the early-adopter segment.

This mission formalizes that answer, §4 of the paper: the preorder profit as a function of the demand correlation $\rho$.

Setting

A seller sells a perishable product over two periods. High-type consumers, with valuation $v_H$, arrive in the first period and may preorder at price $p_1$. Low-type consumers, with valuation $v_L < v_H$, arrive in the second period, when the price is $p_2$. A high type who waits values the product at $\delta v_H$, where $\delta \le 1$ and $\delta v_H > v_L$. The unit cost is $c$, with $0 < c < v_L$. Unsold units have no salvage value and unmet demand carries no penalty. Write $\Delta = \delta v_H - v_L$.

The demands are jointly normal with correlation $\rho \in [0,1)$. The high-type demand has mean $\mu_H$, and $X$ denotes its standardization, a standard normal variable. The low-type demand has mean $\mu_L$, standard deviation $\sigma_L$ and $\lambda_L = \mu_L/\sigma_L$. Given $X = x$, the updated low-type demand $\tilde X_L(x)$ is normal with mean $\tilde\mu_L(x) = \mu_L + \rho\sigma_L x$ and standard deviation $\tilde\sigma_L = \sigma_L\sqrt{1-\rho^2}$. $\Phi$ and $\phi$ are the standard normal distribution function and density, and $z_L$ solves $\Phi(z_L) = (v_L - c)/v_L$.

In the second period the seller charges $p_2 = v_L$ and solves a newsvendor problem. It orders

$$Q(x) = \tilde\mu_L(x) + z_L\tilde\sigma_L \qquad (1)$$

and earns $\Pi_L(x) = (v_L - c)(\mu_L + \rho\sigma_L x) - v_L\phi(z_L)\sigma_L\sqrt{1-\rho^2}$ (2). A waiting high type believes half of the remaining consumers will be served before her, so her belief of product availability is

$$\xi(\rho) = \mathbb E\Big[\Pr\Big(\tfrac{\tilde X_L(X)}{2} < Q(X)\Big)\Big]. \qquad (3)$$

In the rational-expectations equilibrium every high type preorders at $p_1 = v_H - \Delta\xi$. The preorder profit is

$$\Pi^p(\rho) = (v_H - \Delta\xi(\rho) - c)\mu_H + \Pi_L(0). \qquad (4)$$

The threshold is

$$\tilde\mu(\rho) = -\frac{v_L\phi(z_L)\sigma_L}{2\Delta z_L\,\phi\big(2z_L\sqrt{1-\rho^2} + \lambda_L\big)}. \qquad (6)$$

Formalization targets

Goal: PROPOSITION 2

$$\begin{aligned} &\text{(i) } c < v_L < 2c:\ \Pi^p \text{ strictly increases on every interval where } \mu_H < \tilde\mu(\rho),\\ &\qquad\text{and strictly decreases on every interval where } \mu_H \ge \tilde\mu(\rho);\\ &\text{(ii) } v_L \ge 2c:\ \Pi^p \text{ strictly increases on } [0,1). \end{aligned}$$

Milestones

1. (1)–(2): $Q(x)$ is the unique maximizer of $\mathbb E[v_L\min(Q,\tilde X_L(x)) - cQ]$, and its value is $\Pi_L(x)$.
2. (3): $\xi(\rho) = \mathbb E\big[\Phi\big((\lambda_L + \rho X)/\sqrt{1-\rho^2} + 2z_L\big)\big]$.
3. LEMMA 1(i): if $c < v_L < 2c$, then $z_L < 0$ and $\xi$ is strictly increasing in $\rho$.
4. LEMMA 1(ii): if $v_L \ge 2c$, then $z_L \ge 0$ and $\xi$ is non-increasing in $\rho$, strictly so when $v_L > 2c$.
5. After (5): $\dfrac{d}{d\rho}\Pi_L(0) = v_L\phi(z_L)\sigma_L\,\rho/\sqrt{1-\rho^2} > 0$ for $\rho \in (0,1)$.
6. PROPOSITION 2(i), pointwise: for $\rho \in (0,1)$, $d\Pi^p/d\rho > 0 \iff \mu_H < \tilde\mu(\rho)$ and $d\Pi^p/d\rho < 0 \iff \mu_H > \tilde\mu(\rho)$.
7. LEMMA 2(i): if $-\lambda_L/2 < z_L < 0$, then $\tilde\mu$ is strictly increasing in $\rho$.
8. LEMMA 2(ii): if $z_L \le -\lambda_L/2$, then $\tilde\mu$ is quasi-convex in $\rho$.

Significance

The proposition splits the value of advance demand information into two effects with opposite signs. Better information always raises the second-period profit (milestone 5). Its effect on the preorder price depends on the margin. When $v_L < 2c$, the seller stocks below the conditional mean. A more precise forecast then raises the stock and the availability $\xi$, and waiting becomes more attractive, which lowers the preorder price. The threshold $\tilde\mu(\rho)$ says which effect wins, and LEMMA 2 describes its shape. This is the basis for the paper's later comparisons of preorder, price-guarantee and no-preorder strategies.

The paper states these results and leaves the proofs to an online appendix. None of them has a machine-checked proof. A complete development would also give reusable facts about normal laws: the expectation $\mathbb E[\Phi(a + bX)]$ for standard normal $X$, the normal newsvendor solution with its closed-form optimal profit, and derivatives of Gaussian integrals with respect to a correlation parameter.

Difficulty

The model is explicit, so the difficulty is not in modelling. It is in turning the two expectations into closed forms and differentiating them. The availability $\xi$ is an integral over $X$ of a normal probability whose mean and variance both move with $\rho$. The expected newsvendor profit involves $\mathbb E[\min(Q, Y)]$ for a normal $Y$. Neither closed form is in Mathlib, and neither is a derivative in $\rho$ of a Gaussian integral. The obvious route, differentiating under the integral sign in (3), needs domination estimates that are uniform in $\rho$ near each point, and these degenerate as $\rho \to 1$.

Signs are the second difficulty. $z_L$ changes sign at $v_L = 2c$, $\tilde\mu$ carries a leading minus and divides by $z_L$, and the derivative of $\Pi^p$ vanishes at $\rho = 0$ and wherever $\tilde\mu(\rho) = \mu_H$. Strict monotonicity on an interval has to be recovered from a derivative that is positive except at finitely many points.

Formalization scope

Everything lives in the namespace PreorderADI.Correlation. A structure Params holds $v_H, v_L, c, \delta, \mu_H, \mu_L, \sigma_L, z_L$. The predicate Params.Standing records the model's assumptions: $v_H > v_L$, $c < v_L$, $\delta \le 1$ and $\delta v_H > v_L$, together with $\Phi(z_L) = (v_L-c)/v_L$. $\sigma_H$ is omitted because nothing in §4 uses it after standardization. $\Phi$ is ProbabilityTheory.cdf (gaussianReal 0 1) and $\phi$ is gaussianPDFReal 0 1. The normal law with mean $m$ and standard deviation $s$ is gaussianReal m (s^2).

The formalization commits to the following conventions and additions:

• Added hypotheses. Four hypotheses are added to the page's assumptions:
  • $c > 0$, so that $z_L$ exists;
  • $\sigma_L > 0$, so that the conditional law is a genuine normal law;
  • $\mu_L > 0$, so that $\lambda_L > 0$, as LEMMA 2 presupposes;
  • $\mu_H > 0$, which PROPOSITION 2(ii) needs.
• $z_L$. $z_L$ is a parameter pinned down by $\Phi(z_L) = (v_L-c)/v_L$, not an inverse function with junk values.
• Range of $\rho$. $\rho$ ranges over $[0,1)$, the paper's "we will focus on $\rho \ge 0$" together with $\rho < 1$. Derivative statements use $(0,1)$.
• $\xi$ and $\Pi^p$. $\xi$ is defined as the first expression of (3), the expected probability, so that no closed form is assumed. $\Pi^p$ is defined by (4). PROPOSITION 1, which derives (4) as the unique equilibrium profit, is not formalized: the paper defines the equilibrium only through conditions that already assume every high type preorders.
• Monotonicity. "Increases in $\rho$ when $\mu_H < \tilde\mu(\rho)$" is formalized as strict monotonicity on every order-connected $I \subseteq [0,1)$ on which the condition holds. "Decreasing" in LEMMA 1(ii) is non-strict, since $\xi$ is constant when $v_L = 2c$. Quasi-convexity is Mathlib's QuasiconvexOn.
• The ε_v sentence is omitted. PROPOSITION 2(i) also claims that some $\varepsilon_v > 0$ makes $\Pi^p$ always decrease when $v_L < c + \varepsilon_v$. That claim is false in the paper's own model. As $v_L \downarrow c$, $\tilde\mu(\rho) \to \infty$ for $\rho$ below roughly $\sqrt 3/2$, so $\Pi^p$ increases there for every fixed $\mu_H$. The paper's Figure 1 shows the same behaviour.
• Out of scope. §5 rests on an approximation that treats normal demands as nonnegative, so it is excluded. §§6–7 depend on models given only in the online appendix and are excluded too.

A statement about the closed form $\Phi(\lambda_L + 2z_L\sqrt{1-\rho^2})$ in place of $\xi$ would make LEMMA 1 a one-line monotonicity fact. So would a definition of $\Pi^p$ that bypasses (3). The definitions rule both out.

Welcome contributions include proofs of the milestones, general Mathlib-style lemmas on Gaussian expectations of $\Phi$ and of $\min(Q, Y)$, and a formalization of PROPOSITION 1 from conditions (i)–(v).

Selected references

• C. Li and F. Zhang, Advance Demand Information, Price Discrimination, and Preorder Strategies, Manufacturing & Service Operations Management 15(1):57–71, 2013. https://doi.org/10.1287/msom.1120.0398
• G. P. Cachon and R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• X. Su and F. Zhang, On the Value of Commitment and Availability Guarantees When Selling to Strategic Consumers, Management Science 55(5):713–726, 2009. https://doi.org/10.1287/mnsc.1080.0967

Motivation

Value-at-Risk (VaR) is the loss level that a portfolio exceeds with probability at most $\varepsilon$. It is the standard risk measure of banking regulation, and its classical computation assumes Gaussian returns: for a Gaussian return vector with mean $\hat x$ and covariance $\Gamma$ it equals $-\Phi^{-1}(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$, where $\Phi$ is the standard normal distribution function. Real returns are not exactly Gaussian, and a VaR computed from a misspecified distribution can badly understate risk.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the single distribution by a class $\mathcal P$ of distributions and define the worst-case VaR as the smallest loss level whose probability is at most $\varepsilon$ under every distribution of the class. Their first class, distributions with a given mean and covariance, leads to the Chebyshev-type bound of their Theorem 1, whose worst case is attained by discrete distributions. §4.2 of the paper asks instead for distributions that stay close to a Gaussian, measured by relative entropy (Kullback–Leibler divergence). Such balls are the basic uncertainty sets of distributionally robust optimization and of robust control in economics (Hansen and Sargent's multiplier and constraint preferences), and they give a smooth worst case. Theorem 9 computes the resulting worst-case VaR in closed form.

Setting

Returns are random vectors $x \in \mathbb R^n$ and a portfolio is a vector $w \in \mathbb R^n$ with $w \neq 0$; its return is $r(w,x) = w^\top x$. For a level $\gamma \in \mathbb R$ the loss set is $\mathcal S_\gamma = \{x : \gamma \le -x^\top w\}$ (Eq. 13 of the paper).

Given a class $\mathcal P$ of probability distributions on $\mathbb R^n$ and $\varepsilon \in (0,1)$, the worst-case Value-at-Risk (Eq. 4) is

$$V_{\mathcal P}(w) = \min\Big\{\gamma \in \mathbb R : \sup_{P \in \mathcal P} P(\mathcal S_\gamma) \le \varepsilon\Big\}.$$

Fix a mean $\hat x \in \mathbb R^n$ and a positive definite covariance $\Gamma \succ 0$, and let $P_0 = \mathcal N(\hat x, \Gamma)$ be the reference Gaussian. For $d \ge 0$ the relative-entropy class (Eq. 43) is

$$\mathcal P_d = \Big\{P \text{ probability on } \mathbb R^n : \mathrm{KL}(P, P_0) = \int \log\frac{dP}{dP_0}\,dP \le d\Big\},$$

with $\mathrm{KL}(P,P_0) = +\infty$ unless $P$ is absolutely continuous with respect to $P_0$.

The risk factor (Eq. 45) is

$$f(\varepsilon,d) = \sup_{\lambda>0}\frac{e^{\varepsilon/\lambda - d} - 1}{e^{1/\lambda} - 1}, \qquad \kappa(\varepsilon,d) = -\Phi^{-1}\big(f(\varepsilon,d)\big),$$

and the Gaussian tail of the loss set is $\phi(\gamma) = P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.

Formalization targets

Goal: Theorem 9 (p. 553)

For $\Gamma \succ 0$, $w \neq 0$, $d \ge 0$ and $0 < \varepsilon < 1$, the minimum in (4) over $\mathcal P_d$ exists and

$$V_{\mathcal P_d}(w) = \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - \hat x^\top w. \tag{44}$$

Milestones

The milestones follow the proof of Theorem 9 on pp. 553–554, in attack order.

1. Eq. (45). The two expressions of $f$ agree: $\sup_{\lambda>0}\frac{e^{\varepsilon/\lambda-d}-1}{e^{1/\lambda}-1} = \sup_{v>0}\frac{e^{-d}(v+1)^\varepsilon - 1}{v}$.
2. Gaussian tail. $P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.
3. Eq. (47). For $\lambda > 0$, the Lagrangian $L(Q) = Q(\mathcal S_\gamma) + \lambda_0(1 - Q(\mathbb R^n)) + \lambda(d - \mathrm{KL}\text{-integral})$ is maximised over finite measures $Q \ll P_0$ by the exponentially tilted density $dQ^\star/dP_0 = \exp((\chi_{\mathcal S} - \lambda_0)/\lambda - 1)$, with value

$$\theta(\lambda_0,\lambda) = \lambda_0 + \lambda d + \lambda e^{-\lambda_0/\lambda - 1}\big((e^{1/\lambda}-1)\phi(\gamma) + 1\big).$$

4. Eq. (48). $\min_{\lambda_0\in\mathbb R}\theta(\lambda_0,\lambda) = \lambda d + \lambda\log\big((e^{1/\lambda}-1)\phi(\gamma)+1\big)$.
5. Duality. $\sup_{P\in\mathcal P_d} P(\mathcal S_\gamma) = \inf_{\lambda>0}\big(\lambda d + \lambda\log((e^{1/\lambda}-1)\phi(\gamma)+1)\big)$.
6. Inversion. For $d > 0$: some $\lambda > 0$ makes the dual value at most $\varepsilon$ if and only if $\gamma \ge \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - w^\top\hat x$.
7. Remark after Theorem 9. $f(\varepsilon, 0) = \varepsilon$, so $\kappa(\varepsilon,0) = -\Phi^{-1}(\varepsilon)$. The risk factor $\kappa(\varepsilon, d)$ is strictly increasing in $d \ge 0$.

Significance

Theorem 9 says that an entropy ball around a Gaussian leaves the form of the Gaussian VaR unchanged: only the risk factor moves, from $-\Phi^{-1}(\varepsilon)$ to $\kappa(\varepsilon,d)$, a scalar computed by a one-dimensional maximisation. The worst-case VaR therefore stays a convex function of $w$ whenever $\kappa \ge 0$, and minimising it over a polytope of portfolios is a second-order cone program (problem (3) of the paper). The number $f(\varepsilon,d)$ is the largest $p$ with $\mathrm{KL}(\mathrm{Bernoulli}(\varepsilon)\,\|\,\mathrm{Bernoulli}(p)) \le d$, which ties the result to the binary-divergence bounds used throughout information theory.

The theorem was proved in 2003. The worst-case-probability step (milestone 5) is an instance of the Donsker–Varadhan / Gibbs variational duality for relative-entropy balls, which the paper imports from the literature (Smith 1995). No machine-checked proof of Theorem 9 or of this duality on $\mathbb R^n$ is known. A formalization would give a verified closed form for a relative-entropy distributionally robust chance constraint, and the duality and tilting lemmas would serve any mission on KL-ball robust optimization.

Difficulty

The obvious argument is Lagrangian duality for the infinite-dimensional problem $\sup\{P(\mathcal S_\gamma) : \mathrm{KL}(P,P_0) \le d\}$. Weak duality and the pointwise maximisation that produces the tilted density are elementary. The difficulty is the step the paper cites rather than proves: that the duality gap is zero, and that the supremum over distributions equals the infimum of the dual over $\lambda > 0$. The feasible set is a set of measures, the objective is an indicator, and the constraint is a divergence that is $+\infty$ off a set of absolutely continuous measures, so a finite-dimensional Slater argument does not apply as stated.

The second difficulty is at the boundary of the parameters. At $d = 0$ the supremum defining $f(\varepsilon,0)$ is approached only as $\lambda \to \infty$, so the final inversion step behaves differently from $d > 0$. At $\varepsilon = 1$ the theorem is false, since every level $\gamma$ is feasible and (4) has no minimum.

Formalization scope

Returns live in EuclideanSpace ℝ (Fin n). $P_0$ is Mathlib's multivariateGaussian xhat Γ with Γ.PosDef, and $\mathrm{KL}$ is InformationTheory.klDiv, which is $\infty$ unless $P \ll P_0$ with integrable log-likelihood ratio and equals $\int\log\frac{dP}{dP_0}\,dP$ otherwise for probability measures. The class $\mathcal P_d$ requires IsProbabilityMeasure P. $\Phi$ is cdf (gaussianReal 0 1), and $\Phi^{-1}(p)$ is defined as $\inf\{t : p \le \Phi(t)\}$, which inverts $\Phi$ on $(0,1)$. The quadratic form $w^\top\Gamma w$ is a double sum, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$.

Conventions the Lean statements commit to:

• "min" in (4) is IsLeast of the feasible set $\{\gamma : P(\mathcal S_\gamma) \le \varepsilon \ \forall P \in \mathcal P_d\}$. "$\sup_{P}P(\mathcal S_\gamma) \le \varepsilon$" is written "for every $P$", with probabilities compared in $[0,\infty]$.
• The paper prints $\varepsilon \in (0,1]$. The mission assumes $0 < \varepsilon < 1$, because the goal is false at $\varepsilon = 1$.
• $w \neq 0$ is the paper's assumption that the admissible set of portfolios excludes $0$.
• $f(\varepsilon,d)$ is a Lean sSup of a set that is nonempty and bounded above by $1$ for $\varepsilon \le 1$, $d \ge 0$.
• The duality of milestone 5 is stated as the existence of one real number that is both the least upper bound of the worst-case probabilities and the greatest lower bound of the dual values, not as an equality of Lean's sSup and sInf.
• Eq. (48) is stated as an attained minimum (IsLeast), which the calculus gives.
• Milestone 3 works with finite measures $Q \ll P_0$ with integrable log-likelihood ratio in place of the paper's densities $p$. It uses the complement of $\mathcal S_\gamma$ where the paper writes $\{\gamma \ge -x^\top w\}$, which differs by a $P_0$-null hyperplane.
• Milestone 6 assumes $d > 0$; the goal keeps $d \ge 0$.

Restricting $\mathcal P_d$ to $\{P_0\}$, dropping IsProbabilityMeasure, or taking an arbitrary reference measure would trivialize or change the theorem. The class is the full KL ball around the nondegenerate Gaussian.

Infrastructure a complete development needs: the pushforward of a multivariate Gaussian under a linear functional (a one-dimensional Gaussian), the Gibbs variational principle for relative entropy, the strong duality for KL balls, and properties of $\Phi$ and its quantile (continuity, strict monotonicity, symmetry $\Phi(-t) = 1 - \Phi(t)$). The Gaussian-quantile and KL-ball duality lemmas are reusable beyond this mission. Contributions of any of these as separate lemmas are welcome.

Selected references

• L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
• M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102
• L. P. Hansen, T. J. Sargent, Robust Control and Model Uncertainty, American Economic Review 91(2):60–66, 2001. https://doi.org/10.1257/aer.91.2.60

Motivation

A forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.

Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.

Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.

Setting

Player 2 has $n\ge 1$ pure strategies $j\in\{0,\dots,n-1\}$. In every round, player 1 announces a forecast $p\in\mathbb R^n$, a probability vector ($p_j\ge 0$, $\sum_j p_j = 1$), and player 2 plays a strategy $j$. The two moves are simultaneous: player 2 does not see the current forecast.

A history $h$ of length $t$ is the list of the $t$ pairs (forecast, play), oldest first. For a forecast vector $p$ and a strategy $j$:

• $N(p,t)$ is the number of rounds of $h$ in which $p$ was forecast;
• $\rho(p,j,t)$ is the fraction of those rounds in which player 2 played $j$ (and $0$ if $N(p,t)=0$);
• the calibration score (Eq. (1), p. 49) is

$$C_t = \sum_p\sum_j \bigl|\rho(p,j,t) - p_j\bigr|\,\frac{N(p,t)}{t}.$$

A randomized forecaster $F$ maps each history to a probability distribution on forecasts. A learning rule $A$ of player 2 maps each history to a probability distribution on strategies. In round $t+1$ the forecast is drawn from $F(h)$ and the play from $A(h)$, independently given the history $h$ of the first $t$ rounds. This defines the law $\mathbb P_{F,A}$ of the first $t$ rounds (histLaw F A t).

For the Appendix: with $k$ forecasts, losses $L_t^i$ and mixing weights $w_t^i$, the pairwise regret of replacing forecast $i$ by forecast $j$ is

$$R_T^{i\to j} = \max\Bigl\{0,\ \sum_{t=1}^T w_t^i\,(L_t^i - L_t^j)\Bigr\}.$$

Formalization targets

Goal: Theorem 3 (p. 49)

There is a forecaster $F$, with probability-vector forecasts, such that for every learning rule $A$ of player 2 and every $\varepsilon>0$,

$$\lim_{t\to\infty}\mathbb P_{F,A}\bigl(C_t<\varepsilon\bigr) = 1.$$

The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on $A$.

Milestones, in the order the Appendix uses them

1. Flow conservation is solvable (p. 52). For every nonnegative $k\times k$ matrix $R$, $k\ge 1$, there is a probability vector $w$ with $w^i\sum_j R^{i\to j} = \sum_j w^j R^{j\to i}$ for all $i$.
2. Lemma 1 (No-Regret) (p. 52). With losses in $[0,1]$ and weights solving flow conservation for the previous regrets,

$$R_T^{i\to j}\le\sqrt{2kT}\quad\text{for all } i,j,T.$$

3. Regrets sandwich L-2 calibration (p. 54). For a grid $p^1,\dots,p^k$ that is $\varepsilon$-dense in squared distance and losses $L_t^i = |X_t - p^i|^2$,

$$\sum_i\max_j \frac{R_T^{i\to j}}{T}\ \le\ C_{2,w}(T)\ \le\ \varepsilon + \sum_i\max_j\frac{R_T^{i\to j}}{T},$$

with $C_{2,w}$ the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each $j$, $\sum_p|\rho(p,j,t)-p_j|\,N(p,t)/t \le \sqrt{\sum_p(\rho(p,j,t)-p_j)^2 N(p,t)/t}$.

Significance

The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.

Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.

Difficulty

The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret $R^{i\to j}$ at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.

Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast $p^i$ was issued" is replaced by its probability $w_t^i$. The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh $\varepsilon$. Exact convergence requires letting the grid size $k$ grow and $\varepsilon$ shrink over time, and the scores of the different phases must be combined.

Formalization scope

• Model. Strategies are Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. $\mathbb P(C_t<\varepsilon)$ is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.
• Opponent. The opponent may be randomized and may depend on all past forecasts and plays; fixed sequences and deterministic rules are special cases. The opponent never sees the current forecast. Letting it see the current forecast would make the goal false, and restricting to fixed sequences would make it weaker than the paper.
• Quantifiers. The forecaster is chosen before the opponent (∃ F, ∀ A). The reverse order is trivial, since one can forecast $A$'s next play.
• Conventions. Rounds are counted from $0$, so the paper's rounds $1,\dots,t$ are the first $t$ list entries. The paper's $R_{t-1}$ is the regret over the $0$-based rounds before $t$. Forecasts are grouped by exact equality of real vectors. Sums over $p$ run over the forecasts that occur, and every other term vanishes. Scores divide by the history length, and are $0$ for the empty history. "Converges in probability" is the $\lim\mathbb P(C_t<\varepsilon)=1$ form the page states. The grid of milestone 3 is indexed $1,\dots,k$ (the page writes $i = 0,\dots,k$ on p. 53 and $1,\dots,k$ in Lemma 1), and "within $\varepsilon$" is read in squared Euclidean distance.
• Pinned reading. The page writes the middle term of milestone 3 as $E(C_2(t))$ with a garbled formula. The mission states the inequality for the fractional score $C_{2,w}$, for which it holds.
• Steps the paper leaves informal, not stated as milestones. (a) "$E(C_2(t))\le\varepsilon + O(k/\sqrt2)$" when the weights solve flow conservation; the $O$-term is garbled and should decay in $t$. (b) "if we let $k$ grow slowly and $\varepsilon$ go slowly to zero … $C_2(t)\to 0$ in expectation which implies $C_2(t)\to0$ in probability by Jensen's inequality", together with the passage from the fractional score to the realized one. Solvers will have to formalize these steps on the way to the goal.
• Not included. The Corollary on p. 49 (convergence in probability of play to the correlated equilibria when both players use the scheme). It needs the game layer and a quantitative form of Theorem 1, and the page gives no proof.
• Infrastructure welcome. Finite Markov chain stationary distributions (for milestone 1), for which Prove2Me has MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.

Selected references

• 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. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85 (1998) 379–390. https://doi.org/10.1093/biomet/85.2.379
• A. P. Dawid, The well-calibrated Bayesian, J. Amer. Statist. Assoc. 77 (1982) 605–613. https://doi.org/10.1080/01621459.1982.10477856
• D. Oakes, Self-calibrating priors do not exist, J. Amer. Statist. Assoc. 80 (1985) 339. https://doi.org/10.1080/01621459.1985.10478117
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153