Statistics

Motivation

The Standard Model of particle physics does not explain the values of its dimensionless constants, nor does it require them to be constant in time. The proton-to-electron mass ratio $\mu = m_p/m_e \approx 1836$ is one such constant: it compares the scale of the strong interaction (which sets most of the proton mass) with the electroweak scale (which sets the electron mass). A measured change of $\mu$ over cosmic time would signal physics beyond the Standard Model, while a tight null result constrains models with additional scalar fields.

The standard test compares the frequencies of molecular transitions observed in distant galaxies with laboratory values. Different transitions respond differently to a change of $\mu$, so a relative shift between them cannot be confused with the overall cosmological redshift.

Timeline. Optical studies of molecular hydrogen at redshifts $z>2$ reached $|\Delta\mu/\mu| < 10^{-5}$ (Malec et al. 2010; van Weerdenburg et al. 2011). Ammonia inversion lines, about 100 times more sensitive, moved the field to radio astronomy and gave constraints at the $10^{-7}$ level toward the lensing galaxy of PKS 1830−211 at $z=0.89$ (Henkel et al. 2009; Kanekar 2011). Jansen et al. (2011) and Levshakov, Kozlov & Reimers (2011) pointed out that methanol transitions have sensitivity coefficients ranging from about $-42$ to $+53$. Ellingsen et al. (2012) gave a first methanol limit from two lines. Bagdonaite et al. (Science, 2013) observed four methanol lines in PKS 1830−211 with the Effelsberg 100-m telescope and derived the limit $\Delta\mu/\mu = (0.0\pm1.0)\times10^{-7}$ at a look-back time of about 7 billion years.

Setting

A transition with frequency $\nu$ has sensitivity coefficient $K_\mu$ defined by

$$\frac{\Delta\nu}{\nu} = K_\mu\,\frac{\Delta\mu}{\mu},$$

or, in infinitesimal form, $K_\mu = \frac{\mu}{\nu}\frac{d\nu}{d\mu}$. Pure rotational transitions have frequency inversely proportional to the reduced mass, hence to $\mu$, so $K_\mu=-1$. Mixed torsion–rotation transitions of methanol have strongly enhanced coefficients (Table 1 of the paper: $-32.8$ and $-7.4$).

Each observed line is assigned a position $V$, a velocity (km/s) on a common scale centred on redshift $z=0.88582$. If $\mu$ in the absorbing galaxy differs from the laboratory value by $\Delta\mu = \mu_z-\mu_{\mathrm{lab}}$, the positions satisfy

$$\frac{V}{c} = -K_\mu\,\frac{\Delta\mu}{\mu}$$

up to a velocity offset common to all lines, where $c$ is the speed of light. Plotting $V$ against $K_\mu$ and fitting a straight line $V = a + bK_\mu$ therefore gives $\Delta\mu/\mu = -b/c$.

The fit is a weighted least-squares fit with weights $1/\sigma_i^2$, where $\sigma_i$ is the 1σ uncertainty of the $i$-th position. With $S=\sum 1/\sigma_i^2$, $S_K=\sum K_i/\sigma_i^2$, $S_V=\sum V_i/\sigma_i^2$, $S_{KK}=\sum K_i^2/\sigma_i^2$, $S_{KV}=\sum K_iV_i/\sigma_i^2$ and $\Delta=SS_{KK}-S_K^2$, the slope, intercept and slope standard error are $b=(SS_{KV}-S_KS_V)/\Delta$, $a=(S_{KK}S_V-S_KS_{KV})/\Delta$ and $\sigma_b=\sqrt{S/\Delta}$. The reduced chi-squared is $\chi^2_\nu=\frac{1}{n-2}\sum_i\big((V_i-a-bK_i)/\sigma_i\big)^2$.

The data (Table 1) are four lines: $3_{-1}$–$2_0\,E$ ($K_\mu=-32.8$, $V=9.06\pm0.67$), $0_0$–$1_0\,A^+$ ($-1$, $8.40\pm0.10$), $0_0$–$1_0\,E$ ($-1$, $9.12\pm0.30$) and $2_{-1}$–$1_0\,E$ ($-7.4$, $9.83\pm0.43$). Because A- and E-symmetry methanol behave as separate species that may be spatially segregated, the fiducial fit uses only the three E lines.

Formalization targets

Goal: the headline limit

With the E-line estimate $\widehat{\Delta\mu/\mu}=-b/c$, its statistical error $\sigma_{\mathrm{stat}}=\sigma_b/c$ and the adopted systematic error $\sigma_{\mathrm{sys}}=7.0\times10^{-8}$,

$$\big|\widehat{\Delta\mu/\mu}\big| < 0.05\times10^{-7},\qquad \Big|\sqrt{\sigma_{\mathrm{stat}}^2+\sigma_{\mathrm{sys}}^2}-1.0\times10^{-7}\Big| < 0.05\times10^{-7},$$

i.e. $\Delta\mu/\mu=(0.0\pm1.0)\times10^{-7}$ to the printed precision.

Milestones

