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.

Unbiasedness and variance of the stratified total estimator

Statement

Let $(U, y)$ be a finite population with a partition and stratified SRSWOR design as in Stratified sampling designs and the stratified total estimator. Under the design probability $P_{d}$ , the stratified total estimator satisfies $E_{d} [{\hat{T}}_{s t}] = \sum_{i \in U} y_{i} .$ Its design variance is ${Var}_{d} ({\hat{T}}_{s t}) = \sum_{h : n_{h} < N_{h}} N_{h}^{2} (1 - \frac{n_{h}}{N_{h}}) \frac{S_{h}^{2}}{n_{h}} .$ Thus certainty strata contribute zero and require no within-stratum variance term.

Facts & Assumptions

Given: A fixed finite population $(U, y)$ , a finite partition $U = ⨆_{h = 1}^{H} U_{h}$ , and independent within-stratum SRSWOR samples with $1 \leq n_{h} \leq N_{h}$ .

[F1]

Stratified sampling designs and the stratified total estimator: The joint design mass on stratum samples is the product of the uniform SRSWOR masses; ${\hat{T}}_{s t} = \sum_{h} N_{h} {\overset{ˉ}{y}}_{h, R}$ ; and $S_{h}^{2}$ is defined for noncertainty strata.

[F2]

Finite populations and sampling designs: Population values are fixed, the design is a finite probability mass function, the observed record contains selected labels and their values, and $π_{i} = P_{d} (i \in S)$ is the first-order inclusion probability.

[F3]

The Horvitz–Thompson total and mean are design-unbiased under positive inclusion probabilities: If every $π_{i} > 0$ , then $\sum_{i \in U} I_{i} y_{i} / π_{i}$ is design-unbiased for $\sum_{i \in U} y_{i}$ .

[F4]

SRSWOR inclusion covariance and sample-mean variance: For SRSWOR of $n$ from a fixed population of size $N > 1$ , ${Var}_{d} ({\overset{ˉ}{y}}_{S}) = (1 - n / N) S_{U}^{2} / n$ ; this includes $n = 1$ and the census $n = N$ .

[F5]

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.

[F6]

Variance of a finite sum as the sum of all variances and covariances: For a finite family of square-integrable variables on one probability space, the variance of their sum is the sum of all pairwise covariances, including diagonal terms.

Proof

1.1F1F2F3algebra

For $i \in U_{h}$ , counting the $n_{h}$ -subsets containing $i$ gives $π_{i} = (\binom{N_{h} - 1}{n_{h} - 1}) / (\binom{N_{h}}{n_{h}}) = n_{h} / N_{h} > 0$ . On observed record $O_{y} (R) = (R, y ∣_{R})$ , the recorded values are $y_{i}$ by [F2], so the Horvitz–Thompson total is $\sum_{h} (N_{h} / n_{h}) \sum_{i \in R_{h}} y_{i} = {\hat{T}}_{s t}$ ; [F3] gives $E_{d} [{\hat{T}}_{s t}] = \sum_{i \in U} y_{i}$ .

1.2F1F4F5algebra

Put $Z_{h} = N_{h} {\overset{ˉ}{y}}_{h, R}$ . Each $Z_{h}$ has finite support and is square-integrable. If $n_{h} < N_{h}$ , then $N_{h} > 1$ and [F4] gives ${Var}_{d} ({\overset{ˉ}{y}}_{h, R}) = (1 - n_{h} / N_{h}) S_{h}^{2} / n_{h}$ ; variance scaling from [F5] gives ${Var}_{d} (Z_{h}) = N_{h}^{2} (1 - n_{h} / N_{h}) S_{h}^{2} / n_{h}$ . If $n_{h} = N_{h}$ , $Z_{h} = \sum_{i \in U_{h}} y_{i}$ is constant with variance zero.

1.3F1F5algebra

For distinct strata $h, k$ , write $q_{g} (r_{g}) = {(\binom{N_{g}}{n_{g}})}^{- 1}$ . The product law in [F1] gives $E_{d} [Z_{h} Z_{k}] = (\sum_{r_{h}} q_{h} (r_{h}) Z_{h} (r_{h})) (\sum_{r_{k}} q_{k} (r_{k}) Z_{k} (r_{k})) \prod_{g \notin {h, k}} \sum_{r_{g}} q_{g} (r_{g}) = E_{d} [Z_{h}] E_{d} [Z_{k}]$ , since each remaining mass sum is one. Thus [F5] gives ${Cov}_{d} (Z_{h}, Z_{k}) = 0$ .

2.1F6step 1.1step 1.2step 1.3algebra∎

Since ${\hat{T}}_{s t} = \sum_{h} Z_{h}$ , [F6] and steps 1.2–1.3 give ${Var}_{d} ({\hat{T}}_{s t}) = \sum_{h} {Var}_{d} (Z_{h})$ . Substituting step 1.2's noncertainty and certainty cases yields the stated variance, and step 1.1 gives unbiasedness.

Depends on

Used by

Dependency tree · two levels

27 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, MTH 417 lecture notes, Chapter 4: Stratified Sampling, PDF pp. 3–6, Indian Institute of Technology Kanpur (standard reference, not scraped)
Robin Arnold, STAT392 Sample Surveys, Chapter 8: Stratified Sampling, §§8.1–8.3 (standard reference, not scraped)
Tommy Wright, A Simple Method of Exact Optimal Sample Allocation under Stratification with Any Mixed Constraint Patterns, U.S. Census Bureau, §2.1 (standard reference, not scraped)