Statistics

Motivation

Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).

In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates $d$ is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with $d$. Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in $d$. The paper evaluates the method on warfarin dosing data.

Timeline:

• 2002–2003: Auer introduces linear-reward contextual bandits with confidence bounds.
• 2013: Goldenshluger and Zeevi give a forced-sampling algorithm for two arms in low dimension with $O(\log T)$ regret under a margin condition and an arm-optimality condition, and an information-theoretic lower bound of the same order.
• 2020: Bastani and Bayati extend the forced-sampling scheme to $K$ arms and high-dimensional sparse parameters, with regret $O(s_0^2[\log T+\log d]^2)$.

Setting

There are $K$ arms with unknown parameters $\beta_1,\dots,\beta_K\in\mathbb R^d$. At each time $t=1,2,\dots,T$ a covariate vector $X_t\in\mathbb R^d$ arrives; the $X_t$ are i.i.d. with law $\mathcal P_X$ and take values in a fixed set $\mathcal X$. If arm $i$ is pulled, the reward is $X_t^\top\beta_i+\varepsilon_{i,t}$, where the noises $\varepsilon_{i,t}$ are independent, $\sigma$-subgaussian ($\mathbb E[e^{s\varepsilon}]\le e^{\sigma^2s^2/2}$ for all $s$), and independent of the covariates. A policy chooses the arm $\pi_t$ from $X_t$ and the past covariates, arms and observed rewards. Its cumulative expected regret is

$$R_T=\sum_{t=1}^T\mathbb E\Big[\max_jX_t^\top\beta_j-X_t^\top\beta_{\pi_t}\Big].$$

The sparsity $s_0$ is the smallest integer $s_0\ge1$ with $\|\beta_i\|_0\le s_0$ for all $i$.

The four assumptions are: (1) $\|x\|_\infty\le x_{\max}$ on $\mathcal X$ and $\|\beta_i\|_1\le b$; (2) a margin condition $\Pr[0<|X^\top(\beta_i-\beta_j)|\le\kappa]\le C_0\kappa$; (3) arm optimality: every arm is either suboptimal by a margin $h$ at every covariate, or optimal by margin $h$ on a region $U_i$ of probability at least $p_*$; (4) a compatibility condition: the conditional second-moment matrix $\Sigma_i=\mathbb E[XX^\top\mid X\in U_i]$ of each optimal arm lies in the set $\mathcal C(\mathrm{supp}(\beta_i),\phi_0)$ of matrices $M\succeq0$ with $\|v_I\|_1^2\le|I|\,v^\top Mv/\phi_0^2$ whenever $\|v_{I^c}\|_1\le3\|v_I\|_1$.

The LASSO estimator on $n$ samples is any minimizer of $\|Y-\mathbf X\beta'\|_2^2/n+\lambda\|\beta'\|_1$. The LASSO Bandit forces arm $i$ at the prescribed times $\mathcal T_i=\{(2^n-1)Kq+j : n\ge0,\ q(i-1)<j\le qi\}$. At every other time it keeps the arms whose forced-sample estimate $\hat\beta(\mathcal T_{i,t-1},\lambda_1)$ is within $h/2$ of the best. Among them it plays the arm with the largest all-sample estimate $\hat\beta(\mathcal S_{i,t-1},\lambda_{2,t-1})$, trained on every past pull of the arm, with $\lambda_{2,t}=\lambda_{2,0}\sqrt{(\log t+\log d)/t}$.

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

For $q\ge4\lceil q_0\rceil$, $K\ge2$, $d>2$, $T\ge C_5$, $\lambda_1=\phi_0^2p_*h/(64s_0x_{\max})$ and $\lambda_{2,0}=[\phi_0^2/(2s_0)]\sqrt{1/(p_*C_1)}$,

$$R_T\le C_3(\log T)^2+\big[2Kbx_{\max}(6q+4)+C_3\log d\big]\log T+\big(2bx_{\max}C_5+2Kbx_{\max}+C_4\big),$$

with the explicit constants $C_1,\dots,C_5$, $q_0$ of the paper (p. 285).

Milestones

1. Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
2. Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
3. Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^4$.
4. Proposition 3: the all-sample estimator of an optimal arm is within $16\sqrt{(\log t+\log d)/(p_*^3C_1t)}$ of $\beta_i$ except with probability $2/t+2e^{-p_*^2C_2^2t/32}$.

Significance

The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through $\log d$, while its dependence on the horizon is within one $\log T$ factor of the $\Omega(\log T)$ lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.

The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.

Difficulty

The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only $O(\log t)$ in number, too few for the $\sqrt{\log t/t}$ rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.

Formalization scope

Arms are Fin K (paper arm $i$ is i.val + 1), coordinates Fin d, times are natural numbers from $1$. The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set $\mathcal X$, independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter $\sigma^2$), noise independent of covariates. Assumptions 1–4 are separate predicates. $\|x\|_\infty$ is Mathlib's sup norm, logarithms are natural, and $\Sigma_i$ is the uncentred conditional second moment.

The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set $\mathcal S_{i,t}$ is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in $R_T$ could be integrals of non-measurable functions, which Lean evaluates to $0$ and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and $T\ge C_5$ is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing $O(s_0^2[\log T+\log d]^2)$ or $q_0=O(s_0^2\log d)$. Proposition 2 is stated for optimal arms (see its note).

A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.

Selected references

• H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1):276–294, 2020. https://doi.org/10.1287/opre.2019.1902
• A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1):230–261, 2013. https://doi.org/10.1287/11-SSY032
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Motivation

The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).

For a class of Vapnik–Chervonenkis (VC) dimension $d$ the answer was known up to a logarithmic factor for about 25 years:

• 1982–1989. Vapnik (1982) and Blumer, Ehrenfeucht, Haussler and Warmuth (J. ACM 1989) showed that any learner that outputs a classifier consistent with the sample succeeds with $O\left(\frac1\varepsilon\left(d\log\frac1\varepsilon+\log\frac1\delta\right)\right)$ examples.
• 1989. Ehrenfeucht, Haussler, Kearns and Valiant (Inform. Comput. 1989) together with Blumer et al. proved the lower bound $\Omega\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$ for every learner.
• 1994. Haussler, Littlestone and Warmuth (Inform. Comput. 1994) showed $\mathcal M(\varepsilon,\delta)=O\left(\frac d\varepsilon\mathrm{Log}\frac1\delta\right)$ with a variant of the one-inclusion graph predictor, which is sometimes better but also does not match the lower bound.
• 2007–2015. The gap was closed for restricted classes, such as intersection-closed classes (Auer and Ortner 2007; Darnstädt 2015), but not for classes such as linear separators.
• 2015. Simon (COLT 2015) analysed a majority vote of consistent classifiers trained on disjoint parts of the data and reduced the logarithmic factor to a very slowly growing function of $1/\varepsilon$.
• 2016. Hanneke (JMLR 17(38), 2016; arXiv:1507.00473) removed the logarithmic factor for every class, with an explicit learner: a majority vote of consistent classifiers trained on recursively constructed, overlapping subsamples.

Setting

Let $\mathcal X$ be a set with a $\sigma$-algebra and $\mathcal Y=\{-1,+1\}$. A classifier is a measurable map $h:\mathcal X\to\mathcal Y$; the concept space $\mathbb C$ is a set of classifiers with $|\mathbb C|\ge3$. A finite sequence $x_1,\ldots,x_k$ is shattered by $\mathbb C$ if every labelling $y_1,\ldots,y_k$ is realized by some $h\in\mathbb C$; the VC dimension $d$ is the largest such $k$, assumed finite (then $d\ge1$).

A data set is a finite sequence $S$ of pairs in $\mathcal X\times\mathcal Y$, and $\mathbb C[S]$ is the set of $h\in\mathbb C$ with $h(x)=y$ for all $(x,y)\in S$. For a probability measure $P$ and a target $f^\star\in\mathbb C$, the error of $h$ is $\mathrm{er}_P(h;f^\star)=P(\mathrm{ER}(h))$, where $\mathrm{ER}(h)=\{x:h(x)\ne f^\star(x)\}$. A learning algorithm maps data sets to classifiers.