1. Pure rotational transitions ($\nu\propto1/\mu$) have $K_\mu=-1$.
2. Under the exact relation $V_i=a-c\,\delta\,K_i$, the weighted fit returns $-b/c=\delta$ and intercept $a$.
3. E-line fit: $\Delta\mu/\mu=(-0.1\pm7.6)\times10^{-8}$, $\chi^2_\nu\approx2.0$.
4. The E-line result is consistent with $\Delta\mu=0$ at the $1.5\times10^{-7}$ (two-standard-error) level.
5. Four-line fit: $\Delta\mu/\mu=(11.0\pm6.8)\times10^{-8}$, $\chi^2_\nu\approx6.4$.
6. The $0_0$–$1_0$ $A^+$ and $E$ lines are separated by $0.72\pm0.32$ km/s.
7. The $A^+$ anchor line shifted by $0.48\pm0.26$ km/s between December 2011 and April 2012.

Significance

The result. The authors report the limit as statistically more constraining than previous radio-domain tests of a drifting $\mu$. Because it uses a single molecular species, it is much less exposed to the main systematic of multi-species comparisons, namely that different molecules sit in different gas at slightly different velocities. The milestones record the internal evidence behind the choice of the fiducial fit: the poor four-line $\chi^2_\nu$ and the A–E velocity separation.

Formalizing it. The physical inputs (sensitivity coefficients, measured positions, the systematic budget) are taken as data. What the mission checks by machine is the chain from those data to the printed numbers: the definition of the sensitivity coefficient and its value for rotational lines, the correctness of the line-fit estimator, and the arithmetic of every reported fit, separation and error combination.

Difficulty

The numerical milestones are exact statements about explicit rational data, but they involve nested sums, quotients and square roots, so a certified proof requires careful interval bounds rather than floating-point evaluation. The paper's numbers are rounded from unrounded measurements: recomputing from the rounded Table 1 entries gives, for example, $\sigma_b/c\approx7.69\times10^{-8}$ instead of $7.6\times10^{-8}$, and $\chi^2_\nu\approx6.27$ instead of $6.4$ for the four-line fit. Tolerances therefore had to be chosen so that every statement is both faithful to the printed value and true for the tabulated data. The general recovery milestone requires showing that the normal equations are nondegenerate whenever the $K_i$ are not all equal.

Formalization scope

• All quantities are real numbers in Lean; data are finite families indexed by Fin n. Velocities are in km/s and $c=299792.458$ km/s.
• The sensitivity coefficient is the logarithmic derivative $(\mu/\nu(\mu))\,\nu'(\mu)$ using Mathlib's deriv.
• The fit uses the closed-form weighted least-squares formulas above; the reduced chi-squared divides by $n-2$.
• The systematic uncertainty $7.0\times10^{-8}$ is an input; the variability model behind it is out of scope, as are the radiative-transfer column densities and the spectroscopic computation of $K_\mu$ for mixed transitions.
• "95% confidence level" is formalized as the two-standard-error interval.
• Trivializing readings are excluded: every numerical statement is a closed statement about the tabulated data, with no free hypotheses, and the general recovery statement requires non-constant $K$ and nonzero uncertainties.

Reusable pieces: the weighted least-squares definitions and the exact-recovery lemma apply to any straight-line fit with known uncertainties.

Selected references

• J. Bagdonaite, P. Jansen, C. Henkel, H. L. Bethlem, K. M. Menten, W. Ubachs, A Stringent Limit on a Drifting Proton-to-Electron Mass Ratio from Alcohol in the Early Universe, Science, 2013. https://doi.org/10.1126/science.1224898
• P. Jansen, L.-H. Xu, I. Kleiner, W. Ubachs, H. L. Bethlem, Methanol as a sensitive probe for spatial and temporal variations of the proton-to-electron mass ratio, Phys. Rev. Lett. 106, 100801, 2011. https://doi.org/10.1103/PhysRevLett.106.100801
• S. P. Ellingsen, M. A. Voronkov, S. L. Breen, J. E. J. Lovell, First cosmological constraints on the proton-to-electron mass ratio from observations of rotational transitions of methanol, Astrophys. J. Lett. 747, L7, 2012. https://doi.org/10.1088/2041-8205/747/1/L7
• Ph. R. Bevington, D. K. Robinson, Data Reduction and Error Analysis for the Physical Sciences, 3rd ed., McGraw-Hill, 2003.

Motivation

Best subset selection with a ridge term, the $\ell_0\ell_2$-regularized least squares problem

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2,$$

