noncomputable def Chapter3.MSE {n : ℕ} (fhat f : Fin n → ℝ) : ℝ

MSE of a prediction vector f̂ relative to the true signal f: MSE(f̂) = (1/n)|f̂ − f|₂²

noncomputable def Chapter3.support_size {M : ℕ} (θ : Fin M → ℝ) : ℕ

ℓ₀ "norm" (support size) of a vector

noncomputable def Chapter3.l1norm {M : ℕ} (θ : Fin M → ℝ) : ℝ

ℓ₁ norm of a vector

noncomputable def Chapter3.lsObjective {n M : ℕ} (Y : Fin n → ℝ) (Φ : Matrix (Fin n) (Fin M) ℝ) (θ : Fin M → ℝ) : ℝ

The LS objective: (1/n)|Y − Φθ|². Used by both the unconstrained LS and constrained LS estimators.

noncomputable def Chapter3.bicObjective {n M : ℕ} (Y : Fin n → ℝ) (Φ : Matrix (Fin n) (Fin M) ℝ) (τ : ℝ) (θ : Fin M → ℝ) : ℝ

The BIC objective: (1/n)|Y − Φθ|² + τ²|θ|₀

noncomputable def Chapter3.lassoObjective {n M : ℕ} (Y : Fin n → ℝ) (Φ : Matrix (Fin n) (Fin M) ℝ) (τ : ℝ) (θ : Fin M → ℝ) : ℝ

The Lasso objective: (1/n)|Y − Φθ|² + 2τ|θ|₁

theorem Chapter3.MSE_nonneg {n : ℕ} (fhat f : Fin n → ℝ) : 0 ≤ MSE fhat f

MSE is always nonneg: product of (1/n ≥ 0) and (sum of squares ≥ 0).

theorem Chapter3.lsObjective_nonneg {n M : ℕ} (Y : Fin n → ℝ) (Φ : Matrix (Fin n) (Fin M) ℝ) (θ : Fin M → ℝ) : 0 ≤ lsObjective Y Φ θ

The LS objective is always nonneg.

theorem Chapter3.l1norm_nonneg {M : ℕ} (θ : Fin M → ℝ) : 0 ≤ l1norm θ

The ℓ₁ norm is always nonneg.