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.

Front-door adjustment identifies an interventional mean

Statement

Assume AC and a finite Markovian SCM with pairwise distinct observed vertices $A, M, Y$ , where $A$ is a countable-valued treatment, $M$ a standard-Borel mediator, and $Y$ a real outcome. Fix an atom $a$ with $P (A = a) > 0$ . Suppose in the full DAG: (i) $M$ lies on every directed path from $A$ to $Y$ ; (ii) $A$ and $M$ are d-separated by the empty set in $G_{\underline{A}}$ ; and (iii) $A$ d-separates $M$ and $Y$ in $G_{\underline{M}}$ . Write $μ_{a} = P (M \in \cdot ∣ A = a)$ and, for every positive-probability treatment atom $a^{'}$ , write $μ_{a^{'}} = P (M \in \cdot ∣ A = a^{'})$ . Assume the nested-law support condition $μ_{a} ≪ μ_{a^{'}} for every a^{'} with P (A = a^{'}) > 0,$ and absolute integrability of the nested conditional means: $\int ⁣ \int E (∣ Y ∣ ∣ M = m, A = a^{'}) P_{A} (d a^{'}) μ_{a} (d m) < \infty .$ Then $E [Y^{a}] = \int P (d m ∣ A = a) \int E (Y ∣ M = m, A = a^{'}) P_{A} (d a^{'}) .$ The right side is determined by the observed law, so the interventional mean is identifiable on any statistical model of SCMs satisfying these assumptions. For a discrete mediator, the support condition says that every mediator value having positive probability under $A = a$ also has positive probability under every positive-probability treatment atom. These are sufficient conditions only. For non-atomic treatment values, regular conditional formulas are determined only $P_{A}$ -almost everywhere; this item makes no pointwise claim at a null treatment value.

Facts & Assumptions

Given: The SCM, three graph conditions, target atom, nested-law support, and absolute-integrability conditions in the statement.

[F1]

The front-door graph conditions give $M^{a} ⊥ A$ , $M ⊥ U_{I_{Y}} ∣ A$ , $M^{a} ⊥ U_{I_{Y}}$ , and $Y^{a} = Y^{M^{a}}$ , where $I_{Y}$ is the finite set of exogenous coordinates defined in the helper. Counterfactual identities under the front-door conditions

[F2]

Standard-Borel variables have regular conditional laws; a disintegration is unique almost everywhere with respect to its conditioning law. Regular conditional distribution, Existence of regular conditional distributions for standard borel targets, Disintegration of a joint law on standard borel spaces, Conditional expectation as a measurable function of the conditioning variable

[F3]

Integration of a jointly measurable function against a probability kernel is measurable, and Fubini applies on the resulting finite product probability spaces. Measure kernel and probability kernel, Measurability of integration against a kernel, Fubini's theorem for L^1 functions on a sigma-finite product

[F4]

Conditional expectation has the tower property; increasing nonnegative approximations and monotone convergence justify the integrable limit operations. Conditional expectation given a sigma algebra, Tower property of conditional expectation, Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral, The Axiom of Choice

[F5]

Identifiability means constancy over parameter values inducing the same observed law. Parametric statistical models, Observational equivalence, Estimands on a statistical model, Identifiability of an estimand, Identifiability is constancy on observational classes

Proof

technique · represent the outcome response by its exogenous coordinates, use conditional independence to recover its observed conditional kernel, and integrate that kernel against the intervention mediator law

Given: The hypotheses in the statement.

1.1F1F2F3F4givenconstruct

Let $I_{Y}$ be as in [F1], let $U_{Y} = \prod_{v \in I_{Y}} E_{v}$ , and let $ν$ be the law of $U_{I_{Y}}$ . Recursion under $d o (M = m)$ gives a jointly measurable function $F : S_{M} \times U_{Y} \to R$ with $Y^{m} = F (m, U_{I_{Y}})$ . Under the factual equations, the same recursion gives $Y = F (M, U_{I_{Y}})$ , because $U_{M}$ enters only the equation for $M$ and all other exogenous coordinates that can affect $Y$ after fixing $M$ lie in $I_{Y}$ . For each supported atom $a^{'}$ , let $ν_{a^{'}} (D) = P (U_{I_{Y}} \in D ∣ A = a^{'})$ . By [F1], conditional independence gives $P ((M, U_{I_{Y}}) \in \cdot ∣ A = a^{'}) = μ_{a^{'}} \otimes ν_{a^{'}} .$ Thus, for every Borel set $B \subseteq R$ , the measurable function $λ_{a^{'}} (m, B) = \int 1_{B} (F (m, u)) ν_{a^{'}} (d u)$ satisfies, for each Borel mediator set $D$ , $P (Y \in B, M \in D ∣ A = a^{'}) = \int_{D} λ_{a^{'}} (m, B) μ_{a^{'}} (d m) .$ It is therefore a regular conditional law of $Y$ given $(M, A = a^{'})$ ; uniqueness in [F2] identifies it with the observed conditional kernel $μ_{a^{'}}$ -almost everywhere. Applying this identity to bounded truncations and then using [F4] gives $\int ∣ F (m, u) ∣ ν_{a^{'}} (d u) = E (∣ Y ∣ ∣ M = m, A = a^{'})$ for $μ_{a^{'}}$ -almost every $m$ .

2.1step 1.1F2F4givenalgebra

For each positive-probability atom $a^{'}$ , the support assumption $μ_{a} ≪ μ_{a^{'}}$ transfers the full-measure identity from step 1.1 to a $μ_{a}$ -full set. The treatment support is countable, so the intersection of these sets is still $μ_{a}$ -full. The integrability hypothesis and the nonnegative identity in step 1.1 imply $\int ⁣ \int ∣ F (m, u) ∣ ν_{a^{'}} (d u) P_{A} (d a^{'}) μ_{a} (d m) < \infty .$ Since $A$ is countable-valued, the law of $U_{I_{Y}}$ is the mixture $ν = \int ν_{a^{'}} P_{A} (d a^{'})$ . Hence $\int ⁣ \int ∣ F (m, u) ∣ ν (d u) μ_{a} (d m) < \infty,$ and the conditional mean kernel has the observed-law representation $\int F (m, u) ν (d u) = \int E (Y ∣ M = m, A = a^{'}) P_{A} (d a^{'})$ for $μ_{a}$ -almost every $m$ .

3.1F1step 2.1F3givenalgebra

By [F1], $Y^{a} = Y^{M^{a}} = F (M^{a}, U_{I_{Y}})$ and $M^{a}$ is independent of $U_{I_{Y}}$ . The integrability from step 2.1 permits Fubini [F3], so $E [Y^{a}] = \int ⁣ \int F (m, u) ν (d u) P_{M^{a}} (d m) .$ Also [F1] gives $M^{a} ⊥ A$ , and consistency on ${A = a}$ gives $P_{M^{a}} = P (M \in \cdot ∣ A = a) = μ_{a}$ . Substituting step 2.1 proves the displayed front-door formula.

4.1givenF2F5step 3.1∎

The right side of the formula uses only the observed law of $(Y, M, A)$ . Conditional-mean versions agree $μ_{a}$ -almost everywhere by step 2.1 and the domination assumption. Therefore any two SCM parameter values with the same observed law give the same target mean, which is identifiability by [F5].

Depends on

Used by

A binary SCM where front-door adjustment works Example

Dependency tree · two levels

73 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-2, pp. 675–676 (standard reference, not scraped)
Miguel A. Hernán and James M. Robins, Causal Inference: What If, Technical Point 7.4, p. 101 (standard reference, not scraped)