is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box $|\beta_i| \le M z_i$ (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces $\beta_i^2$ by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.

Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, $\mathrm{PR}(\infty)$, studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.

Setting

Fix a design matrix $X \in \mathbb R^{n\times p}$, a response $y \in \mathbb R^n$, parameters $\lambda_0, \lambda_2 > 0$ and a bound $M > 0$. Write $[p] = \{1,\dots,p\}$ and $\|\beta\|_\infty \le M$ for $|\beta_i| \le M$ for every $i \in [p]$.

The Big-M formulation (2) is

$$\min_{\beta, z}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\sum_{i\in[p]} z_i + \lambda_2\|\beta\|_2^2 \quad\text{s.t.}\quad -Mz_i \le \beta_i \le Mz_i,\ z_i\in\{0,1\}.$$

Its interval relaxation replaces $z_i \in \{0,1\}$ by $z_i \in [0,1]$; its optimal value is $V_{B(M)}$. Eliminating $z$ gives the equivalent form (37),

$$V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta),\qquad H(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\Big(\frac{\lambda_0}{M}|\beta_i| + \lambda_2\beta_i^2\Big).$$

The reverse Huber penalty is $\mathcal B(t) = |t|$ for $|t| \le 1$ and $\mathcal B(t) = (t^2+1)/2$ for $|t| \ge 1$, and $\psi_1(b;\lambda_0,\lambda_2) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$. The interval relaxation of $\mathrm{PR}(\infty)$ has the value (6),

$$V_{PR(\infty)} = \min_{\beta\in\mathbb R^p} G(\beta),\qquad G(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2).$$

Let $\mathcal S(\lambda_2)$ be the set of minimizers of $G$, and, as in (9),

$$\mathcal L(M) = \{\lambda_2 > 0 \;:\; \exists\beta\in\mathcal S(\lambda_2) \text{ with } \|\beta\|_\infty \le M\}.$$

The comparison runs through the scalar function $t(b) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0}) - \frac{\lambda_0}{M}|b| - \lambda_2 b^2 = \psi_1(b) - \big(\tfrac{\lambda_0}{M}|b| + \lambda_2 b^2\big)$ and through $v^*(M) = \min_{\|\beta\|_\infty\le M} G(\beta)$.

Formalization targets

Goal: Proposition 2 (p. 7)

$$V_{B(M)} \ge V_{PR(\infty)}\quad\text{if } M \le \tfrac12\sqrt{\lambda_0/\lambda_2},\qquad (10)$$ $$V_{B(M)} \le V_{PR(\infty)}\quad\text{if } M \ge \sqrt{\lambda_0/\lambda_2} \text{ and } \lambda_2 \in \mathcal L(M).\qquad (11)$$

Milestones, in the order of the paper's proof

1. (37): $V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta)$, attained.
2. (10) on its own.
3. Lemma 1: for $M \ge \sqrt{\lambda_0/\lambda_2}$ and $b \in [-M, M]$, $t(b) \ge 0$.
4. (41): for $M \ge \sqrt{\lambda_0/\lambda_2}$, $v^*(M) \ge V_{B(M)}$.

The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for $M \le \frac12\sqrt{\lambda_0/\lambda_2}$ and $|b| \le M$, $t(b) = (2\sqrt{\lambda_0\lambda_2} - \lambda_0/M)|b| - \lambda_2 b^2 \le 0$.

Significance

Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of $\mathrm{PR}(\infty)$ lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small $\lambda_2$ favours the Big-M relaxation and a large $\lambda_2$ favours $\mathrm{PR}(\infty)$ (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation $\mathrm{PR}(M)$ beats both when $\sqrt{\lambda_0/\lambda_2} > M$, this motivates the paper's choice of $\mathrm{PR}(M)$ as the formulation on which its BnB solver is built.

The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.

Difficulty

The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, $|b| = \sqrt{\lambda_0/\lambda_2}$, and at the sign of $2\sqrt{\lambda_0\lambda_2} - \lambda_0/M$. The passage from coordinatewise inequalities to optimal values is where care is needed. $V_{B(M)}$ is defined over pairs $(\beta, z)$, and its identification with a minimum of $H$ over a compact box requires eliminating $z$ and showing attainment. For (11) a pointwise comparison of $G$ and $H$ on the box only bounds $V_{B(M)}$ by the box-restricted value $v^*(M)$, not by $V_{PR(\infty)}$, which is an infimum over all of $\mathbb R^p$; the hypothesis $\lambda_2 \in \mathcal L(M)$ is what closes this gap, and dropping it gives a statement the paper does not prove.

Formalization scope

All declarations live in the namespace L0BnB.BigMvsPR. Vectors are Fin p → ℝ, $X$ is a Matrix (Fin n) (Fin p) ℝ, and $X\beta$ is X *ᵥ β. Every norm is an explicit sum: $\|v\|_2^2 = \sum_i v_i^2$, and $\|\beta\|_\infty \le M$ is $\forall i,\ |\beta_i| \le M$. The reverse Huber penalty is an if on $|t| \le 1$.

Optimal values are real infima (sInf): $V_{B(M)}$ over the feasible pairs $(\beta, z)$ of the interval relaxation, $V_{PR(\infty)}$ over all of $\mathbb R^p$, $v^*(M)$ over the box. For $\lambda_0, \lambda_2 > 0$ each set of values is nonempty ($\beta = z = 0$) and bounded below by $0$, so no infimum takes Lean's junk value. $V_{PR(\infty)}$ is defined as the displayed minimum (6); its identification with the interval relaxation of $\mathrm{PR}(\infty)$ is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. $\mathcal S(\lambda_2)$ is the set of minimizers of $G$, as the paper uses it in the proof of (11).

All theorems assume $\lambda_0, \lambda_2, M > 0$. The paper remarks that Proposition 2 applies for any $M \ge 0$; $M = 0$ is excluded because $H$ and $t$ divide by $M$. The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of $H$ and $G$ is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.

The paper states no $O(\cdot)$ bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of $H$), and of the goal.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming, 2022. https://arxiv.org/abs/2004.06152
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv preprint, 2015. https://arxiv.org/abs/1510.06083
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, The Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388
• A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
• O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
• A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007 (the reverse Huber penalty).

