TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Discrete-treatment potential-outcome means are identifiable

Statement

Assume the Axiom of Choice. Let $A$ be a countable discrete set containing treatment versions $0$ and $1$ . On a full-data probability space $(Ω, F, P)$ , let $A$ take values in $A$ , let $L$ take values in a standard-Borel space $L$ (Standard Borel spaces), let $Y$ be the observed real outcome, and let $(Y^{b})_{b \in A}$ be the potential outcomes of Potential outcomes and consistency. For each treatment value $a$ under consideration, assume $Y^{a} \in L^{1} (P)$ , consistency $Y = Y^{A}$ almost surely, conditional exchangeability $σ (Y^{b} : b \in A) ⊥ ⁣ ⁣ ⁣ ⊥ σ (A) ∣ σ (L)$ , and positivity $P (A = a) > 0$ and $E [1_{{A = a}} ∣ σ (L)] > 0$ almost surely. These are assumptions on the full-data law; Choice is required for the stated conditional-expectation classes and regular conditional distributions.

Write $P_{L} (B) = P (L \in B)$ for the target-population law of $L$ . For such an $a$ , define the treatment-stratum probability $P_{a} (C) = P (C \cap {A = a}) / P (A = a)$ for $C \in F$ . Under $P_{a}$ , let $K_{a} (l, d y)$ be a regular conditional law of $Y$ given the standard-Borel random element $L$ , and put $m_{a} (l) = \int y K_{a} (l, d y)$ wherever the absolute integral is finite, with value $0$ on the exceptional set. The suppliers Conditional law given a random element, Existence of regular conditional distributions for standard borel targets, Regular conditional kernels factor through a standard borel conditioning variable, and Conditional integration through a regular conditional law give this construction. Then $m_{a}$ is $P_{L}$ -integrable and is uniquely determined $P_{L}$ -almost everywhere by the observed-data law, and

$E_{P} [Y^{a}] = \int_{L} m_{a} (l) P_{L} (d l) .$

If $L$ is countably discrete, this is

$E_{P} [Y^{a}] = \sum_{l : P (L = l) > 0} E_{P} [Y ∣ A = a, L = l] P (L = l) .$

In this sum, $E [Y ∣ A = a, L = l]$ denotes $E [Y 1_{{A = a, L = l}}] / P (A = a, L = l)$ , whose denominator is positive for each displayed atom.

For the binary contrast, both treatment levels must satisfy positivity. The CATE is then represented $P_{L}$ -almost everywhere by $m_{1} - m_{0}$ , and the ATE is $\int (m_{1} - m_{0}) d P_{L}$ . In the model whose parameters are all full-data laws satisfying these assumptions and whose observation map sends a full-data law to its $(A, L, Y)$ marginal, each $E [Y^{a}]$ is identifiable in the sense of Identifiability of an estimand: it is constant over full-data laws with the same observed-data law.

Facts & Assumptions

Given: Choice; a full-data probability law; countable discrete treatment versions; a standard-Borel covariate $L$ ; integrable potential outcomes for the treatment values considered; consistency; conditional exchangeability; and positivity.

[A1]

The Axiom of Choice is assumed. It supplies the conditional-expectation classes and standard-Borel regular conditional distributions used below. The Axiom of Choice

[F1]

Potential outcomes are indexed by specified treatment versions, the observed outcome is $Y^{A}$ , and consistency is $Y = Y^{A}$ almost surely. Potential outcomes and consistency

[F2]

Conditional exchangeability means the sigma-algebra generated by the potential-outcome family is conditionally independent of the treatment sigma-algebra given $σ (L)$ . Conditional exchangeability of potential outcomes

[F3]

For each treatment $a$ under consideration, $P (A = a) > 0$ and $E [1_{{A = a}} ∣ σ (L)] > 0$ almost surely under the target law. Positivity for discrete treatment

[F4]

The ATE is $E [Y^{1} - Y^{0}]$ , and the CATE is the conditional-expectation class $E [Y^{1} - Y^{0} ∣ σ (L)]$ . Average and conditional average treatment effects

