Local copies of Thm_4_10 definitions

We repeat the Thm_4_10 definitions here so we can state bridge lemmas without importing Thm_4_10.lean. These are connected to the Thm_4_10 versions by definitional equality (they have exactly the same body).

noncomputable def Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) : ℝ

The operator norm (spectral norm) of a matrix, defined as the supremum of ‖A v‖₂ over L2 unit vectors. Same definition as Thm_4_6.matrixOpNorm.

Bridging IsSubGaussianVector ↔ IsSubGaussianVec

The definition IsSubGaussianVector (from Thm_4_10) has the same body as IsSubGaussianVec (from Thm_4_6). Since we can't import Thm_4_10 here, we note that any proof about IsSubGaussianVec applies directly to IsSubGaussianVector by definitional equality.

Bridging empiricalCov ↔ empiricalCovariance

Same situation: identical bodies. Any proof about empiricalCovariance applies directly to empiricalCov by definitional equality.

Bridging matOpNorm ↔ matrixOpNorm

The bridge's matOpNorm uses the same iSup-over-unit-vectors definition as Thm_4_6.matrixOpNorm, so they are definitionally equal.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm_eq_matrixOpNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) : matOpNorm A = Thm_4_6.matrixOpNorm A

The bridge's matOpNorm is definitionally equal to Thm_4_6.matrixOpNorm.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm_le_matrixOpNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) : matOpNorm A ≤ Thm_4_6.matrixOpNorm A

matOpNorm A ≤ matrixOpNorm A.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matrixOpNorm_le_matOpNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) : Thm_4_6.matrixOpNorm A ≤ matOpNorm A

matrixOpNorm A ≤ matOpNorm A.

Submatrix restriction

Given X : Fin n → Ω → Fin d → ℝ and a subset S ⊆ Fin d with |S| = m, we construct the restricted samples X_S : Fin n → Ω → Fin m → ℝ and show that covariance and sub-Gaussianity transfer to the subproblem.

def Rigollet.Chapter4.Thm_4_10_Bridges.finsetEquivFin {d : ℕ} (S : Finset (Fin d)) : Fin S.card ≃ ↥S

Given a Finset S of Fin d of size m, construct an order-preserving equivalence Fin m ≃ S, allowing us to index into S by Fin m.

def Rigollet.Chapter4.Thm_4_10_Bridges.restrictVec {d m : ℕ} {Ω : Type u_1} (S : Finset (Fin d)) (hcard : S.card = m) (X : Ω → Fin d → ℝ) : Ω → Fin m → ℝ

Restrict a vector X : Ω → Fin d → ℝ to a subset S ⊆ Fin d of size m, producing X_S : Ω → Fin m → ℝ. We use the canonical ordering of S.

def Rigollet.Chapter4.Thm_4_10_Bridges.restrictSamples {d m : ℕ} {Ω : Type u_1} {n : ℕ} (S : Finset (Fin d)) (hcard : S.card = m) (X : Fin n → Ω → Fin d → ℝ) : Fin n → Ω → Fin m → ℝ

