The empirical second-moment matrix

For a finite sample v : ι → n → 𝕜 of vectors over ℝ or ℂ, the uncentered empirical second-moment matrix is

M̂ = r⁻¹ ∑ᵢ vᵢ vᵢᴴ, with entries M̂ₖₗ = r⁻¹ ∑ᵢ vᵢₖ conj (vᵢₗ),

where r = card ι. It is the mean (TauCeti.finiteMean) of the rank-one matrices vᵢ vᵢᴴ, so it is Hermitian and positive semidefinite. Evaluated on random samples it is the natural estimator of a population second-moment matrix E[V Vᴴ]; each of its entries is a sample mean of products of coordinates, which is what makes the second-moment bounds for sample means apply to it entry by entry.

Main declarations

• TauCeti.sampleSecondMoment: the empirical second-moment matrix of a finite sample.
• TauCeti.sampleSecondMoment_apply: its entries are sample means of coordinate products.
• TauCeti.isHermitian_sampleSecondMoment, TauCeti.posSemidef_sampleSecondMoment: it is Hermitian, and positive semidefinite in finite dimension.
• Matrix.sampleCovariance: the sample covariance matrix X Xᴴ / n of a p × n data matrix, whose columns are the samples; Matrix.sampleCovariance_eq_sampleSecondMoment identifies it with the empirical second-moment matrix of the columns, and Matrix.isHermitian_sampleCovariance and Matrix.posSemidef_sampleCovariance give Hermitian and positive semidefinite.
• Matrix.re_trace_sampleCovariance: its real trace is the column-normalized sum of squared entry norms.

References

• R. Vershynin, High-Dimensional Probability (2018), §4.7: the sample covariance matrix.

noncomputable def TauCeti.sampleSecondMoment {𝕜 : Type u_1} {ι : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype ι] (v : ι → n → 𝕜) : Matrix n n 𝕜

The uncentered empirical second-moment matrix r⁻¹ ∑ᵢ vᵢ vᵢᴴ of a finite sample v : ι → n → 𝕜, where r = card ι: the mean of the rank-one matrices vᵢ vᵢᴴ. The empty sample has second-moment matrix 0.

theorem TauCeti.sampleSecondMoment_def {𝕜 : Type u_1} {ι : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype ι] (v : ι → n → 𝕜) : sampleSecondMoment v = finiteMean 𝕜 fun (i : ι) => Matrix.vecMulVec (v i) (star (v i))

@[simp]

theorem TauCeti.sampleSecondMoment_apply {𝕜 : Type u_1} {ι : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype ι] (v : ι → n → 𝕜) (k l : n) : sampleSecondMoment v k l = finiteMean 𝕜 fun (i : ι) => v i k * star (v i l)

The (k, l) entry of the empirical second-moment matrix is the sample mean of the products vᵢₖ conj (vᵢₗ).

theorem TauCeti.isHermitian_sampleSecondMoment {𝕜 : Type u_1} {ι : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype ι] (v : ι → n → 𝕜) : (sampleSecondMoment v).IsHermitian

The empirical second-moment matrix is Hermitian.

theorem TauCeti.posSemidef_sampleSecondMoment {𝕜 : Type u_1} {ι : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype ι] [Finite n] (v : ι → n → 𝕜) : (sampleSecondMoment v).PosSemidef

The empirical second-moment matrix is positive semidefinite.

noncomputable def Matrix.sampleCovariance {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] (X : Matrix p n 𝕜) : Matrix p p 𝕜

The sample covariance matrix X Xᴴ / n of a p × n data matrix X, with the n columns as samples. When n is empty it is 0.

theorem Matrix.sampleCovariance_def {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] (X : Matrix p n 𝕜) : X.sampleCovariance = (1 / ↑(Fintype.card n)) • (X * X.conjTranspose)

@[simp]

theorem Matrix.sampleCovariance_apply {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] (X : Matrix p n 𝕜) (i j : p) : X.sampleCovariance i j = (1 / ↑(Fintype.card n)) • ∑ k : n, X i k * star (X j k)

The (i, j) entry of the sample covariance matrix.

theorem Matrix.re_trace_sampleCovariance {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] [Fintype p] (X : Matrix p n 𝕜) : RCLike.re X.sampleCovariance.trace = 1 / ↑(Fintype.card n) * ∑ i : p, ∑ j : n, ‖X i j‖ ^ 2

The real trace of a sample covariance matrix is the column-normalized sum of squared entry norms. This holds for empty index types, with the usual zero conventions.

theorem Matrix.sampleCovariance_eq_sampleSecondMoment {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] (X : Matrix p n 𝕜) : X.sampleCovariance = TauCeti.sampleSecondMoment fun (k : n) (i : p) => X i k

The sample covariance matrix of X is the empirical second-moment matrix of its columns.

theorem Matrix.isHermitian_sampleCovariance {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] (X : Matrix p n 𝕜) : X.sampleCovariance.IsHermitian

The sample covariance matrix is Hermitian.

theorem Matrix.posSemidef_sampleCovariance {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {n : Type u_3} [Fintype n] [Finite p] (X : Matrix p n 𝕜) : X.sampleCovariance.PosSemidef

The sample covariance matrix is positive semidefinite.