Machine Learning

Motivation

In a linear regression with many more candidate variables than observations, least squares is not defined uniquely and does not estimate anything useful. The Lasso (Tibshirani, 1996) replaces it by an $\ell_1$-penalised least-squares problem, which is convex, can be solved at scale, and returns sparse coefficient vectors. The question that a statistician, a signal-processing engineer or an operations researcher fitting a sparse model must answer before trusting it is quantitative: how far is the Lasso estimate from the true coefficient vector, how well does it predict, and how many variables does it select, as functions of the sample size $n$, the number of variables $M$ and the sparsity $s$ of the truth?

Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) answered this under the restricted eigenvalue (RE) condition, which they introduced, with explicit constants and an explicit failure probability. Their Theorem 7.2, the goal of this mission, is a standard reference result of high-dimensional statistics and a model for the Lasso analyses in the textbooks of Bühlmann and van de Geer (2011) and Wainwright (2019).

Timeline, restricted to what each work proved:

• 2007: Candès and Tao (arXiv:math/0506081) prove $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle.
• 2007: Bunea, Tsybakov and Wegkamp (doi:10.1214/07-EJS008) prove sparsity oracle inequalities for the Lasso under mutual-coherence conditions; Lemma B.1 of the present paper is essentially their Lemma 1.
• 2008/2009: Bickel, Ritov and Tsybakov prove Theorem 7.2 under RE$(s,3)$ and RE$(s,m,3)$, conditions weaker than those of the previous works.

Setting

A deterministic design matrix $X\in\mathbb R^{n\times M}$ with columns $x_{(1)},\dots,x_{(M)}$ is observed together with

$$y=X\beta^*+w,$$

where $\beta^*\in\mathbb R^M$ is unknown and $w=(W_1,\dots,W_n)$ has independent $\mathcal N(0,\sigma^2)$ entries with $\sigma>0$. Throughout, $n\ge1$, $M\ge2$, and every diagonal entry of the Gram matrix $\Psi_n=X^\top X/n$ equals $1$.

For $\delta\in\mathbb R^M$ write $|\delta|_p=(\sum_j|\delta_j|^p)^{1/p}$, $J(\delta)=\{j:\delta_j\ne0\}$ for the support, $\mathcal M(\delta)=|J(\delta)|$ for the sparsity, and $\delta_J$ for the vector that agrees with $\delta$ on $J$ and vanishes off $J$. The largest eigenvalue of $\Psi_n$ is $\phi_{\max}$.

The Lasso estimator with tuning parameter $r>0$ is any minimiser

$$\hat\beta_L\in\arg\min_{\beta\in\mathbb R^M}\Big\{\frac1n|y-X\beta|_2^2+2r|\beta|_1\Big\}.$$

Minimisers exist but need not be unique.

Assumption RE$(s,c_0)$ ($1\le s\le M$, $c_0>0$) asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Assumption RE$(s,m,c_0)$ ($1\le s\le M/2$, $m\ge s$, $s+m\le M$) is the same with $|\delta_{J_{01}}|_2$ in the denominator, where $J_{01}=J_0\cup J_1$ and $J_1$ collects the $m$ largest in absolute value coordinates of $\delta$ outside $J_0$.

Formalization targets

Goal: Theorem 7.2

Let $\mathcal M(\beta^*)\le s$, let RE$(s,3)$ hold, and let $r=A\sigma\sqrt{\log M/n}$ with $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution satisfies

$$|\hat\beta_L-\beta^*|_1\le\frac{16A}{\kappa^2(s,3)}\sigma s\sqrt{\frac{\log M}{n}},\qquad |X(\hat\beta_L-\beta^*)|_2^2\le\frac{16A^2}{\kappa^2(s,3)}\sigma^2s\log M,\qquad \mathcal M(\hat\beta_L)\le\frac{64\phi_{\max}}{\kappa^2(s,3)}s,$$

and, if RE$(s,m,3)$ holds, on the same event and for all $1<p\le2$,

$$|\hat\beta_L-\beta^*|_p^p\le16\Big\{1+3\sqrt{\tfrac sm}\Big\}^{2(p-1)}s\Big(\frac{A\sigma}{\kappa^2(s,m,3)}\sqrt{\frac{\log M}{n}}\Big)^p .$$

