Matrix Operator Norm

noncomputable def matrixOpNorm {d T : ℕ} (A : Matrix (Fin d) (Fin T) ℝ) : ℝ

The operator norm of a matrix A : Matrix (Fin d) (Fin T) ℝ, defined as ‖A‖_op = sup_{‖x‖=1} ‖Ax‖, computed via the ContinuousLinearMap norm on the associated linear map between Euclidean spaces.

Sub-Gaussian Matrix (Definition from equation (4.2))

def IsSubGaussianMatrix {Ω : Type u_1} [MeasurableSpace Ω] {d T : ℕ} (F : Ω → Matrix (Fin d) (Fin T) ℝ) (σsq : ℝ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : Prop

A random matrix F : Ω → Matrix (Fin d) (Fin T) ℝ is sub-Gaussian with variance proxy σsq (denoted F ~ subG_{d×T}(σ²)) if for all unit vectors u ∈ S^{d-1} and v ∈ S^{T-1}, the random variable ω ↦ uᵀ F(ω) v is sub-Gaussian with variance proxy σsq.

This captures the notion that all one-dimensional projections of the matrix are sub-Gaussian random variables.

Sub-Gaussian Matrix Model (4.2)

structure SubGaussianMatrixModel (Ω : Type u_1) [MeasurableSpace Ω] (d T : ℕ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : Type u_1

The sub-Gaussian matrix model (4.2): we observe y(ω) = Θ* + F(ω) where Θ* is the unknown d × T parameter matrix and F is a random noise matrix satisfying F ~ subG_{d×T}(σ²).

• Θstar : Matrix (Fin d) (Fin T) ℝ

  The true (unknown) parameter matrix Θ* ∈ ℝ^{d×T}

• F : Ω → Matrix (Fin d) (Fin T) ℝ

  The noise matrix F : Ω → ℝ^{d×T}

• σsq : ℝ

  Variance proxy σ²

• hF : IsSubGaussianMatrix self.F self.σsq μ

  The noise is sub-Gaussian: F ~ subG_{d×T}(σ²)

def SubGaussianMatrixModel.observed {Ω : Type u_1} [MeasurableSpace Ω] {d T : ℕ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (model : SubGaussianMatrixModel Ω d T μ) (ω : Ω) : Matrix (Fin d) (Fin T) ℝ

The observed matrix in the sub-Gaussian matrix model: y(ω) = Θ* + F(ω).

SVD Decomposition

structure SVD (d T : ℕ) : Type

An SVD decomposition of a d × T real matrix, representing A = Σⱼ σⱼ · uⱼ · vⱼᵀ where:

• r is the number of (possibly nonzero) singular value components (at most min(d, T))
• σval are the singular values (nonnegative)
• u are left singular vectors in ℝ^d
• v are right singular vectors in ℝ^T

• r : ℕ

  Number of singular value components

• hr : self.r ≤ min d T

  The number of components is bounded by min(d, T)

• σval : Fin self.r → ℝ

  Singular values (nonnegative)

• u : Fin self.r → Fin d → ℝ

  Left singular vectors

• v : Fin self.r → Fin T → ℝ

  Right singular vectors

• σval_nonneg (j : Fin self.r) : 0 ≤ self.σval j

  Singular values are nonnegative

def SVD.toMatrix {d T : ℕ} (S : SVD d T) : Matrix (Fin d) (Fin T) ℝ

The matrix reconstructed from an SVD decomposition: Σⱼ σⱼ · uⱼ · vⱼᵀ where uⱼ · vⱼᵀ is the rank-1 outer product.

def SVD.IsDecompOf {d T : ℕ} (S : SVD d T) (A : Matrix (Fin d) (Fin T) ℝ) : Prop

An SVD decomposition S is valid for matrix A if A = S.toMatrix.

Definition 4.1: Singular Value Thresholding (SVT) Estimator

noncomputable def SVD.svtMatrix {d T : ℕ} (S : SVD d T) (τ : ℝ) : Matrix (Fin d) (Fin T) ℝ

Given an SVD decomposition and a threshold τ ≥ 0, apply singular value hard thresholding: keep singular value σⱼ if |σⱼ| > 2τ, set it to zero otherwise. The resulting matrix is Σⱼ σⱼ · 𝟙(|σⱼ| > 2τ) · uⱼ vⱼᵀ.

Since singular values are nonneg, |σⱼ| > 2τ simplifies to σⱼ > 2τ, but we use |σⱼ| to match the textbook formula exactly.

def IsSVTEstimator {d T : ℕ} (y Θhat : Matrix (Fin d) (Fin T) ℝ) (τ : ℝ) : Prop

Definition 4.1. IsSVTEstimator y Θhat τ asserts that Θhat is the singular value thresholding (SVT) estimator of the matrix y with threshold 2τ ≥ 0:

Θ̂^SVT = Σⱼ λ̂ⱼ · 𝟙(|λ̂ⱼ| > 2τ) · ûⱼ v̂ⱼᵀ

where y = Σⱼ λ̂ⱼ ûⱼ v̂ⱼᵀ is the SVD of the observed matrix y.

This is defined as the existence of an SVD decomposition of y such that Θhat equals the result of hard-thresholding the singular values at level 2τ.

Basic properties

theorem SVD.svtMatrix_eq_toMatrix_of_pos {d T : ℕ} (S : SVD d T) (hpos : ∀ (j : Fin S.r), 0 < S.σval j) : S.svtMatrix 0 = S.toMatrix

When the threshold τ is zero (and all singular values are positive), the SVT estimator recovers the original matrix.

theorem SVD.svtMatrix_eq_zero_of_large_threshold {d T : ℕ} (S : SVD d T) {τ : ℝ} (hτ : ∀ (j : Fin S.r), S.σval j ≤ 2 * τ) : S.svtMatrix τ = 0

The SVT estimator with a sufficiently large threshold produces the zero matrix.

Aliases for Definition 4.1

noncomputable def singularValueThresholding {d T : ℕ} (S : SVD d T) (τ : ℝ) : Matrix (Fin d) (Fin T) ℝ

Definition 4.1 (Singular Value Thresholding). Given an SVD decomposition S of a matrix and a threshold τ ≥ 0, the SVT estimator applies hard thresholding to the singular values: Ŝ_τ(y) = Σⱼ λ̂ⱼ · 𝟙(|λ̂ⱼ| > 2τ) · ûⱼ v̂ⱼᵀ. This is an alias for SVD.svtMatrix.

def definition_4_1 {d T : ℕ} (y Θhat : Matrix (Fin d) (Fin T) ℝ) (τ : ℝ) : Prop

Definition 4.1 (SVT Estimator). definition_4_1 y Θhat τ asserts that Θhat is the singular value thresholding estimator of the observed matrix y with threshold 2τ. This is an alias for IsSVTEstimator.