Inline Definitions

def Chapter4.Problem41.frobeniusNormSq {m : Type u_1} {p : Type u_2} [Fintype m] [Fintype p] (A : Matrix m p ℝ) : ℝ

Squared Frobenius norm: ‖M‖_F² = Σᵢⱼ Mᵢⱼ².

def Chapter4.Problem41.matrixL0Norm {m : Type u_1} {p : Type u_2} [Fintype m] [Fintype p] [DecidableEq ℝ] (M : Matrix m p ℝ) : ℕ

Number of nonzero entries in a matrix (the ℓ₀ "norm").

def Chapter4.Problem41.IsSubGaussian {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (σsq : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

A random variable X : Ω → ℝ is sub-Gaussian with variance proxy σ² w.r.t. measure μ if its moment generating function satisfies 𝔼[exp(tX)] ≤ exp(t²σ²/2) for all t ∈ ℝ.

def Chapter4.Problem41.IsSubGaussianMatrix {Ω : Type u_1} [MeasurableSpace Ω] {n T : ℕ} (E : Ω → Matrix (Fin n) (Fin T) ℝ) (σsq : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

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

Problem 4.1, Part 1: Rank-based bound

theorem Chapter4.Problem41.problem_4_1_part1 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {n d T : ℕ} (hn : 0 < n) (X : Matrix (Fin n) (Fin d) ℝ) (Θstar : Matrix (Fin d) (Fin T) ℝ) (E Y : Ω → Matrix (Fin n) (Fin T) ℝ) (hY : ∀ (ω : Ω), Y ω = X * Θstar + E ω) (σ : ℝ) (hσ : 0 < σ) (hE : IsSubGaussianMatrix E (σ ^ 2) μ) : ∃ (Θhat : Matrix (Fin n) (Fin T) ℝ → Matrix (Fin d) (Fin T) ℝ) (C : ℝ), 0 < C ∧ μ {ω : Ω | frobeniusNormSq (X * Θhat (Y ω) - X * Θstar) / ↑n ≤ C * σ ^ 2 * ↑X.rank * ↑T / ↑n} ≥ ENNReal.ofReal 0.99

Problem 4.1, Part 1 (Rank bound). Book statement (Rigollet, Problem 4.1.1): "Using the results of Chapter 2, show that there exists an estimator Θ̂ ∈ ℝ^{d×T} such that (1/n) ‖XΘ̂ − XΘ*‖_F² ≲ σ² · rT / n with probability .99, where r denotes the rank of X."

Proof idea: Decompose Y = XΘ* + E column-wise into T independent univariate regression problems Y^(j) = Xθ*^(j) + ε^(j). Apply the Chapter 2 projection estimator to each column (giving MSE ≲ σ²r/n per column), then sum over T columns. The union bound is not needed since each column's bound holds in expectation.

The estimator takes Y as input (not ω), preventing the trivial witness Θ̂ = Θ*.

Problem 4.1, Part 2: Sparsity-based bound

theorem Chapter4.Problem41.problem_4_1_part2 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {n d T : ℕ} (hn : 0 < n) (hd : 0 < d) (X : Matrix (Fin n) (Fin d) ℝ) (Θstar : Matrix (Fin d) (Fin T) ℝ) (E Y : Ω → Matrix (Fin n) (Fin T) ℝ) (hY : ∀ (ω : Ω), Y ω = X * Θstar + E ω) (σ : ℝ) (hσ : 0 < σ) (hE : IsSubGaussianMatrix E (σ ^ 2) μ) : ∃ (Θhat : Matrix (Fin n) (Fin T) ℝ → Matrix (Fin d) (Fin T) ℝ) (C : ℝ), 0 < C ∧ μ {ω : Ω | frobeniusNormSq (X * Θhat (Y ω) - X * Θstar) / ↑n ≤ C * σ ^ 2 * ↑(matrixL0Norm Θstar) * Real.log (Real.exp 1 * ↑d) / ↑n} ≥ ENNReal.ofReal 0.99

Problem 4.1, Part 2 (Sparsity bound). Book statement (Rigollet, Problem 4.1.2): "There exists an estimator Θ̂ ∈ ℝ^{d×T} such that (1/n) ‖XΘ̂ − XΘ*‖_F² ≲ σ² · |Θ*|₀ · log(ed) / n with probability .99."

Proof idea: Decompose column-wise into T independent regression problems. Apply the Chapter 2 LASSO or best-subset estimator to each column j, giving MSE ≲ σ² · |θ*^(j)|₀ · log(ed) / n. Sum over j = 1,…,T to get total MSE ≲ σ² · |Θ*|₀ · log(ed) / n, since Σⱼ |θ*^(j)|₀ = |Θ*|₀.

The estimator takes Y as input (not ω), preventing the trivial witness Θ̂ = Θ*.