Motivation

Best subset selection with ridge shrinkage asks for a coefficient vector $\beta\in\mathbb R^p$ that fits a response $y\in\mathbb R^n$ through a design matrix $X\in\mathbb R^{n\times p}$ while using few nonzero coefficients:

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2 .$$

This $\ell_0\ell_2$-regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound $M$ instead of the bound-free formulation.

The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.

Setting

Fix $X$, $y$, regularization parameters $\lambda_0,\lambda_2>0$ and a bound $M>0$ on $\|\beta\|_\infty$; write $[p]=\{1,\dots,p\}$.

The Big-M formulation $B(M)$ introduces indicators $z_i$ and minimizes $\tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_i z_i+\lambda_2\|\beta\|_2^2$ subject to $-Mz_i\le\beta_i\le Mz_i$, $z_i\in\{0,1\}$. Its interval relaxation lets $z_i\in[0,1]$; its optimal value is $V_{B(M)}$.

The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The paper's Theorem 1 shows that the interval relaxation of the perspective formulation $\mathrm{PR}(M)$ is equivalent to

$$\min_{\|\beta\|_\infty\le M} F(\beta),\qquad F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M), \tag{5}$$

and $V_{PR(M)}$ denotes the optimal value of (5). Without a bound, the relaxation value of $\mathrm{PR}(\infty)$ is

$$V_{PR(\infty)}=\min_{\beta\in\mathbb R^p}G(\beta),\qquad G(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2). \tag{6}$$

Finally $h(\lambda_0,\lambda_2,M)=\lambda_0/M+\lambda_2M-2\sqrt{\lambda_0\lambda_2}$, and $\beta^*$ denotes an optimal solution of (5).

Formalization targets

Goal: Proposition 1

For $\sqrt{\lambda_0/\lambda_2}>M$,

$$V_{PR(M)}\ \ge\ V_{B(M)}+\lambda_2\big(M\|\beta^*\|_1-\|\beta^*\|_2^2\big), \tag{7}$$ $$V_{PR(M)}\ \ge\ V_{PR(\infty)}+h(\lambda_0,\lambda_2,M)\,\|\beta^*\|_1. \tag{8}$$

Milestones

