Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04
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.

Variance and covariance identities for random variables

Statement

Let X,Y be square-integrable real random variables on one probability space. Then Var⁡(X)=E[X2]−E[X]2, Cov⁡(X,Y)=E[XY]−E[X]E[Y]. Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.

Facts & Assumptions

Given: Square-integrable real random variables X,Y.

[L1]

Variance and covariance are the expectations of the centered square and centered product (Moments, variance, and covariance on a probability space).

[L2]

Expectation is linear on integrable random variables (Linearity, monotonicity, and the modulus bound for expectation).

[L3]

Finite probability spaces agree with the full-power-set probability-space formalism (Finite probability spaces are exactly finite full-power-set probability spaces).

Proof

technique · direct
1.1

Expanding (X−E[X])2 and applying [L2] gives Var⁡(X)=E[X2]−2E[X]E[X]+E[X]2=E[X2]−E[X]2. Likewise, Cov⁡(X,Y)=E[XY]−E[X]E[Y].

L1L2algebra
2.1

The covariance formula in step 1.1 is symmetric in X and Y, so Cov⁡(X,Y)=Cov⁡(Y,X). If U=∑i<maiXi and V=∑j<nbjYj are finite linear combinations of square-integrable real random variables, expanding E[UV]−E[U]E[V] and using [L2] gives Cov⁡(U,V)=∑i<m∑j<naibjCov⁡(Xi,Yj).

step 1.1L2algebra
3.1

On a finite probability space, [L3] identifies the general formulas above with the already-published finite ones, so the finite and general identities agree exactly.

step 1.1step 2.1L3∎

Depends on

Used by

Dependency tree · two levels

10 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