Elementary concentration of random matrices from entrywise second moments

Let μ be any measure, S : Ω → Matrix m n E a matrix-valued function and A a fixed matrix. Suppose every squared entrywise deviation is integrable with ∫ ω, ‖S ω k l - A k l‖² ∂μ ≤ v. For η > 0, Chebyshev's inequality for each of the card m * card n entries, followed by a union bound, bounds the measure of the deviation event:

μ {ω | ∃ k l, η < ‖S ω k l - A k l‖} ≤ ENNReal.ofReal (card m * card n * v / η²).

On a probability space, every deterministic consequence of entrywise η-closeness therefore holds with probability at least 1 - card m * card n * v / η². For square matrices over ℝ or ℂ the entrywise-to-spectral comparison of TauCeti.Analysis.Matrix.Eigenvalues.Basic turns this into simultaneous high-probability control of every sorted eigenvalue, up to the dimension factor card n. For rectangular matrices over ℝ or ℂ the entrywise-to-operator comparison of TauCeti.Analysis.Matrix.EntrywiseOpNorm bounds the operator norm of the Euclidean action of S - A by √(card m) * η * √(card n), which is card n * η for square matrices.

The entrywise measure bound needs no measurability assumption on the entries: Chebyshev's inequality uses the integrability of the squared deviations. For the probability conclusions, 1 - μ sᶜ ≤ μ s holds for every set on a probability space. Measurability of the deviation event is recorded separately.

Finally, for real samples V i, every entry of the empirical second-moment matrix TauCeti.sampleSecondMoment is the sample mean of the products V i k * V i l. When those products are pairwise independent with common mean M k l and second moments about it at most v, the entry has mean-square error at most v / r for r samples. Feeding this into the eigenvalue bound with η = c / (2 d), where d is the dimension, shows that, with probability at least 1 - 4 d⁴ v / (r c²), every eigenvalue of the population matrix M that is at least c stays at least c / 2 for the empirical matrix.

Main statements

• TauCeti.measure_exists_lt_norm_sub_le: the entrywise Chebyshev union bound.
• TauCeti.measurableSet_exists_lt_norm_sub: the entrywise deviation event is measurable when the entries are.
• TauCeti.one_sub_le_measure_of_entry_le: with probability at least 1 - card m * card n * v / η², every consequence of entrywise η-closeness holds.
• TauCeti.one_sub_le_measure_forall_abs_eigenvalues₀_sub_le: eigenvalue concentration.
• TauCeti.one_sub_le_measure_forall_eigenvalues₀_sub_le: the one-sided eigenvalue floor.
• TauCeti.one_sub_le_measure_forall_norm_toEuclideanLin_sub_le: rectangular operator concentration.
• TauCeti.one_sub_le_measure_forall_norm_toEuclideanLin_sub_le_square: square operator concentration.
• TauCeti.integral_sampleSecondMoment_apply_sub_sq_le: the mean-square error of an entry of the empirical second-moment matrix.
• TauCeti.one_sub_le_measure_forall_half_le_eigenvalues₀_sampleSecondMoment: the empirical second-moment matrix keeps every population eigenvalue above c above c / 2.

References

