Helper definitions: ℓ₀ and ℓ₁ norms

noncomputable def Rigollet.l0norm {d : ℕ} (θ : Fin d → ℝ) : ℕ

The ℓ₀ "norm": number of nonzero entries of a vector θ : Fin d → ℝ. This counts the support size |{j : θ_j ≠ 0}|.

noncomputable def Rigollet.l1norm {d : ℕ} (θ : Fin d → ℝ) : ℝ

The ℓ₁ norm: sum of absolute values of entries of a vector θ : Fin d → ℝ. This is ‖θ‖₁ = Σⱼ |θⱼ|.

Basic properties of ℓ₀ and ℓ₁

theorem Rigollet.l0norm_eq {d : ℕ} (θ : Fin d → ℝ) : l0norm θ = {j : Fin d | θ j ≠ 0}.card

theorem Rigollet.l1norm_eq {d : ℕ} (θ : Fin d → ℝ) : l1norm θ = ∑ j : Fin d, |θ j|

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

theorem Rigollet.l0norm_zero {d : ℕ} : l0norm 0 = 0

theorem Rigollet.l1norm_zero {d : ℕ} : l1norm 0 = 0

Squared L2 norm

noncomputable def Rigollet.sqL2norm {n : ℕ} (v : Fin n → ℝ) : ℝ

Squared ℓ₂ norm of a vector: ∑ᵢ vᵢ². This is used in the BIC and Lasso estimator definitions to avoid the sup-norm issue with Mathlib's ‖·‖.

theorem Rigollet.sqL2norm_nonneg {n : ℕ} (v : Fin n → ℝ) : 0 ≤ sqL2norm v

sqL2norm is nonneg.

Definition 2.12: BIC and Lasso estimators

def Rigollet.IsBICEstimator {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (Y : Fin n → ℝ) (τ : ℝ) (θhat : Fin d → ℝ) : Prop

Definition 2.12 (BIC estimator). Fix τ > 0. The BIC estimator θ̂ᴮᴵᶜ minimizes the ℓ₀-penalized objective: (1/n)‖Y - Xθ‖₂² + τ² ‖θ‖₀ where ‖·‖₂² = ∑ᵢ (·)ᵢ² is the squared Euclidean norm, and ‖θ‖₀ counts the number of nonzero entries of θ.

def Rigollet.IsLassoEstimator {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (Y : Fin n → ℝ) (τ : ℝ) (θhat : Fin d → ℝ) : Prop

Definition 2.12 (Lasso estimator). Fix τ > 0. The Lasso estimator θ̂ᴸ minimizes the ℓ₁-penalized objective: (1/n)‖Y - Xθ‖₂² + 2τ ‖θ‖₁ where ‖·‖₂² = ∑ᵢ (·)ᵢ² is the squared Euclidean norm, and ‖θ‖₁ = Σⱼ |θⱼ| is the ℓ₁ norm.

@[reducible, inline]

abbrev Rigollet.IsBICEstimatorL2 {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (Y : Fin n → ℝ) (τ : ℝ) (θhat : Fin d → ℝ) : Prop

Alias: IsBICEstimatorL2 is the same as IsBICEstimator. Kept for backward compatibility with files that reference the L2 variant.

@[reducible, inline]

abbrev Rigollet.IsLassoEstimatorL2 {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (Y : Fin n → ℝ) (τ : ℝ) (θhat : Fin d → ℝ) : Prop

Alias: IsLassoEstimatorL2 is the same as IsLassoEstimator. Kept for backward compatibility with files that reference the L2 variant.