Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Finite-second-moment IID sample covariance converges

Statement

Let d≥1 be finite and let X1,X2,… be IID Rd-valued random vectors with E∥X1∥2<∞. Put μj=EX1j and Σjk=E[(X1j−μj)(X1k−μk)], the coordinate covariance entries from Moments, variance, and covariance on a probability space. Define Xˉn=1n∑i=1nXi,Σ^n=1n∑i=1n(Xi−Xˉn)(Xi−Xˉn)T. Then Xˉn→μ in probability and every entry of Σ^n converges in probability to the corresponding entry of Σ.

Facts & Assumptions

Given: The IID vectors, finite second moment, and definitions in the statement.

[F1]

IID means independent random elements with a common law; it has no moment assumption. Identical distribution and IID families

[F2]

The covariance entry is Σjk=E[(X1j−μj)(X1k−μk)]. Moments, variance, and covariance on a probability space

[F3]

For an integrable IID real sequence, its sample mean converges in L1 and hence in probability to its expectation. Khinchin weak law for integrable IID variables

[F4]

Measurable coordinatewise maps of an independent family remain independent. Measurable coordinatewise functions preserve independence

Proof

1.1F1F3F4given

For each coordinate j, the sequence (Xij)i is IID by [F1] and [F4], and is integrable since E∣X1j∣≤1+E∣X1j∣2<∞. For each pair j,k, (XijXik)i is also IID by [F1] and [F4], and is integrable because 2∣X1jX1k∣≤X1j2+X1k2. Apply [F3] to each of these finitely many sequences. This gives Xˉn,j→μj and n−1∑iXijXik→E[X1jX1k] in probability.

2.1F2step 1.1algebra∎

For each j,k, expand Σ^n,jk=1n∑iXijXik−Xˉn,jXˉn,k. Step 1.1 makes the right side converge in probability to E[X1jX1k]−μjμk=Σjk; the same step gives the claimed mean convergence. Since d is finite, entrywise convergence holds simultaneously in probability.

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