Statistics

Motivation

A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.

Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most $\sqrt{2\sigma^2 I(S;W)/n}$, where $I(S;W)$ is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).

Timeline:

• 2016, Russo and Zou: bias of adaptive analysis bounded by $I(\Lambda_{\mathsf W}(S);W)$, the information carried by the vector of empirical risks, for a finite hypothesis space.
• 2017, Xu and Raginsky: the bound with the input–output mutual information $I(S;W)$, for arbitrary hypothesis spaces (Theorem 1); high-probability versions and an analysis of the Gibbs algorithm.
• 2018–2020: chaining, individual-sample and conditional mutual information refinements.

Setting

There is an instance space $\mathsf Z$, a hypothesis space $\mathsf W$ and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$, written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure $\mu$ on $\mathsf Z$; a dataset of size $n$ is an i.i.d. sample $S=(Z_1,\dots,Z_n)\sim\mu^{\otimes n}$ (sampleLaw μ n).

A learning algorithm is a Markov kernel $P_{W|S}$ (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis $W$. The pair $(S,W)$ has joint law $P_{S,W}=\mu^{\otimes n}\otimes P_{W|S}$ (sampleLaw μ n ⊗ₘ κ), with marginals $P_S=\mu^{\otimes n}$ and $P_W$.

The population risk and the empirical risk of a hypothesis $w$ are

$$L_\mu(w)=\int_{\mathsf Z}\ell(w,z)\,\mu(dz),\qquad L_S(w)=\frac1n\sum_{i=1}^n \ell(w,Z_i)$$

(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is

$$\mathrm{gen}(\mu,P_{W|S})=\mathbb E\big[L_\mu(W)-L_S(W)\big],$$

the expectation taken under $P_{S,W}$ (genError ℓ μ κ).

The mutual information of a pair $(X,Y)$ with joint law $P_{X,Y}$ is the relative entropy $I(X;Y)=D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$ (mutualInfo). A real random variable $U$ is $\sigma$-subgaussian if $\log\mathbb E[e^{\lambda(U-\mathbb EU)}]\le\lambda^2\sigma^2/2$ for all $\lambda\in\mathbb R$.

Formalization targets

Goal: Theorem 1 (p. 4)

If $\ell(w,Z)$ is $\sigma$-subgaussian under $\mu$ for every $w\in\mathsf W$, then

$$\big|\mathrm{gen}(\mu,P_{W|S})\big|\le\sqrt{\frac{2\sigma^2}{n}\,I(S;W)} .$$

The statement fixes no structure on $\mathsf W$ (it may be uncountable) and no bound on the loss beyond subgaussianity.

Milestones

1. (A.1), Donsker–Varadhan (p. 11), the inequality $\int F\,d\pi-D(\pi\|\rho)\le\log\int e^F\,d\rho$. Already proved on the platform and referenced.
2. Lemma 1 (p. 3), the decoupling estimate: if $f(\bar X,\bar Y)$ is $\sigma$-subgaussian under $P_X\otimes P_Y$, then

$$\big|\mathbb E f(X,Y)-\mathbb E f(\bar X,\bar Y)\big|\le\sqrt{2\sigma^2 I(X;Y)} .$$

3. Subgaussianity of the empirical risk (§3.2, p. 4): for every $w$, $L_S(w)-L_\mu(w)$ is $\sigma/\sqrt n$-subgaussian under $\mu^{\otimes n}$.
4. The mixture step (§3.2, p. 4, corrected): under $P_S\otimes P_W$, $f(\bar S,\bar W)=L_{\bar S}(\bar W)-L_\mu(\bar W)$ is $\sigma/\sqrt n$-subgaussian with mean $0$.

Significance

The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits $I(S;W)$, such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in $[a,b]$ is $(b-a)/2$-subgaussian for every $\mu$, so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.

Difficulty

The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs $\mathbb E f(X,Y)$ to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section $w\mapsto f(\cdot,w)$ to integrate over $P_W$, which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk $L_{\bar S}(\bar W)$ mixes laws with different means and is not subgaussian.

A natural first attempt applies Lemma 1 directly to $f(s,w)=L_s(w)$ as printed; it fails on the example $\ell(w,z)=w$ with $W$ uniform on $\{0,1\}$ and independent of $S$.

Formalization scope

• Objects. The sample law, $L_\mu$ and $L_S$ are reused from the published LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in $[0,\infty]$) and genError, the integral of the pointwise difference $L_\mu(w)-L_s(w)$ under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.
• Subgaussianity is Mathlib's HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: $\sigma^2$ for the loss, $\sigma^2/n$ for the empirical risk.
• Added hypotheses, all implicit on the page: $n\ge1$ (the bound divides by $n$); joint measurability of $\ell$ (so that $L_\mu(W)$ and $L_S(W)$ are random variables); and $I\ne\infty$ in Lemma 1 and Theorem 1, because Lean's conversion of $\infty$ to a real number gives $0$, which would turn the page's vacuous bound into a false claim. The page's nonnegativity of $\ell$ is kept. No integrability hypothesis on $f$ or on the losses is assumed beyond subgaussianity.
• Correction of the print. The page says that $f(\bar S,\bar W)=L_{\bar S}(\bar W)$ is $\sigma/\sqrt n$-subgaussian; milestone 4 states it for the centred $L_{\bar S}(\bar W)-L_\mu(\bar W)$, together with its mean being $0$. Equation (9) is not posed separately.
• Ruled out. The goal is stated for genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair $(\bar X,\bar Y)$, through $I(\Lambda_{\mathsf W}(S);W)$ (Theorem 2, out of scope), or with $I$ truncated to a real number would not be this theorem.
• Infrastructure. Integrability transfer from $P_X\otimes P_Y$ to $P_{X,Y}$ under finite relative entropy; sums of independent subgaussian variables on Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.

Selected references

• A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017; arXiv:1705.07809v2. https://arxiv.org/abs/1705.07809
• D. Russo, J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. https://arxiv.org/abs/1511.05219
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• O. Bousquet, A. Elisseeff, Stability and generalization, JMLR 2, 2002. https://www.jmlr.org/papers/v2/bousquet02a.html
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013 (Donsker–Varadhan, Cor. 4.15). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Asadi, E. Abbe, S. Verdú, Chaining mutual information and tightening generalization bounds, NeurIPS 2018. https://arxiv.org/abs/1806.03803
• Y. Bu, S. Zou, V. Veeravalli, Tightening mutual information based bounds on generalization error, IEEE JSAIT 2020. https://arxiv.org/abs/1901.04609
• T. Steinke, L. Zakynthinou, Reasoning about generalization via conditional mutual information, COLT 2020. https://arxiv.org/abs/2001.09122

Motivation

Thompson Sampling is the oldest bandit algorithm: Thompson proposed it in 1933 for allocating patients between two treatments (Thompson 1933). It keeps a posterior distribution over the unknown mean reward of every action, draws one sample from each posterior, and plays the action whose sample is largest. It is simple, widely used, and in experiments competitive with index policies designed for optimality. For decades it had no matching theoretical guarantee.

The benchmark for a stochastic bandit algorithm is the lower bound of Lai and Robbins (1985): every consistent policy draws a suboptimal arm $a$ at least $(1-o(1))\ln T/K(\mu_a,\mu^*)$ times in $T$ rounds, where $K$ is the Kullback–Leibler divergence. A policy that attains this rate is called asymptotically optimal.

Timeline.

• 1933: Thompson introduces the algorithm, without analysis.
• 1985: Lai and Robbins prove the lower bound and construct asymptotically optimal (but complex) policies.
• 2011–2012: KL-UCB (Garivier and Cappé 2011) and Bayes-UCB (Kaufmann, Cappé and Garivier 2012) attain the bound for Bernoulli rewards with simpler index rules.
• 2012: Agrawal and Goyal give the first logarithmic regret bound for Thompson Sampling, $O\big((\sum_a 1/\Delta_a^2)^2\ln T\big)$, which does not have the optimal constant.
• 2012: Kaufmann, Korda and Munos (arXiv:1205.4217) prove that Thompson Sampling with uniform priors is asymptotically optimal for Bernoulli rewards, with a finite-time bound. This mission formalizes that result.

Setting

There are $K\ge2$ arms. Arm $a$ yields reward $1$ with probability $\mu_a\in(0,1)$ and $0$ otherwise. Arm $1$ is the unique optimal arm: $\mu^*=\mu_1>\mu_a$ for every $a\neq1$. The gap of arm $a$ is $\Delta_a=\mu^*-\mu_a$, and $\mu_2$ denotes the largest mean among the suboptimal arms.

Thompson Sampling with uniform priors. Let $N_{a,t}$ be the number of times arm $a$ has been drawn before round $t$ and $S_{a,t}$ the number of rewards equal to $1$ among those draws. With a uniform prior, the posterior of $\mu_a$ is $\mathrm{Beta}(S_{a,t}+1,\,N_{a,t}-S_{a,t}+1)$. In round $t$ the algorithm draws, independently, a sample $\theta_{a,t}$ from each posterior, plays $A_t=\arg\max_a\theta_{a,t}$, and observes the reward of $A_t$.

The regret after $T$ rounds is

$$\mathcal R(T)=T\mu^*-\mathbb E\Big[\sum_{t=1}^T R_t\Big]=\sum_a\Delta_a\,\mathbb E[N_{a,T}],$$

where $N_{a,T}$ now counts the draws of $a$ in rounds $1,\dots,T$. The Bernoulli divergence is $K(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}$.

The analysis compares the Thompson samples with two index rules. For an arm with $S$ successes in $N$ draws, at round $t$ of a horizon $T$, the KL-UCB index is $u=\sup\{x\in[S/N,1):N\,K(S/N,x)\le\ln t+\ln\ln T\}$, and the Bayes-UCB index $q$ is the quantile of order $1-\frac1{t\ln T}$ of the posterior $\mathrm{Beta}(S+1,N-S+1)$.

Formalization targets

Goal: Theorem 1 (p. 3)

For every $\epsilon>0$ there is a constant $C$, depending on $\epsilon$ and the instance, such that for every horizon $T$,

$$\mathcal R(T)\le(1+\epsilon)\sum_{a:\,\mu_a\neq\mu^*}\frac{\Delta_a(\ln T+\ln\ln T)}{K(\mu_a,\mu^*)}+C.$$

Only the existence of $C$ is asserted; its value is not fixed, so improvements of the lower-order terms do not invalidate the goal.

Milestones

1. Eq. (1): $\mathcal R(T)=T\mu^*-\mathbb E[\sum_{t=1}^T R_t]=\sum_a\Delta_a\,\mathbb E[N_{a,T}]$.
2. Theorem 2 (p. 4): for each suboptimal $a$ and $\epsilon>0$, $\mathbb E[N_{a,T}]\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+C$.
3. Proposition 1 (p. 4): there is $b\in(0,1)$ with $\sum_{t\ge1}\mathbb P(N_{1,t}\le t^b)<\infty$.
4. Display (4) (p. 5): $\mathbb E[N_{a,T}]\le A+B+2$, an under-estimation term $A$ for arm $1$ plus a KL-UCB term $B$.
5. Lemma 1 (p. 5): $\sum_t\mathbb P\big(\theta_{1,t}\le\mu_1-\sqrt{6\ln t/N_{1,t}}\big)\le N_0(b)+3+C_b$.
6. Lemma 2 (p. 6): $B\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+D$ for large $T$.
7. Lemma 3 (p. 9), in its analytic form (§3.4): a bound on the probability that the optimal arm's samples stay below $\mu_2+\delta$ for $f$ rounds.
8. Lemma 4 (p. 9): saturated suboptimal arms rarely produce samples above $\mu_a+\delta_a$.
9. §2 (p. 3): the Beta–Binomial identity (referenced) and the comparison $q<u$ of the two indices.

Significance

The result. Theorem 1 shows that the leading constant of Thompson Sampling's regret equals the Lai–Robbins constant, so no consistent policy does asymptotically better on Bernoulli bandits. It settled a question open since 1933 and is the starting point for later optimality proofs of Thompson Sampling for exponential families and Gaussian rewards. Proposition 1, a summable tail bound on the event that the optimal arm is under-sampled, is the reusable core: it is a deviation inequality for the number of draws of the optimal arm, which a bound on its expectation does not imply.

The formalization. The result is proved on paper; no machine-checked proof of an optimal-constant bound for Bernoulli Thompson Sampling exists. The platform already has the Gaussian frequentist analysis of Lattimore and Szepesvári (Theorem 36.3) and the non-optimal Agrawal–Goyal bound. This mission adds the Bernoulli, Beta-posterior case with the KL constant, the KL-UCB and Bayes-UCB indices with the $\ln t+\ln\ln T$ exploration rate, and the optimal-arm tail bound. Corrected statements are part of the output: the explicit constant $D$ printed at the end of Lemma 2's proof is too small, the constant $C_{\lambda,\mu_1,\mu_2}$ printed for Lemma 3 has the wrong sign, and Lemma 3 as printed quantifies over arbitrary random intervals, which its proof does not support.

Difficulty

The standard proof for an optimistic index policy bounds the draws of a suboptimal arm by an under-estimation term $\sum_t\mathbb P(l_{1,t}<\mu_1)$ and a concentration term. For Thompson Sampling the under-estimation term is not small: once the posterior of arm $1$ is concentrated, $\mathbb P(\theta_{1,t}<\mu_1)$ is close to $1/2$ in every round. Comparing $\theta_{1,t}$ with a lower confidence bound $\mu_1-\sqrt{6\ln t/N_{1,t}}$ instead only helps if $N_{1,t}$ is large with overwhelming probability, and a bound on $\mathbb E[N_{1,t}]$ does not give that.

Proposition 1 supplies it, and it carries most of the difficulty. It must control long stretches of rounds in which arm $1$ is never drawn while several suboptimal arms compete, and it needs the samples of arm $1$ conditioned on its successes at a random time while the arm is not played, an optional-skipping step that the paper leaves implicit and that is the main measure-theoretic obstacle in Lean.

Formalization scope

Representation. The algorithm is the published Thompson Sampling run (AgrawalGoyalTS_TwoArmed_ThompsonSampling) on the published Bernoulli bandit (bernoulliRelativeEntropy). That run is Agrawal–Goyal's Algorithm 2, which passes each reward through a Bernoulli trial of success probability equal to the reward; for $\{0,1\}$ rewards the trial returns the reward almost surely, so the posterior is exactly the paper's. Probabilities are values of tsLaw in $[0,\infty]$, expectations of counts and the regret are lower integrals in $[0,\infty]$, and every bound compares with the embedding of a real right-hand side.

Conventions.

• Lean arm $0$ is the paper's arm $1$. Lean round $t$ is the paper's round $t+1$; $N_{a,t}$, $S_{a,t}$ are the counts when $\theta_{a,t}$ is drawn, and the paper's $\ln t$ is $\ln(t+1)$ at Lean round $t$.
• $\sqrt{6\ln t/N_{1,t}}=\infty$ when $N_{1,t}=0$ (p. 4), encoded by cases.
• The KL-UCB supremum ranges over $x<1$, because the real-valued divergence at $q=1$ is a finite junk value; $u=1$ when $N=0$ or $S=N$, cases the page leaves undefined.
• Every constant with a printed dependence list ($C$, $D$, $N$, $b$, $C_b$) is chosen after the instance (and $\epsilon$, the arm) and before $T$.

Added hypotheses and corrections.

• $0<\mu_a<1$ for every arm, and $K\ge2$: not stated in the paper but used by its proof (it divides by $\mu_1(1-\mu_1)$, and $K(\mu_a,1)=\infty$).
• Arm $1$ is the unique optimal arm (the paper's standing assumption of §2; its reduction of several optimal arms to one is cited, not proved).
• Display (4) and the index comparison are stated for $T\ge3$ (the page's $T\ge e$) and rounds $1\le t\le T$.
• Lemma 2 asserts only the existence of $D$; Lemma 3 is formalized as the analytic bound of §3.4 with the sign-corrected constant; Lemma 1's $C_b$ is read with the pre-draw count.

Trivializations ruled out. Thompson Sampling is not characterized by a predicate that an arbitrary policy could satisfy: it is the published run, which fixes the posterior draws, the argmax and the updates. The constant is quantified as $\forall\epsilon\,\exists C\,\forall T$, never $\forall T\,\exists C$, and no real number is extracted from a possibly infinite expectation.

Infrastructure and contributions. A complete development needs Beta–Binomial duality, Chernoff–Hoeffding bounds for binomial tails, optional skipping for the reward stacks of the played arms, and the KL-UCB counting argument. The Beta–Binomial identity is an open milestone shared with the Agrawal–Goyal mission. Proofs of any milestone, in particular Proposition 1, Lemma 4 and the analytic Lemma 3, are welcome; Lemma 3's bound and the index comparison are pure real analysis and reusable beyond bandits.

Selected references

• E. Kaufmann, N. Korda, R. Munos, Thompson Sampling: An Asymptotically Optimal Finite Time Analysis, ALT 2012 (LNCS 7568); arXiv:1205.4217v2. https://arxiv.org/abs/1205.4217
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.2307/2332286
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• S. Agrawal, N. Goyal, Analysis of Thompson Sampling for the multi-armed bandit problem, COLT 2012; arXiv:1111.1797. https://arxiv.org/abs/1111.1797
• A. Garivier, O. Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond, COLT 2011; arXiv:1102.2490. https://arxiv.org/abs/1102.2490
• E. Kaufmann, O. Cappé, A. Garivier, On Bayesian upper confidence bounds for bandit problems, AISTATS 2012. https://proceedings.mlr.press/v22/kaufmann12.html

Motivation

Matrix completion asks to recover a large matrix from a small number of its entries. It is the abstraction behind collaborative filtering (recommender systems in which a users × items rating matrix is observed on a sparse set of pairs), sensor localization from partial distance information, and system identification. Without structure the problem is hopeless; the standard structural assumption is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of singular values.

In the noiseless case, exact recovery by nuclear-norm minimization from about $r(m_1\vee m_2)\,\mathrm{polylog}$ uniformly sampled entries was established by Candès and Recht (2009) and refined by Candès and Tao (2010) and Gross (2011). With noisy observations the relevant question is a rate: how fast does an estimator's error decrease with the number $n$ of observed entries? Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256, Ann. Statist. 2011) introduced a nuclear-norm penalized estimator that uses the known sampling distribution, showed that in matrix completion it is an explicit soft thresholding of the singular values of a rescaled data matrix, and proved for it sharp oracle inequalities (leading constant 1) whose rates are optimal up to logarithmic factors. This mission formalizes the version of that result for bounded responses: Theorem 4 of the paper, together with the probabilistic lemma and the matrix Bernstein inequality it rests on.

Setting

Fix positive integers $n, m_1, m_2$ and write $\mathbb R^{m_1\times m_2}$ for the real $m_1\times m_2$ matrices, with scalar product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$, Frobenius norm $\|A\|_2$, nuclear norm $\|A\|_1$ (sum of singular values) and operator norm $\|A\|_\infty$ (largest singular value). Set $m=m_1+m_2$ and write $m_1\wedge m_2=\min(m_1,m_2)$.

The matrix completion basis is

$$\mathcal X=\{e_j(m_1)e_k^\top(m_2):1\le j\le m_1,\ 1\le k\le m_2\},$$

where $e_k(m)$ are the canonical basis vectors of $\mathbb R^m$. One observes $n$ independent random pairs $(X_i,Y_i)$, where $X_i$ is uniformly distributed on $\mathcal X$ and $Y_i$ is real, following the trace regression model

$$\mathbb E(Y_i\mid X_i)=\operatorname{tr}(X_i^\top A_0),$$

for an unknown $A_0\in\mathbb R^{m_1\times m_2}$. Thus $Y_i$ is a noisy reading of the entry of $A_0$ selected by $X_i$; this is matrix completion under uniform sampling at random (USR), entries possibly sampled more than once.

The estimator is, for a regularization parameter $\lambda>0$,

$$\hat A^\lambda=\operatorname*{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\frac1{m_1m_2}\|A\|_2^2-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1\Big).$$

The stochastic error is the random matrix

$$\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).$$

Formalization targets

Goal: Theorem 4

Assume $\max_i|Y_i|\le\eta$ almost surely. For $t>0$ and

$$\lambda\ge4\eta\max\Big\{\sqrt{\frac{t+\log m}{(m_1\wedge m_2)n}},\ \frac{2(t+\log m)}{n}\Big\},$$

with probability at least $1-e^{-t}$, simultaneously for all $A\in\mathbb R^{m_1\times m_2}$,

$$\|\hat A^\lambda-A_0\|_2^2\le\|A-A_0\|_2^2+m_1m_2\min\Big\{2\lambda\|A\|_1,\ \Big(\frac{1+\sqrt2}2\Big)^2m_1m_2\lambda^2\operatorname{rank}(A)\Big\}.$$

Milestones

1. (1.4): $\|A\|_{L_2(\Pi)}^2=\frac1n\sum_i\mathbb E\langle A,X_i\rangle^2=(m_1m_2)^{-1}\|A\|_2^2$ for the uniform design.
2. Theorem 1 for USR matrix completion: at every sample point where $\lambda\ge2\|\mathbf M\|_\infty$, the inequality above holds for all $A$ (a deterministic statement).
3. Proposition 1 (matrix Bernstein): for independent centred $m_1\times m_2$ random matrices $Z_i$ with $\|Z_i\|\le U$ a.s., with probability at least $1-e^{-t}$,

$$\Big\|\frac{Z_1+\dots+Z_n}n\Big\|\le2\max\Big\{\sigma_Z\sqrt{\frac{t+\log m}n},\ U\frac{t+\log m}n\Big\}.$$

4. (6.2): for $X$ uniform on $\mathcal X$, $\|X\|=1$, $\|\mathbb EX\|=(m_1m_2)^{-1/2}$, $\sigma_X^2=1/(m_1\wedge m_2)$.
5. Lemma 1: with probability at least $1-e^{-t}$, $\|\mathbf M\|\le2\eta\max\{\sqrt{(t+\log m)/((m_1\wedge m_2)n)},\ 2(t+\log m)/n\}$.

Significance

Theorem 4 is a non-asymptotic, sharp oracle inequality: the leading constant in front of $\|A-A_0\|_2^2$ is 1, so the bound applies to misspecified targets ($A_0$ not low rank) without loss. Taking $A=A_0$ and $t$ of order $\log m$ gives a normalized Frobenius error of order $\eta^2(m_1\vee m_2)\operatorname{rank}(A_0)\log(m)/n$, which the paper's minimax lower bounds (§4) show to be optimal up to the logarithm. Because no model is needed for Lemma 1, the same probability bound also drives the paper's statistical-learning reformulation (Theorem 9).

The theorems here are proved in the paper. What is open is their formalization: no matrix Bernstein inequality, and no oracle inequality for nuclear-norm penalized estimators, has a machine-checked proof on this platform. Proposition 1 in particular is a reusable concentration tool well beyond this paper (covariance estimation, random graphs, sketching).

Difficulty

The deterministic part (milestone 2) needs the subdifferential of the nuclear norm, which is not in Mathlib. The probabilistic part is where the obvious argument fails. Bounding $\|\mathbf M\|_\infty$ entrywise and summing, or bounding it by the Frobenius norm, loses a factor polynomial in the dimension; a union bound over a net of the unit sphere loses the factor $m_1\wedge m_2$ that makes the rate optimal. The correct rate requires a noncommutative Bernstein inequality, controlling the operator norm of a sum of independent random matrices through the matrix variance $\sigma_Z^2$ at the price of only a $\log(m_1+m_2)$ factor. The matrix-analytic machinery such inequalities depend on (trace inequalities for matrix exponentials, the passage from rectangular to symmetric matrices) is not currently available in Mathlib.

Formalization scope

All objects are local to the namespace KLTNuclear.Completion, built on the published MatrixCompletion definitions (RealMatrix, nuclearNorm, spectralNorm, frobeniusNormSq, matrixInner, coordinateMatrix). Conventions:

• The probability space carries IsProbabilityMeasure; $n,m_1,m_2\ge1$ are hypotheses. $\log$ is the natural logarithm; $m=m_1+m_2\ge2$.
• The design is encoded by uniform random indices $I_i\in[m_1]\times[m_2]$ with $X_i=e_{j_i}e_{k_i}^\top$. Mathlib has no $\sigma$-algebra on Matrix, so measurability, independence and conditioning on a random matrix use its entry array with the product $\sigma$-algebra; expectations of matrices are entrywise.
• The model (1.1) is a conditional expectation given $\sigma(X_i)$. Independence of the pairs $(X_i,Y_i)$ is the paper's standing assumption (p. 1) and is assumed in Lemma 1 and Theorem 4, whose proof applies Proposition 1 to $Z_i=Y_iX_i-\mathbb E(Y_iX_i)$; the $Y_i$ are not assumed identically distributed. $\lambda>0$ is the standing assumption of (1.6). Integrable responses are assumed in milestone 2, bounded measurable responses in Lemma 1 and Theorem 4.
• $\hat A^\lambda$ is any minimizer of (3.1) at each sample point (it exists and is unique, but neither fact is assumed); the soft-thresholding formula (3.2) is not used as a definition.
• "With probability at least $1-e^{-t}$" is encoded as an upper bound $e^{-t}$ on the outer measure of the failure set; in Theorem 4 the failure set is $\{\omega:\exists A,\ \text{(3.5) fails}\}$, so the bound is uniform in $A$. A formalization that fixes $A$ before the probability is weaker and is not the target.
• No printed slip affects these statements; Corollary 2(ii) of the paper, whose $\lambda$ falls below (3.6), is deliberately not included.

The source is the arXiv preprint arXiv:1011.6256v4. Welcome contributions: a general matrix Bernstein inequality (Hermitian and rectangular forms), the nuclear-norm subdifferential, and proofs of the deterministic milestone.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
• J. A. Tropp, User-friendly tail bounds for sums of random matrices, Found. Comput. Math. 12, 2012. https://doi.org/10.1007/s10208-011-9099-z
• E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://doi.org/10.1007/s10208-009-9045-5
• E. J. Candès, T. Tao, The power of convex relaxation: near-optimal matrix completion, IEEE Trans. Inform. Theory 56, 2010. https://doi.org/10.1109/TIT.2010.2044061
• D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Trans. Inform. Theory 57, 2011. https://doi.org/10.1109/TIT.2011.2104999

Motivation

Noisy low-rank matrix completion asks to reconstruct an $m_1\times m_2$ matrix $A_0$ from $n$ noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order $\operatorname{rank}(A_0)(m_1\vee m_2)\log(m_1+m_2)/n$ up to normalization, which matches the minimax lower bound up to a logarithmic factor.

An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of $A_0$; if the nonzero singular values of $A_0$ are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.

Setting

Fix integers $m_1,m_2,n\ge1$. The matrix completion basis is $\mathcal X=\{e_j(m_1)e_k(m_2)^\top\}$, the $m_1m_2$ matrices with a single entry equal to $1$. A sample consists of $n$ pairs $(X_i,Y_i)$ with $X_i\in\mathcal X$ (an observed position $(j_i,k_i)$) and $Y_i\in\mathbb R$ (a noisy observation of the corresponding entry of the unknown matrix $A_0$). Write $\langle A,B\rangle=\operatorname{tr}(A^\top B)$, $\|A\|_2$ for the Frobenius norm, $\|A\|_1$ for the nuclear norm (the sum of the singular values) and $\|A\|_\infty$ for the operator norm (the largest singular value). The singular values of $B$ are $\sigma_1(B)\ge\sigma_2(B)\ge\dots\ge\sigma_{m_1\wedge m_2}(B)\ge0$.

From the sample form

$$\mathbf X=\frac{m_1m_2}{n}\sum_{i=1}^nY_iX_i,\qquad \mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).$$

In the paper's model $\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle$ with $X_i$ uniform on $\mathcal X$, so $\mathbb E(Y_iX_i)=A_0/(m_1m_2)$ and $\mathbf X-A_0=m_1m_2\mathbf M$: the matrix $\mathbf M$ is the stochastic error. For $\lambda>0$ the estimator (3.1) is

$$\hat A^\lambda=\operatorname{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1\Big).$$

The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of $\mathbf X$ by soft thresholding every singular value at level $\lambda m_1m_2/2$.

Formalization targets

Goal: Theorem 8 (p. 20)

Let $\lambda\ge2\|\mathbf M\|_\infty$, $0<\delta<1$ and $\lambda'=\lambda/(1-\delta)$, and put $\hat r=\operatorname{rank}(\hat A^{\lambda'})$. Then

