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

Unbiasedness and variance decomposition for the two-stage expansion total

Statement

Use the product two-stage design and expansion estimator from Two-stage sampling laws and the expansion estimator. Assume AC and $π_{i}^{(1)} > 0$ for every PSU $i$ and $π_{j ∣ i}^{(2)} > 0$ for every SSU $j \in U_{i}$ . Define $Δ_{i r}^{(1)} = π_{i r}^{(1)} - π_{i}^{(1)} π_{r}^{(1)}, Δ_{j ℓ ∣ i}^{(2)} = π_{j ℓ ∣ i}^{(2)} - π_{j ∣ i}^{(2)} π_{ℓ ∣ i}^{(2)} .$ Then $E_{d} [\hat{T}] = T$ and ${Var}_{d} (\hat{T}) = \sum_{i = 1}^{M} \sum_{r = 1}^{M} \frac{Δ_{i r}^{(1)}}{π_{i}^{(1)} π_{r}^{(1)}} T_{i} T_{r} + \sum_{i = 1}^{M} \frac{1}{π_{i}^{(1)}} \sum_{j \in U_{i}} \sum_{ℓ \in U_{i}} \frac{Δ_{j ℓ ∣ i}^{(2)}}{π_{j ∣ i}^{(2)} π_{ℓ ∣ i}^{(2)}} y_{i j} y_{i ℓ} .$ The first term is the design variance of the expansion based on the true PSU totals. The second is the expected within-PSU sampling variance. Zero pair inclusion probabilities are permitted because the formula divides only by positive first-order inclusion probabilities.

Facts & Assumptions

Given: AC; a finite fixed population partitioned into PSUs $U_{i}$ with fixed SSU values $y_{i j}$ ; the product two-stage sampling law; positive first-order inclusion probabilities at both stages; and the expansion estimators and stage-specific inclusion probabilities in the Statement.

[F1]

Two-stage sampling laws and the expansion estimator: Given $S_{1}$ , the second-stage samples are independent with joint mass $\prod_{i \in S_{1}} p_{2 i} (S_{i})$ ; the full joint mass is $p_{1} (S_{1}) \prod_{i \in S_{1}} p_{2 i} (S_{i})$ .

[F10]

Two-stage sampling laws and the expansion estimator: It defines the first- and second-order inclusion probabilities, their covariance differences, and ${\hat{T}}_{i}$ and $\hat{T}$ using positive first-order inclusion probabilities.

[F11]

Two-stage sampling laws and the expansion estimator: The first-stage $E_{1}$ and ${Var}_{1}$ , and conditional second-stage $E_{2} [\cdot ∣ S_{1}]$ and centered-square ${Var}_{2} (\cdot ∣ S_{1})$ , are defined as finite-law expectations and variances.

[F2]

Sigma-algebras: A sigma-algebra is an algebra of subsets closed under countable unions.

[F3]

Conditional expectation given a sigma algebra: A conditional expectation version is a measurable integrable function whose integral on each conditioning event equals the integral of the input.

[F4]

Conditional expectation as an ae class: Assume AC for the supplied existence theorem; $E [X ∣ G]$ is the unique almost-sure class of conditional-expectation versions.

[F5]

Conditional variance: Assume AC; for $X \in L^{2}$ , conditional variance is $E [(X - E [X ∣ G])^{2} ∣ G]$ as an almost-sure class.

[F6]

Conditional variance decomposition: Assume AC. For real $X \in L^{2} (P)$ and a sub-sigma-algebra $G$ , $Var (X) = E [Var (X ∣ G)] + Var (E [X ∣ G])$ .

[F7]

Moments, variance, and covariance on a probability space: Variance and covariance are the expectations of the centered square and centered product.

[F8]

Covariance is symmetric and bilinear in finite linear combinations: Covariance is symmetric and bilinear in finite linear combinations of square-integrable variables.

[F9]

Variance of a finite sum as the sum of all variances and covariances: The variance of a finite sum of square-integrable real random variables is the sum of all pairwise covariances.

[A1]

The Axiom of Choice: AC states that every family of nonempty sets has a choice function. It is used here only through the conditional expectation and conditional-variance supplier branch [F3]–[F5].

Proof

1.1givenF1F10algebra

For each selected PSU $i \in S_{1}$ , let $J_{i j} = 1 {j \in S_{i}}$ ; by [F1] and [F10], $E_{2} [J_{i j} ∣ S_{1}] = π_{j ∣ i}^{(2)}$ , so finite linearity gives $E_{2} [{\hat{T}}_{i} ∣ S_{1}] = \sum_{j \in U_{i}} E_{2} [J_{i j} ∣ S_{1}] y_{i j} / π_{j ∣ i}^{(2)} = \sum_{j \in U_{i}} y_{i j} = T_{i}$ .

1.2F7F8F9F10algebra

For PSU $i$ and SSU $j$ put $J_{i j} = 1 {j \in S_{i}}$ . By [F10], [F7]–[F9] give $V_{i} = {Var}_{2 i} (\sum_{j \in U_{i}} J_{i j} y_{i j} / π_{j ∣ i}^{(2)}) = \sum_{j, ℓ \in U_{i}} {Cov}_{2 i} (J_{i j}, J_{i ℓ}) y_{i j} y_{i ℓ} / (π_{j ∣ i}^{(2)} π_{ℓ ∣ i}^{(2)}) = \sum_{j, ℓ \in U_{i}} Δ_{j ℓ ∣ i}^{(2)} y_{i j} y_{i ℓ} / (π_{j ∣ i}^{(2)} π_{ℓ ∣ i}^{(2)})$ . Only first-order probabilities occur in denominators.

