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

Horvitz–Thompson exposure-specific mean is design-unbiased

Statement

Let $U = {(i, j) : 1 \leq i \leq N, 1 \leq j \leq n_{i}}$ be a fixed population of $M = \sum_{i} n_{i}$ units. Let $Z$ have a known finite assignment law $p$ and fixed potential-outcome schedule satisfying partial interference. Fix an exposure label $d$ for which the mapping in Exposure mappings and exposure consistency is sufficient and $π_{i j} (d) > 0$ for every $(i, j) \in U$ . Then ${\hat{μ}}_{H T} (d) = \frac{1}{M} \sum_{(i, j) \in U} \frac{1 {D_{i j} = d} Y_{i j}^{o b s}}{π_{i j} (d)}$ is an estimator of the finite-population exposure mean $μ (d) = M^{- 1} \sum_{(i, j) \in U} Y_{i j} (d)$ and satisfies $E_{p} [{\hat{μ}}_{H T} (d)] = μ (d)$ . Therefore, for two labels $d, e$ with the same positivity and sufficiency conditions, ${\hat{μ}}_{H T} (d) - {\hat{μ}}_{H T} (e)$ is design-unbiased for $μ (d) - μ (e)$ . Dependence among units' exposures does not affect these expectation identities.

Facts & Assumptions

Given: A finite assignment space $Z$ with weights $p (z)$ summing to one, fixed potential outcomes $Y_{i j} (z_{i})$ , a fixed finite population $U$ , and an exposure label $d$ satisfying the conditions in the Statement.

[F1]

Finite-population potential outcomes under partial interference: $Y_{i j} (z_{i})$ is fixed for each allowed group assignment, and $Y_{i j}^{o b s} = Y_{i j} (Z_{i})$ .

[F2]

Exposure mappings and exposure consistency: $D_{i j} = f_{i j} (Z_{i})$ , $π_{i j} (d) = \sum_{z} p (z) 1 {f_{i j} (z_{i}) = d}$ , and exposure sufficiency means $Y_{i j} (z_{i}) = Y_{i j} (d)$ whenever $f_{i j} (z_{i}) = d$ .

[F3]

Finite probability spaces, outcome weights, events, and event probabilities: the allowed assignments form a finite probability space with event probabilities given by their weights.

[F4]

Expectation of a real random variable on a finite probability space: expectation is the finite weighted sum $E [X] = \sum_{ω \in Ω} X (ω) w (ω)$ .

[F5]

Statistics and estimators: an estimator is a statistic with the target space of its estimand; here the assignment and observed outcomes form the data, and the displayed formula is a real-valued function of that data.

[F6]

Laws of finite sums and finite products: finite sums are additive and scaling distributes over them.

[F7]

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

Proof

1.1F1F2F3F4given

Fix a unit $(i, j)$ . Since $π_{i j} (d) > 0$ , the finite sum for the design expectation of its weighted contribution is defined. By [F1], [F2], [F3], and [F4], $E_{p} ⁣ [\frac{1 {D_{i j} = d} Y_{i j}^{o b s}}{π_{i j} (d)}] = \frac{1}{π_{i j} (d)} \sum_{z \in Z} p (z) 1 {f_{i j} (z_{i}) = d} Y_{i j} (z_{i}) .$ For every term with nonzero indicator, [F2] makes the outcome equal to the fixed value $Y_{i j} (d)$ ; terms with zero indicator vanish.

2.1step 1.1F2givenalgebra

The remaining sum in step 1.1 is $Y_{i j} (d) π_{i j} (d) / π_{i j} (d) = Y_{i j} (d)$ by the definition of $π_{i j} (d)$ and its strict positivity.

3.1step 2.1F3F4F5F6F7givenalgebra

The population has finitely many units. By expectation linearity [F7], distributing the estimator's finite sum and applying step 2.1 to each unit gives $E_{p} [{\hat{μ}}_{H T} (d)] = M^{- 1} \sum_{(i, j) \in U} Y_{i j} (d) = μ (d)$ . The displayed map is a statistic with the same real target space as $μ (d)$ , so it is an estimator by [F5].

4.1step 3.1F4F7givenalgebra∎

Applying step 3.1 to each of $d$ and $e$ and distributing the same finite expectation over their difference by [F7] proves the exposure-contrast identity. The argument used only marginal exposure probabilities, so it requires no independence between units' exposures.

Depends on

Used by

An own-treatment-only exposure map can be misspecified Counterexample
Horvitz–Thompson exposure mean in a two-unit design Example

Dependency tree · two levels

31 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

Peter M. Aronow and Cyrus Samii, Estimating Average Causal Effects Under General Interference, Lemma 4.1 and Appendix A.2 (standard reference, not scraped)