1. (37): $V_{B(M)}=\min_{\|\beta\|_\infty\le M}H(\beta)$ with $H(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_i\big(\tfrac{\lambda_0}{M}|\beta_i|+\lambda_2\beta_i^2\big)$; the Big-M relaxation expressed in $\beta$ alone. It holds for every $M>0$.
2. (7) alone.
3. The linear case of $\psi_1$: if $|b|\le M<\sqrt{\lambda_0/\lambda_2}$ then $\psi_1(b;\lambda_0,\lambda_2)=2|b|\sqrt{\lambda_0\lambda_2}$.
4. (8) alone (the paper's (38)).

The goal is the conjunction of milestones 2 and 4.

Significance

In the regime $\sqrt{\lambda_0/\lambda_2}>M$ both added terms are nonnegative: $M\|\beta^*\|_1\ge\|\beta^*\|_2^2$ because $\|\beta^*\|_\infty\le M$, and $h>0$ because $\lambda_0/M+\lambda_2M>2\sqrt{\lambda_0\lambda_2}$ whenever $M\ne\sqrt{\lambda_0/\lambda_2}$. So the perspective relaxation is at least as strong as both the Big-M relaxation and $\mathrm{PR}(\infty)$, strictly so as soon as one coordinate of $\beta^*$ lies strictly inside $(0,M)$ in absolute value (for (7)) or $\beta^*\ne0$ (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on $\mathrm{PR}(M)$ with a valid, tight $M$; the regime $\sqrt{\lambda_0/\lambda_2}\le M$, where (5) is (6) with the additional box constraint $\|\beta\|_\infty\le M$, is complementary.

Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.

Difficulty

The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "$V_{PR(M)}-V_{B(M)}\ge F(\beta^*)-H(\beta^*)$" requires that the Big-M relaxation, which is posed over pairs $(\beta,z)$, have value at most $H(\beta^*)$; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs $V_{PR(\infty)}\le G(\beta^*)$, i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime $\sqrt{\lambda_0/\lambda_2}>M$, in which $\psi=\psi_2$. Dropping the regime hypothesis makes (8) false in general: for $\sqrt{\lambda_0/\lambda_2}\le M$ one has $\psi=\psi_1$ and $h\ge0$, and the right side can exceed $V_{PR(M)}=V_{PR(\infty)}$.

Formalization scope

All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms are explicit sums: $\|v\|_2^2$ is ∑ i, v i ^ 2, $\|\beta\|_1$ is ∑ i, |β i|, and $\|\beta\|_\infty\le M$ is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).

Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty ($\beta=0$, $z=0$) and bounded below by $0$ under the positivity hypotheses, so sInf is the true infimum and never a junk value. $V_{B(M)}$ is defined over pairs $(\beta,z)$ with $z_i\in[0,1]$, not through $H$; (37) is a theorem. $V_{PR(\infty)}$ is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of $\mathrm{PR}(\infty)$ in $(\beta,z,s)$ variables, and that identification is not part of the mission. $V_{PR(M)}$ is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the $(\beta,z,s)$ relaxation) belongs to a sibling mission.

The optimal solution $\beta^*$ is a binder with the hypotheses $\|\beta^*\|_\infty\le M$ and $F(\beta^*)\le F(\beta)$ for every $\beta$ in the box. A formalization in which $\beta^*$ is an arbitrary feasible point, or in which $V_{B(M)}$ or $V_{PR(\infty)}$ is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no $O(\cdot)$ in this result, so no constant is instantiated.

Needed infrastructure is light: continuity of $H$ and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming (2022). https://arxiv.org/abs/2004.06152
• H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 1517–1537, 2020. https://doi.org/10.1287/opre.2019.1919
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv e-prints, 2015 (the paper's reference [21], source of (6) for $\mathrm{PR}(\infty)$). https://arxiv.org/abs/1510.06083

Motivation

Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix $X\in\mathbb R^{n\times p}$ and responses $y\in\mathbb R^n$, minimize

$$\tfrac12\|y-X\beta\|_2^2+\lambda_0\|\beta\|_0+\lambda_2\|\beta\|_2^2 ,$$

where $\|\beta\|_0$ counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.

Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in $\beta$ alone. This mission formalizes Theorem 1.

Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes $\ell_1$.

Setting

Fix $X\in\mathbb R^{n\times p}$, $y\in\mathbb R^n$, $\lambda_0>0$, $\lambda_2>0$ and $M>0$, and write $[p]=\{1,\dots,p\}$. The perspective formulation $\mathrm{PR}(M)$ is problem (3) of the paper:

$$\min_{\beta,z,s}\ \tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_{i\in[p]}z_i+\lambda_2\sum_{i\in[p]}s_i \quad\text{s.t.}\quad \beta_i^2\le s_iz_i,\ \ -Mz_i\le\beta_i\le Mz_i,\ \ z_i\in\{0,1\},\ \ s_i\ge0 .$$

Here $z_i$ indicates whether $\beta_i$ may be nonzero, $s_i$ stands in for $\beta_i^2$ through the rotated second-order cone constraint $\beta_i^2\le s_iz_i$, and $M$ bounds $|\beta_i|$. The interval relaxation replaces $z_i\in\{0,1\}$ with $z_i\in[0,1]$.

The reverse Huber penalty (4) is $\mathcal B(t)=|t|$ for $|t|\le1$ and $\mathcal B(t)=(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The reduced relaxation (5) is

$$\min_{\beta\in\mathbb R^p}\ F(\beta):=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M)\quad\text{s.t.}\quad\|\beta\|_\infty\le M ,$$

with optimal value $V_{\mathrm{PR}(M)}$. For one coordinate $b$, $\omega(b;\lambda_0,\lambda_2,M)$ is the minimum of $\lambda_0z+\lambda_2s$ over $b^2\le sz$, $-Mz\le b\le Mz$, $z\in[0,1]$, $s\ge0$.

Formalization targets

Goal: Theorem 1 (Reduced Relaxation), p. 6

The interval relaxation of (3) is equivalent to (5):

$$\exists\,(z,s):\ (\beta,z,s)\ \text{feasible}\iff\|\beta\|_\infty\le M,\qquad \min_{z,s}\Big\{\tfrac12\|y-X\beta\|_2^2+\lambda_0\textstyle\sum_i z_i+\lambda_2\sum_i s_i\Big\}=F(\beta)\ \ (\|\beta\|_\infty\le M),$$

and both problems attain the common optimal value $V_{\mathrm{PR}(M)}$.

Milestones (proof of Theorem 1, p. 28)

1. Reduction to (36). For $|b|\le M$, the smallest feasible $z$ is $\hat z=\max\{b^2/s,|b|/M\}$, so

$$\omega(b;\lambda_0,\lambda_2,M)=\min_{s\ge b^2}\max\Big\{\lambda_0\tfrac{b^2}{s}+\lambda_2s,\ \lambda_0\tfrac{|b|}{M}+\lambda_2s\Big\}.$$

2. Case I. If $\sqrt{\lambda_0/\lambda_2}\le M$ and $|b|\le M$, then $\omega(b;\lambda_0,\lambda_2,M)=2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$.
3. Case II. If $\sqrt{\lambda_0/\lambda_2}>M$ and $|b|\le M$, then $\omega(b;\lambda_0,\lambda_2,M)=(\lambda_0/M+\lambda_2M)|b|$.

Significance

The result. Theorem 1 removes the $2p$ auxiliary variables $z,s$ and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when $\sqrt{\lambda_0/\lambda_2}>M$, the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure $\ell_1$. Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and $\mathrm{PR}(\infty)$ relaxations, use this reduced form.

Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary $\sqrt{\lambda_0/\lambda_2}=M$, where the two formulas must agree with the stated tie-breaking.

Difficulty

The obvious approach, "minimize over $z$ and $s$ coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint $\beta_i^2\le s_iz_i$ degenerates at $s_i=0$ or $z_i=0$, where $\beta_i^2/s_i$ is undefined, and the paper's convention for $\beta_i=s_i=0$ must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of $s$, one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover $s=|b|M$, depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible $s$, not just evaluate at a candidate. Finally, the minimum over $(z,s)\in\mathbb R^{2p}$ must be shown to split into a sum of coordinate minima, each attained.

Formalization scope

Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's $[p]$ is Fin p. The squared norm $\|y-X\beta\|_2^2$ is the explicit sum $\sum_r(y_r-(X\beta)_r)^2$, and $\|\beta\|_\infty\le M$ is $|\beta_i|\le M$ for all $i$. The cone constraint is kept in product form $\beta_i^2\le s_iz_i$. In $\hat z$ and (36), Lean's $b^2/0=0$ coincides with the paper's convention $\beta_i^2/s_i=0$ for $\beta_i=s_i=0$. Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. $V_{\mathrm{PR}(M)}$ is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of $X$ or $y$ is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no $O(\cdot)$ in these results, so there are no constants to instantiate.

A goal stating only one inequality (that $F(\beta)$ is achieved by some $(z,s)$, or that it bounds the relaxation from below), or a goal over $z_i\in\{0,1\}$, would not be Theorem 1. The IsLeast form rules out both. The goal uses $\psi$ with both regimes.

A complete development needs: a two-variable convexity argument for $\lambda_0b^2/s+\lambda_2s$ on $s>0$; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of $F$ with compactness of the box to obtain an optimal $\beta$. The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2 (2021); Mathematical Programming (2022). https://arxiv.org/abs/2004.06152v2
• A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
• O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv:1510.06083, 2015. https://arxiv.org/abs/1510.06083
• A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007. https://doi.org/10.1090/conm/443/08555
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388

Motivation

A single exact linear equation $y = \langle x, s\rangle$ about an unknown unit vector $s \in \mathbb{R}^d$ carries arbitrarily fine information: $d$ independent Gaussian equations determine $s$ almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision $\epsilon$, as a function of its memory.

This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update $z_t = z_{t-1} + \frac{y_t - \langle x_t, z_{t-1}\rangle}{\|x_t\|^2} x_t$ satisfies $\mathbb{E}\|z_t - s\|^2 = (1 - 1/d)^t$ on isotropic Gaussian rows, so order $d\log(1/\epsilon)$ samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly $d^2$ bits can do better than this scale.

Background

• 1937. Kaczmarz introduces the projection method for linear systems; Strohmer and Vershynin (2009) give the randomized version with exponential convergence.
• 2014. Shamir's finite-message framework for online and distributed learning includes bounded-memory online processing as a special case.
• 2015. Steinhardt and Duchi prove memory-dependent minimax rates for sparse linear regression with noise.
• 2016. Steinhardt, Valiant and Wager relate memory, communication and statistical queries and pose a quadratic-memory versus exponential-sample conjecture for parity learning; Raz proves a time–space lower bound for parity learning, and in 2017 extends the method to a large class of learning problems.
• 2019. Sharan, Sidford and Valiant prove that for Gaussian regression with tiny uniform additive noise, a learner with at most $d^2/4$ bits needs $\Omega(d\log r)$ samples to reach Euclidean accuracy $d^{-r}$, in a stated range of $r$, and ask (Section 1.1) whether the first-order sample dependence on precision is optimal under bounded memory. In the same year Dagan, Kur and Shamir prove quadratic-space lower bounds for two different linear-prediction tasks in the streaming model.
• 2026. The OpenAI preprint Memory and precision in noiseless Gaussian regression (dated September 27, 2026) states an $\Omega_A(d\log(1/\epsilon))$ lower bound for exact observations and memory $Ad^2$. It has not been peer reviewed, and the Lean statement of its main theorem is open on this platform.

Setting

Fix integers $d \ge 2$, $M \ge 0$, $T \ge 0$. A signal $s$ lies on the unit sphere $S^{d-1} \subset \mathbb{R}^d$. At step $t \in \{1,\dots,T\}$ the learner receives the pair $(x_t, y_t)$ with $x_t \sim N(0, I_d)$ independent and $y_t = \langle x_t, s\rangle$ exactly (no noise).

A finite-state learner with $M$ bits keeps a state in a set of at most $2^M$ elements. A data-independent shared seed $\omega$ (drawn from a probability space $(\Omega,\rho)$) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon $T$. Its output $\hat s \in S^{d-1}$ is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision $\epsilon$ means angular error $\arccos\langle \hat s, s\rangle \le \epsilon$.

Write $\sigma_d$ for the uniform probability measure on $S^{d-1}$. Uniform success is the probability of success when $S \sim \sigma_d$ is drawn independently of the rows and the seed.

In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space $\Omega$.

Formalization targets

Goal: OAI.NoiselessRegression.main

The goal is the conjunction of two statements.

Fixed quadratic memory (Theorem 1.2): for every $A > 0$ there are $c_A > 0$ and $d_A$ such that, for $d \ge d_A$, $M \le A d^2$, $0 < \epsilon \le 1/10$, and every admissible learner,

$$\Pr_{S\sim\sigma_d}\big\{\arccos\langle \hat s, S\rangle \le \epsilon\big\} \ge \tfrac23 \;\Longrightarrow\; T \ge c_A\, d \log(1/\epsilon).$$

Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute $c > 0$ such that for every memory sequence $M(d) = o(d^2)$ there is $d_0$ with the same conclusion $T \ge c\, d\log(1/\epsilon)$ for $d \ge d_0$, under either uniform success at least $2/3$ or success at least $2/3$ for every fixed signal $s$.

No relation between $\epsilon$ and $M$ is assumed; the constant is absolute in the subquadratic case.

Milestone: supporting estimates (OAI.MemoryPrecision.main)

A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):

$$\Pr\{\arccos\langle \hat s, S\rangle \le \epsilon\} \le \min\Big\{1, \Big[2\epsilon\, e^{C(1+M/d^2)\lceil T/q\rceil}\Big]^{(d-1)/2}\Big\},\qquad q = \lfloor (d-1)/8 \rfloor.$$

Significance

The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with $O(d^2)$ bits, the $d\log(1/\epsilon)$ scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all $0<\epsilon\le 1/10$. Because an exact-observation learner can simulate added noise, the preprint derives from it an $\Omega_A(d r \log d)$ lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy $d^{-r}$, which strengthens their $\Omega(d\log r)$ bound in that range.

Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed $A$ (Corollary 1.4), which the Lean goal states only in the subquadratic case.

Difficulty

Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in $\epsilon$ with no relation between $\epsilon$ and $M$, so a learner with $\Theta(d^2)$ bits must be prevented from storing $\log(1/\epsilon)$ bits per coordinate for very small $\epsilon$.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.
• States are Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index $T$.
• Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.
• Probabilities are ℝ≥0∞-valued; the threshold is $2/3$; angular error is Real.arccos ⟪ŝ, s⟫; $\log$ is natural.
• The seed space $\Omega$ is an arbitrary probability space in universe u, so randomized learners are covered by placing their randomness in the seed.

The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold $2/3$ is achievable (with large $T$), so the implication has content.

A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, $L^q$ densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.

Selected references

• OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403 (full version https://arxiv.org/abs/1904.08544)
• R. Raz, Fast Learning Requires Good Memory: A Time-Space Lower Bound for Parity Learning, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• O. Shamir, Fundamental Limits of Online and Distributed Algorithms for Statistical Learning and Estimation, NeurIPS 2014. https://proceedings.neurips.cc/paper_files/paper/2014/hash/cc427d934a7f6c0663e5923f49eba531-Abstract.html
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• T. Strohmer, R. Vershynin, A Randomized Kaczmarz Algorithm with Exponential Convergence, J. Fourier Anal. Appl. 15 (2009). https://doi.org/10.1007/s00041-008-9030-4

Why robustness and the Lasso belong together

The Lasso (Tibshirani 1996; Chen, Donoho and Saunders 1998) fits a linear model $b \approx Ax$ by penalizing the ℓ¹ norm of the coefficients. It is one of the standard tools of high-dimensional statistics and signal processing, and its usual justification is statistical or geometric: the ℓ¹ penalty is a convex surrogate for sparsity, or the negative log-density of a Laplace prior. Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) give a different justification: an ℓ¹-regularized regression is exactly a robust regression, the problem of fitting the data well in the worst case when every feature of the observation matrix may be corrupted by a bounded disturbance.

This observation is the foundation of the rest of their paper (dual-norm regularizers from coupled disturbances, sparsity from robustness, consistency of the Lasso through a worst-case-expectation reading). It also connects two literatures. On the robust side, El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) computed the worst-case residual when the whole data matrix $[A\ b]$ is disturbed in a Frobenius-norm ball, obtaining $\|Ax-b\|+\sqrt{\|x\|^2+1}$; that result is already on the platform as RobustLS.Unstructured.worst_case_residual_closed_form. On the distributional side, Blanchet, Kang and Murthy (J. Appl. Probab. 56(3), 2019) obtained the square-root Lasso as a Wasserstein distributionally robust problem (RWPI.SqrtLasso.theorem_1). The present mission formalizes the feature-wise result that sits between them.

