Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adapted
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 adds for every finite pairwise-independent family

Statement

If (Xi)i∈I is a finite pairwise-independent family of square-integrable real random variables on a common probability space, then Var⁡ ⁣(∑i∈IXi)=∑i∈IVar⁡(Xi). Pairwise independence, rather than mutual independence, is sufficient. In particular, the original finite-probability-space case is included, with pairwise atom independence as in the finite-valued convention. The empty sum has variance zero.

Facts & Assumptions

Given: A finite pairwise-independent family (Xi)i∈I of square-integrable real random variables on one probability space.

[L1]

Expectations of products of independent integrable real random variables factor; the finite-valued atom-independence convention is included. (Expectation factors over a finite product of mutually independent random variables)

[L2]

For square-integrable real random variables, covariance equals E[XY]−E[X]E[Y], is symmetric and bilinear on finite linear combinations, and variance equals the self-covariance. These identities agree with the original finite-space definitions. (Variance and covariance identities for random variables)

Proof

technique · direct
1.1givenL1L2algebra

Each Xi is integrable because 2∣Xi∣≤1+Xi2 and the measure has total mass one. For distinct i,j, pairwise independence and [L1] give E[XiXj]=E[Xi]E[Xj], so [L2] gives Cov⁡(Xi,Xj)=0.

2.1step 1.1L2algebra∎

The finite sum S=∑i∈IXi is square-integrable: repeated use of (a+b)2≤2a2+2b2 gives an integrable bound for S2. By [L2], Var⁡(S)=Cov⁡(S,S)=∑i,j∈ICov⁡(Xi,Xj)=∑i∈IVar⁡(Xi), where step 1.1 removes all off-diagonal terms. The empty sum is the constant zero, and the singleton case is the identity.

Depends on

Used by

Dependency tree · two levels

11 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