2.1A1F1F2F3F4F10step 1.1algebra

Let $Ω$ be the finite joint outcome space with law $P_{d}$ and $F = 2^{Ω}$ ; since first-stage fibers partition $Ω$ , complements and countable unions of their unions are again unions of fibers, so they form a sigma-algebra $G \subseteq F$ by [F2]. The function $H (S_{1}) = \sum_{i \in S_{1}} T_{i} / π_{i}^{(1)}$ is finite, integrable and $G$ -measurable. For each $A = {S_{1} \in B_{A}} \in G$ , [F1] and step 1.1 give $E_{d} [1_{A} \hat{T}] = \sum_{s_{1} \in B_{A}} p_{1} (s_{1}) \sum_{(s_{i})} (\prod_{i \in s_{1}} p_{2 i} (s_{i})) \sum_{i \in s_{1}} {\hat{T}}_{i} / π_{i}^{(1)} = \sum_{s_{1} \in B_{A}} p_{1} (s_{1}) H (s_{1}) = E_{d} [1_{A} H]$ . Thus [F3] makes $H$ a conditional-expectation version and [F4] identifies its class as $E_{d} [\hat{T} ∣ G]$ ; the finite support also gives $\hat{T} \in L^{2}$ .

3.1givenF1F10step 2.1algebra

Taking the first-stage expectation of $H$ in step 2.1 and using $E_{1} [1 {i \in S_{1}}] = π_{i}^{(1)}$ gives $E_{d} [\hat{T}] = E_{1} [\sum_{i \in S_{1}} T_{i} / π_{i}^{(1)}] = \sum_{i = 1}^{M} T_{i} = T$ .

3.2A1F1F3F4F5F6F10F11step 1.1step 2.1algebra

For each first-stage outcome $s$ , let $K (s) = {Var}_{2} (\hat{T} ∣ S_{1} = s) = E_{2} [(\hat{T} - H (s))^{2} ∣ S_{1} = s]$ , where [F10] and step 1.1 give $E_{2} [\hat{T} ∣ S_{1} = s] = H (s)$ by finite linearity; $K$ is finite, hence integrable, and $G$ -measurable. For any $A = {S_{1} \in B_{A}} \in G$ , summing the product law over fibers gives $E_{d} [1_{A} (\hat{T} - H)^{2}] = \sum_{s \in B_{A}} p_{1} (s) K (s) = E_{d} [1_{A} K]$ . Thus [F3] and [F4] identify $K$ as the conditional-expectation class of the squared residual, and [F5] identifies it with $Var (\hat{T} ∣ G)$ ; consequently its expectation is $E_{1} [{Var}_{2} (\hat{T} ∣ S_{1})]$ , while the conditional-mean variance is ${Var}_{1} (H)$ because $H$ is a function of $S_{1} \sim p_{1}$ . Applying [F6] under AC yields ${Var}_{d} (\hat{T}) = {Var}_{1} (\sum_{i \in S_{1}} T_{i} / π_{i}^{(1)}) + E_{1} [{Var}_{2} (\hat{T} ∣ S_{1})]$ .

3.3F7F8F9F10F11step 2.1algebra

Write $I_{i}^{(1)} = 1 {i \in S_{1}}$ . The conditional mean in step 2.1 is the first-stage HT estimator of the fixed totals; [F7]–[F9] give ${Var}_{1} (\sum_{i \in S_{1}} T_{i} / π_{i}^{(1)}) = \sum_{i, r} {Cov}_{1} (I_{i}^{(1)}, I_{r}^{(1)}) T_{i} T_{r} / (π_{i}^{(1)} π_{r}^{(1)}) = \sum_{i, r} Δ_{i r}^{(1)} T_{i} T_{r} / (π_{i}^{(1)} π_{r}^{(1)})$ by [F10].

4.1F1F7F8F9F10F11step 1.1step 1.2step 3.2algebra

Conditional on $S_{1}$ , [F1] factors the product law across PSUs; for distinct selected $i, r$ , $E_{2} [({\hat{T}}_{i} - T_{i}) ({\hat{T}}_{r} - T_{r}) ∣ S_{1}] = E_{2} [{\hat{T}}_{i} - T_{i} ∣ S_{1}] E_{2} [{\hat{T}}_{r} - T_{r} ∣ S_{1}] = 0$ by step 1.1, so [F7] gives zero covariance. With $V_{i}$ from step 1.2, [F8] and [F9] give ${Var}_{2} (\hat{T} ∣ S_{1}) = \sum_{i \in S_{1}} V_{i} / (π_{i}^{(1)})^{2}$ , whose first-stage expectation is $\sum_{i} π_{i}^{(1)} V_{i} / (π_{i}^{(1)})^{2} = \sum_{i} V_{i} / π_{i}^{(1)}$ .

5.1step 1.2step 3.1step 3.2step 3.3step 4.1algebra∎

Substituting the within-stage expression from step 1.2 and step 4.1 and the between-stage expression from step 3.3 into the decomposition in step 3.2 gives the stated variance, while step 3.1 gives unbiasedness.

Remarks

The AC hypothesis is carried from the published conditional-expectation and conditional-variance suppliers used in step 2.1; it is not used in the one-stage theorem or the direct finite enumeration on the B page. The stage-2 independence assumption is essential: dependent second-stage samples across PSUs add conditional covariance terms.

Depends on

Used by

Nothing in the library uses this result yet.

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 10: Two Stage Sampling (Subsampling), PDF pp. 3–7, IIT Kanpur (standard reference, not scraped)
Sharon L. Lohr, Sampling: Design and Analysis, 2nd ed., §5.3 and §6.6, printed pp. 145–150 and 204–210 (standard reference, not scraped)