$$\hat r\le\operatorname{rank}(A_0).\tag{5.1}$$

If in addition $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$, then

$$\hat r\ge\operatorname{rank}(A_0)\tag{5.2}$$

and

$$\|\hat A^{\lambda'}-A_0\|_2^2\ge\frac{\delta^2}{4(1-\delta)^2}\operatorname{rank}(A_0)\,(\lambda m_1m_2)^2.\tag{5.3}$$

Milestones

The milestones follow the proof on p. 20 in order:

1. the singular value perturbation display $|\sigma_j(\mathbf X)-\sigma_j(A_0)|\le\sigma_1(\mathbf X-A_0)=m_1m_2\|\mathbf M\|_\infty\le\lambda m_1m_2/2$;
2. the rank of $\hat A^\lambda$ equals the number of singular values of $\mathbf X$ above $\lambda m_1m_2/2$ (the consequence of (3.2) the proof uses);
3. (5.1);
4. (5.2);
5. $\|\mathcal P(\hat A^{\lambda'}-\mathbf X)\|_2=\sqrt r\,\lambda'm_1m_2/2$ when $\hat r=r$, for the projector $\mathcal P$ onto the span of the top $r$ singular pairs $u_j(\mathbf X)v_j(\mathbf X)^\top$;
6. $\|\mathcal P(\mathbf X-A_0)\|_2\le\sqrt r\|\mathbf M\|_\infty m_1m_2\le\sqrt r\lambda m_1m_2/2$.

Significance

The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for $\|\mathbf M\|_\infty$ (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event $\lambda\ge2\|\mathbf M\|_\infty$, it applies unchanged to any noise model for which such a bound on the stochastic error is available.

Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.

Difficulty

The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality $|\sigma_j(B)-\sigma_j(C)|\le\|B-C\|_\infty$, which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of $T^*T$ but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of $\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1$: one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with $\mathbf X$ entrywise gives nothing about the rank; the proof needs the spectral structure.

Formalization scope

Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's $\sigma_{j+1}(B)$. The conventions committed to:

• The statements are realization-wise: positions idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying $\lambda\ge2\|\mathbf M\|_\infty$. The matrix $\mathbf M$ is written as $\frac1n\sum_iY_iX_i-A_0/(m_1m_2)$, which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that $\mathbf X-A_0=m_1m_2\mathbf M$". The probabilistic hypotheses are used for nothing else.
• $n,m_1,m_2\ge1$ and $\lambda>0$ are assumed, as in the paper.
• The estimator is any minimizer of (3.1) over all matrices, never the soft-thresholding formula; replacing the minimizer by formula (3.2) would assume the open Cai–Candès–Shen item.
• $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ is written "for every $j$ with $\sigma_j(A_0)\ne0$"; for $A_0=0$ it is vacuous, as on the page. No real infimum over a possibly empty set is used.
• The projector $\mathcal P$ is built from a singular value decomposition of $\mathbf X$ carried as data, with decreasing singular values, from its first $r$ pairs.

No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.

Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top-$r$ projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.

The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
• G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press, 1990 (reference [25] of the paper, p. 203).
• E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722

Motivation

Principal component analysis finds the best low-rank approximation of a data matrix, and it is used everywhere data come as a table: images, video, genomics, web and survey data. Its weakness is well known: a single grossly corrupted entry can move the classical principal components arbitrarily far. In many applications the corruptions are not small noise but gross errors at a fraction of the entries: occlusions and specularities in face images, moving foreground objects in surveillance video, corrupted or adversarial records. Robust variants of PCA built on robust statistics or on alternating heuristics came without guarantees of exact recovery.

Candès, Li, Ma and Wright (J. ACM 58(3), 2011) showed that a single convex program recovers both the low-rank part and the corruptions exactly, under a randomness assumption on the corruption pattern only, with a weight that needs no tuning.

Timeline.

• 2009: Candès and Recht prove exact matrix completion by nuclear-norm minimization under incoherence (FoCM 2009). Their concentration results reappear here as Theorem 2.6 and Lemma 3.2.
• 2009: Chandrasekaran, Sanghavi, Parrilo and Willsky give deterministic conditions for the same convex decomposition (SIAM J. Optim. 2011, arXiv:0906.2220). As compared on p. 7 of the present paper, these conditions allow only a vanishing fraction $O((nr)^{-1/2})$ of corrupted entries, and they leave the weight $\lambda$ to be searched for.
• 2009: Gross introduces the golfing scheme for constructing dual certificates (IEEE Trans. Inf. Theory 2011, arXiv:0910.1879). This paper adapts it.
• 2009–2011: the present paper (preprint of 17 December 2009) proves Theorem 1.1: a constant fraction of corrupted entries and rank up to $n/(\log n)^2$.

Setting

Let $L_0\in\mathbb R^{n\times n}$ have rank $r$ and compact singular value decomposition $L_0=\sum_{k=1}^r\sigma_k u_kv_k^*$ with $\sigma_k>0$, where $U=[u_1,\dots,u_r]$ and $V=[v_1,\dots,v_r]$ have orthonormal columns. The nuclear norm $\|M\|_*$ is the sum of the singular values of $M$, and $\|M\|_1=\sum_{ij}|M_{ij}|$ is the entrywise $\ell_1$ norm. Given $M=L_0+S_0$, Principal Component Pursuit (PCP) solves

$$\text{minimize }\ \|L\|_*+\lambda\|S\|_1\qquad\text{subject to}\qquad L+S=M. \tag{1.1}$$

PCP is exact when $(L_0,S_0)$ is its unique solution.

$L_0$ satisfies the incoherence condition with parameter $\mu$ when

$$\max_i\|U^*e_i\|^2\le\frac{\mu r}{n},\qquad\max_i\|V^*e_i\|^2\le\frac{\mu r}{n},\qquad\|UV^*\|_\infty\le\sqrt{\frac{\mu r}{n^2}},\tag{1.2–1.3}$$

where $\|X\|_\infty=\max_{ij}|X_{ij}|$. This excludes low-rank matrices that are themselves sparse, which no method could tell apart from corruptions.

The sparse component is $S_0=\mathcal P_\Omega S$, where $S$ is an arbitrary fixed matrix and $\mathcal P_\Omega$ keeps the entries in a random support $\Omega$ and zeros the others. In Theorem 1.1, $\Omega$ is uniform among all subsets of $[n]\times[n]$ of cardinality $m$. In the Bernoulli model $\Omega\sim\mathrm{Ber}(\rho)$ each entry belongs to $\Omega$ independently with probability $\rho$. Nothing is assumed about the magnitudes or signs of $S$.

The proof works with the tangent space $T=\{UX^*+YV^*\}$ of the rank-$r$ matrices at $L_0$, its orthogonal projections $\mathcal P_T$ and $\mathcal P_{T^\perp}$, and the operator norm $\|\cdot\|$ (largest singular value).

Formalization targets

Goal: Theorem 1.1, square case

There are positive numerical constants $c,\rho_r,\rho_s$ such that, whenever $L_0$ obeys (1.2)–(1.3) and

$$\operatorname{rank}(L_0)\le\rho_r\,n\,\mu^{-1}(\log n)^{-2}\qquad\text{and}\qquad m\le\rho_s\,n^2,\tag{1.4}$$

PCP with $\lambda=1/\sqrt n$ is exact with probability at least $1-c\,n^{-10}$ over the support of $S_0$.

The constants are not specified, so the goal survives any improvement of them.

Milestones

They are listed in the order the proof uses them:

• the coordinate bound (2.2);
• the elimination theorem (Theorem 2.2): exactness passes to trimmed sparse components;
• the transfer from the Bernoulli model to the uniform model (§7.1);
• derandomization (Theorem 2.3): random signs suffice;
• the dual certificate conditions (Lemma 2.4, Lemma 2.5, (2.4));
• the concentration results (Theorem 2.6, Corollary 2.7, Lemmas 3.1 and 3.2);
• the two halves of the certificate: the golfing certificate $W^L$ (Lemma 2.8) and the least-squares certificate $W^S$ (Lemma 2.9).

Significance

The result. Theorem 1.1 is the founding guarantee of robust PCA by convex optimization. It allows a constant fraction of arbitrarily large corruptions and a rank as large as $n/(\log n)^2$, with a universal weight $\lambda=1/\sqrt n$. It supports applications such as background modeling in video and the removal of shadows and specularities from face images, and it is the template for later work on noisy and partially observed variants, e.g. stable PCP (Zhou et al., ISIT 2010, arXiv:1001.2363).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. A formal proof would check a chain that combines convex duality for the nuclear and $\ell_1$ norms, operator concentration for random sampling, and a probabilistic coupling. The reusable parts are general: the elimination and derandomization arguments, the certificate lemmas, the golfing scheme and the Bernoulli-to-uniform transfer. They also serve matrix completion and other sparse-plus-low-rank problems. The matrix-completion definitions this mission builds on are already published on the platform.

Difficulty

The obvious plan is to write down the subgradient optimality conditions of (1.1) and exhibit a dual certificate. The difficulty is the exact certificate (2.3). It requires $\mathcal P_\Omega(UV^*+W)=\lambda\operatorname{sgn}(S_0)$ exactly, and at the same time $\|W\|<1$ and $\|\mathcal P_{\Omega^\perp}(UV^*+W)\|_\infty<\lambda$, with $\Omega$ a constant fraction of all entries. The natural least-squares candidate cannot be controlled in the sup norm on $\Omega^\perp$ by moment methods at this sparsity level.

A second difficulty is probabilistic. The theorem allows fixed, adversarial signs. The concentration tools need independence, which fixed signs do not give.

Finally, every step must hold uniformly with failure probability $O(n^{-10})$ and with constants independent of $n$, $L_0$ and $S$.

Formalization scope

All statements are for square real matrices RealMatrix n n. The rectangular sentences of the paper are not stated. The mission reuses the published matrix-completion definitions for the following objects:

• the nuclear norm (sum of Mathlib singular values);
• the operator norm;
• the Frobenius norm and inner product;
• $\|\cdot\|_\infty$ and $\mathcal P_\Omega$;
• SVD data SVD L0 r, with $UV^*$ = signMatrix;
• $\mathcal P_T$ and $\mathcal P_{T^\perp}$;
• the Bernoulli and uniform laws on supports.

The following conventions are fixed:

• Rank. The rank is carried by SVD data SVD L0 r with positive singular values, so $r=\operatorname{rank}L_0$. Every statement holds for every such decomposition.
• Exactness. "Exact" means unique optimality: every other feasible pair has a strictly larger objective.
• Probabilities. Probabilities are finite sums of product weights. Operator norms of operators on matrices are taken with respect to the Frobenius norm.
• Rank condition. It is written multiplied out, $r\mu(\log n)^2\le\rho_rn$, with the natural logarithm.
• Constants. "With high probability" means probability at least $1-c\,n^{-10}$, with $c$ a numerical constant. Every numerical constant is quantified before $n$, the matrices and the parameters.
• Least-squares certificate. $W^S$ is defined by the Neumann series (2.7), which the paper gives as an equivalent definition of (2.6), and it is used only on the event $\|\mathcal P_\Omega\mathcal P_T\|<1/2$.
• Golfing. The golfing sets are indexed from $0$.
• Citations. Theorem numbers and pages are those of the preprint dated 17 December 2009, which is the cited source of the J. ACM article.

Trivializing formalizations are excluded. A constant $c$ chosen after $n$ would make the goal vacuous, so all constants come first. A non-strict "optimal" would make exactness much weaker, so exactness is strict. The values of $S_0$ are fixed before the support is drawn.

Contributions of any kind are welcome. Proofs of the deterministic milestones (Theorem 2.2, Lemmas 2.4 and 2.5, (2.4), (2.2)) are self-contained convex analysis and linear algebra. The concentration milestones need matrix Bernstein-type inequalities and operator concentration, which are reusable well beyond this mission.

Selected references

• E. J. Candès, X. Li, Y. Ma, J. Wright, Robust principal component analysis?, Journal of the ACM 58(3), Article 11, 2011. https://doi.org/10.1145/1970392.1970395
• E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Foundations of Computational Mathematics 9(6), 717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Transactions on Information Theory 57(3), 1548–1566, 2011. https://arxiv.org/abs/0910.1879
• V. Chandrasekaran, S. Sanghavi, P. A. Parrilo, A. S. Willsky, Rank-sparsity incoherence for matrix decomposition, SIAM Journal on Optimization 21(2), 572–596, 2011. https://arxiv.org/abs/0906.2220
• Z. Zhou, X. Li, J. Wright, E. J. Candès, Y. Ma, Stable principal component pursuit, ISIT 2010. https://arxiv.org/abs/1001.2363

Motivation

Binary classification asks for a rule that predicts a label $Y\in\{0,1\}$ from a feature vector $X\in\mathbb R^d$, given $n$ labelled examples. A classical way to measure how hard this is, due to Mammen and Tsybakov (1999), treats classification as the estimation of a set, the region where label $1$ is more likely, and asks how fast the excess misclassification risk of a data-driven classifier can tend to zero. The answer depends on two parameters: the complexity $\rho$ of the class of candidate sets, measured by entropy with bracketing, and the margin parameter $\kappa$, which measures how sharply the conditional probability of label $1$ moves away from $1/2$ near the decision boundary.

Tsybakov (2004) showed that empirical risk minimization over a suitable net attains the rate $n^{-\kappa/(2\kappa+\rho-1)}$, which approaches $n^{-1}$ ("fast rates") for favourable margins and simple classes, and that this rate is minimax optimal. In practice neither $\rho$ nor $\kappa$ is known. The main result of the paper, Theorem 3, constructs a single classifier that adapts to both and attains the optimal rate up to a logarithmic factor simultaneously over a whole family of classes. The margin condition introduced here, often called the Tsybakov margin (or noise) condition, became a standard assumption of statistical learning theory, used for instance in the analysis of support vector machines and of plug-in rules (Audibert and Tsybakov 2007).

Setting

Observations are i.i.d. pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with law $\pi$. Write $P_X$ for the law of $X$ and $\eta(x)=P(Y=1\mid X=x)$ for the regression function. A classifier is a Borel set $G\subseteq\mathbb R^d$, predicting $1$ on $G$. The Bayes classifier is $G^*=\{x:\eta(x)\ge1/2\}$, and the excess risk of $G$ is

$$d(G,G^*)=\int_{G\triangle G^*}|2\eta(x)-1|\,P_X(dx)=R(G)-R(G^*),$$

where $R(G)=P(Y\ne I(X\in G))$. Two pseudodistances between sets are used: $d_\triangle(G,G')=P_X(G\triangle G')$ and its empirical analogue $d_{\triangle,e}(G,G')=\frac1n\sum_iI(X_i\in G\triangle G')$. The empirical risk is $R_n(G)=\frac1n\sum_i(Y_i-I(X_i\in G))^2$.

A class $\mathcal G$ of sets has complexity bound $\rho>0$ if its $\delta$-entropy with bracketing for $d_\triangle$ is at most $A\delta^{-\rho}$ for $0<\delta\le1$. The margin assumption (A1) requires $d(G,G^*)\ge c_0\,d_\triangle^\kappa(G,G^*)$ whenever $d_\triangle(G,G^*)\le\varepsilon_0$, with $\kappa\ge1$. A class $\mathcal P$ of distributions is a $(\mathcal G^*,\kappa,\rho)$-class if every $\pi\in\mathcal P$ has $G^*_\pi\in\mathcal G^*$, satisfies (A1), and $\mathcal G^*$ has complexity bound $\rho<1$ (Definition 4).

Aggregation. Given classes $\mathcal G_1,\dots,\mathcal G_N$ with complexities $\rho_1\le\dots\le\rho_N$ and nested approximating sets $\mathcal N_1\subseteq\dots\subseteq\mathcal N_N$, let $G_{nk}$ minimize $R_n$ over $\mathcal N_k$. With the thresholds

$$T_{nk}(G,G')=(\log^2n)\max\Big\{n^{-1/(1+\rho_k)},\ \tfrac1{\sqrt n}d_{\triangle,e}^{(1-\rho_k)/2}(G,G')\Big\},$$

an index $j$ is admissible if, for every $k\ge j$, some $G\in\mathcal N_j$ has $|R_n(G)-R_n(G_{nk})|\le T_{nk}(G,G_{nk})$. The adaptive classifier is $G^*_n=G_{n\hat j}$ with $\hat j$ the smallest admissible index.

Formalization targets

Goal: Theorem 3

Under assumptions (A3)–(A4), with $\mathcal P_j$ a $(\mathcal G_j,\kappa,\rho_j)$-class for each $j$, $N=O(n^\beta)$, and $\rho_1=\rho_{\min}$, $\rho_N=\rho_{\max}$ fixed, there is $C<\infty$ such that for all $n>1$ and every $j$,

$$\sup_{\pi\in\mathcal P_j}E_{\pi,n}\,d(G^*_n,G^*)\le C\left(\frac{\log^4n}{n}\right)^{\kappa/(2\kappa+\rho_j-1)}.$$

Milestones

1. Appendix, Lemmas 7–11: exponential tail bounds for suprema of ratio-type empirical processes over a class with complexity bound $\rho$.
2. Theorem 1: ERM over an $an^{-1/(1+\rho)}$-net of $\mathcal G^*$ attains $\sup_{\pi}E\,d(\hat G_n,G^*)=O(n^{-\kappa/(2\kappa+\rho-1)})$.
3. Lemma 2: the deterministic comparison inequalities (27)–(28) for an admissible index.
4. Lemma 1: $\sup_\pi P(\hat j>j^*)=o(1/n)$.
5. Lemmas 3, 5, 6, 4: the moment and probability bounds that combine into Theorem 3.

Significance

Theorem 3 says that a procedure which knows neither the class containing $G^*$ nor the margin parameter loses at most a factor $(\log n)^{4\kappa/(2\kappa+\rho_j-1)}$ against the optimal rate on every class at once; combined with the lower bound of Theorem 2 it identifies the optimal adaptive rate up to logarithms. Corollary 1 extends it to a continuum of classes $\{\mathcal G_\rho\}_{\rho\in[\rho_{\min},\rho_{\max}]}$. The selection rule is a Lepski-type pairwise comparison of empirical risks, and the analysis is one of the early results on adaptation to the margin.

The result is proved in the paper, with an Appendix that derives the empirical-process inequalities from van de Geer (2000). No part of it is known to have a machine-checked proof. A formalization would produce reusable infrastructure: entropy with bracketing for classes of sets, ratio-type deviation inequalities for empirical processes, and the excess-risk identity for 0–1 loss.

Difficulty

The obvious argument controls each $G_{nk}$ separately and takes a union bound over $k$. That fails: the bound for $G_{nk}$ at a class $\mathcal G_k$ that does not contain $G^*$ says nothing about $d(G_{nk},G^*)$, and the adaptive rule compares classifiers from different classes through random thresholds that depend on the empirical distance $d_{\triangle,e}$. The central steps are to show that the true index $j^*$ is admissible with probability $1-o(1/n)$ uniformly over a polynomially growing number of classes, and to replace $d_{\triangle,e}$ by $d_\triangle$ inside the thresholds at a constant-factor cost. Both rest on exponential, ratio-type deviation bounds for suprema over classes of infinite entropy, which are not in Mathlib.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, labels are Bool with true ↔ 1, and a distribution is a pair $(P_X,\eta)$ with $P_X$ a probability measure and $\eta$ measurable with values in $[0,1]$; the law of a pair is the published UnderstandingML.condLaw ($X\sim P_X$, then $Y\sim\mathrm{Bernoulli}(\eta(X))$). Classifiers are sets, risk is measured by $d$ via identity (2), and the complexity bound is stated as "some bracketing with $\log m\le A\delta^{-\rho}$ exists".

The Section 3 data ($N_n$, classes, nets, complexities, distribution classes) are indexed by $n$. The formalization commits to the following readings of the page, all disclosed in the items:

• one constant $A$, $c_0$, $\varepsilon_0$ for all classes;
• condition (7) uniformly over the whole family unless $\varepsilon_0=1$;
• complexity bounds for the design law of every distribution in the family;
• constants in Theorem 3 and Lemmas 1, 3–6 uniform in the class index $j$;
• "arg min" as any minimizer;
• the pseudoclassifier $G_{nkj}$ extended by its fallback branch to $j>k$;
• Lemmas 8–10 stated for every $c_1$ (or $c_2$), with constants that may depend on it.

Expectations are Lebesgue integrals over the sample, so each one carries the hypothesis that the data-dependent set is jointly measurable in (sample, point). This rules out the trivializing formalization in which a non-measurable classifier has integral $0$ and every rate bound holds for free. Probabilities of events involving suprema over uncountable classes are outer measures. Appendix suprema are real suprema over index sets bounded above. The goal is not vacuous: a solution-folder check exhibits a setup satisfying all hypotheses with $\hat j=1$.

Contributions welcome: bracketing-entropy chaining bounds, the van de Geer inequalities (5.42)–(5.43), and the Appendix lemmas as standalone results.

Selected references

• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Ann. Statist. 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131
• E. Mammen and A. B. Tsybakov, Smooth discrimination analysis, Ann. Statist. 27(6), 1808–1829, 1999. https://doi.org/10.1214/aos/1017939240
• S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511802256
• J.-Y. Audibert and A. B. Tsybakov, Fast learning rates for plug-in classifiers, Ann. Statist. 35(2), 608–633, 2007. https://doi.org/10.1214/009053606000001217
• L. Devroye, L. Györfi and G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5