For $\varepsilon,\delta\in(0,1)$, the sample complexity $\mathcal M(\varepsilon,\delta)$ (Definition 1) is the least $m$ such that some algorithm $\mathcal A$ satisfies, for every probability measure $\mathcal P$ on $\mathcal X$ and every $f^\star\in\mathbb C$, with $X_1,\ldots,X_m$ independent with law $\mathcal P$,

$$\mathbb P\left(\mathrm{er}_{\mathcal P}\left(\mathcal A\big((X_i,f^\star(X_i))_{i\le m}\big);f^\star\right)\le\varepsilon\right)\ge1-\delta,$$

and $\mathcal M(\varepsilon,\delta)=\infty$ if there is no such $m$.

The learner of the paper uses three ingredients. A sample-consistent learner $L$ returns an element of $\mathbb C[S]$ whenever that set is nonempty. The majority vote is $\mathrm{Majority}(h_1,\ldots,h_k)(x)=2\mathbb 1\left[\sum_i h_i(x)\ge0\right]-1$. The subsample algorithm $\mathbb A(S;T)$ returns $\{S\cup T\}$ if $|S|\le3$; otherwise it splits $S$ into a head $S_0$ of $|S|-3\lfloor|S|/4\rfloor$ points and three blocks $S_1,S_2,S_3$ of $\lfloor|S|/4\rfloor$ points, and returns the concatenation of $\mathbb A(S_0;S_2\cup S_3\cup T)$, $\mathbb A(S_0;S_1\cup S_3\cup T)$ and $\mathbb A(S_0;S_1\cup S_2\cup T)$. The learned classifier is $\hat h=\mathrm{Majority}(L(\mathbb A(S;\emptyset)))$.

Formalization targets

Goal: Theorem 2 with its explicit constant

$$\mathcal M(\varepsilon,\delta)\le\frac{1800}{\varepsilon}\left(d+\ln\left(\frac{18}{\delta}\right)\right)\qquad(\varepsilon,\delta\in(0,1)).$$

The paper states Theorem 2 as $\mathcal M(\varepsilon,\delta)=O\left(\frac1\varepsilon\left(d+\mathrm{Log}\frac1\delta\right)\right)$ with a numerical constant; its proof establishes the bound above with $c=1800$, and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.

Milestones, in attack order

1. Lemma 4 (Blumer et al. 1989): with probability $1-\delta$, every $h\in\mathbb C[\{(Z_i,f^\star(Z_i))\}_{i\le m}]$ has $\mathrm{er}_P(h;f^\star)\le\frac2m\left(d\,\mathrm{Log}_2\frac{2em}d+\mathrm{Log}_2\frac2\delta\right)$.
2. Lemma 5: $a\ln(c_1(c_2+b/a))\le a\ln(c_1(c_2+e))+b/e$ for $a,b,c_1\ge1$, $c_2\ge0$.
3. Structure of $\mathbb A$: every subsample $\hat S$ satisfies $T\subseteq\hat S\subseteq S\cup T$, and the number of subsamples does not depend on $T$.
4. The Chernoff event $E_i''$: if $Q(E)\ge\frac{23}n\ln\frac9\delta$, then with probability $1-\delta/9$ at least $\frac7{10}Q(E)n$ of $n$ i.i.d. points fall in $E$.
5. The bound (8) and its comparison with $\frac{150}{m+1}\left(d+\ln\frac{18}\delta\right)$.
6. Majority averaging: $\mathrm{er}(h_{\mathrm{maj}})\le12\,\mathbb E\left[\mathcal P(\mathrm{ER}(h_I)\cap\mathrm{ER}(\tilde h))\right]$ for three equal-size committees.
7. Claim (9): with probability $1-\delta$, $\mathrm{er}_{\mathcal P}(\hat h_{m,T};f^\star)\le\frac{1800}{m+1}\left(d+\ln\frac{18}\delta\right)$.
8. Sample size (10): $\mathrm{Majority}(L(\mathbb A(\cdot;\emptyset)))$ is $(\varepsilon,\delta)$-PAC from $\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$ examples.

Significance

