LemmaStatement: Literature-sourcedProof: 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.

Finite two-stage sampling variance identities

Statement

Let $N \geq 4$ groups be completely randomized, with exactly $C$ groups assigned $ψ$ and $N - C$ assigned $ϕ$ , where $2 \leq C \leq N - 2$ . For each group $i$ and strategy $s \in {ϕ, ψ}$ , let $a_{i} (s)$ be a fixed real value and let $X_{i} (s)$ be a real-valued random variable from that group's finite second-stage assignment law, with $E [X_{i} (s)] = a_{i} (s)$ and $v_{i} (s) = Var (X_{i} (s))$ . Conditional on the first-stage vector, the group-specific second-stage random variables are independent. Let $C_{ψ} = C$ , $C_{ϕ} = N - C$ , and define ${\hat{μ}}_{s} = \frac{1}{C_{s}} \sum_{i : S_{i} = s} X_{i} (s), s_{X, s}^{2} = \frac{1}{C_{s} - 1} \sum_{i : S_{i} = s} (X_{i} (s) - {\hat{μ}}_{s})^{2} .$ For $S_{s}^{2} = (N - 1)^{- 1} \sum_{i} (a_{i} (s) - \overset{ˉ}{a} (s))^{2}$ and $S_{ψ - ϕ}^{2} = (N - 1)^{- 1} \sum_{i} {a_{i} (ψ) - a_{i} (ϕ) - \overline{a (ψ) - a (ϕ)}}^{2}$ , one has $Var ({\hat{μ}}_{s}) = (1 - \frac{C_{s}}{N}) \frac{S_{s}^{2}}{C_{s}} + \frac{1}{C_{s} N} \sum_{i = 1}^{N} v_{i} (s), E [s_{X, s}^{2}] = S_{s}^{2} + \frac{1}{N} \sum_{i = 1}^{N} v_{i} (s),$ and $Var ({\hat{μ}}_{ψ} - {\hat{μ}}_{ϕ}) = \frac{S_{ψ}^{2}}{C} + \frac{S_{ϕ}^{2}}{N - C} - \frac{S_{ψ - ϕ}^{2}}{N} + \frac{1}{C N} \sum_{i} v_{i} (ψ) + \frac{1}{(N - C) N} \sum_{i} v_{i} (ϕ) .$ Consequently, $E ⁣ [\frac{s_{X, ψ}^{2}}{C} + \frac{s_{X, ϕ}^{2}}{N - C}] = Var ({\hat{μ}}_{ψ} - {\hat{μ}}_{ϕ}) + \frac{S_{ψ - ϕ}^{2}}{N} .$

Facts & Assumptions

Given: The finite two-stage assignment law with fixed strategy-arm sizes, fixed real group values $a_{i} (s)$ , and finite second-stage random variables $X_{i} (s)$ whose conditional laws are independent across groups and have means $a_{i} (s)$ and variances $v_{i} (s)$ .

[F1]

Two-stage randomized design and strategy-specific effects: the first-stage strategy- $ψ$ groups are a uniform $C$ -element subset of the $N$ groups, and the second-stage assignments are independent across groups conditional on the strategy vector.

[F2]

Finite simple-random-sampling moment identities: for a uniform fixed-size subset, sample means have covariance $(1 - m / n) S_{x y} / m$ , and sample covariance is unbiased for the corresponding finite-population covariance.

[F3]

Expectation of a real random variable on a finite probability space and Variance, standard deviation, and covariance on a finite probability space: expectations and variances are finite weighted sums and centered second moments on the finite assignment space.

[F4]

Laws of finite sums and finite products: finite sums distribute over addition and scalar multiplication.

[F5]

Expectation is linear for every finite family of random variables, without any independence hypothesis: expectation distributes over finite sums on a finite probability space.

[F6]

Conditional expectation on positive-probability events in finite spaces: averaging conditional expectations over a finite partition recovers unconditional expectation.

[F7]

Variance adds for every finite pairwise-independent family: for a finite pairwise-independent family of square-integrable real random variables, the variance of the sum is the sum of their variances.

Proof

1.1F1F2F3F5F6givenalgebra

For a fixed strategy $s$ , write $A_{s} (S) = C_{s}^{- 1} \sum_{i : S_{i} = s} a_{i} (s)$ and $E_{s} = C_{s}^{- 1} \sum_{i : S_{i} = s} ϵ_{i} (s)$ , where $ϵ_{i} (s) = X_{i} (s) - a_{i} (s)$ ; then ${\hat{μ}}_{s} = A_{s} + E_{s}$ . By [F2], $E [A_{s}] = \overset{ˉ}{a} (s)$ . Conditional on each first-stage vector, $E [E_{s} ∣ S] = 0$ by centering; [F6] therefore gives $E [E_{s}] = 0$ and $E [(A_{s} - \overset{ˉ}{a} (s)) E_{s}] = 0$ . Expanding the variance definition [F3] and using [F5] now gives $Var ({\hat{μ}}_{s}) = Var (A_{s}) + E [E_{s}^{2}] = Var (A_{s}) + E [Var (E_{s} ∣ S)]$ .

1.2F1F2F4F5F6F7algebra