• R. Vershynin, High-Dimensional Probability (2018), §1.2 (Chebyshev's inequality) and §4.7 (covariance estimation).
• R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed. (2013), Theorem 4.3.1 (Weyl's inequality).

theorem TauCeti.measure_exists_lt_norm_sub_le {Ω : Type u_1} {m : Type u_2} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype m] [Fintype n] {E : Type u_4} {S : Ω → Matrix m n E} {A : Matrix m n E} {v η : ℝ} [Norm E] [Sub E] (hint : ∀ (k : m) (l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k : m) (l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) : μ {ω : Ω | ∃ (k : m) (l : n), η < ‖S ω k l - A k l‖} ≤ ENNReal.ofReal (↑(Fintype.card m) * ↑(Fintype.card n) * v / η ^ 2)

Entrywise Chebyshev union bound. For any measure μ, if every squared entrywise deviation of a matrix-valued function S from a fixed matrix A is integrable with integral at most v, then the measure of the event where some entry deviates by more than η > 0 is at most ENNReal.ofReal (card m * card n * v / η²).

theorem TauCeti.measurableSet_exists_lt_norm_sub {Ω : Type u_1} {m : Type u_2} {n : Type u_3} {mΩ : MeasurableSpace Ω} {E : Type u_4} {S : Ω → Matrix m n E} {A : Matrix m n E} [SeminormedAddGroup E] [Countable m] [Countable n] [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSub E] (hS : ∀ (k : m) (l : n), Measurable fun (ω : Ω) => S ω k l) (η : ℝ) : MeasurableSet {ω : Ω | ∃ (k : m) (l : n), η < ‖S ω k l - A k l‖}

For countable row and column index types, the event that some entry of a random matrix deviates from a fixed matrix by more than η is measurable when every entry is measurable.

theorem TauCeti.one_sub_le_measure_of_entry_le {Ω : Type u_1} {m : Type u_2} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype m] [Fintype n] {E : Type u_4} {S : Ω → Matrix m n E} {A : Matrix m n E} {v η : ℝ} [Norm E] [Sub E] [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hint : ∀ (k : m) (l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k : m) (l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) (hs : ∀ (ω : Ω), (∀ (k : m) (l : n), ‖S ω k l - A k l‖ ≤ η) → ω ∈ s) : 1 - ENNReal.ofReal (↑(Fintype.card m) * ↑(Fintype.card n) * v / η ^ 2) ≤ μ s

High-probability entrywise closeness. On a probability space, if every entrywise deviation of a random matrix S from a fixed matrix A has second moment at most v, then any set s containing every outcome at which all entries of S are within η > 0 of those of A has probability at least 1 - card m * card n * v / η².

theorem TauCeti.one_sub_le_measure_forall_abs_eigenvalues₀_sub_le {Ω : Type u_1} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype n] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq n] [MeasureTheory.IsProbabilityMeasure μ] {S : Ω → Matrix n n 𝕜} {A : Matrix n n 𝕜} {v η : ℝ} (hS : ∀ (ω : Ω), (S ω).IsHermitian) (hA : A.IsHermitian) (hint : ∀ (k l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) : 1 - ENNReal.ofReal (↑(Fintype.card n) ^ 2 * v / η ^ 2) ≤ μ {ω : Ω | ∀ (k : Fin (Fintype.card n)), |⋯.eigenvalues₀ k - hA.eigenvalues₀ k| ≤ ↑(Fintype.card n) * η}

Eigenvalue concentration. If every entrywise deviation of a random Hermitian matrix S from a fixed Hermitian matrix A has second moment at most v, then with probability at least 1 - (card n)² v / η² every sorted eigenvalue of S is within card n * η of the corresponding eigenvalue of A.

theorem TauCeti.one_sub_le_measure_forall_eigenvalues₀_sub_le {Ω : Type u_1} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype n] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq n] [MeasureTheory.IsProbabilityMeasure μ] {S : Ω → Matrix n n 𝕜} {A : Matrix n n 𝕜} {v η : ℝ} (hS : ∀ (ω : Ω), (S ω).IsHermitian) (hA : A.IsHermitian) (hint : ∀ (k l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) : 1 - ENNReal.ofReal (↑(Fintype.card n) ^ 2 * v / η ^ 2) ≤ μ {ω : Ω | ∀ (k : Fin (Fintype.card n)), hA.eigenvalues₀ k - ↑(Fintype.card n) * η ≤ ⋯.eigenvalues₀ k}

One-sided eigenvalue floor. Under the hypotheses of TauCeti.one_sub_le_measure_forall_abs_eigenvalues₀_sub_le, with probability at least 1 - (card n)² v / η² every sorted eigenvalue of S is at least the corresponding eigenvalue of A minus card n * η.

theorem TauCeti.one_sub_le_measure_forall_norm_toEuclideanLin_sub_le {Ω : Type u_1} {m : Type u_2} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype m] [Fintype n] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq n] [MeasureTheory.IsProbabilityMeasure μ] {v η : ℝ} {S : Ω → Matrix m n 𝕜} {A : Matrix m n 𝕜} (hint : ∀ (k : m) (l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k : m) (l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) : 1 - ENNReal.ofReal (↑(Fintype.card m) * ↑(Fintype.card n) * v / η ^ 2) ≤ μ {ω : Ω | ∀ (x : EuclideanSpace 𝕜 n), ‖(Matrix.toEuclideanLin (S ω - A)) x‖ ≤ √↑(Fintype.card m) * η * √↑(Fintype.card n) * ‖x‖}

Operator concentration for rectangular matrices. If every entrywise deviation of a random m × n matrix S from a fixed matrix A has second moment at most v, then with probability at least 1 - card m * card n * v / η² the Euclidean action of S - A has operator norm at most √(card m) * η * √(card n), that is, ‖(S - A) x‖ ≤ √(card m) * η * √(card n) * ‖x‖ for every x.

theorem TauCeti.one_sub_le_measure_forall_norm_toEuclideanLin_sub_le_square {Ω : Type u_1} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype n] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq n] [MeasureTheory.IsProbabilityMeasure μ] {S : Ω → Matrix n n 𝕜} {A : Matrix n n 𝕜} {v η : ℝ} (hint : ∀ (k l : n), MeasureTheory.Integrable (fun (ω : Ω) => ‖S ω k l - A k l‖ ^ 2) μ) (hmoment : ∀ (k l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) : 1 - ENNReal.ofReal (↑(Fintype.card n) ^ 2 * v / η ^ 2) ≤ μ {ω : Ω | ∀ (x : EuclideanSpace 𝕜 n), ‖(Matrix.toEuclideanLin (S ω - A)) x‖ ≤ ↑(Fintype.card n) * η * ‖x‖}

Operator concentration for square matrices. If every entrywise deviation of a random square matrix S from a fixed matrix A has second moment at most v, then with probability at least 1 - (card n)² v / η² the Euclidean action of S - A has operator norm at most card n * η.

theorem TauCeti.integral_sampleSecondMoment_apply_sub_sq_le {Ω : Type u_1} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_4} [Fintype ι] [Nonempty ι] [MeasureTheory.IsProbabilityMeasure μ] {V : ι → Ω → n → ℝ} {M : Matrix n n ℝ} {v : ℝ} {k l : n} (hV : ∀ (i : ι), MeasureTheory.MemLp (fun (ω : Ω) => V i ω k * V i ω l) 2 μ) (hmean : ∀ (i : ι), ∫ (x : Ω), (fun (ω : Ω) => V i ω k * V i ω l) x ∂μ = M k l) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (fun (ω : Ω) => V i ω k * V i ω l) (fun (ω : Ω) => V j ω k * V j ω l) μ) (hv : ∀ (i : ι), ∫ (ω : Ω), (V i ω k * V i ω l - M k l) ^ 2 ∂μ ≤ v) : ∫ (ω : Ω), (sampleSecondMoment (fun (x : ι) => V x ω) k l - M k l) ^ 2 ∂μ ≤ v / ↑(Fintype.card ι)

