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

SRSWOR inclusion covariance and sample-mean variance

Statement

Let $(U, y)$ be a finite population of size $N > 1$ , and draw an SRSWOR sample $S$ of size $n$ , where $1 \leq n \leq N$ . Write $I_{i} = 1$ if $i \in S$ and $I_{i} = 0$ otherwise. Define ${\overset{ˉ}{y}}_{U} : = \frac{1}{N} \sum_{i \in U} y_{i}, {\overset{ˉ}{y}}_{S} : = \frac{1}{n} \sum_{i \in S} y_{i}, S_{U}^{2} : = \frac{1}{N - 1} \sum_{i \in U} (y_{i} - {\overset{ˉ}{y}}_{U})^{2} .$ For distinct $i, j \in U$ , ${Cov}_{d} (I_{i}, I_{j}) = - \frac{n (N - n)}{N^{2} (N - 1)},$ and ${Var}_{d} ({\overset{ˉ}{y}}_{S}) = (1 - \frac{n}{N}) \frac{S_{U}^{2}}{n} .$ Both formulas include $n = 1$ and the census case $n = N$ .

Facts & Assumptions

Given: A finite population with fixed real values, $N > 1$ , and a uniform design on the $n$ -element subsets of $U$ for an integer $1 \leq n \leq N$ .

[F1]

Finite populations and sampling designs: The population values are fixed; the design defines $I_{i}$ , $π_{i}$ , $π_{i j}$ , design expectation, the total $T (y) = \sum_{i} y_{i}$ , and the population mean ${\overset{ˉ}{y}}_{U} = T (y) / N$ .

[F2]

Simple random sampling without replacement: Every $n$ -element subset is in the design support and has probability ${(\binom{N}{n})}^{- 1}$ .

[F3]

Inclusion-covariance difference: $Δ_{i j} = π_{i j} - π_{i} π_{j}$ .

[F4]

Horvitz–Thompson variance and pair-inclusion estimate: When $π_{i} > 0$ , the design variance of $\sum_{i} I_{i} y_{i} / π_{i}$ is $\sum_{i, j} Δ_{i j} y_{i} y_{j} / (π_{i} π_{j})$ .

[F5]

Moments, variance, and covariance on a probability space: Covariance is the expectation of the product of centered variables; variance is covariance with itself.

Proof

1.1givenF2choosealgebra

There are $(\binom{N}{n})$ supported samples; a fixed unit occurs in $(\binom{N - 1}{n - 1})$ of them, so $π_{i} = n / N$ . If $n = 1$ , no sample contains distinct $i, j$ ; if $2 \leq n \leq N$ , $(\binom{N - 2}{n - 2})$ samples contain them, hence in either case $π_{i j} = n (n - 1) / (N (N - 1))$ for $i \neq j$ .

2.1F1F3F5step 1.1algebra

By [F1], $E_{d} [I_{i}] = π_{i}$ and $E_{d} [I_{i} I_{j}] = \sum_{s : i, j \in s} p_{d} (s) = π_{i j}$ , while $π_{i i} = π_{i}$ ; expanding [F5] gives ${Cov}_{d} (I_{i}, I_{j}) = E_{d} [I_{i} I_{j}] - E_{d} [I_{i}] E_{d} [I_{j}] = π_{i j} - π_{i} π_{j} = Δ_{i j}$ . Substitution from step 1.1 gives ${Cov}_{d} (I_{i}, I_{j}) = \frac{n (n - 1)}{N (N - 1)} - \frac{n^{2}}{N^{2}} = - \frac{n (N - n)}{N^{2} (N - 1)}$ for $i \neq j$ .

3.1F1F4step 1.1step 2.1algebra

Since $π_{i} = n / N$ , $N^{- 1} \sum_{i} I_{i} y_{i} / π_{i} = {\overset{ˉ}{y}}_{S}$ ; by [F4], ${Var}_{d} ({\overset{ˉ}{y}}_{S}) = \frac{1}{N^{2}} (\sum_{i} \frac{Δ_{i i} y_{i}^{2}}{π_{i}^{2}} + \sum_{i \neq j} \frac{Δ_{i j} y_{i} y_{j}}{π_{i}^{2}})$ . From $π_{i i} = π_{i}$ , $Δ_{i i} / π_{i}^{2} = (N - n) / n$ , and step 2.1 gives $Δ_{i j} / π_{i}^{2} = - (N - n) / (n (N - 1))$ for $i \neq j$ ; thus ${Var}_{d} ({\overset{ˉ}{y}}_{S}) = \frac{N - n}{N^{2} n} (\sum_{i} y_{i}^{2} - \frac{1}{N - 1} \sum_{i \neq j} y_{i} y_{j}) = \frac{N - n}{N^{2} n} \frac{N \sum_{i} y_{i}^{2} - (\sum_{i} y_{i})^{2}}{N - 1} = \frac{N - n}{N n} S_{U}^{2}$ .

4.1F1F2step 3.1algebra∎

When $n = N$ , the sample is the population and the factor $1 - n / N$ is zero. When $n = 1$ , step 3.1 gives $(1 - 1 / N) S_{U}^{2}$ ; the usual sample variance denominator $n - 1$ is unavailable, but the design variance is defined.

Remarks

The PDF p. 14 covariance display in Shalabh's Chapter 2 has a positive-sign typo. The inclusion probabilities on that page and the defining identity $Cov (I_{i}, I_{j}) = π_{i j} - π_{i} π_{j}$ give the negative value proved above. The sample space has only $(\binom{N}{n})$ points, so the design distribution is finitely supported; the displayed variance alone is not an exact normal or $t$ calibration.

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

Shalabh, Sampling Theory, Chapter 2: Simple Random Sampling, PDF pp. 1–15 (standard reference, not scraped)