Milestones

In the order in which the paper's proof uses them:

1. (B.4): the noise event $\mathcal A=\bigcap_j\{2|\tfrac1n x_{(j)}^\top w|\le r\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$.
2. (B.6): the optimality conditions of the Lasso.
3. Lemma B.1 (Section 7 case): the basic inequality (B.1) for all $\beta$, the residual bound (B.2) and the sparsity bound $\mathcal M(\hat\beta_L)\le4\phi_{\max}\|f_{\hat\beta_L}-f\|_n^2/r^2$ (B.3).
4. Corollary B.2: the error $\delta=\hat\beta_L-\beta$ lies in the cone $|\delta_{J_0^c}|_1\le3|\delta_{J_0}|_1$.
5. (B.30)–(B.31): on $\mathcal A$, $\frac1n|X\delta|_2^2\le16r^2s/\kappa^2$ and $|\delta_{J_0}|_2\le4r\sqrt s/\kappa^2$.
6. (B.27) and (B.28) with $c_0=3$: $\ell_1$ and $\ell_2$ norms of a cone vector.
7. The $\ell_p$ interpolation $\sum a_j^p\le b_1^{2-p}b_2^{p-1}$.

Significance

The result. Theorem 7.2 gives, for fixed $n$ and $M$ rather than asymptotically, the rate $s\log M/n$ for the prediction loss and $s\sqrt{\log M/n}$ for the $\ell_1$ loss of the Lasso, under a condition on the design only (RE), with no assumption on how $M$ compares with $n$. The dependence on $M$ is only logarithmic, which is what makes the Lasso usable when $M\gg n$. Bound (7.9) shows that the Lasso selects at most a constant multiple of $s$ variables, and (7.10) covers every $\ell_p$ loss between $\ell_1$ and $\ell_2$. Together with Theorem 7.1 for the Dantzig selector, the result shows that the two estimators have the same rates.

Formalizing it. The theorem is proved on paper. As far as a search of the platform shows, there is no machine-checked proof of a probabilistic Lasso rate. The closest platform statement, HighDimStat.SparseLinear.lasso_l2_error_bound (Wainwright, Theorem 7.13(a)), is deterministic, assumes a lower bound on the regularisation parameter in place of Gaussian noise, uses a restricted eigenvalue condition over the cone of one fixed support, and concludes an $\ell_2$ bound with a different constant. A formal proof of Theorem 7.2 would supply the Gaussian maximal inequality, the Lasso optimality conditions, and the cone and interpolation inequalities as reusable lemmas.

Difficulty

Each step is short on paper, and none of the steps is deep. The main work is in three places. First, the probability: the event on which the deterministic argument runs involves all $M$ correlations $\frac1n x_{(j)}^\top w$ at once, and its probability must be bounded by exactly $M^{1-A^2/8}$, which requires the law of a linear combination of independent Gaussians and a sharp Gaussian tail estimate, not a generic concentration bound with unspecified constants. Second, the Lasso is defined only through its minimising property, while the sparsity bound (7.9) is a statement about the number of non-zero coordinates of a minimiser of a non-differentiable objective; the characterisation (B.6) of minimisers is not in Mathlib. Third, (7.10) involves two restricted eigenvalue constants, a ranking of coordinates with possible ties, and real exponents, and every constant has to come out exactly.

The obvious idea of proving (7.7)–(7.10) for one fixed minimiser does not suffice: the statement quantifies over every minimiser on a single event.

Formalization scope

The design $X$ is a Matrix (Fin n) (Fin M) ℝ; vectors are functions Fin M → ℝ. The noise is a family W : Fin n → Ω → ℝ of independent, measurable random variables with law gaussianReal 0 σ² on a probability space, and $y(\omega)=X\beta^*+W(\omega)$. The probabilistic conclusion is one measurable event $E$ with $\mathbb P(E)\ge1-M^{1-A^2/8}$ on which every minimiser of (7.2) satisfies all bounds; the event does not depend on the minimiser, on $m$ or on $p$. $\log$ is the natural logarithm.

RE$(s,3)$ and RE$(s,m,3)$ are stated through witnesses: a predicate "$\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ for every admissible $J_0$ and $\delta$", and the theorem holds for every witness $\kappa>0$. Because the paper's $\kappa(s,c_0)$ is an attained minimum, every witness is at most it and the bounds decrease in $\kappa$, so this is equivalent to the printed statement. The assumption quantifies over every $J_0$ with $|J_0|\le s$, as on page 7, not only over the support of $\beta^*$. $\phi_{\max}$ is the supremum of $\frac1n|Xx|_2^2$ over unit vectors $x$. Lemma B.1 is stated in its Section-7 specialisation (unit column norms, $f=X\beta^*$), the form used in the proof of Theorem 7.2; (B.28) is stated for every $c_0>0$ and (B.27) likewise, since the paper writes them with $c_0=1$ and invokes them with $c_0=3$. The printed Theorem 7.2 needs no correction; all four constants were checked against the proof.

A formalization in which the noise is not Gaussian, the Lasso predicate can be vacuous, the RE condition is imposed only on the support of $\beta^*$, or the probability is that of a non-measurable set, is not this theorem and is ruled out by the statement.

Needed infrastructure: Gaussian tail bounds and the law of a linear combination of independent Gaussians (largely in Mathlib), subdifferential calculus for $\ell_1$-penalised least squares, and elementary finite-sum inequalities. The cone inequalities (B.27)–(B.28), the interpolation inequality and the optimality conditions (B.6) are reusable in other sparse-estimation missions; contributions to any milestone are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3, https://arxiv.org/abs/0801.1095 ; https://doi.org/10.1214/08-AOS620
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://arxiv.org/abs/math/0506081
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Statist. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 7. https://doi.org/10.1017/9781108627771

Motivation

In high-dimensional linear regression the number of unknown coefficients $M$ may be much larger than the number of observations $n$, and the coefficient vector can only be recovered because it is assumed to be sparse: few of its entries are non-zero. Two convex estimators dominate this setting: the Lasso of Tibshirani (1996), an $\ell_1$-penalized least-squares estimator, and the Dantzig selector of Candès and Tao (2007), which minimizes the $\ell_1$ norm subject to a bound on the correlation between the residual and the columns of the design. Both are used routinely in statistics, signal processing and machine learning, and their rates of convergence determine how many observations suffice to estimate a sparse vector.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009) analysed the two estimators side by side under a single, weak condition on the design, the restricted eigenvalue (RE) assumption. This mission formalizes their rates for the Dantzig selector, Theorem 7.1 of the paper.