Together with the classical lower bound, Theorem 2 gives $\mathcal M(\varepsilon,\delta)=\Theta\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$: the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the $\log\frac1\varepsilon$ factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.

The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.

Difficulty

The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the $\log\frac1\varepsilon$ factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth $\log_4 m$. In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set $T$ that varies with the level, and the numerical constants, which are tight (the key comparison is $149.9997<150$).

Formalization scope

• Representation. Labels are Bool (true for $+1$); data sets are lists and $\cup$ is concatenation; $\mathbb C$ is a set of measurable functions with $|\mathbb C|\ge3$; the VC dimension is a supremum in $\mathbb N\cup\{\infty\}$, assumed equal to a natural number $d$. The i.i.d. sample is the product measure $\mathcal P^m$ on $\mathrm{Fin}\,m\to\mathcal X$. "With probability at least $1-\delta$" is stated as a bound $\le\delta$ on the outer measure of the failure event. $\mathcal M$ takes values in $\mathbb N\cup\{\infty\}$, so the goal is stated as $\mathcal M(\varepsilon,\delta)\le\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$, which is equivalent. Ties in the majority vote go to $+1$, as printed.
• Algorithms. $\mathcal M$ quantifies over deterministic algorithms that output measurable classifiers, chosen before $\mathcal P$ and $f^\star$ and seeing only the labelled sample. The paper also admits randomized algorithms (footnote 2), which can only lower $\mathcal M$, so the goal implies the paper's statement.
• Measurability. The paper assumes that every event in its probability claims is measurable (p. 3). The formalization makes this explicit with two hypotheses: the class is well-behaved (the event of Lemma 4 and the double-sample event of Blumer et al. are null-measurable for every distribution), and the base learner $L$ is jointly measurable in the sample and the point. Both hold for every countable class of measurable classifiers, with $L$ returning the first consistent classifier of an enumeration. Without the first hypothesis Lemma 4 fails for some classes of VC dimension 1.
• Ruled out. The following formalizations would make the goal trivial or weaker, and are not used here:
  • a sample complexity whose algorithm may depend on $\mathcal P$ or $f^\star$, which gives $\mathcal M\equiv0$;
  • a goal with an existential constant or a ceiling in place of $1800$ and the floor;
  • measurability hypotheses that no infinite class satisfies;
  • milestones 7–8 stated for an arbitrary family of subsamples instead of the algorithm $\mathbb A$.
• Needed infrastructure. VC theory for consistent learners (Lemma 4, via the double-sample argument), multiplicative Chernoff bounds for binomial counts, and conditioning of product measures on coordinate blocks. These are reusable beyond this mission. Contributions welcome: a proof of Lemma 4, the Chernoff milestone, the numerical milestone 5, and the majority-vote averaging step, each of which is independent of the others.

Selected references

• S. Hanneke, The Optimal Sample Complexity of PAC Learning, Journal of Machine Learning Research 17(38):1–15, 2016. arXiv:1507.00473v4
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4):929–965, 1989. doi:10.1145/76359.76371
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3):247–261, 1989. doi:10.1016/0890-5401(89)90002-3
• H. U. Simon, An almost optimal PAC algorithm, Proceedings of the 28th Conference on Learning Theory (COLT), PMLR 40:1552–1563, 2015. proceedings.mlr.press/v40/Simon15a
• D. Haussler, N. Littlestone, M. K. Warmuth, Predicting {0,1}-functions on randomly drawn points, Information and Computation 115(2):248–292, 1994. doi:10.1006/inco.1994.1097
• P. Auer, R. Ortner, A new PAC bound for intersection-closed concept classes, Machine Learning 66(2–3):151–163, 2007. doi:10.1007/s10994-006-8638-3
• V. Vapnik, Estimation of Dependences Based on Empirical Data, Springer, 1982.

Motivation

Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from $O(n^{6/5} r \log n)$ random entries under incoherence assumptions.

Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum $n r\log n$. This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.

Timeline:

