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.

Sen–Yates–Grundy variance identity

Statement

Let $(U, y)$ be a finite population with a fixed-size sampling design as in Finite populations and sampling designs, so every supported sample has the same size $n$ . Assume $π_{i} > 0$ for every $i \in U$ and put $x_{i} : = y_{i} / π_{i}$ . Then $\sum_{j \in U} Δ_{i j} = 0 (i \in U),$ and the Horvitz–Thompson variance satisfies the Sen–Yates–Grundy identity ${Var}_{d} ({\hat{T}}_{H T}) = - \frac{1}{2} \sum_{i, j \in U} Δ_{i j} (x_{i} - x_{j})^{2} .$ If additionally $π_{i j} > 0$ for every ordered pair, then the sample expression ${\hat{V}}_{S Y G} : = - \frac{1}{2} \sum_{i, j \in U} I_{i} I_{j} \frac{Δ_{i j}}{π_{i j}} (x_{i} - x_{j})^{2}$ is unbiased for ${Var}_{d} ({\hat{T}}_{H T})$ . If $Δ_{i j} \leq 0$ for every distinct pair, this condition guarantees that ${\hat{V}}_{S Y G}$ is nonnegative for every supported sample. It is a sufficient sign condition for the sample expression; the true variance in the identity is nonnegative for every valid design.

Facts & Assumptions

Given: A fixed finite population and design with sample size $n$ on every supported outcome, $π_{i} > 0$ for every unit, and additionally $π_{i j} > 0$ for every pair when proving the sample-estimate claim.

[F1]

Finite populations and sampling designs: $I_{i}$ indicates inclusion of unit $i$ , $π_{i} = P_{d} (I_{i} = 1)$ , $π_{i j} = P_{d} (I_{i} = I_{j} = 1)$ , and $π_{i j} = π_{j i}$ .

[F2]

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

[F3]

Horvitz–Thompson variance and pair-inclusion estimate: For $π_{i} > 0$ , ${Var}_{d} ({\hat{T}}_{H T}) = \sum_{i, j \in U} Δ_{i j} x_{i} x_{j} .$

[F4]

The expectation of an indicator is the probability of the event: An event indicator has expectation equal to the probability of its event.

[F5]

Linearity, monotonicity, and the modulus bound for expectation: For integrable random variables $X, Y$ and scalars $a, b$ on one probability space, $E [a X + b Y] = a E [X] + b E [Y]$ .

[F6]

Moments, variance, and covariance on a probability space: Variance is the expectation of a square and therefore is nonnegative.

Proof

1.1F1F2F4F5algebra

For each i,j, $I_{i} I_{j}$ indicates joint inclusion and $I_{i}$ indicates inclusion by [F1], so [F4] gives their expectations as $π_{i j}$ and $π_{i}$ . Since $\sum_{j} I_{j} = n$ on every sample, finite linearity by induction using [F5] gives $\sum_{j} π_{i j} = E_{d} [I_{i} \sum_{j} I_{j}] = n π_{i}$ and $\sum_{j} π_{i} π_{j} = π_{i} E_{d} [\sum_{j} I_{j}] = n π_{i}$ ; subtracting by [F2] gives $\sum_{j} Δ_{i j} = 0$ .

2.1F1F2F3F6step 1.1algebra

By [F1] and [F2], $Δ_{i j} = Δ_{j i}$ and the column sums also vanish; expansion gives $- \frac{1}{2} \sum_{i, j} Δ_{i j} (x_{i} - x_{j})^{2} = - \frac{1}{2} (\sum_{i} x_{i}^{2} \sum_{j} Δ_{i j} + \sum_{j} x_{j}^{2} \sum_{i} Δ_{i j} - 2 \sum_{i, j} Δ_{i j} x_{i} x_{j}) = \sum_{i, j} Δ_{i j} x_{i} x_{j}$ , which is ${Var}_{d} ({\hat{T}}_{H T})$ by [F3] and is nonnegative by [F6].

3.1givenF1F3F4F5step 2.1algebra

If every $π_{i j} > 0$ , each coefficient in ${\hat{V}}_{S Y G}$ is defined and every term is integrable on the finite support. Finite-sum linearity follows by induction from [F5]; by [F1], each $I_{i} I_{j}$ indicates joint inclusion, so [F4] gives $E_{d} [I_{i} I_{j}] = π_{i j}$ and $E_{d} [{\hat{V}}_{S Y G}] = - \frac{1}{2} \sum_{i, j} \frac{Δ_{i j}}{π_{i j}} E_{d} [I_{i} I_{j}] (x_{i} - x_{j})^{2} = - \frac{1}{2} \sum_{i, j} Δ_{i j} (x_{i} - x_{j})^{2} = {Var}_{d} ({\hat{T}}_{H T})$ by step 2.1.

4.1givenF1step 3.1algebra∎

On a supported sample, diagonal terms vanish and symmetry gives ${\hat{V}}_{S Y G} (s) = - \sum_{i < j, i, j \in s} \frac{Δ_{i j}}{π_{i j}} (x_{i} - x_{j})^{2}$ ; if every distinct-pair $Δ_{i j} \leq 0$ , every summand is nonnegative, proving the sufficient condition.

Depends on

Used by

A three-unit SRSWOR variance calculation Example
Positive pair covariances and a negative SYG estimate Example

Dependency tree · two levels

26 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 7: Varying Probability Sampling, PDF pp. 28–30 (standard reference, not scraped)
John J. Borkowski, Horvitz–Thompson Estimators, STAT 446 Lecture 6, §6.2, printed pp. 143–146 (standard reference, not scraped)