Timeline. Candès and Tao (Ann. Statist. 35, 2007) introduced the Dantzig selector and bounded its $\ell_2$ error under a uniform uncertainty principle on the design. Bickel, Ritov and Tsybakov (2009) replaced that condition by the RE assumptions, which are implied by it (their Lemma 4.1), and obtained $\ell_p$ bounds for every $1\le p\le2$ and a prediction bound, with explicit constants. Later work (van de Geer and Bühlmann, EJS 2009) compared RE with the compatibility condition and other design conditions.

Setting

Observations follow the linear model

$$y=X\beta^*+w,$$

where $X\in\mathbb R^{n\times M}$ is a deterministic design matrix, $n\ge1$, $M\ge2$, $\beta^*\in\mathbb R^M$ is unknown, and $w=(W_1,\dots,W_n)$ has independent $\mathcal N(0,\sigma^2)$ coordinates with $\sigma>0$. The columns are normalized: every diagonal element of the Gram matrix $X^TX/n$ equals 1.

For $\beta\in\mathbb R^M$, $J(\beta)=\{j:\beta_j\ne0\}$ is its support and $\mathcal M(\beta)=|J(\beta)|$ its sparsity; $\beta^*$ satisfies $\mathcal M(\beta^*)\le s$ for an integer $1\le s\le M$. Norms are $|\delta|_p=(\sum_j|\delta_j|^p)^{1/p}$ and $|v|_2^2=\sum_iv_i^2$; for an index set $J$, $\delta_J$ keeps the coordinates of $\delta$ in $J$ and sets the others to 0, and $J^c$ is the complement of $J$.

With a tuning level $r=A\sigma\sqrt{\log M/n}$, $A>\sqrt2$, the Dantzig selector is any minimizer