Setting

Fix integers $n$ (samples) and $m$ (features). The observation matrix $A\in\mathbb R^{n\times m}$ has columns $a_1,\dots,a_m\in\mathbb R^n$, the features. The response is $b\in\mathbb R^n$ and a coefficient vector is $x\in\mathbb R^m$, so that $Ax=\sum_{i=1}^m x_i a_i$. All norms on $\mathbb R^n$ are Euclidean, $\|\cdot\|_2$.

A disturbance of $A$ is a family $\Delta A=(\delta_1,\dots,\delta_m)$ of vectors $\delta_i\in\mathbb R^n$, one per column; the disturbed matrix $A+\Delta A$ has columns $a_i+\delta_i$. Given budgets $c_1,\dots,c_m\ge 0$, the feature-wise uncoupled uncertainty set is

$$\mathcal U=\bigl\{(\delta_1,\dots,\delta_m)\;\big|\;\|\delta_i\|_2\le c_i,\ i=1,\dots,m\bigr\}. \tag{2}$$

Each feature is disturbed independently: no constraint couples the $\delta_i$. The robust objective is the worst-case residual

$$R(x)=\sup_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2,$$

and robust linear regression is problem (1), $\min_{x\in\mathbb R^m} R(x)$. The ℓ¹-regularized regression problem is (3), $\min_{x\in\mathbb R^m} L(x)$ with

