LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The empirical spectral distribution of a sample covariance matrix is a probability measure

Statement

For positive integers $n, p$ and a real matrix $X \in R^{n \times p}$ , set $S (X) = X^{T} X / n$ and $μ_{S (X)} = p^{- 1} \sum_{j = 1}^{p} δ_{λ_{j} (S (X))}$ , where the eigenvalues are counted with multiplicity. Then $μ_{S (X)}$ is a Borel probability measure on $R$ , supported on $[0, \infty)$ .

Statement references

Bai and Silverstein, Chapter 3, §3.1, printed pp. 39–40 (complete book PDF).

Facts & Assumptions

Given: Positive integers $n, p$ and $X \in R^{n \times p}$ .

[F1]

Sample covariance matrices and their empirical spectral distributions defines $S (X) = X^{T} X / n$ and $μ_{S (X)} = p^{- 1} \sum_{j = 1}^{p} δ_{λ_{j} (S (X))}$ .

[F2]

A real symmetric matrix has a real orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

[F3]

For every finite list of points of a measurable space, the equally weighted sum of their Dirac measures is a probability measure (A finite empirical measure is a probability law).

Proof

1.1givenF1F2algebra

The matrix $S (X)$ is symmetric because $(X^{T} X)^{T} = X^{T} X$ . For every $v \in R^{p}$ , $v^{T} S (X) v = \frac{1}{n} ∥ X v ∥_{2}^{2} \geq 0.$ By [F2], its eigenvalues are real; if $S (X) v = λ v$ with $v \neq 0$ , the displayed quadratic-form identity gives $λ ∥ v ∥_{2}^{2} \geq 0$ , hence $λ \geq 0$ .

2.1F1F3step 1.1∎

Apply [F3] to the finite list $λ_{1} (S (X)), \dots, λ_{p} (S (X))$ in the Borel space $R$ . The resulting empirical measure is exactly [F1] and is a Borel probability measure. Step 1.1 shows it assigns no mass outside $[0, \infty)$ .

Depends on

Used by

Almost-sure Marchenko–Pastur law for finite-fourth-moment sample covariance matrices Theorem

Cited to discharge well-definedness by Sample covariance matrices and their empirical spectral distributions.

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bai and Silverstein, Spectral Analysis of Large Dimensional Random Matrices, 2nd ed., Chapter 3 (standard reference, not scraped)