Restrict samples X : Fin n → Ω → Fin d → ℝ to a subset S of size m, producing X_S : Fin n → Ω → Fin m → ℝ.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.subGaussian_restrict {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {m n : ℕ} (X : Fin n → Ω → Fin d → ℝ) (S : Finset (Fin d)) (hcard : S.card = m) (σsq : ℝ) (hSubG : ∀ (i : Fin n), Thm_4_6.IsSubGaussianVec μ (X i) σsq) (i : Fin n) : Thm_4_6.IsSubGaussianVec μ (restrictSamples S hcard X i) σsq

The sub-Gaussianity of the full vector implies sub-Gaussianity of the restricted vector (with the same variance proxy). This follows because for any unit vector u on Fin m, we can extend it to a unit vector u' on Fin d by padding with zeros, and the sub-Gaussian bound for the full vector applies since the dot products agree.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.covariance_restrict {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {m n : ℕ} (X : Fin n → Ω → Fin d → ℝ) (covMat : Matrix (Fin d) (Fin d) ℝ) (S : Finset (Fin d)) (hcard : S.card = m) (hcov : ∀ (i : Fin n) (j k : Fin d), ∫ (ω : Ω), X i ω j * X i ω k ∂μ = covMat j k) (i : Fin n) (j k : Fin m) : ∫ (ω : Ω), restrictSamples S hcard X i ω j * restrictSamples S hcard X i ω k ∂μ = covMat ↑((finsetEquivFin S) (Fin.cast ⋯ j)) ↑((finsetEquivFin S) (Fin.cast ⋯ k))

The covariance structure is preserved under restriction: if E[X_i(j) X_i(k)] = covMat j k, then the covariance of the restricted vectors equals the principal submatrix of covMat.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm_le_of_bound {k : ℕ} (A : Matrix (Fin k) (Fin k) ℝ) (M : ℝ) (hM : 0 ≤ M) (h : ∀ (v : EuclideanSpace ℝ (Fin k)), ‖v‖ = 1 → ‖(EuclideanSpace.equiv (Fin k) ℝ).symm (A.mulVec v.ofLp)‖ ≤ M) : matOpNorm A ≤ M

Helper: the iSup-based operator norm is bounded above by any M ≥ 0 if ‖A.mulVec v‖_L2 ≤ M for all L2-unit v.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm_bddAbove {k : ℕ} (A : Matrix (Fin k) (Fin k) ℝ) : BddAbove (Set.range fun (v : EuclideanSpace ℝ (Fin k)) => ⨆ (_ : ‖v‖ = 1), ‖(EuclideanSpace.equiv (Fin k) ℝ).symm (A.mulVec v.ofLp)‖)

Helper: the iSup-based operator norm is bounded above.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.matOpNorm_submatrix_le {d m : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (S : Finset (Fin d)) (hcard : S.card = m) : matOpNorm (A.submatrix (fun (j : Fin m) => ↑((finsetEquivFin S) (Fin.cast ⋯ j))) fun (j : Fin m) => ↑((finsetEquivFin S) (Fin.cast ⋯ j))) ≤ matOpNorm A

The operator norm of a principal submatrix is bounded by the operator norm of the full matrix. This is because restriction to a subspace doesn't increase the operator norm.

Main bridge: whitening_reduction in the matOpNorm type system

This provides the key result from Thm_4_6 restated using matOpNorm instead of matrixOpNorm. Since Thm_4_10 uses matOpNorm, this is the form that can be directly applied in Thm_4_10.lean.

theorem Rigollet.Chapter4.Thm_4_10_Bridges.whitening_reduction_bridge {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (hn : 0 < n) (hd : 0 < d) (X : Fin n → Ω → Fin d → ℝ) (covMat : Matrix (Fin d) (Fin d) ℝ) (hcov : ∀ (i : Fin n) (j k : Fin d), ∫ (ω : Ω), X i ω j * X i ω k ∂μ = covMat j k) (hSubG : ∀ (i : Fin n), Thm_4_6.IsSubGaussianVec μ (X i) (matOpNorm covMat)) (hIndepFun : ProbabilityTheory.iIndepFun X μ) (hPD : covMat.PosDef) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | matOpNorm (Thm_4_6.empiricalCovariance X ω - covMat) > matOpNorm covMat * t} ≤ ENNReal.ofReal (288 ^ d * Real.exp (-(↑n / 2 * min ((t / 32) ^ 2) (t / 32))))

whitening_reduction restated using matOpNorm instead of matrixOpNorm. The result: for sub-Gaussian vectors with covariance matrix covMat, P(‖Σ̂ - Σ‖_op > ‖Σ‖_op · t) ≤ 288^d · exp(-(n/2) · min((t/32)², t/32)).

theorem Rigollet.Chapter4.Thm_4_10_Bridges.whitening_reduction_subproblem {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ} (n : ℕ) (hn : 0 < n) (hm : 0 < m) (Y : Fin n → Ω → Fin m → ℝ) (covMatSub : Matrix (Fin m) (Fin m) ℝ) (hcov : ∀ (i : Fin n) (j k : Fin m), ∫ (ω : Ω), Y i ω j * Y i ω k ∂μ = covMatSub j k) (hSubG : ∀ (i : Fin n), Thm_4_6.IsSubGaussianVec μ (Y i) (matOpNorm covMatSub)) (hIndepFun : ProbabilityTheory.iIndepFun Y μ) (hPD : covMatSub.PosDef) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | matOpNorm (Thm_4_6.empiricalCovariance Y ω - covMatSub) > matOpNorm covMatSub * t} ≤ ENNReal.ofReal (288 ^ m * Real.exp (-(↑n / 2 * min ((t / 32) ^ 2) (t / 32))))

Restated whitening_reduction for a sub-problem of dimension m. When applied to the restriction of X to a subset S of size m, gives: P(‖Σ̂_S - Σ_S‖_op > ‖Σ_S‖_op · t) ≤ 288^m · exp(-(n/2) · min((t/32)², t/32)).