$$\hat\beta_D\in\arg\min_{\beta\in\Lambda}|\beta|_1,\qquad \Lambda=\Big\{\beta\in\mathbb R^M:\ \Big|\tfrac1nX^T(y-X\beta)\Big|_\infty\le r\Big\}.$$

The cone condition at an index set $J_0$ with constant $c_0>0$ is $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$. Assumption RE$(s,c_0)$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Assumption RE$(s,m,c_0)$ is the same with $|\delta_{J_{01}}|_2$ in the denominator, where $J_{01}=J_0\cup J_1$ and $J_1$ collects the $m$ largest $|\delta_j|$ outside $J_0$; it is used for $s\le m$, $s+m\le M$.

Formalization targets

Goal: Theorem 7.1

With probability at least $1-M^{1-A^2/2}$, every Dantzig selector satisfies

$$|\hat\beta_D-\beta^*|_1\le\frac{8A}{\kappa^2(s,1)}\,\sigma s\sqrt{\frac{\log M}{n}},\qquad |X(\hat\beta_D-\beta^*)|_2^2\le\frac{16A^2}{\kappa^2(s,1)}\,\sigma^2s\log M,$$

and, on the same event, if RE$(s,m,1)$ holds, simultaneously for all $1<p\le2$,

$$|\hat\beta_D-\beta^*|_p^p\le2^{p-1}\,8\Big\{1+\sqrt{\tfrac sm}\Big\}^{2(p-1)}s\Big(\frac{A\sigma}{\kappa^2(s,m,1)}\sqrt{\frac{\log M}{n}}\Big)^p .$$

Milestones

In the order the proof of the paper uses them:

