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.

Horvitz–Thompson variance and pair-inclusion estimate

Statement

Let $(U, y)$ be a finite population with a sampling design as in Finite populations and sampling designs. Write $I_{i}$ for the indicator that unit $i$ is included, and assume $π_{i} > 0$ for every $i \in U$ . The Horvitz–Thompson total is ${\hat{T}}_{H T} : = \sum_{i \in U} \frac{I_{i} y_{i}}{π_{i}} .$ Its design variance is ${Var}_{d} ({\hat{T}}_{H T}) = \sum_{i, j \in U} \frac{Δ_{i j} y_{i} y_{j}}{π_{i} π_{j}},$ where $Δ_{i j}$ is defined in Inclusion-covariance difference. If, in addition, $π_{i j} > 0$ for every ordered pair $(i, j)$ , the all-pairs inverse-inclusion expression ${\hat{V}}_{H T} : = \sum_{i, j \in U} I_{i} I_{j} \frac{Δ_{i j}}{π_{i j}} \frac{y_{i}}{π_{i}} \frac{y_{j}}{π_{j}}$ is defined and satisfies $E_{d} [{\hat{V}}_{H T}] = {Var}_{d} ({\hat{T}}_{H T}) .$ When a pair has zero inclusion probability, the corresponding all-pairs coefficient $Δ_{i j} / π_{i j}$ is undefined; omitting unsupported pairs is a different expression and does not by itself prove unbiasedness or non-estimability by some other method.

Facts & Assumptions

Given: A finite population $(U, y)$ , a finite sampling design, $π_{i} > 0$ for every unit, and additionally $π_{i j} > 0$ for every ordered pair when proving the pair-inclusion identity.

[F1]

Finite populations and sampling designs: The population values are fixed; the finite design has support $S_{d}$ and weights $p_{d}$ ; $I_{i}$ is the inclusion indicator; $π_{i} = P_{d} (I_{i} = 1)$ and $π_{i j} = P_{d} (I_{i} = I_{j} = 1)$ ; also $π_{i i} = π_{i}$ .

[F2]

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

[F3]

Moments, variance, and covariance on a probability space: Variance is the expectation of the squared centered variable, and covariance is the expectation of the product of centered variables.

[F4]

The expectation of an indicator is the probability of the event: The expectation of an event indicator equals the probability of its event.

[F5]

Variance of a finite sum as the sum of all variances and covariances: The variance of a finite sum of square-integrable variables on one probability space is the double sum of their pairwise covariances.

[F6]

Covariance is symmetric and bilinear in finite linear combinations: Covariance is bilinear for finite linear combinations of square-integrable variables on one probability space.

[F7]

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]$ .

Proof

1.1givenF1choose

For each $i \in U$ , set $X_{i} = I_{i} y_{i} / π_{i}$ . The design support is finite by [F1], each $I_{i}$ is bounded, and $y_{i} / π_{i}$ is finite by the positivity assumption; hence every $X_{i}$ is square-integrable and ${\hat{T}}_{H T} = \sum_{i \in U} X_{i}$ .

2.1F1F5step 1.1

Apply [F5] to this finite family on the common design probability space to obtain ${Var}_{d} ({\hat{T}}_{H T}) = \sum_{i, j \in U} {Cov}_{d} (X_{i}, X_{j})$ .

3.1F1F2F3F4F6step 2.1algebra

By [F6], ${Cov}_{d} (X_{i}, X_{j}) = \frac{y_{i} y_{j}}{π_{i} π_{j}} {Cov}_{d} (I_{i}, I_{j})$ . For $A_{i} = {s : i \in s}$ , $I_{i} = 1_{A_{i}}$ and $I_{i} I_{j} = 1_{A_{i} \cap A_{j}}$ , so [F4] and [F1] give $E_{d} [I_{i}] = π_{i}$ and $E_{d} [I_{i} I_{j}] = π_{i j}$ ; expanding [F3] gives ${Cov}_{d} (I_{i}, I_{j}) = π_{i j} - π_{i} π_{j} = Δ_{i j}$ by [F2], and substitution in step 2.1 proves the variance formula.

4.1givenF1F4F7step 3.1algebra

Under the additional pair-positivity assumption every coefficient in ${\hat{V}}_{H T}$ is defined and every term is integrable on the finite support. Linearity over the finite index set $U \times U$ follows by induction: the empty sum has expectation zero, and adjoining one term uses the two-variable rule [F7]. For each pair, $I_{i} I_{j}$ is the indicator of joint inclusion by [F1], so [F4] gives $E_{d} [I_{i} I_{j}] = π_{i j}$ ; hence $E_{d} [{\hat{V}}_{H T}] = \sum_{i, j \in U} \frac{Δ_{i j}}{π_{i j}} \frac{y_{i} y_{j}}{π_{i} π_{j}} E_{d} [I_{i} I_{j}] = \sum_{i, j \in U} \frac{Δ_{i j} y_{i} y_{j}}{π_{i} π_{j}} = {Var}_{d} ({\hat{T}}_{H T})$ by step 3.1.

5.1givenstep 4.1algebra∎

If $π_{i j} = 0$ , the coefficient $Δ_{i j} / π_{i j}$ in the all-pairs expression is undefined; removing that unsupported term changes the expression, and step 4.1 no longer proves unbiasedness, without ruling out another design-specific estimator.

Depends on

Used by

A three-unit SRSWOR variance calculation Example
Zero pair support can prevent universal unbiased variance estimation Example
Sen–Yates–Grundy variance identity Theorem
SRSWOR inclusion covariance and sample-mean variance Theorem

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. 25–27 (standard reference, not scraped)
John J. Borkowski, Horvitz–Thompson Estimators, STAT 446 Lecture 6, §6.2, printed pp. 141–143 (standard reference, not scraped)