Skip to content

Least squares, ridge and lasso regression

DefinitionResidual sum of squares#✓fully proved

For a real design matrix \(X\) with \(m\) rows and columns indexed by a finite type \(\iota\), responses \(y \in \mathbb{R}^m\) and \(\theta \in \mathbb{R}^\iota\), the residual sum of squares is \(S(\theta) = (y - X\theta) \cdot (y - X\theta) = \sum_{k=1}^{m} (y_k - (X\theta)_k)^2\).

noncomputable def rss (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (θ : ι → ℝ) : ℝ :=
  (y - X *ᵥ θ) ⬝ᵥ (y - X *ᵥ θ)
Used by 13
Used byConvexity of the lasso objective · Convexity of the residual sum of squares · The Gaussian likelihood decreases with the residual sum of squares · Least squares is maximum likelihood · Lasso objective · Lasso is MAP estimation · Lasso with an orthonormal design · Ridge objective · Expansion of the ridge objective around a solution of its normal equations · Ridge regression is MAP estimation · Expansion of the residual sum of squares · Pythagoras for least squares · Least squares and the normal equations

TheoremExpansion of the residual sum of squares#✓fully proved

Let \(X\) be a real design matrix with \(m\) rows and columns indexed by a finite type \(\iota\), let \(y \in \mathbb{R}^m\), and write \(S(\theta) = (y - X\theta) \cdot (y - X\theta)\) for the residual sum of squares. Then for all \(\theta, v \in \mathbb{R}^\iota\),

\[S(\theta + v) = S(\theta) - 2\, v \cdot \bigl(X^\top (y - X\theta)\bigr) + (Xv) \cdot (Xv).\]
theorem rss_add (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (θ v : ι → ℝ) :
    rss X y (θ + v) =
      rss X y θ - 2 * (v ⬝ᵥ (Xᵀ *ᵥ (y - X *ᵥ θ))) + (X *ᵥ v) ⬝ᵥ (X *ᵥ v)
Uses 1 · Used by 3
Statement usesResidual sum of squares
Used byExpansion of the ridge objective around a solution of its normal equations · Pythagoras for least squares · Least squares and the normal equations

TheoremPythagoras for least squares#✓fully proved

Let \(X\) be a real design matrix with \(m\) rows and columns indexed by a finite type \(\iota\), let \(y \in \mathbb{R}^m\), write \(S\) for the residual sum of squares, and let \(\theta_0 \in \mathbb{R}^\iota\) solve the normal equations \(X^\top X \theta_0 = X^\top y\). Then for every \(\theta \in \mathbb{R}^\iota\),

\[S(\theta) = S(\theta_0) + (X(\theta - \theta_0)) \cdot (X(\theta - \theta_0)).\]
theorem rss_eq_of_normal {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {θ₀ : ι → ℝ}
    (h : Xᵀ *ᵥ (X *ᵥ θ₀) = Xᵀ *ᵥ y) (θ : ι → ℝ) :
    rss X y θ = rss X y θ₀ + (X *ᵥ (θ - θ₀)) ⬝ᵥ (X *ᵥ (θ - θ₀))
Uses 2 · Used by 2
Statement usesResidual sum of squares
Proof usesExpansion of the residual sum of squares
Used byLasso with an orthonormal design · Least squares and the normal equations

TheoremLeast squares and the normal equations#✓fully proved

Let \(X\) be a real design matrix with \(m\) rows and columns indexed by a finite type \(\iota\), let \(y \in \mathbb{R}^m\), and write \(S\) for the residual sum of squares. A vector \(\theta_0 \in \mathbb{R}^\iota\) satisfies \(S(\theta_0) \le S(\theta)\) for every \(\theta \in \mathbb{R}^\iota\) if and only if \(X^\top X \theta_0 = X^\top y\).

theorem rss_le_iff_normal (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (θ₀ : ι → ℝ) :
    (∀ θ, rss X y θ₀ ≤ rss X y θ) ↔ Xᵀ *ᵥ (X *ᵥ θ₀) = Xᵀ *ᵥ y
Uses 3 · Used by 1
Statement usesResidual sum of squares
Proof usesExpansion of the residual sum of squares · Pythagoras for least squares
Used byLeast squares is maximum likelihood

TheoremLeast-squares estimates exist#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), and let \(y \in \mathbb{R}^m\). Then there is \(\theta \in \mathbb{R}^\iota\) with \(X^\top X \theta = X^\top y\): the normal equations always have a solution, whatever the rank of \(X\).

The reason is that the range of \(X^\top X\) is contained in that of \(X^\top\) and the two matrices have the same rank, so their ranges coincide.

theorem exists_normal (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) :
    ∃ θ, Xᵀ *ᵥ (X *ᵥ θ) = Xᵀ *ᵥ y
Used by 1
Used byExistence of the Gaussian maximum likelihood estimate

TheoremClosed-form solution of the normal equations#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\) such that \(X^\top X\) is invertible, and let \(y \in \mathbb{R}^m\). Then \(\hat\theta = (X^\top X)^{-1} X^\top y\) solves the normal equations \(X^\top X \hat\theta = X^\top y\).

theorem normal_inv {X : Matrix (Fin m) ι ℝ} (hX : IsUnit (Xᵀ * X).det) (y : Fin m → ℝ) :
    Xᵀ *ᵥ (X *ᵥ (((Xᵀ * X)⁻¹ * Xᵀ) *ᵥ y)) = Xᵀ *ᵥ y

TheoremConvexity of the residual sum of squares#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), and let \(y \in \mathbb{R}^m\). Then the residual sum of squares \(\theta \mapsto \sum_k (y_k - (X\theta)_k)^2\) is a convex function on all of \(\mathbb{R}^\iota\).

theorem convexOn_rss (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) :
    ConvexOn ℝ Set.univ (rss X y)
Uses 1 · Used by 1
Statement usesResidual sum of squares
Used byConvexity of the lasso objective
29 fully proved

Gaussian noise: least squares is maximum likelihood

DefinitionGaussian likelihood of linear regression#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and let \(v \ge 0\). The Gaussian likelihood with noise variance \(v\) is the function of \(\theta \in \mathbb{R}^\iota\) given by

\[ L(\theta) = \prod_{k=1}^{m} \frac{1}{\sqrt{2 \pi v}} \exp\left(-\frac{(y_k - (X\theta)_k)^2}{2 v}\right). \]

This is the likelihood of \(y\) when \(y_k = (X\theta)_k + \varepsilon_k\) with independent \(\varepsilon_k \sim N(0, v)\).

For \(v = 0\) each factor is the zero function (with the convention \(1/0 = 0\)), not a Dirac kernel; the results about this likelihood assume \(v \neq 0\).

noncomputable def gaussLikelihood (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (v : ℝ≥0)
    (θ : ι → ℝ) : ℝ :=
  ∏ k, gaussianPDFReal ((X *ᵥ θ) k) v (y k)
Used by 7
Used byExistence of the Gaussian maximum likelihood estimate · The Gaussian likelihood decreases with the residual sum of squares · Least squares is maximum likelihood · Lasso posterior kernel · Lasso is MAP estimation · Posterior kernel of ridge regression · Ridge regression is MAP estimation

TheoremThe Gaussian likelihood decreases with the residual sum of squares#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(v > 0\), let \(L\) be the Gaussian likelihood of linear regression with noise variance \(v\), and let \(\mathrm{RSS}(\theta) = \sum_k (y_k - (X\theta)_k)^2\) be the residual sum of squares. Then for all \(\theta, \theta' \in \mathbb{R}^\iota\), \(L(\theta) \le L(\theta')\) if and only if \(\mathrm{RSS}(\theta') \le \mathrm{RSS}(\theta)\).

theorem gaussLikelihood_le_iff {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {v : ℝ≥0} (hv : v ≠ 0)
    (θ θ' : ι → ℝ) :
    gaussLikelihood X y v θ ≤ gaussLikelihood X y v θ' ↔ rss X y θ' ≤ rss X y θ
Uses 2 · Used by 1
Statement usesGaussian likelihood of linear regression · Residual sum of squares
Used byLeast squares is maximum likelihood

TheoremLeast squares is maximum likelihood#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(v > 0\), and let \(L\) be the Gaussian likelihood of linear regression with noise variance \(v\). Then \(\theta_0 \in \mathbb{R}^\iota\) maximizes \(L\) over \(\mathbb{R}^\iota\) if and only if it solves the normal equations \(X^\top X \theta_0 = X^\top y\).

theorem isMaxOn_gaussLikelihood_iff {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {v : ℝ≥0}
    (hv : v ≠ 0) (θ₀ : ι → ℝ) :
    IsMaxOn (gaussLikelihood X y v) Set.univ θ₀ ↔ Xᵀ *ᵥ (X *ᵥ θ₀) = Xᵀ *ᵥ y
Uses 4 · Used by 1
Statement usesGaussian likelihood of linear regression
Proof usesThe Gaussian likelihood decreases with the residual sum of squares · Residual sum of squares · Least squares and the normal equations
Used byExistence of the Gaussian maximum likelihood estimate

TheoremExistence of the Gaussian maximum likelihood estimate#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(v > 0\), and let \(L\) be the Gaussian likelihood of linear regression with noise variance \(v\). Then \(L\) attains its maximum on \(\mathbb{R}^\iota\): there is \(\theta_0 \in \mathbb{R}^\iota\) with \(L(\theta) \le L(\theta_0)\) for every \(\theta \in \mathbb{R}^\iota\).

theorem exists_isMaxOn_gaussLikelihood (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {v : ℝ≥0}
    (hv : v ≠ 0) : ∃ θ₀, IsMaxOn (gaussLikelihood X y v) Set.univ θ₀
Uses 3
Statement usesGaussian likelihood of linear regression
Proof usesLeast-squares estimates exist · Least squares is maximum likelihood

Ridge regression: MAP under a Gaussian prior

DefinitionRidge objective#✓fully proved

For a real design matrix \(X\) with \(m\) rows and columns indexed by a finite type \(\iota\), responses \(y \in \mathbb{R}^m\), a real number \(\lambda\) and \(\theta \in \mathbb{R}^\iota\), let \(S(\theta) = \sum_{k=1}^{m} (y_k - (X\theta)_k)^2\) be the residual sum of squares. The ridge objective is \(S(\theta) + \lambda \sum_{i} \theta_i^2\).

noncomputable def ridge (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (lam : ℝ) (θ : ι → ℝ) : ℝ :=
  rss X y θ + lam * (θ ⬝ᵥ θ)
Uses 1 · Used by 5
Statement usesResidual sum of squares
Used byThe ridge estimate maximizes the ridge posterior · Expansion of the ridge objective around a solution of its normal equations · Solutions of the ridge normal equations minimize the ridge objective · Closed form of ridge regression · Ridge regression is MAP estimation

TheoremExpansion of the ridge objective around a solution of its normal equations#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(\lambda \in \mathbb{R}\), and write \(\|\cdot\|\) for the Euclidean norm and \(R(\theta) = \|y - X\theta\|^2 + \lambda \|\theta\|^2\) for the ridge objective. If \(\theta_0 \in \mathbb{R}^\iota\) satisfies \((X^\top X + \lambda I)\theta_0 = X^\top y\), then for every \(\theta \in \mathbb{R}^\iota\), \(R(\theta) = R(\theta_0) + \|X(\theta - \theta_0)\|^2 + \lambda \|\theta - \theta_0\|^2\).

theorem ridge_eq_of_normal {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {lam : ℝ} {θ₀ : ι → ℝ}
    (h : (Xᵀ * X + lam • 1) *ᵥ θ₀ = Xᵀ *ᵥ y) (θ : ι → ℝ) :
    ridge X y lam θ = ridge X y lam θ₀ + (X *ᵥ (θ - θ₀)) ⬝ᵥ (X *ᵥ (θ - θ₀)) +
      lam * ((θ - θ₀) ⬝ᵥ (θ - θ₀))
Uses 3 · Used by 1
Statement usesRidge objective
Proof usesResidual sum of squares · Expansion of the residual sum of squares
Used bySolutions of the ridge normal equations minimize the ridge objective

TheoremSolutions of the ridge normal equations minimize the ridge objective#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(\lambda \ge 0\), and write \(\|\cdot\|\) for the Euclidean norm. If \(\theta_0 \in \mathbb{R}^\iota\) satisfies \((X^\top X + \lambda I)\theta_0 = X^\top y\), then for every \(\theta \in \mathbb{R}^\iota\), \(\|y - X\theta_0\|^2 + \lambda \|\theta_0\|^2 \le \|y - X\theta\|^2 + \lambda \|\theta\|^2\).

theorem ridge_le_of_normal {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {lam : ℝ} (hlam : 0 ≤ lam)
    {θ₀ : ι → ℝ} (h : (Xᵀ * X + lam • 1) *ᵥ θ₀ = Xᵀ *ᵥ y) (θ : ι → ℝ) :
    ridge X y lam θ₀ ≤ ridge X y lam θ
Uses 2 · Used by 1
Statement usesRidge objective
Proof usesExpansion of the ridge objective around a solution of its normal equations
Used byClosed form of ridge regression

TheoremThe ridge matrix is positive definite#✓fully proved

For every real matrix \(X\) with \(m\) rows and columns indexed by a finite set \(\iota\) and every real \(\lambda > 0\), the matrix \(X^\top X + \lambda I\) is positive definite.

theorem posDef_ridge [Finite ι] (X : Matrix (Fin m) ι ℝ) {lam : ℝ} (hlam : 0 < lam) :
    (Xᵀ * X + lam • (1 : Matrix ι ι ℝ)).PosDef
Used by 2
Used byPush-through identity for ridge regression · Closed form of ridge regression

DefinitionRidge estimate#✓fully proved

For a real matrix \(X\) with \(m\) rows and columns indexed by a finite set \(\iota\), responses \(y \in \mathbb{R}^m\) and a real number \(\lambda\), the ridge estimate is \((X^\top X + \lambda I)^{-1} X^\top y \in \mathbb{R}^\iota\).

The inverse of a singular matrix is taken to be \(0\); for \(\lambda > 0\) the matrix \(X^\top X + \lambda I\) is always invertible.

noncomputable def ridgeEstimate (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (lam : ℝ) : ι → ℝ :=
  (Xᵀ * X + lam • 1)⁻¹ *ᵥ (Xᵀ *ᵥ y)
Used by 6
Used byGP posterior mean = RR-BLUP · Kernel ridge regression = GBLUP = RR-BLUP · RR-BLUP = GBLUP · Ridge marker effects are back-solved from GBLUP · The ridge estimate maximizes the ridge posterior · Closed form of ridge regression

TheoremClosed form of ridge regression#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and \(\lambda > 0\), and write \(\|\cdot\|\) for the Euclidean norm. The ridge estimate \(\hat\theta = (X^\top X + \lambda I)^{-1} X^\top y\) minimizes the ridge objective: for every \(\theta \in \mathbb{R}^\iota\), \(\|y - X\hat\theta\|^2 + \lambda \|\hat\theta\|^2 \le \|y - X\theta\|^2 + \lambda \|\theta\|^2\).

theorem ridge_le_ridgeEstimate (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {lam : ℝ}
    (hlam : 0 < lam) (θ : ι → ℝ) : ridge X y lam (ridgeEstimate X y lam) ≤ ridge X y lam θ
Uses 4 · Used by 1
Statement usesRidge objective · Ridge estimate
Proof usesThe ridge matrix is positive definite · Solutions of the ridge normal equations minimize the ridge objective
Used byThe ridge estimate maximizes the ridge posterior

TheoremDensity of independent centred Gaussian coordinates#✓fully proved

For a finite set \(\iota\), a variance \(\tau \ge 0\) and \(\theta \in \mathbb{R}^\iota\), the product over \(i \in \iota\) of the densities of the normal distribution \(N(0, \tau)\) at \(\theta_i\) equals \(\left(\frac{1}{\sqrt{2\pi\tau}}\right)^{|\iota|} \exp\left(-\frac{1}{2\tau} \sum_{i \in \iota} \theta_i^2\right)\).

This also holds at \(\tau = 0\), where the normal density is the zero function, with the convention \(1/0 = 0\).

theorem prod_gaussianPDFReal_zero (τ : ℝ≥0) (θ : ι → ℝ) :
    ∏ i, gaussianPDFReal 0 τ (θ i) =
      (√(2 * π * τ))⁻¹ ^ Fintype.card ι * exp (-(θ ⬝ᵥ θ) / (2 * τ))
Used by 1
Used byRidge regression is MAP estimation

DefinitionPosterior kernel of ridge regression#✓fully proved

For \(s \ge 0\) let \(\varphi_s\) be the density of \(N(0, s)\), \(\varphi_s(x) = (2 \pi s)^{-1/2} e^{-x^2 / (2 s)}\), with \(\varphi_0\) the zero function. For a real design matrix \(X\) with \(m\) rows and columns indexed by a finite type \(\iota\), responses \(y \in \mathbb{R}^m\), variances \(v, \tau \ge 0\) and \(\theta \in \mathbb{R}^\iota\), the posterior kernel is the Gaussian likelihood of \(y\) times the prior density of \(\theta\):

\[p(\theta) = \prod_{k=1}^{m} \varphi_v(y_k - (X\theta)_k) \prod_{i} \varphi_\tau(\theta_i).\]

This is the posterior kernel of linear regression with Gaussian noise of variance \(v\) and independent \(N(0, \tau)\) priors on the coordinates of \(\theta\); it is meaningful for \(v, \tau > 0\).

noncomputable def ridgePosterior (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (v τ : ℝ≥0)
    (θ : ι → ℝ) : ℝ :=
  gaussLikelihood X y v θ * ∏ i, gaussianPDFReal 0 τ (θ i)
Uses 1 · Used by 2
Statement usesGaussian likelihood of linear regression
Used byThe ridge estimate maximizes the ridge posterior · Ridge regression is MAP estimation

TheoremRidge regression is MAP estimation#✓fully proved

Let \(X\) be a real design matrix with \(m\) rows and columns indexed by a finite type \(\iota\), let \(y \in \mathbb{R}^m\), and let \(v\) and \(\tau\) be positive reals. Let \(p\) be the posterior kernel of linear regression with Gaussian noise of variance \(v\) and independent \(N(0, \tau)\) priors on the coordinates of the parameter, and let \(R\) be the ridge objective with \(\lambda = v / \tau\). Then for all \(\theta, \theta' \in \mathbb{R}^\iota\) we have \(p(\theta) \le p(\theta')\) if and only if \(R(\theta') \le R(\theta)\).

So the posterior kernel is a decreasing function of the ridge objective.

theorem ridgePosterior_le_iff {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {v τ : ℝ≥0} (hv : v ≠ 0)
    (hτ : τ ≠ 0) (θ θ' : ι → ℝ) :
    ridgePosterior X y v τ θ ≤ ridgePosterior X y v τ θ' ↔
      ridge X y (v / τ) θ' ≤ ridge X y (v / τ) θ
Uses 5 · Used by 1
Statement usesRidge objective · Posterior kernel of ridge regression
Proof usesGaussian likelihood of linear regression · Density of independent centred Gaussian coordinates · Residual sum of squares
Used byThe ridge estimate maximizes the ridge posterior

TheoremThe ridge estimate maximizes the ridge posterior#✓fully proved

Let \(X\) be a real design matrix with \(m\) rows and columns indexed by a finite type \(\iota\), let \(y \in \mathbb{R}^m\), and let \(v\) and \(\tau\) be positive reals. Let \(p\) be the posterior kernel of linear regression with Gaussian noise of variance \(v\) and independent \(N(0, \tau)\) priors on the coordinates of the parameter, and let \(\hat\theta = (X^\top X + \lambda I)^{-1} X^\top y\) be the ridge estimate with \(\lambda = v / \tau\). Then \(\hat\theta\) maximizes \(p\): for every \(\theta \in \mathbb{R}^\iota\) we have \(p(\theta) \le p(\hat\theta)\).

theorem isMaxOn_ridgePosterior (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {v τ : ℝ≥0}
    (hv : v ≠ 0) (hτ : τ ≠ 0) :
    IsMaxOn (ridgePosterior X y v τ) Set.univ (ridgeEstimate X y (v / τ))
Uses 5
Statement usesRidge estimate · Posterior kernel of ridge regression
Proof usesRidge objective · Ridge regression is MAP estimation · Closed form of ridge regression

Lasso: MAP under a Laplace prior

DefinitionLasso objective#✓fully proved

For a real matrix \(X\) with \(m\) rows and columns indexed by a finite set \(\iota\), responses \(y \in \mathbb{R}^m\) and a real number \(\lambda\), the lasso objective at \(\theta \in \mathbb{R}^\iota\) is \(\sum_{k=1}^m (y_k - (X\theta)_k)^2 + \lambda \sum_{i \in \iota} |\theta_i|\), the residual sum of squares plus \(\lambda\) times the \(\ell^1\) norm of \(\theta\).

noncomputable def lasso (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (lam : ℝ) (θ : ι → ℝ) : ℝ :=
  rss X y θ + lam * ∑ i, |θ i|
Uses 1 · Used by 3
Statement usesResidual sum of squares
Used byConvexity of the lasso objective · Lasso is MAP estimation · Lasso with an orthonormal design

DefinitionLaplace density#✓fully proved

For a scale \(b \ge 0\), the density of the Laplace distribution with location \(0\) and scale \(b\) is the function on \(\mathbb{R}\)

\[ f_b(x) = \frac{1}{2b} \exp\left(-\frac{|x|}{b}\right). \]

For \(b = 0\) this is read with the convention \(1/0 = 0\) and gives the zero function; the results about this density assume \(b \neq 0\).

noncomputable def laplacePDF (b : NNReal) (x : ℝ) : ℝ :=
  exp (-|x| / b) / (2 * b)
Used by 2
Used byLasso posterior kernel · Lasso is MAP estimation

DefinitionLasso posterior kernel#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\), and let \(v \ge 0\) and \(b \ge 0\). The lasso posterior kernel at \(\theta \in \mathbb{R}^\iota\) is

\[\prod_{k=1}^{m} \varphi_v\bigl(y_k - (X\theta)_k\bigr) \cdot \prod_{i \in \iota} p_b(\theta_i),\]

where \(\varphi_v(x) = e^{-x^2/(2v)} / \sqrt{2\pi v}\) is the density of the normal distribution with mean \(0\) and variance \(v\) and \(p_b(x) = e^{-|x|/b} / (2b)\) is the density of the Laplace distribution with location \(0\) and scale \(b\): the Gaussian likelihood of \(y\) with noise variance \(v\) times the Laplace prior density of \(\theta\).

It is a meaningful kernel for \(v \ne 0\) and \(b \ne 0\); for \(v = 0\) (respectively \(b = 0\)) the normal (respectively Laplace) density is the zero function.

noncomputable def lassoPosterior (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) (v b : NNReal)
    (θ : ι → ℝ) : ℝ :=
  gaussLikelihood X y v θ * ∏ i, laplacePDF b (θ i)
Uses 2 · Used by 1
Statement usesGaussian likelihood of linear regression · Laplace density
Used byLasso is MAP estimation

TheoremLasso is MAP estimation#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\), and let \(v > 0\) and \(b > 0\). Let \(P\) be the posterior kernel of linear regression with Gaussian noise of variance \(v\) and the Laplace prior with scale \(b\) on each coordinate, and let \(\ell\) be the lasso objective with \(\lambda = 2v/b\), \(\ell(\theta) = \sum_k (y_k - (X\theta)_k)^2 + \lambda \sum_{i \in \iota} |\theta_i|\). Then for all \(\theta, \theta' \in \mathbb{R}^\iota\), \(P(\theta) \le P(\theta')\) if and only if \(\ell(\theta') \le \ell(\theta)\).

theorem lassoPosterior_le_iff {X : Matrix (Fin m) ι ℝ} {y : Fin m → ℝ} {v : NNReal} (hv : v ≠ 0)
    {b : NNReal} (hb : b ≠ 0) (θ θ' : ι → ℝ) :
    lassoPosterior X y v b θ ≤ lassoPosterior X y v b θ' ↔
      lasso X y (2 * v / b) θ' ≤ lasso X y (2 * v / b) θ
Uses 5
Statement usesLasso objective · Lasso posterior kernel
Proof usesGaussian likelihood of linear regression · Laplace density · Residual sum of squares

TheoremConvexity of the lasso objective#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\), let \(y \in \mathbb{R}^m\) and let \(\lambda \ge 0\). Then the lasso objective \(\theta \mapsto \sum_k (y_k - (X\theta)_k)^2 + \lambda \sum_{i \in \iota} |\theta_i|\) is a convex function on all of \(\mathbb{R}^\iota\).

theorem convexOn_lasso (X : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {lam : ℝ} (hlam : 0 ≤ lam) :
    ConvexOn ℝ Set.univ (lasso X y lam)
Uses 3
Statement usesLasso objective
Proof usesConvexity of the residual sum of squares · Residual sum of squares

DefinitionSoft thresholding#✓fully proved

For real numbers \(t\) and \(z\), the soft thresholding of \(z\) at \(t\) is \(S_t(z) = z - t\) if \(z > t\); otherwise \(S_t(z) = z + t\) if \(z < -t\); and \(S_t(z) = 0\) in the remaining case.

For \(t \ge 0\) this shrinks \(z\) towards \(0\) by \(t\) and sets it to \(0\) when \(|z| \le t\).

noncomputable def softThreshold (t z : ℝ) : ℝ :=
  if t < z then z - t else if z < -t then z + t else 0
Used by 2
Used byLasso with an orthonormal design · Soft thresholding solves the one-dimensional lasso

TheoremSoft thresholding solves the one-dimensional lasso#✓fully proved

Let \(t \ge 0\) and \(z \in \mathbb{R}\), and let \(S_t(z)\) be the soft thresholding of \(z\) at \(t\). Then for every \(s \in \mathbb{R}\),

\[(z - S_t(z))^2 + 2t\,|S_t(z)| \le (z - s)^2 + 2t\,|s|,\]

so \(S_t(z)\) minimizes \((z - s)^2 + 2t\,|s|\) over \(s \in \mathbb{R}\).

theorem softThreshold_le {t : ℝ} (ht : 0 ≤ t) (z s : ℝ) :
    (z - softThreshold t z) ^ 2 + 2 * t * |softThreshold t z| ≤ (z - s) ^ 2 + 2 * t * |s|
Uses 1 · Used by 1
Statement usesSoft thresholding
Used byLasso with an orthonormal design

TheoremLasso with an orthonormal design#✓fully proved

Let \(X\) be a real matrix with \(m\) rows and columns indexed by a finite set \(\iota\) such that \(X^\top X = I\), let \(y \in \mathbb{R}^m\) and let \(\lambda \ge 0\). Let \(\hat\theta \in \mathbb{R}^\iota\) be given by \(\hat\theta_i = S_{\lambda/2}((X^\top y)_i)\), where \(S_t\) is soft thresholding at \(t\). Then \(\hat\theta\) minimizes the lasso objective: for every \(\theta \in \mathbb{R}^\iota\), \(\sum_{k=1}^m (y_k - (X\hat\theta)_k)^2 + \lambda \sum_{i \in \iota} |\hat\theta_i| \le \sum_{k=1}^m (y_k - (X\theta)_k)^2 + \lambda \sum_{i \in \iota} |\theta_i|\).

theorem lasso_softThreshold_le {X : Matrix (Fin m) ι ℝ} (hX : Xᵀ * X = 1) (y : Fin m → ℝ)
    {lam : ℝ} (hlam : 0 ≤ lam) (θ : ι → ℝ) :
    lasso X y lam (fun i => softThreshold (lam / 2) ((Xᵀ *ᵥ y) i)) ≤ lasso X y lam θ
Uses 5
Statement usesLasso objective · Soft thresholding
Proof usesResidual sum of squares · Pythagoras for least squares · Soft thresholding solves the one-dimensional lasso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.