[F5]

A conditional-expectation version is an integrable $σ (L)$ -measurable function satisfying the defining event-integral identities; under Choice its unique almost-sure class is available. Conditional expectation given a sigma algebra, Conditional expectation as an ae class

[F6]

Conditional independence of an integrable real variable and a random element extends the bounded-product identity to any bounded measurable function of that random element. Integrable factorization under conditional independence

[F7]

Under Choice, a real-valued random element has a regular conditional distribution given any sub-sigma-algebra. Existence of regular conditional distributions for standard borel targets

[F8]

For standard-Borel $L$ , a regular conditional distribution given $σ (L)$ factors through an everywhere probability kernel on the value space of $L$ ; this is the conditional law given $L$ . Regular conditional kernels factor through a standard borel conditioning variable, Conditional law given a random element

[F9]

Integrating the identity function against that conditional law, with zero fill where the absolute integral is infinite, gives a real conditional-expectation version under $P_{a}$ . Conditional integration through a regular conditional law

[F10]

Conditional-expectation versions with the same defining event integrals agree almost surely. Conditional expectation is unique almost surely

[F11]

A finite $σ (L)$ -measurable factor can be taken out of conditional expectation when the products are integrable. Taking out what is known

[F12]

Conditional expectation preserves ordinary expectation and is the tower of nested conditional expectations. Basic algebra and order properties of conditional expectation, Tower property of conditional expectation

[F13]

The expectation of a measurable function of a random element is its integral against that random element's law. Law or distribution of a random element, Change of variables for expectation

[F14]

An estimand is identifiable when it is constant on parameter values with the same observed sampling law. Identifiability of an estimand

Proof

technique · Construct each observed treatment-stratum law, transport its conditional mean to the target covariate law by exchangeability and positivity, and then apply the definition of identifiability

1.1A1F3F5construct

Fix a treatment value $a$ satisfying the hypotheses, write $e_{a} = E [1_{{A = a}} ∣ σ (L)]$ , and define $P_{a} (C) = P (C \cap {A = a}) / P (A = a)$ . For every Borel $B \subseteq L$ , the defining event-integral identity for $e_{a}$ gives $P_{a} (L \in B) = E_{P} [1_{{L \in B}} e_{a}] / P (A = a)$ .

1.2A1F1F7F8F9

Under $P_{a}$ , $Y$ is integrable because $Y = Y^{a}$ on ${A = a}$ by consistency and $E_{P_{a}} ∣ Y ∣ = E_{P} [1_{{A = a}} ∣ Y^{a} ∣] / P (A = a) \leq E_{P} ∣ Y^{a} ∣ / P (A = a)$ . By [A1, F7, F8], choose a conditional law $K_{a} (l, d y)$ of $Y$ given $L$ under $P_{a}$ ; [F9] makes its zero-filled integral $m_{a} (L)$ a real integrable version of $E_{P_{a}} [Y ∣ σ (L)]$ .

1.3A1F2F3F6

Put $v_{a} = E_{P} [Y^{a} ∣ σ (L)]$ . Conditional independence in [F2], applied to the coordinate $Y^{a}$ and the bounded indicator $1_{{A = a}}$ , together with [F6], gives $E_{P} [1_{{A = a}} Y^{a} ∣ σ (L)] = e_{a} v_{a}$ almost surely.

2.1step 1.1F3algebra

The covariate laws $P_{a, L}$ and $P_{L}$ are equivalent. Indeed, $P_{L} (B) = 0$ makes the numerator in step 1.1 zero. Conversely, if $P_{L} (B) > 0$ , positivity gives $P (L \in B, e_{a} > 0) > 0$ ; since ${e_{a} > 0} = ⋃_{n \geq 1} {e_{a} \geq 1 / n}$ up to a null set, some $n$ has $P (L \in B, e_{a} \geq 1 / n) > 0$ , so the numerator is positive.

2.2F1F9F11step 1.3