$$L(x)=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i| .$$

The loss in $L$ is the norm of the residual, not its square. In the Lean development, $Ax$ is matVec a x, $\mathcal U$ is uncertaintySet c, $R$ is robustObjective a b c, $L$ is l1RegularizedObjective a b c, and the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ of the proof is worstCaseDisturbance c x u.

Formalization targets

Goal: Theorem 1 (p. 4)

For $n\ge1$ and budgets $c_i\ge 0$, problem (1) with uncertainty set (2) is equivalent to problem (3): for every $x\in\mathbb R^m$,

$$x\ \text{minimizes}\ R\iff x\ \text{minimizes}\ L,\qquad\text{and}\qquad \inf_{x} R(x)=\inf_x L(x).$$

No minimizer is asserted to exist; the paper does not claim one.

Milestones (in the order the proof uses them)

1. Eq. (4), the upper bound: for every $\Delta A\in\mathcal U$, $\|b-(A+\Delta A)x\|_2\le\|b-Ax\|_2+\sum_i|x_i|c_i$.
2. Eq. (5), the attained worst case: with $u$ a unit vector equal to $(b-Ax)/\|b-Ax\|_2$ when $Ax\ne b$, the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ lies in $\mathcal U$ and

$$\|b-(A+\Delta A^*)x\|_2=\|b-Ax\|_2+\sum_i c_i|x_i| .$$