• 2009, Candès–Recht: exact recovery from $m \gtrsim \mu_0 n^{6/5} r \log n$ entries.
• 2010, Candès–Tao (this paper): $m \gtrsim \mu^4 n r^2 (\log n)^2$ (Theorem 1.1, general-rank form) and $m \gtrsim \mu^2 n r \log^6 n$ (Theorem 1.2), plus a lower bound of order $n r \log n$ for every method (Theorem 1.7).
• 2011, Gross (IEEE Trans. Inf. Theory) and Recht (JMLR): $m \gtrsim \mu_0 n r \log^2 n$ by the "golfing scheme", with a different proof.

Setting

Let $M \in \mathbb R^{n\times n}$ have rank $r$ and singular value decomposition $M = \sum_{k=1}^r \sigma_k u_k v_k^*$ with $\sigma_k > 0$ and orthonormal $u_k$, $v_k$. Write $P_U = \sum_k u_k u_k^*$, $P_V = \sum_k v_k v_k^*$ and $E = \sum_k u_k v_k^*$. The matrix obeys the strong incoherence property with parameter $\mu > 0$ if, for all indices $a, a', b, b'$,

$$\Bigl|\langle e_a, P_U e_{a'}\rangle - \tfrac{r}{n}1_{a=a'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad \Bigl|\langle e_b, P_V e_{b'}\rangle - \tfrac{r}{n}1_{b=b'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad |E_{ab}| \le \mu\tfrac{\sqrt r}{n}.$$

For a set $\Omega \subset [n]\times[n]$ of observed positions, the nuclear-norm program is

$$\text{minimize } \|X\|_* \quad \text{subject to } X_{ab} = M_{ab}\ \ ((a,b)\in\Omega). \qquad \text{(I.3)}$$

In the uniform model $\Omega$ is a uniformly random $m$-subset of $[n]\times[n]$; in the Bernoulli model each entry is included independently with probability $p = m/n^2$.

The proof works with the tangent space $T$ at $M$ and its projection $\mathcal P_T(X) = P_UX + XP_V - P_UXP_V$, the sampling projection $\mathcal P_\Omega$, and the centered operators $\mathcal Q_\Omega = p^{-1}\mathcal P_\Omega - \mathcal I$ and $\mathcal Q_T = \mathcal P_T - \rho'\mathcal I$, where $\rho = r/n$ and $\rho' = 2\rho - \rho^2$. The candidate certificate $Y$ of (III.10) is the matrix of least Frobenius norm with $\mathcal P_\Omega(Y) = Y$ and $\mathcal P_T(Y) = E$.

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

There is an absolute constant $C$ such that, for every strongly incoherent $M$ of rank $r$ and every $m \le n^2$,

$$m \ge C\mu^4 n r^2(\log n)^2 \implies \Pr_{\text{uniform}}\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.$$

Milestones

1. Lemma 3.1: a matrix $Y$ supported on $\Omega$ with $\mathcal P_T(Y) = E$ and $\|\mathcal P_{T^\perp}(Y)\| < 1$, together with injectivity of $\mathcal P_\Omega$ on $T$, certifies that $M$ is the unique solution (already proved on the platform).
2. Lemma 5.1 (exponent bound): $|J|+|K|-|Q|-|\Omega| \le -|Q'|+1$ for every admissible pair.
3. Lemma 5.2 (pair counting): at most $(Cj(k+1))^{2j(k+1)+q}$ strongly admissible pairs have $|Q'| = q$.
4. Theorem 3.4 (moment bound I): with $A = (\mathcal Q_\Omega\mathcal Q_T)^k\mathcal Q_\Omega(E)$ and $r_\mu = \mu^2 r$,

$$\mathbb E\operatorname{trace}(A^*A)^j \le (Cj(k+1))^{2j(k+1)}\, n\,(n r_\mu^2/m)^{j(k+1)}.$$

5. Corollary 3.5: under the goal's sampling condition and the Bernoulli model, with probability at least $1-n^{-3}$, $\mathcal P_\Omega$ is injective on $T$ and $\|\mathcal P_{T^\perp}(Y)\| \le 1/2$.

The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.

Significance

Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from $O(n(\log n)^2)$ random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order $n\log n$. The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.

The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.

Difficulty

The obvious route bounds the Neumann series $\sum_k \|(\mathcal Q_\Omega\mathcal P_T)^k\mathcal Q_\Omega(E)\|$ term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier $n^{6/5}$ bound was obtained, and it degrades as $k$ grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of $\mathbb E\operatorname{trace}(A^*A)^j$ as a sum over "spider" configurations of paths in $[n]\times[n]$. The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of $n$ has to be matched against the powers of $1/p$ (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over $q$ converges (Lemma 5.2). A naive count of pairs gives $(2j(k+1))^{4j(k+1)}$, which is too large by a square.

Formalization scope

• Square case. Theorem 1.1 is printed for $n_1\times n_2$ matrices, but the paper proves only the square case (Section I-H: "we shall work exclusively with square matrices"). Every statement is for Matrix (Fin n) (Fin n) ℝ.
• General rank. The goal and Corollary 3.5 are stated in the general-rank form (I.11), $m \ge C\mu^4 n r^2(\log n)^2$. The paper states this form explicitly on p. 2055, and the proof of Corollary 3.5 derives it as (III.26). For $r = O(1)$ it is the printed Theorem 1.1 and the printed Corollary 3.5.
• Constants. Every constant ("numerical constant $C$", $c_0$, and $O(M)^M := (CM)^M$) is an existential absolute constant quantified before $n$, $r$, $m$, $M$, $\mu$, $j$, $k$ and $q$. A constant allowed to depend on $n$ or $M$ would make (I.11) unsatisfiable for large $C$ and the goal vacuous; that formalization is ruled out.
• Standing assumptions. The paper assumes $n \ge C'$ and $m \ge 2nr$ (I.22) throughout. In the goal and in Corollary 3.5 they are absorbed by $C$, since strong incoherence forces $\mu \ge 1$. Theorem 3.4 carries $2nr \le m$ explicitly. Theorem 3.4 omits $r = O(1)$ and (I.10), since Section V uses only its own proviso $m \ge n r_\mu^2$. Every statement also carries $m \le n^2$, without which the uniform model is empty.
• Probability. The uniform model is the platform's successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with $p = m/n^2$. The logarithm is natural, and the failure probability is written 1 / n^3.
• Recovery. "Unique solution of (I.3)" is IsUniqueMinimizer: every other matrix that agrees with $M$ on $\Omega$ has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.
• Admissible pairs. The index $i \in [j]$ is 0-based, the cyclic successor is finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.
• New definitions. centeredTangentProjection ($\mathcal Q_T$), momentMatrix ($A$), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The $\mathcal Q_T$ definition is drafted independently in mission II.

Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing $\mathcal P_T$ by $\mathcal Q_T$), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.

Selected references

• E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
• E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 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 Trans. Inf. Theory 57(3):1548–1566, 2011. https://doi.org/10.1109/TIT.2011.2104999
• B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://jmlr.org/papers/v12/recht11a.html

Motivation

Regression is usually taught with a fixed parametric model: linear regression fits a $d$-dimensional coefficient vector, and the estimation error is controlled by $d/n$. Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size $n$? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.

Setting

Fix $n$ design points $x_1,\dots,x_n$ in an arbitrary covariate space $\mathcal X$ (fixed, not random — this is the fixed-design setting) and observe

$$y_i = f^*(x_i) + \sigma w_i, \qquad i = 1,\dots,n,$$

where $f^*$ is the unknown regression function, $\sigma > 0$ is a known noise level, and $w_1,\dots,w_n$ are i.i.d. standard Gaussian. Given a class $F$ of candidate functions, the nonparametric least-squares estimate is any minimizer

$$\hat f_n \in \arg\min_{f\in F}\ \frac1n\sum_{i=1}^n \big(y_i - f(x_i)\big)^2.$$

Error is measured in the empirical (design-dependent) seminorm $\|g\|_n^2 := \frac1n\sum_{i=1}^n g(x_i)^2$. A class $H$ of functions is star-shaped if $h\in H$ and $\alpha\in[0,1]$ together imply $\alpha h \in H$ — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class $H$ and radius $\delta>0$, the local Gaussian complexity

$$G_n(\delta; H) := \mathbb E_w\Big[\ \sup_{h\in H,\ \|h\|_n\le\delta}\ \Big|\tfrac1n \sum_{i=1}^n w_i h(x_i)\Big|\ \Big]$$

measures how much a mean-zero Gaussian process can be made to look like a member of $H$ restricted to the ball of radius $\delta$. A critical radius $\delta_n$ is any positive solution of $G_n(\delta;H)/\delta \le \delta/(2\sigma)$; by Lemma 13.6, $\delta\mapsto G_n(\delta;H)/\delta$ is non-increasing on $H$ star-shaped, so this inequality always has a smallest positive solution.

Formalization targets

Lemma 13.6. For any star-shaped $H$, $\delta \mapsto G_n(\delta;H)/\delta$ is non-increasing on $(0,\infty)$, and consequently $G_n(\delta;H)/\delta \le c\delta$ has a smallest positive solution for every $c>0$.

Theorem 13.5 (special case, $f^*\in F$).

$$\mathbb P\big[\|\hat f_n - f^*\|_n^2 \ge 16\,t\delta_n\big] \le e^{-nt\delta_n/(2\sigma^2)} \qquad \text{for all } t \ge \delta_n.$$

Theorem 13.13 (goal — general oracle inequality, $f^*$ not assumed in $F$). With $\delta_n$ solving the critical inequality for $\partial F := F - F$, there are universal constants $(c_0,c_1,c_2)$ such that for all $t\ge\delta_n$,

$$\|\hat f_n-f^*\|_n^2 \le \inf_{\gamma\in(0,1)}\left[\frac{1+\gamma}{1-\gamma}\|f-f^*\|_n^2 +\frac{c_0}{\gamma(1-\gamma)}t\delta_n\right]\quad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt\delta_n/\sigma^2}$. The goal is deliberately the statement with unresolved universal constants and an infimum over $\gamma$, rather than any single instantiated bound, so the target survives sharper constant tracking.

Significance

Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding $G_n$ for a particular $F$ and reading off $\delta_n$. Its value is that it isolates exactly the one place where the geometry of $F$ enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.

Difficulty

The naive route to Theorem 13.13 is to bound $\|\hat f_n - f^*\|_n$ pointwise via the basic inequality $\tfrac12\|\hat f_n-f^*\|_n^2 \le \tfrac{\sigma}{n}\sum_i w_i(\hat f_n(x_i)-f^*(x_i))$ and then bound the right side by $\sigma\,G_n(\delta;\partial F)$ for $\delta = \|\hat f_n-f^*\|_n$ — but $\delta$ is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus $\|\hat f_n-f^*\|_n$ falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius $\delta$ is what makes the per-annulus bound tight enough for the final sum to converge.

Formalization scope

Design points are an arbitrary type X (no topology or metric structure is needed for the statements themselves); the least-squares estimate is represented as a Prop (IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector on an abstract probability space, with the inner supremum taken over the subtype of the radius-restricted slice of the class — this is well-defined (not the junk value 0 of an unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any nonempty star-shaped class (taking $\alpha=0$ exhibits $0$ in the class). Since neither X nor H carries a topology, separability or countability constraint, SatisfiesCriticalInequality adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable integrand — a value that would otherwise trivially satisfy the critical inequality for every positive δ, regardless of the function class's actual local complexity. The trivializing formalization to rule out here is stating Theorem 13.13's universal constants after the quantification over the function class and sample size, which would let $(c_0,c_1,c_2)$ secretly depend on the instance and make the "universal" claim vacuous; this mission places the constant quantifiers first, before the class, design and noise data they must not depend on. A complete downstream development would add: the concentration-of-Gaussian-complexity step (Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy / Dudley-integral machinery of Section 13.2.1 for bounding $G_n$ explicitly on concrete classes (Sobolev balls, RKHS balls) — none of which is attempted here.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 13. https://doi.org/10.1017/9781108627771
• S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000.
• S. van de Geer, "Estimating a regression function," Annals of Statistics, 18(2):907-924, 1990. https://doi.org/10.1214/aos/1176347627

Motivation

Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.

Setting

A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for this notion throughout. A linear functional $L:H\to\mathbb R$ is bounded if $|L(f)|\le M\|f\|_H$ for some $M<\infty$ and all $f\in H$; the Riesz representation theorem (Theorem 12.5) says every such functional is $L(f)=\langle f,g\rangle_H$ for a unique $g\in H$.

A bivariate function $K:X\times X\to\mathbb R$ is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix $(K(x_i,x_j))_{i,j=1}^n$ is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set $X$, with no topological structure on $X$ required. A reproducing kernel Hilbert space (RKHS) for a kernel $K$ is a Hilbert space $H$ of functions on $X$ such that, for every $x\in X$, the function $K(\cdot,x)$ belongs to $H$ and

$$\langle f, K(\cdot,x)\rangle_H = f(x) \qquad \text{for all } f\in H \tag{12.3}$$

— the reproducing property. Equivalently (Definition 12.12), $H$ is an RKHS exactly when every evaluation functional $f\mapsto f(x)$ is bounded on $H$.

Formalization targets

Goal (Theorem 12.11, the Moore-Aronszajn theorem)

Given any PSD kernel function $K$ on any set $X$, there is a Hilbert space $H$ (embedded into functions on $X$) in which $K$ satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same $K$ are linearly isometric via an isometry intertwining their embeddings into functions on $X$.

Milestones

• Theorem 12.5 (Riesz representation). Every bounded linear functional on a Hilbert space $H$ has a unique representer $g\in H$: $L(f)=\langle f,g\rangle_H$ for all $f$. Used inside the proof of Theorem 12.13 to produce the representer $R_x$ of each evaluation functional.
• Theorem 12.13 (the converse correspondence). Given any Hilbert space $H$ of functions on $X$ in which every evaluation functional is bounded, there is a unique PSD kernel $K$ satisfying the reproducing property for $H$ — completing the Moore-Aronszajn equivalence between PSD kernels and Hilbert spaces with bounded evaluation functionals.
• Theorem 12.20 (Mercer's theorem). Under compactness of $X$, continuity of $K$, and the Hilbert-Schmidt condition $\int_{X\times X}K^2\,dP\,dP<\infty$, the integral operator $T_K(f)(x)=\int_XK(x,z)f(z)\,dP(z)$ has an orthonormal eigenbasis $(\varphi_j)$ of $L^2(X;P)$ with non-negative eigenvalues $(\mu_j)$, and $K(x,z)=\sum_j\mu_j\varphi_j(x)\varphi_j(z)$, with the series converging absolutely and uniformly.

Significance

Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with $K$" is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions $(\sqrt{\mu_j}\varphi_j)_j$ give an explicit feature map into $\ell^2(\mathbb N)$ realizing $K$, and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in $\ell^2(\mathbb N)$-coordinates.

Difficulty

The formalization difficulty is concentrated in getting the type of the existence-and- uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a subtype of a fixed ambient space in Lean, so "the Hilbert space $H$" of Theorem 12.11 is formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on $X$" via an injective linear embedding into $X\to\mathbb R$ — and uniqueness must then be stated as an isometric equivalence between any two witnessing Hilbert spaces that respects this embedding, the faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses (a bare PSD kernel, no topology on $X$) cleanly separated from Mercer's theorem's additional compactness, continuity and measure-theoretic apparatus — the two theorems are frequently conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's structure.

Formalization scope

$X$ is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that scope. The integral operator $T_K$ of Eq. (12.11a) is presented as an abstract linear map on Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than constructed as a def, since constructing it as a genuine well-defined operator (needing integrability and a.e.-measurability arguments) is proof content, not definitional content, and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X (Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly warned against by this chapter's own brief), or state Mercer's convergence merely pointwise or in $L^2$ rather than absolutely and uniformly; this mission avoids both. Out of scope: the constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof content, not part of the statement), the chapter's worked kernel examples (linear, polynomial, Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem (Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13, mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather than importing this mission's draft, per this book's series-wide convention.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 12. DOI: 10.1017/9781108627771.
• Aronszajn, N. "Theory of reproducing kernels." Transactions of the American Mathematical Society, 68(3), 1950, 337–404.
• Mercer, J. "Functions of positive and negative type, and their connection with the theory of integral equations." Philosophical Transactions of the Royal Society A, 209, 1909, 415–446.