Conditional on a first-stage vector, expand the within-arm sum of squares using [F4]: $\sum_{i : S_{i} = s} (X_{i} (s) - {\hat{μ}}_{s})^{2} = \sum_{i : S_{i} = s} (a_{i} (s) - A_{s})^{2} + \sum_{i : S_{i} = s} ϵ_{i} (s)^{2} - C_{s} E_{s}^{2} + 2 \sum_{i : S_{i} = s} (a_{i} (s) - A_{s}) ϵ_{i} (s)$ . The last term has conditional mean zero. By expectation linearity [F5] and variance addition [F7], the conditional mean of $\sum_{i} ϵ_{i} (s)^{2} - C_{s} E_{s}^{2}$ is $(1 - 1 / C_{s}) \sum_{i : S_{i} = s} v_{i} (s)$ . Dividing by $C_{s} - 1$ , then averaging over the first-stage partition by [F5] and [F6], gives the expected fixed selected sample variance plus $N^{- 1} \sum_{i} v_{i} (s)$ ; the fixed sample-variance identity and inclusion probabilities in [F2] make these terms $S_{s}^{2}$ and $N^{- 1} \sum_{i} v_{i} (s)$ . Thus $E [s_{X, s}^{2}] = S_{s}^{2} + N^{- 1} \sum_{i} v_{i} (s)$ .

1.3F1F2F3F4algebra

Let $S_{ψ ϕ} = (N - 1)^{- 1} \sum_{i} (a_{i} (ψ) - \overset{ˉ}{a} (ψ)) (a_{i} (ϕ) - \overset{ˉ}{a} (ϕ))$ . If ${\overset{ˉ}{a}}_{ϕ}^{S}$ is the sample mean of the fixed $a_{i} (ϕ)$ values in the $ψ$ -selected groups, the complementary $ϕ$ -group mean equals $(N \overset{ˉ}{a} (ϕ) - C {\overset{ˉ}{a}}_{ϕ}^{S}) / (N - C)$ . Applying the covariance identity in [F2] to both fixed lists on the same $C$ -group sample gives $Cov ({\overset{ˉ}{a}}_{ψ}^{S}, {\overset{ˉ}{a}}_{ϕ}^{S}) = (1 - C / N) S_{ψ ϕ} / C$ ; the complement identity then makes the covariance between the fixed $ψ$ -sample mean and the fixed $ϕ$ -complement mean equal to $- S_{ψ ϕ} / N$ .

2.1F1F2F5F6F7step 1.1algebra

Conditional on a first-stage vector, the selected errors are a finite pairwise-independent family, so [F7] gives $Var (E_{s} ∣ S) = C_{s}^{- 2} \sum_{i : S_{i} = s} v_{i} (s)$ . The selected groups form a uniform $C_{s}$ -element sample, with inclusion probabilities $C_{s} / N$ by [F2]. Averaging the conditional variance over first-stage vectors using [F5] and [F6] yields $E [Var (E_{s} ∣ S)] = C_{s}^{- 2} \sum_{i} (C_{s} / N) v_{i} (s) = \sum_{i} v_{i} (s) / (C_{s} N)$ . The fixed component $Var (A_{s}) = (1 - C_{s} / N) S_{s}^{2} / C_{s}$ by [F2]; step 1.1 then proves the first one-arm variance identity.

2.2F1F2F3F5F6F7step 1.3algebra

Write $A_{Δ} = A_{ψ} - A_{ϕ}$ and $E_{Δ} = E_{ψ} - E_{ϕ}$ . Conditional on the first-stage vector, all selected group errors are centered and independent across groups; [F7] gives $Var (E_{Δ} ∣ S) = C^{- 2} \sum_{i : S_{i} = ψ} v_{i} (ψ) + (N - C)^{- 2} \sum_{i : S_{i} = ϕ} v_{i} (ϕ)$ . By [F6], its covariance with the fixed $A_{Δ}$ is zero and its conditional variance averages over the design to $\sum_{i} v_{i} (ψ) / (C N) + \sum_{i} v_{i} (ϕ) / ((N - C) N)$ , using the inclusion probabilities in [F2]. Expanding the variance definition [F3] with linearity [F5] shows the total contrast variance is the fixed component plus this averaged error variance. The fixed component has variance $(1 - C / N) S_{ψ}^{2} / C + (C / N) S_{ϕ}^{2} / (N - C) + 2 S_{ψ ϕ} / N$ by [F2] and step 1.3. Since $S_{ψ - ϕ}^{2} = S_{ψ}^{2} + S_{ϕ}^{2} - 2 S_{ψ ϕ}$ , this is $S_{ψ}^{2} / C + S_{ϕ}^{2} / (N - C) - S_{ψ - ϕ}^{2} / N$ . Adding the second-stage terms proves the stated contrast-variance identity.

3.1F5step 1.2step 2.2algebra∎

By step 1.2 and expectation linearity [F5], the expected arm-wise variance sum is $S_{ψ}^{2} / C + S_{ϕ}^{2} / (N - C) + \sum_{i} v_{i} (ψ) / (C N) + \sum_{i} v_{i} (ϕ) / ((N - C) N)$ . Comparing with step 2.2 leaves exactly $S_{ψ - ϕ}^{2} / N$ .

Depends on

Used by

Stratified-interference variance estimators are conservative Theorem

Dependency tree · two levels

38 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

Michael G. Hudgens and M. Elizabeth Halloran, Toward Causal Inference With Interference, Appendices A.4 and A.6–A.9 (standard reference, not scraped)