3. The per-$x$ identity stated at the start of the proof: for every $x$,

$$\max_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i|,$$

with the maximum attained.

Significance

The result. Theorem 1 turns a min–max problem whose inner maximization is nonconvex into a single convex, second-order-cone-representable problem, and it gives the regularization weights a concrete meaning: $c_i$ is the size of the disturbance feature $i$ is protected against. With equal budgets $c_i=c$ it recovers the Lasso with the unsquared loss, which coincides with the usual Lasso up to a data-dependent change of the regularization coefficient. Every later result of the paper (Theorem 3 for arbitrary norms, the coupled uncertainty sets of Corollary 1, the sparsity theorems of §IV, the kernel-density reading of §V) builds on this identity or its proof pattern.

Formalizing it. The theorem is proved in the paper; the mission formalizes that proof. No machine-checked version of it exists on the platform or, to our knowledge, elsewhere. The definitions here (the uncertainty set, the worst-case objective as a genuine supremum, the explicit worst-case disturbance) are the base on which the companion missions of this series (coupled norms, sparsity, worst-case expectation) restate their own objects.

Difficulty

The upper bound (4) is the triangle inequality. The substance is the lower bound: one must exhibit a single admissible disturbance that makes every column perturbation push the residual in the same direction, and check that it is admissible and that the resulting norm adds up exactly. Two edge cases make the obvious argument fail as written. When $Ax=b$ the direction $(b-Ax)/\|b-Ax\|_2$ is undefined and an arbitrary unit vector must be used instead, which requires $n\ge1$; for $n=0$ the identity reads $0=\sum_i c_i|x_i|$ and is false. When $x_i=0$ the sign must be $0$, not $\pm1$, for the computation in (5) to go through. Passing from the per-$x$ identity to the equivalence of the two minimization problems is then routine, but it must be done without assuming that either problem has a minimizer.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $A$ is the family of its columns a : Fin m → EuclideanSpace ℝ (Fin n), and $Ax=\sum_i x_i\,a_i$. Indices $1,\dots,m$ are Fin m. A disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n), and $(A+\Delta A)x$ is matVec (a + δ) x.
• Readings of "max" and "min". The paper writes "max" over $\mathcal U$. $R(x)$ is defined as the supremum over $\mathcal U$ taken in EReal, so it is $-\infty$ on an empty set and $+\infty$ on an unbounded one and carries no junk value. That the maximum is attained is stated separately, as IsGreatest of the set of residual norms (milestone 3). "min" in (1) and (3) is read as: the same set of minimizers (IsMinOn … Set.univ) and the same infimum, computed in EReal. No existence of minimizers is claimed.
• Added hypothesis. $n\ge1$ (0 < n), which the paper leaves implicit. The budgets $c_i\ge0$ are the paper's own assumption on (2).
• Sign convention. $\mathrm{sgn}$ is Real.sign, with $\mathrm{sgn}(0)=0$.
• Trivializing formalizations ruled out. The robust objective is defined as the supremum over $\mathcal U$, never by its closed form $\|b-Ax\|_2+\sum_i c_i|x_i|$, which would make milestone 3 and the goal hold by definition; and no real sSup with junk value $0$ is used, so the identities cannot hold vacuously.
• Not in scope. The remark that (3) "recovers the well-known Lasso" (it has the unsquared loss), §II-B and Theorem 2 (probabilistic construction of the budgets), and the other sections of the paper, which are separate missions.
• Infrastructure. Only Mathlib's inner-product-space and EReal order theory are needed. The squared-loss Lasso definitions already on the platform (XuMannorRobust.Lasso.*, LassoDantzig.*) are different objects and are not used. Contributions are welcome on each milestone independently; a proof of the per-$x$ identity for an arbitrary norm on $\mathbb R^n$ would also serve Theorem 3 of the paper.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• 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. S. Chen, D. L. Donoho, M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1):33–61, 1998. https://doi.org/10.1137/S1064827596304010
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein profile inference and applications to machine learning, J. Appl. Probab. 56(3):830–857, 2019. https://doi.org/10.1017/jpr.2019.49