LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 covariance matrix variance ratio is at least one

Statement

Let $X \in R^{p}$ have finite fourth moment, mean $μ$ , nonzero covariance $Σ$ , and matrix variance $σ_{0}^{2}$ as in Covariance matrix of a finite-dimensional random vector and Matrix variance for covariance estimation. Then $d : = \frac{σ_{0}^{2}}{∥ Σ ∥_{o p}^{2}} \geq 1.$

Facts & Assumptions

Given: A finite-dimensional random vector $X$ with $E ∥ X - μ ∥_{2}^{4} < \infty$ and nonzero covariance $Σ$ .

[F1]

Covariance matrix of a finite-dimensional random vector: $Σ$ is symmetric positive semidefinite and $E [(v^{T} (X - μ))^{2}] = v^{T} Σ v$ .

[F2]

Matrix variance for covariance estimation: $σ_{0}^{2} = ∥ E [∥ X - μ ∥_{2}^{2} (X - μ) (X - μ)^{T}] ∥_{o p}$ .

[F3]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: a nonzero positive semidefinite matrix has a unit eigenvector for its largest eigenvalue, equal to its operator norm.

[F4]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: for square-integrable real random variables $W$ and $1$ , $(E W)^{2} \leq E W^{2}$ .

Proof

1.1F1F2F3algebra

Put $Y = X - μ$ and choose a unit top eigenvector $v$ of $Σ$ , with $λ = v^{T} Σ v = ∥ Σ ∥_{o p} > 0$ by [F1] and [F3]. The positive semidefinite matrix inside [F2] has operator norm at least its quadratic form at $v$ , so $σ_{0}^{2} \geq E [∥ Y ∥_{2}^{2} (v^{T} Y)^{2}] \geq E [(v^{T} Y)^{4}] .$ The second inequality follows pointwise from $∥ Y ∥_{2}^{2} \geq (v^{T} Y)^{2}$ .

2.1F1F4step 1.1algebra∎

The finite fourth moment makes $W = v^{T} Y$ square-integrable. By [F4], $E [W^{4}] \geq (E [W^{2}])^{2} = λ^{2}$ . Hence $σ_{0}^{2} \geq ∥ Σ ∥_{o p}^{2}$ , and division by this positive quantity proves $d \geq 1$ .

Depends on

Used by

Dependency tree · two levels

19 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

Stanislav Minsker and Xiaohan Wei, Estimation of the Covariance Structure of Heavy-Tailed Distributions, §2 (standard reference, not scraped)
Philippe Rigollet, 18.S997 High-Dimensional Statistics Lecture Notes, MIT OpenCourseWare, Chapter 4 (standard reference, not scraped)