Alphabeta Math
TheoremStatement: 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.

Bai–Yin lower singular-value limits and full rank away from aspect one

Statement

Let (ξij)i,j≥1 be one infinite iid array of real random variables with mean zero, variance one and finite fourth moment. For each positive integer n, let pn be a positive integer and let Xn=(ξij)1≤i≤n,1≤j≤pn and suppose pn/n→γ∈(0,∞). Let srn(Xn) be the smallest among the rn:=min⁡(n,pn) singular values, counting zero values. Then, almost surely: if γ<1, srn(Xn)/n→1−γ, so Xn has full column rank for all sufficiently large n; if γ>1, srn(Xn)/n→γ−1, so Xn has full row rank for all sufficiently large n; and if γ=1, the smallest positive singular value is eventually defined and, divided by n, tends to zero.

Statement references

Bai and Yin, Theorem 1, official publication record; the complete paper was not retrieved (publication record).

Bai and Silverstein, Theorem 5.11, printed p. 106 (complete book PDF).

Facts & Assumptions

[F1]

Finite-fourth-moment covariance spectral confinement supplies the nonbacktracking finite-fourth-moment confinement of the smaller Gram matrix.

[F2]

Nonbacktracking covariance high moments and an independent coarse norm bound supplies the independent coarse norm bound needed by Fixed-degree covariance trace moments and independent edge witnesses. The latter proves lim sup⁡λmin⁡+(XnXnT/n)≤(1−γ)2 and eventual existence of positive eigenvalues using fixed polynomial witnesses.

[F3]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition identifies the eigenvalues of the smaller Gram matrix with the squares of all rn=min⁡(n,pn) singular values, including zeros; The rank of a linear map is the number of its nonzero singular values identifies full rectangular rank with positivity of all these values.

Proof

Given: The nested iid array, its upper-left blocks, and the hypotheses in the Statement.

1.1givenF1F3algebra

Write Nn=max⁡(n,pn), rn=min⁡(n,pn), cn=Nn/n→c=max⁡(1,γ) and yn=rn/Nn→y:=min⁡(γ,γ−1). Orient Xn as Zn with rn rows. F1 and the quadratic-form lower bound give lim inf⁡λmin⁡(ZnZnT/Nn)≥(1−y)2 almost surely. By F3, srn(Xn)2/n=cnλmin⁡(ZnZnT/Nn), so its liminf is at least c(1−y)2=(1−γ)2.

2.1F2F3step 1.1algebra

If γ≠1, this last constant is positive. Thus all rn singular values are positive eventually, and F3 gives eventual full column rank when γ<1 and full row rank when γ>1. The smallest positive eigenvalue of XnXnT/n then equals srn(Xn)2/n. Its limsup is at most (1−γ)2 by F2; combined with step 1.1 this proves convergence of that squared singular value. Taking the nonnegative square root gives respectively 1−γ and γ−1.

3.1F2F3algebrastep 2.1∎

If γ=1, F2 supplies positive eigenvalues eventually and a smallest positive eigenvalue with limsup at most zero. Nonnegativity makes its limit zero. F3 transfers this to the square of the smallest positive singular value divided by n, and the nonnegative square root tends to zero. No claim of eventual full rank at aspect one is needed. The argument for either endpoint uses confinement and independent trace witnesses, not MP weak convergence.

Depends on

Used by

Dependency tree · two levels

24 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