LemmaStatement: Literature-sourcedProof: 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.

Finite simple-random-sampling moment identities

Statement

Let $n \geq 2$ , let $x_{1}, \dots, x_{n}$ and $y_{1}, \dots, y_{n}$ be fixed real numbers, and choose a subset $A$ uniformly from the $m$ -element subsets of ${1, \dots, n}$ , where $1 \leq m \leq n$ . Put $\overset{ˉ}{x} = \frac{1}{n} \sum_{i = 1}^{n} x_{i}, {\overset{ˉ}{x}}_{A} = \frac{1}{m} \sum_{i \in A} x_{i},$ and define $\overset{ˉ}{y}, {\overset{ˉ}{y}}_{A}$ analogously. Define the finite-population covariance $S_{x y} = \frac{1}{n - 1} \sum_{i = 1}^{n} (x_{i} - \overset{ˉ}{x}) (y_{i} - \overset{ˉ}{y}) .$ Then $E [{\overset{ˉ}{x}}_{A}] = \overset{ˉ}{x}, Cov ({\overset{ˉ}{x}}_{A}, {\overset{ˉ}{y}}_{A}) = (1 - \frac{m}{n}) \frac{S_{x y}}{m} .$ When $m \geq 2$ , define the sample covariance $s_{x y, A} = \frac{1}{m - 1} \sum_{i \in A} (x_{i} - {\overset{ˉ}{x}}_{A}) (y_{i} - {\overset{ˉ}{y}}_{A}) .$ Then $E [s_{x y, A}] = S_{x y}$ . Taking $y_{i} = x_{i}$ gives the corresponding variance identities.

Facts & Assumptions

Given: Fixed real lists $x_{1}, \dots, x_{n}$ and $y_{1}, \dots, y_{n}$ , and the uniform finite probability law on the $m$ -element subsets of ${1, \dots, n}$ .

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: the sample space is finite, every subset is an event, and event probabilities are finite sums of outcome weights.

[F2]

Expectation of a real random variable on a finite probability space: for a real random variable $X$ on a finite probability space $(Ω, w)$ , $E [X] = \sum_{ω \in Ω} X (ω) w (ω)$ .

[F3]

Variance, standard deviation, and covariance on a finite probability space: for real random variables on a finite probability space, covariance is the expectation of the product of their centered values.

[F4]

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ : $(\binom{n}{m})$ is the cardinality of the set of $m$ -element subsets of an $n$ -element set.

[F5]

Laws of finite sums and finite products: finite sums are additive, scaling distributes over finite sums, and finite sums can be split into consecutive ranges.

[F6]

Expectation is linear for every finite family of random variables, without any independence hypothesis: on a finite probability space, expectation distributes over every finite real linear combination without any independence assumption.

[F7]

Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule: finite sums over products split into iterated sums, and finite sums over disjoint subsets add to the sum over their union.

Proof

1.1givenF1F4algebra

There are $(\binom{n}{m})$ equally likely subsets by [F4]. Count pairs $(i, A)$ with $i \in A$ in two ways: each $m$ -element $A$ contributes $m$ pairs and each of the $n$ indices occurs in $(\binom{n - 1}{m - 1})$ such subsets, so $m (\binom{n}{m}) = n (\binom{n - 1}{m - 1})$ and $P (i \in A) = m / n$ . For distinct ordered indices $i, j$ , count pairs $(i, j, A)$ with both in $A$ : each subset contributes $m (m - 1)$ pairs and each ordered pair occurs in $(\binom{n - 2}{m - 2})$ subsets when $m \geq 2$ , so $m (m - 1) (\binom{n}{m}) = n (n - 1) (\binom{n - 2}{m - 2})$ . Thus $P (i, j \in A) = m (m - 1) / (n (n - 1))$ , also zero for $m = 1$ .

2.1F2F5F6step 1.1algebra

Using ${\overset{ˉ}{x}}_{A} = m^{- 1} \sum_{i} 1 {i \in A} x_{i}$ , expectation linearity [F6] and the inclusion probability from step 1.1 give $E [{\overset{ˉ}{x}}_{A}] = m^{- 1} \sum_{i} (m / n) x_{i} = \overset{ˉ}{x}$ . The same identity holds for $y$ .

2.2givenF1F2F3F5F6F7step 1.1algebra

Set $d_{i} = x_{i} - \overset{ˉ}{x}$ and $e_{i} = y_{i} - \overset{ˉ}{y}$ , so $\sum_{i} d_{i} = \sum_{i} e_{i} = 0$ . Since the centered sample means have expectation zero, [F3], expectation linearity [F6], and the inclusion probabilities in step 1.1 give $Cov ({\overset{ˉ}{x}}_{A}, {\overset{ˉ}{y}}_{A}) = \frac{1}{m^{2}} \sum_{i, j} Cov (1 {i \in A}, 1 {j \in A}) d_{i} e_{j} .$ The diagonal indicator covariance is $m (n - m) / n^{2}$ , and for $i \neq j$ it is $- m (n - m) / (n^{2} (n - 1))$ , by subtracting the products of the marginal probabilities in step 1.1. Finite Fubini and splitting [F7] give $\sum_{i \neq j} d_{i} e_{j} = (\sum_{i} d_{i}) (\sum_{j} e_{j}) - \sum_{i} d_{i} e_{i} = - \sum_{i} d_{i} e_{i}$ . Substitution yields $(n - m) / (m n (n - 1)) \sum_{i} d_{i} e_{i} = (1 - m / n) S_{x y} / m$ .

3.1givenF2F5F6step 1.1step 2.2algebra∎

For $m \geq 2$ , expansion around the population means gives $\sum_{i \in A} (x_{i} - {\overset{ˉ}{x}}_{A}) (y_{i} - {\overset{ˉ}{y}}_{A}) = \sum_{i \in A} d_{i} e_{i} - m ({\overset{ˉ}{x}}_{A} - \overset{ˉ}{x}) ({\overset{ˉ}{y}}_{A} - \overset{ˉ}{y}) .$ By expectation linearity [F6] and the inclusion probability in step 1.1, the expectation of the first term is $(m / n) \sum_{i} d_{i} e_{i} = m (n - 1) S_{x y} / n$ . The expectation of the second term is $m Cov ({\overset{ˉ}{x}}_{A}, {\overset{ˉ}{y}}_{A}) = (n - m) S_{x y} / n$ by step 2.2. Their difference is $(m - 1) S_{x y}$ , so division by $m - 1$ proves $E [s_{x y, A}] = S_{x y}$ .

Depends on

Used by

Dependency tree · two levels

37 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

Michael G. Hudgens and M. Elizabeth Halloran, Toward Causal Inference With Interference, Appendix A.4 (standard reference, not scraped)