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.

Backdoor adjustment identifies an interventional law

Statement

Assume AC and a finite Markovian SCM on a finite DAG $G$ . Let $A$ and $Y$ be distinct observed vertices, with $A$ a countable-valued treatment and $Y$ an observed standard-Borel outcome. Let $L$ be an observed finite vector of standard-Borel vertices whose vertex set is disjoint from ${A, Y}$ and contains no descendant of $A$ . Fix an atom $a$ with $P (A = a) > 0$ . Suppose (i) $L$ d-separates $A$ and $Y$ in $G_{\underline{A}}$ and (ii) a regular conditional propensity $e_{a} (L) = P (A = a ∣ L)$ is strictly positive $P_{L}$ -almost surely. Then for every Borel set $B$ in the state space of $Y$ , $P (Y^{a} \in B) = \int P (Y \in B ∣ A = a, L = l) P_{L} (d l) .$ The right side depends only on the observed law. Thus the law of $Y^{a}$ is an identifiable estimand on any statistical model consisting of such SCMs with the same observed variables. If $Y$ is real and $Y^{a}$ is integrable, applying the identity to bounded truncations and taking limits gives $E [Y^{a}] = \int E (Y ∣ A = a, L = l) P_{L} (d l) .$ For a continuous treatment, the corresponding regular conditional formula is identified only for $P_{A}$ -almost every $a$ ; this theorem makes no pointwise claim at a null treatment value.

Facts & Assumptions

Given: The SCM, observed variables, atom $a$ , backdoor separation, and positivity stated above.

[F1]

The graph criterion implies $Y^{a} ⊥ A ∣ L$ in the Markovian SCM. The backdoor criterion implies conditional exchangeability

[F2]

Under AC, standard-Borel variables have regular conditional laws and joint laws disintegrate in either declared coordinate direction. Existence of regular conditional distributions for standard borel targets, Disintegration of a joint law on standard borel spaces

[F3]

On ${A = a}$ the structural response agrees with the factual outcome: $Y = Y^{a}$ . Recursive structural causal models on finite DAGs

[F4]

An estimand is identifiable when it is constant over parameter values with the same observational law. Parametric statistical models, Observational equivalence, Estimands on a statistical model, Identifiability of an estimand, Identifiability is constancy on observational classes

Proof

technique · conditional exchangeability, consistency, and positivity give the adjustment functional

Given: The hypotheses in the statement.

1.1F1F2given

By [F1], $Y^{a}$ and $A$ are conditionally independent given $L$ . By [F2] take regular conditional laws of $Y^{a}$ given $L$ and given $(A, L)$ . The conditional-independence identity implies that, for $P_{A, L}$ -almost every $(a^{'}, l)$ , the latter law equals the former law at $l$ . Since $a$ is an atom with $e_{a} (l) > 0$ for $P_{L}$ -almost every $l$ , the measure $P_{L ∣ A = a}$ is equivalent to $P_{L}$ : its density with respect to $P_{L}$ is $e_{a} (l) / P (A = a)$ , which is positive and integrates to one. Hence the conditional-law equality at $A = a$ holds for $P_{L}$ -almost every $l$ .

2.1givenF3step 1.1algebra

On the event $A = a$ , the factual structural recursion and the recursion with the $A$ equation replaced by $a$ agree at $A$ . Induction down the fixed topological order shows that they agree at every descendant, in particular $Y = Y^{a}$ . Therefore the conditional law of $Y^{a}$ given $A = a, L = l$ equals that of $Y$ given $A = a, L = l$ for $P_{L}$ -almost every $l$ . Combining with step 1.1 identifies the conditional law of $Y^{a}$ given $L = l$ with the observed conditional law in the formula.

3.1step 2.1F2F4algebra∎

Disintegrating the joint law of $(Y^{a}, L)$ by [F2] gives $P (Y^{a} \in B) = \int P (Y^{a} \in B ∣ L = l) P_{L} (d l)$ . Substitute the equality from step 2.1 to obtain the displayed formula. If two SCM parameter values induce the same observed law, the integrand kernel and $P_{L}$ agree outside their common null sets; positivity makes those sets null for the target integral. Hence the right side, and so the estimand, is constant on each observational-equivalence class by [F4]. The real-valued expectation formula follows by applying the distribution identity to bounded truncations of $Y$ and using integrability to pass to the limit.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

Judea Pearl, Causal Diagrams for Empirical Research, §3-1, pp. 674–675 (standard reference, not scraped)
Miguel A. Hernán and James M. Robins, Causal Inference: What If, §§7.2–7.3, pp. 87–89 (standard reference, not scraped)