1. The noise event $\mathcal B=\bigcap_j\{|\frac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P\{\mathcal B^c\}\le M^{1-A^2/2}$ (proof of Lemma B.3).
2. Lemma B.3, (B.9): for any $\beta$ satisfying the Dantzig constraint, $\delta=\hat\beta_D-\beta$ satisfies the cone condition at $J(\beta)$ with $c_0=1$.
3. (B.25): on $\mathcal B$, $\beta^*\in\Lambda$, $\frac1n|X^TX\delta|_\infty\le2r$, and $\frac1n|X\delta|_2^2\le4r\sqrt s\,|\delta_{J_0}|_2$.
4. (B.26): under RE$(s,1)$, $\frac1n|X\delta|_2^2\le16r^2s/\kappa^2$ and $|\delta_{J_0}|_2\le4r\sqrt s/\kappa^2$.
5. (B.27): on the cone, $|\delta|_1\le(1+c_0)\sqrt s\,|\delta_{J_0}|_2$.
6. (B.28): on the cone, $|\delta|_2\le(1+c_0\sqrt{s/m})\,|\delta_{J_{01}}|_2$.
7. (B.29): under RE$(s,m,1)$, $|\delta|_2^2\le16(1+\sqrt{s/m})^2(r\sqrt s/\kappa^2)^2$.
8. Interpolation: $\sum_ja_j\le b_1$, $\sum_ja_j^2\le b_2$, $a_j\ge0$ imply $\sum_ja_j^p\le b_1^{2-p}b_2^{p-1}$ for $1<p\le2$.

Significance

The result. Theorem 7.1 shows that, up to the factor $\log M$, the Dantzig selector estimates an $s$-sparse vector as well as least squares would if the support were known: the prediction error $\frac1n|X(\hat\beta_D-\beta^*)|_2^2$ is of order $\sigma^2s\log M/n$, and the $\ell_p$ errors are of order $s^{1/p}\sigma\sqrt{\log M/n}$. The bounds hold for any $M$, including $M\gg n$, provided only that RE holds, and every constant is explicit. The paper's Theorem 7.2 gives the same rates for the Lasso; comparing the two is the paper's main message.

Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has not been machine-checked. A complete formal proof would provide: a verified Gaussian maximal inequality for the noise event, the deterministic cone and RE arithmetic that underlies essentially all $\ell_1$-regularized estimation theory, and a reusable $\ell_1$–$\ell_2$ interpolation lemma. Most milestones are deterministic and independent of the probability layer.

Difficulty

The obvious argument — compare $\hat\beta_D$ with $\beta^*$ in Euclidean norm using the smallest eigenvalue of $X^TX/n$ — fails because that eigenvalue is 0 whenever $M>n$. The proof must instead show that the error vector lies in a cone on which $X$ is injective in a quantitative sense, and this uses the optimality of $\hat\beta_D$ (not just feasibility) together with the event $\mathcal B$ on which $\beta^*$ itself is feasible. The $\ell_p$ bound needs a second, stronger condition RE$(s,m,1)$ and a control of the tail of the error outside the $m$ largest coordinates. On the formal side, handling the non-uniqueness of the minimizer, real powers with exponent $p-1$ or $2-p$, and the union over $M$ Gaussian tails with the exact constant $M^{1-A^2/2}$ all need care.

Formalization scope

Vectors are functions Fin M → ℝ, the design is Matrix (Fin n) (Fin M) ℝ; the paper's dictionary of functions enters only through $X$. The unit diagonal of $X^TX/n$ is a hypothesis, not a normalization performed in the proof. The noise is W : Fin n → Ω → ℝ on a probability space, measurable, mutually independent, each of law $\mathcal N(0,\sigma^2)$; $\log$ is the natural logarithm. The Dantzig selector is a predicate (feasible and of minimal $\ell_1$ norm among feasible vectors), and every result is stated for every minimizer. RE$(s,c_0)$ and RE$(s,m,c_0)$ are stated through a witness $\kappa$ (a number with the defining lower-bound property); $\kappa(s,c_0)$ is the largest witness and the bounds decrease in $\kappa$, so the statements are equivalent to the paper's while avoiding the value of a real infimum over an empty set. Two witnesses are kept apart: $\kappa$ for RE$(s,1)$ in (7.4)–(7.5), $\kappa'$ for RE$(s,m,1)$ in (7.6). Ties in the choice of the $m$ largest coordinates are handled by quantifying over every admissible $J_1$. The probability statement asserts one measurable event $E$ with $\mathbb P(E)\ge1-M^{1-A^2/2}$ on which all three bounds hold for every minimizer, every admissible $m$, every witness $\kappa'$ and every $p$.

The event $E$ is fixed before the minimizer is quantified, so a formalization in which the event depends on $\hat\beta_D$, or in which RE is a hypothesis about the random error vector rather than the design, would be a different (weaker) statement and is not accepted. The deterministic milestones (B.26)–(B.29) take the conclusion of (B.25) as a hypothesis; they are true for every vector satisfying their hypotheses and are not restricted to the event.

A complete development needs Gaussian tail bounds and a union bound (Mathlib's gaussianReal), finite Hölder-type inequalities for real exponents, and elementary sorting arguments for the tail outside $J_{01}$. The cone, RE and interpolation lemmas are reusable for the Lasso (Theorem 7.2, a sister mission) and beyond. Proofs of any milestone are welcome independently.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• S. van de Geer, P. Bühlmann, On the conditions used to prove oracle results for the Lasso, Electron. J. Statist. 3, 1360–1392, 2009. https://doi.org/10.1214/09-EJS506

Motivation

Two estimators dominate sparse high-dimensional regression, where the number $M$ of candidate regressors can far exceed the sample size $n$. The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an $\ell_1$ penalty. The Dantzig selector (Candès and Tao, 2007) minimises the $\ell_1$ norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.

Setting

Let $f_1,\dots,f_M$ be real functions (the dictionary) on a set $\mathcal Z$, and $Z_1,\dots,Z_n\in\mathcal Z$ fixed design points, with $n\ge1$ and $M\ge2$. The design matrix is $X=(f_j(Z_i))\in\mathbb R^{n\times M}$. Observations are $Y_i=f(Z_i)+W_i$, where $f$ is an unknown function and $W_1,\dots,W_n$ are independent $\mathcal N(0,\sigma^2)$ with $\sigma>0$. Write $y=(Y_i)$, $\boldsymbol f=(f(Z_i))$ and $w=(W_i)$, so $y=\boldsymbol f+w$.

The empirical norm of $g$ is $\|g\|_n=(\tfrac1n\sum_i g(Z_i)^2)^{1/2}$. Every column has $\|f_j\|_n\neq0$, and $f_{\max}=\max_j\|f_j\|_n$. For $\beta\in\mathbb R^M$, $f_\beta=\sum_j\beta_jf_j$ has value vector $X\beta$. The support is $J(\beta)=\{j:\beta_j\ne0\}$ and the sparsity is $\mathcal M(\beta)=|J(\beta)|$. For $J\subseteq\{1,\dots,M\}$, $\delta_J$ agrees with $\delta$ on $J$ and vanishes elsewhere.

Fix $r>0$. The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(Y_i-f_\beta(Z_i)\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j| .$$

With $D=\mathrm{diag}(\|f_1\|_n^2,\dots,\|f_M\|_n^2)$, the Dantzig constraint is $|\tfrac1nD^{-1/2}X^\top(y-X\beta)|_\infty\le r$. The Dantzig selector $\hat\beta_D$ is any vector of smallest $|\beta|_1=\sum_j|\beta_j|$ that satisfies it. The estimators are $\hat f_L=f_{\hat\beta_L}$ and $\hat f_D=f_{\hat\beta_D}$.

Assumption RE$(s,c_0)$ with $1\le s\le M$, $c_0>0$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\ \frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Throughout, $r=A\sigma\sqrt{\log M/n}$, where $\log$ is the natural logarithm.

Formalization targets

Goal: Theorem 5.1

Assume RE$(s,1)$ with $1\le s\le M$, and let $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution with $\mathcal M(\hat\beta_L)\le s$ and every Dantzig selector satisfy

$$\Big|\,\|\hat f_D-f\|_n^2-\|\hat f_L-f\|_n^2\,\Big|\le16A^2\,\frac{\mathcal M(\hat\beta_L)\sigma^2}{n}\,\frac{f_{\max}^2}{\kappa^2(s,1)}\,\log M .$$

Milestones

The proof uses one probabilistic event and two one-sided deterministic inequalities.

1. The Lasso satisfies the Dantzig constraint (2.3).
2. The noise event $\mathcal A=\bigcap_j\{2|\tfrac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$ (B.4).
3. On $\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_L)|_\infty\le 3rf_{\max}/2$ (Lemma B.1, (B.2)).
4. The Dantzig error lies in the cone $|\delta_{J_0^c}|_1\le|\delta_{J_0}|_1$ (Lemma B.3, (B.9)).
5. On the larger event $\mathcal B\supseteq\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_D)|_\infty\le 2rf_{\max}$ (Lemma B.3, (B.10)).
6. $\|\hat f_D-f\|_n^2\le\|\hat f_L-f\|_n^2+16f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal B$ (B.15).
7. $\|\hat f_L-f\|_n^2\le\|\hat f_D-f\|_n^2+9f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal A$ (B.17).

Further result: Theorem 5.2

Assume $\|f_j\|_n=1$ for all $j$ and RE$(s,5)$. With probability at least $1-M^{1-A^2/8}$, whenever $\mathcal M(\hat\beta_D)\le s$,

$$\|\hat f_L-f\|_n^2\le10\|\hat f_D-f\|_n^2+81A^2\,\frac{\mathcal M(\hat\beta_D)\sigma^2}{n}\,\frac{\log M}{\kappa^2(s,5)} .$$

Significance

The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate $\mathcal M(\hat\beta_L)\sigma^2\log M/n$ of a sparse regression with $\mathcal M(\hat\beta_L)$ parameters. The bound carries a factor $f^2_{\max}/\kappa^2(s,1)$ that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating $f$ to the dictionary.

Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, $16A^2$ and the thresholds $2\sqrt2$ and $M^{1-A^2/8}$, which appear in all later analyses.

Difficulty

Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives $\pm\tfrac2n\delta^\top X^\top(\boldsymbol f-X\hat\beta)$ plus $\tfrac1n|X\delta|_2^2$ with $\delta=\hat\beta_L-\hat\beta_D$. A crude bound on the cross term, $|\delta|_1\cdot|X^\top(\cdot)|_\infty$, yields an error proportional to $|\delta|_1$. This does not produce the sparse rate unless $|\delta|_1$ is controlled by $|X\delta|_2$. That control needs $\delta$ to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector $\hat\beta_L$. The restricted eigenvalue condition must therefore hold uniformly over supports of size at most $s$; a condition for one fixed support does not suffice. The probabilistic part is a union bound over $M$ Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.

Formalization scope

The dictionary and the design points enter every statement only through $X$ and $\boldsymbol f$, so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and $f$ is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and $y=f+W(\omega)$. The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as $|\tfrac1n\sum_iX_{ij}(y_i-(X\beta)_i)|\le r\|f_j\|_n$. The Lasso penalty and the Dantzig constraint are weighted by $\|f_j\|_n$, and the Dantzig objective $|\beta|_1$ is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.

RE$(s,c_0)$ is stated through a witness: a real $\kappa>0$ with $\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ on the cone, for all $|J_0|\le s$. The paper's $\kappa(s,c_0)$ is attained, so it is the largest witness. Every bound decreases in $\kappa$, so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least $p$" becomes the existence of a measurable event $E$ with $\mathbb P(E)\ge p$ on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition $\mathcal M(\hat\beta_L)\le s$ is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events $\mathcal A$ and $\mathcal B$ as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every $A>0$, which is stronger than the paper's $A>2\sqrt2$ and still true.

The goal cannot be made vacuous. For $A>2\sqrt2$ the probability bound $1-M^{1-A^2/8}$ is positive. Lasso solutions exist because $r>0$ and every $\|f_j\|_n>0$, and Dantzig selectors exist because the Lasso is feasible. RE$(s,1)$ with $\kappa=1$ holds for $X=\sqrt n\,I$.

A complete development needs:

• subgradient optimality for the weighted Lasso;
• a Gaussian tail bound $\mathbb P(|\eta|\ge t)\le e^{-t^2/2}$ together with the law of a weighted sum of independent Gaussians;
• Cauchy–Schwarz on supports;
• the quadratic bound $bx-x^2\le b^2/4$.

The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095 ; doi:10.1214/08-AOS620
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Stat. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision $x_t$ from a fixed set $D\subseteq\mathbb R^n$ and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function $\mu^\top x_t$. The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where $D$ is the set of standard basis vectors.

Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is $O^*(n\sqrt T)$ with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).

Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the $O^*(n\sqrt T)$ bound and a matching $\Omega(n\sqrt T)$ lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.

Setting

Fix $n\ge1$ and a compact decision set $D\subseteq\mathbb R^n$ whose standard basis $e_1,\dots,e_n$ is a barycentric spanner: each $e_i\in D$ and every $x\in D$ lies in the cube $[-1,1]^n$. The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector $\mu\in\mathbb R^n$ satisfies $|\mu^\top x|\le1$ for $x\in D$, and $x^*\in D$ minimises $\mu^\top x$.

On round $t=1,2,\dots$ the learner plays $x_t\in D$, measurable with respect to the information $\mathcal F_t$ before round $t$, and observes a loss $\ell_t\in[-1,1]$ with $\mathbb E[\ell_t\mid\mathcal F_t]=\mu^\top x_t$. The regret after $T$ rounds is

$$R_T=\sum_{t=1}^T\big(\mu^\top x_t-\mu^\top x^*\big).$$

ConfidenceBall₂$(D,\delta)$ maintains the design matrix $A_t=I+\sum_{\tau<t}x_\tau x_\tau^\top$, the least-squares estimate $\hat\mu_t=A_t^{-1}\sum_{\tau<t}\ell_\tau x_\tau$, the radius

$$\beta_t=\max\Big(128\,n\ln t\ln(t^2/\delta),\ \big(\tfrac83\ln(t^2/\delta)\big)^2\Big),$$

and the confidence ellipsoid $B^2_t=\{\nu:(\nu-\hat\mu_t)^\top A_t(\nu-\hat\mu_t)\le\beta_t\}$. It plays the optimistic decision $x_t\in\operatorname{argmin}_{x\in D}\min_{\nu\in B^2_t}\nu^\top x$. The analysis uses the width $w_t=\sqrt{x_t^\top A_t^{-1}x_t}$, the error $Z_t=(\hat\mu_t-\mu)^\top A_t(\hat\mu_t-\mu)$, and the noise $\eta_t=\ell_t-\mu^\top x_t$.

Formalization targets

Goal: Theorem 2, ConfidenceBall₂ bullet (corrected)

For $0<\delta<1$ with $n\le\beta_1$ and noise $|\eta_t|\le1$,

$$\Pr\Big(\forall T\ge1,\ R_T\le\sqrt{8nT\beta_T\ln(T+1)}\Big)\ge1-\delta.$$

A single event covers every horizon, so the bound is anytime.

Milestones

• Lemma 8. If $\mu\in B^2_t$ then $r_t\le2\min(\sqrt{\beta_t}w_t,1)$.
• Lemma 10. $\det A_{t+1}=\prod_{\tau=1}^t(1+w_\tau^2)$.
• Lemma 9 (corrected). $\sum_{\tau=1}^t\min(w_\tau^2,1)\le2n\ln(t+1)$.
• Theorem 6 (corrected). If $\mu\in B^2_t$ for all $t\le T$, then $\sum_{t\le T}r_t^2\le8n\beta_T\ln(T+1)$.
• Theorem 4 (Freedman). $\Pr(\sum X_i\ge a,\ V\le v)\le\exp(-a^2/(2v+2ab/3))$ for martingale differences bounded above by $b$.
• Lemma 12. $Z_t\le n+2\sum_{\tau<t}\eta_\tau\frac{x_\tau^\top(\hat\mu_\tau-\mu)}{1+w_\tau^2}+\sum_{\tau<t}\eta_\tau^2\frac{w_\tau^2}{1+w_\tau^2}$.
• Lemma 14. $\Pr(\forall t,\ \sum_{\tau<t}M_\tau\le\beta_t/2)\ge1-\delta$.
• Theorem 5 (Confidence). $\Pr(\forall t,\ \mu\in B^2_t)\ge1-\delta$.

Significance

The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension $n$ rather than on $|D|$, holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor $\Theta^*(\sqrt n)$. The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on $\log\det A_t$, are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.

The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).