For every $B \in B (L)$ , the defining event integrals of $m_{a} (L)$ under $P_{a}$ , consistency [F1], step 1.3, and the take-out rule [F11] give $E_{P_{a}} [1_{{L \in B}} m_{a} (L)] = E_{P_{a}} [1_{{L \in B}} Y] = E_{P_{a}} [1_{{L \in B}} Y^{a}] = E_{P_{a}} [1_{{L \in B}} v_{a}]$ .

3.1F5F9F10step 2.1step 2.2

By [F5], $v_{a} \in L^{1} (P)$ . Since $P_{a}$ is the law conditional on $A = a$ and $P (A = a) > 0$ , $E_{P_{a}} ∣ v_{a} ∣ = \frac{E_{P} [1_{{A = a}} ∣ v_{a} ∣]}{P (A = a)} \leq \frac{E_{P} ∣ v_{a} ∣}{P (A = a)} < \infty,$ so $v_{a} \in L^{1} (P_{a})$ . Also $m_{a} (L) \in L^{1} (P_{a})$ by [F9]. These are $σ (L)$ -measurable versions under $P_{a}$ with the same event integrals for $Y$ by step 2.2. Uniqueness [F10] gives $m_{a} (L) = v_{a}$ $P_{a}$ -almost surely. Step 2.1 transfers this equality to $P_{L}$ -almost every covariate value, so the integral in the statement is finite and independent of the conditional-law version and its null-set filler.

4.1F12F13step 3.1

By [F12], $E_{P} [v_{a}] = E_{P} [Y^{a}]$ . Since $m_{a} (L) = v_{a}$ $P$ -almost surely on the target covariate law by step 3.1, the change-of-variables identity [F13] yields $\int m_{a} (l) P_{L} (d l) = E_{P} [Y^{a}]$ .

5.1F3F4F9F10F12F13F14step 2.1step 4.1algebra∎

If $L$ is countably discrete, positivity implies $P (A = a, L = l) > 0$ for every atom $l$ with $P (L = l) > 0$ , so the conditional-mean definition in the statement and the version identity [F9] give $m_{a} (l) = E [Y ∣ A = a, L = l]$ there. Splitting the integral in step 4.1 over the countable support proves the displayed sum; its absolute convergence follows from the integrability of $v_{a}$ . For $a = 0, 1$ , linearity of conditional expectation [F12] gives the CATE version $m_{1} (L) - m_{0} (L),$ and subtraction of the two mean identities gives the ATE formula. Equal observed-data laws give the same $P_{L}$ and the same law $Q_{a}$ of $(L, Y)$ conditional on $A = a$ , since $Q_{a} (D) = P ((L, Y) \in D, A = a) / P (A = a)$ for measurable $D \subseteq L \times R$ . Under this common $Q_{a}$ , the conditional means of $Y$ given $L$ have the same defining event integrals, so [F10] makes their measurable versions equal $P_{a, L}$ -almost everywhere. Step 2.1 transfers that equality to $P_{L}$ -almost everywhere. Hence [F14] identifies each $E [Y^{a}]$ and the ATE.

Remarks

This theorem is for discrete treatment values. For continuous $A$ , conditional-law versions are uniquely determined only $P_{A}$ -almost everywhere: any two regular conditional laws agree outside a single conditioning-law null set by Simultaneous ae uniqueness of regular conditional distributions, and factoring through $A$ transfers that qualification to $P_{A}$ . The theorem asserts no pointwise causal effect at a $P_{A}$ -null value; a specified version and any continuity or smoothness assumptions need a separate proof. Conditional exchangeability is generally untestable from the observed law. If positivity fails on a target stratum, that stratum's counterfactual mean is unsupported by the observed treatment data; the theorem does not identify the full target by this formula.

Depends on

Used by

Dependency tree · two levels

70 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

Miguel A. Hernán and James M. Robins, Causal Inference: What If, 2020 (author revision 19 August 2026) (standard reference, not scraped)
Hyunseung Kang, Causal Inference: Identification Under Strong Ignorability, UW–Madison STAT 992 lecture note (standard reference, not scraped)