Mean-square error of an empirical second moment. For real random vectors V i, if the products V i k * V i l of two fixed coordinates are square-integrable, pairwise independent and have a common mean M k l, and each has second moment about M k l at most v, then the (k, l) entry of the empirical second-moment matrix has mean-square error at most v / r, where r is the number of samples.

theorem TauCeti.one_sub_le_measure_forall_half_le_eigenvalues₀_sampleSecondMoment {Ω : Type u_1} {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype n] {ι : Type u_4} [Fintype ι] [Nonempty ι] [DecidableEq n] [MeasureTheory.IsProbabilityMeasure μ] {V : ι → Ω → n → ℝ} {M : Matrix n n ℝ} {v : ℝ} (hM : M.IsHermitian) (hV : ∀ (k l : n) (i : ι), MeasureTheory.MemLp (fun (ω : Ω) => V i ω k * V i ω l) 2 μ) (hmean : ∀ (k l : n) (i : ι), ∫ (x : Ω), (fun (ω : Ω) => V i ω k * V i ω l) x ∂μ = M k l) (hindep : ∀ (k l : n), Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (fun (ω : Ω) => V i ω k * V i ω l) (fun (ω : Ω) => V j ω k * V j ω l) μ) (hv : ∀ (k l : n) (i : ι), ∫ (ω : Ω), (V i ω k * V i ω l - M k l) ^ 2 ∂μ ≤ v) {c : ℝ} (hc : 0 < c) : 1 - ENNReal.ofReal (4 * ↑(Fintype.card n) ^ 4 * v / (↑(Fintype.card ι) * c ^ 2)) ≤ μ {ω : Ω | ∀ (k : Fin (Fintype.card n)), c ≤ hM.eigenvalues₀ k → c / 2 ≤ ⋯.eigenvalues₀ k}

Eigenvalue floor for the empirical second-moment matrix. Let V i be r real random vectors of dimension d. Suppose that for every pair of coordinates k, l the products V i k * V i l are square-integrable, pairwise independent and have a common mean M k l, with second moments about it at most v, and that M is symmetric. Then for every c > 0, with probability at least 1 - 4 d⁴ v / (r c²), every sorted eigenvalue of M that is at least c has the corresponding eigenvalue of the empirical second-moment matrix at least c / 2.