Difficulty

The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to $\sum_\tau M_\tau$ would need a deterministic step bound, and the natural one gives only a $T^{3/4}$ regret. The step sizes of $M_t$ are bounded in terms of the random widths $w_t$, so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event $\{V\le v\}$ is random. The escape indicator $E_t$, which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all $t$ simultaneously. Freedman's inequality itself is not in Mathlib.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed $t=1,2,\dots$ in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration $(\mathcal F_t)$; $x_t$ is $\mathcal F_t$-measurable and $\ell_t$ is $\mathcal F_{t+1}$-measurable. The argmin is encoded as a joint minimiser over $D\times B^2_t$, which admits every tie-break and is required on every outcome; measurability of $x_t$ is a hypothesis, not derived from the selection. The optimum $x^*$ is a hypothesis ($x^*\in D$, minimising), not an sInf.

Corrections of the printed statements, each labelled in the item's Formalization Note:

1. $\ln(T+1)$ for $\ln T$ in Lemma 9, Theorem 6 and Theorem 2. The printed bounds are false at $T=1$ (with $n=1$, $D=[-1,1]$, $\mu>0$, the tie-break $x_1=1$ gives $R_1=2\mu>0$ against a bound of $0$); the proof of Lemma 9 gives $2\ln\det A_{t+1}\le2n\ln(t+1)$.
2. $n\le\beta_1=(\tfrac83\ln(1/\delta))^2$ is added to Theorems 5 and 2: the proof of Theorem 5 claims $Z_1\le n<\beta_1$, which fails for $\delta$ near $1$. Theorem 6 takes the proof's "$1<\beta_1$" as the hypothesis $\beta_1\ge1$.
3. $|\ell_t-\mu^\top x_t|\le1$ is added to Lemma 14, Theorems 5 and 2: Section 5.2 uses $|\eta_t|\le1$, while the model gives only $|\eta_t|\le2$. It holds when costs lie in $[0,1]$.
4. Theorem 5's "$\delta>0$" is stated with $0<\delta<1$; Lemma 10's index typo ($w_t$ for $w_\tau$) and Theorem 4's $\sum_{i=1}^n$ (for $T$) are corrected.

A regret bound for an arbitrary decision sequence under the assumption $\mu\in B^2_t$ for all $t$ is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and $\delta$ as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite $D$ with a fixed tie-break and i.i.d. costs in $[0,1]$.

Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.

Selected references

• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• D. A. Freedman, On Tail Probabilities for Martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• B. Awerbuch, R. Kleinberg, Adaptive Routing with End-to-End Feedback, STOC 2004. https://doi.org/10.1145/1007352.1007367
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://arxiv.org/abs/1102.2670
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401