SCM.ID
Identification on structural causal models: graphical criteria and theorems (back-door, c-component factorization) stated in SCM terms.
Toolkit 3 core · 13 supporting · 3 submodules Reusable SCM identification toolkit: graphical derivation helpers, frontdoor graph premises, and observational-chain-rule disintegration lemmas. Assumptions 15 core · 8 supporting · 1 submodule Structural assumptions used by SCM identification results, including monotone Boolean mechanisms and finite Boolean-chain example models. Discrete ID 12 core · 25 supporting · 3 submodules Discrete ID support: point-mass algebra, positivity conditions, and the executable checker for finite/discrete identification formulas. GraphicalThms 46 core · 66 supporting · 9 submodules Graphical identification theorems: c-component factorization and related structure results. Density 65 core · 94 supporting · 14 submodules Density-based SCM identification tools: reference measures, observational chain-rule factorization, c-component density factors, and do-law marginal bridges.
Identifiable 7 core · 1 supporting This file defines the query-level interface used by SCM identification theorems. ★ CausalQuery★ Identifiable★ nonIdentifiable_iff★ IdentifiableUnder★ identifiableUnder_mono
Identifiability
This file defines the query-level interface used by SCM identification theorems.
CausalQuery is a functional of an SCM, obsEquiv compares observational
kernels with heterogeneous equality, Identifiable and NonIdentifiable express
whether a query is a functional of the observational law on a fixed SWIG graph,
and IdentifiableUnder adds functional and structural assumption predicates.
The helper theorems expose witness-based non-identifiability and monotonicity
under stronger assumptions.
abbrev CausalQuery reviewed
⚑ flagged
Causalean.SCM.ID
A causal query is a functional of a causal model, producing a value in some type α.
Definition (Lean source)
abbrev CausalQuery (N : Type*) [DecidableEq N] [Fintype N]
(Ω : N → Type*) [∀ n, MeasurableSpace (Ω n)] (α : Type*) :=
SCM N Ω → α
def obsEquiv reviewed
⚑ flagged
Causalean.SCM.ID
Two SCMs are observationally equivalent if their derived observational kernels agree. Because obsKernel has dependent domain/codomain (FixedValues M and ObservedValues M), we use HEq to accommodate two models whose fixed/observed sets may only be propositionally equal.
def Identifiable reviewed
⚑ flagged
Causalean.SCM.ID
A causal query Φ is identifiable from the observational distribution if any two causal models sharing the same SWIG graph and observational kernel must agree on Φ.
Definition (Lean source)
def Identifiable {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*}
(G : SWIGGraph N) (Φ : CausalQuery N Ω α) : Prop :=
∀ M₁ M₂ : SCM N Ω,
M₁.toSWIGGraph = G → M₂.toSWIGGraph = G →
obsEquiv M₁ M₂ →
Φ M₁ = Φ M₂
def NonIdentifiable reviewed
⚑ flagged
Causalean.SCM.ID
A causal query is non-identifiable if there exist two models with the same SWIG graph and observational kernel but different query values.
Definition (Lean source)
def NonIdentifiable {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*}
(G : SWIGGraph N) (Φ : CausalQuery N Ω α) : Prop :=
¬Identifiable G Φ
theorem nonIdentifiable_iff reviewed
⚑ flagged
Causalean.SCM.ID
For a SWIG graph G and a causal query Φ, the causal query is non-identifiable from the observational distribution if and only if there exist two causal models with SWIG graph G and the same observational law that disagree on the value of Φ.
Formal statement
hypotheses
conclusion
NonIdentifiable G Φ
Proof (Lean source)
theorem nonIdentifiable_iff {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)]
{α : Type*} (G : SWIGGraph N) (Φ : CausalQuery N Ω α) :
NonIdentifiable G Φ ↔
∃ M₁ M₂ : SCM N Ω,
M₁.toSWIGGraph = G ∧ M₂.toSWIGGraph = G ∧
obsEquiv M₁ M₂ ∧
Φ M₁ ≠ Φ M₂ := by
simp only [NonIdentifiable, Identifiable, not_forall]
constructor
· intro ⟨M₁, M₂, h1, h2, h3, h4⟩
exact ⟨M₁, M₂, h1, h2, h3, h4⟩
· intro ⟨M₁, M₂, h1, h2, h3, h4⟩
exact ⟨M₁, M₂, h1, h2, h3, h4⟩
def IdentifiableUnder reviewed
⚑ flagged
Causalean.SCM.ID
Identifiability given both functional and structural assumptions.
Definition (Lean source)
def IdentifiableUnder {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*}
(G : SWIGGraph N)
(Af : SCM N Ω → Prop) -- functional assumptions
(As : SCM N Ω → Prop) -- structural assumptions
(Φ : CausalQuery N Ω α) : Prop :=
∀ M₁ M₂ : SCM N Ω,
M₁.toSWIGGraph = G → M₂.toSWIGGraph = G →
Af M₁ → Af M₂ → As M₁ → As M₂ →
obsEquiv M₁ M₂ →
Φ M₁ = Φ M₂
theorem identifiableUnder_mono reviewed
⚑ flagged
Causalean.SCM.ID
Monotonicity of identifiability under assumptions. Fix functional-assumption predicates Af₁, Af₂ and structural-assumption predicates As₁, As₂ on causal models sharing a graph G, together with a causal query Φ. If every model satisfying Af₂ also satisfies Af₁, every model satisfying As₂ also satisfies As₁, and Φ is identifiable under the assumption pair (Af₁, As₁), then Φ is identifiable under (Af₂, As₂): passing to the more restrictive assumption predicates Af₂, As₂ cannot destroy identifiability.
Formal statement
hypotheses
Ω :
N → Type*
∀ n, MeasurableSpace (Ω n)
α :
Type*
G :
Af₁ Af₂ :
SCM N Ω → Prop
As₁ As₂ :
SCM N Ω → Prop
Φ :
CausalQuery N Ω α
hf :
∀ M
if
Af₂ M
then
Af₁ M
hs :
∀ M
if
As₂ M
then
As₁ M
h_id :
IdentifiableUnder G Af₁ As₁ Φ
conclusion
IdentifiableUnder G Af₂ As₂ Φ
Proof (Lean source)
theorem identifiableUnder_mono {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)]
{α : Type*}
(G : SWIGGraph N)
(Af₁ Af₂ : SCM N Ω → Prop)
(As₁ As₂ : SCM N Ω → Prop)
(Φ : CausalQuery N Ω α)
(hf : ∀ M, Af₂ M → Af₁ M)
(hs : ∀ M, As₂ M → As₁ M)
(h_id : IdentifiableUnder G Af₁ As₁ Φ) :
IdentifiableUnder G Af₂ As₂ Φ :=
fun M₁ M₂ hG₁ hG₂ hAf₁ hAf₂ hAs₁ hAs₂ hObs =>
h_id M₁ M₂ hG₁ hG₂ (hf M₁ hAf₁) (hf M₂ hAf₂) (hs M₁ hAs₁) (hs M₂ hAs₂) hObs
1 supporting declaration (lemmas, instances)
-
identifiable_eq_identifiableUnder_truetheorem — Identifiability without additional assumptions is the special case where both Af and As are trivially satisfied.hypothesesconclusionProof (Lean source)
theorem identifiable_eq_identifiableUnder_true {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*} (G : SWIGGraph N) (Φ : CausalQuery N Ω α) : Identifiable G Φ ↔ IdentifiableUnder G (fun _ => True) (fun _ => True) Φ := by simp [Identifiable, IdentifiableUnder]
Overlap 1 core · 0 supporting This file defines the kernel-level overlap condition used by do-calculus identification rules. ★ Rule2JointOverlap
Overlap
This file defines the kernel-level overlap condition used by do-calculus
identification rules. The main predicate, Rule2JointOverlap, requires the
post-intervention marginal on Z.random ∪ W to be absolutely continuous with
respect to the corresponding observational marginal. This continuous-friendly
support condition feeds the kernel-native Rule 2 and the backdoor/frontdoor
identification theorems without imposing pointwise singleton positivity.
def Rule2JointOverlap reviewed
⚑ flagged
Causalean.SCM.ID
Rule 2 joint overlap (canonical, continuous-friendly). Absolute continuity of the (Z.image .random ∪ W)-marginal of (M'.fixSet Z).obsKernel s' w.r.t. the same marginal of M'.obsKernel (fixSetProj s').
Definition (Lean source)
def Rule2JointOverlap (M' : SCM N Ω) (Z : Finset N)
(hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed)
(hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed)
(W : Finset (SWIGNode N))
(hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed)
(s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) :
Prop :=
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'
|>.map (valuesProjection
((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW)))
≪
(M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')
|>.map (valuesProjection hZrW))
BackdoorCriterion 2 core · 0 supporting This file defines the SWIG backdoor criterion used by SCM backdoor identification and proves the Rule 3 marginal-invariance step for the adjustment set. ★ backdoor_rule3_Z_marginal
Backdoor criterion and Rule 3 marginal leg
This file defines the SWIG backdoor criterion used by SCM backdoor
identification and proves the Rule 3 marginal-invariance step for the adjustment
set. The full backdoor completeness and identifiability theorems live in
Causalean/SCM/ID/Backdoor.lean; this module supplies their reusable graphical
criterion and the Z-marginal equality needed in the do-calculus assembly.
def backdoorCriterion reviewed
⚑ flagged
Causalean.SWIGGraph
Backdoor criterion of Z relative to (X, Y) in the SWIG graph G.
Definition (Lean source)
def backdoorCriterion
(X : Finset N)
(hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed)
(hX_fix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed)
(Y Z : Finset (SWIGNode N)) : Prop :=
-- (0) Standard adjustment-set guards.
Z ⊆ G.observed ∧
Disjoint Z Y ∧
Disjoint Z (X.image SWIGNode.random) ∧
-- (i) Non-descendant condition: no z ∈ Z is a descendant of any random D with D ∈ X
(∀ z ∈ Z, ∀ D ∈ X, ¬ G.dag.isAncestor (SWIGNode.random D) z) ∧
-- (ii) d-separation in the splitMono graph (encodes G_{X̲})
(G.splitMono X hX_obs hX_fix).dag.dSep Y (X.image SWIGNode.random)
(Z ∪ X.image SWIGNode.fixed)
theorem backdoor_rule3_Z_marginal reviewed
⚑ flagged
Causalean.SCM
Backdoor Rule-3 leg. Fix a causal model M and a treatment set X whose random copy is observed and whose fixed copy is not already held fixed in M, and a set Z that is observed in M such that no node of Z is a descendant of any treatment random node — the non-descendant clause of the backdoor criterion. Then, at any post-intervention configuration s_post, the Z-marginal of the post-intervention observational law at s_post equals the Z-marginal of the original observational law at the pre-intervention configuration underlying s_post.
Formal statement
hypotheses
M :
SCM N Ω
X :
Finset N
hX_obs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hX_fixed :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
hZ :
Z ⊆ M.observed
h_crit_i :
∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z
s_post :
(M.fixSet X hX_obs hX_fixed).FixedValues
conclusion
((M.fixSet X hX_obs hX_fixed).obsKernel s_post).map (valuesProjection ((SCM.fixSet_observed M X hX_obs hX_fixed).symm ▸ hZ))
= (M.obsKernel (M.fixSetProj X hX_obs hX_fixed s_post)).map (valuesProjection hZ)
Proof (Lean source)
theorem backdoor_rule3_Z_marginal
(M : SCM N Ω) (X : Finset N)
(hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Z : Finset (SWIGNode N)) (hZ : Z ⊆ M.observed)
(h_crit_i : ∀ z ∈ Z, ∀ D ∈ X,
¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z)
(s_post : (M.fixSet X hX_obs hX_fixed).FixedValues) :
((M.fixSet X hX_obs hX_fixed).obsKernel s_post).map
(valuesProjection
((SCM.fixSet_observed M X hX_obs hX_fixed).symm ▸ hZ))
=
(M.obsKernel (M.fixSetProj X hX_obs hX_fixed s_post)).map
(valuesProjection hZ) := by
-- Compose criterion (i) with A2-forward to get Rule 3's `hNoDesc`.
have hNoDesc : ∀ v ∈ (∅ : Finset (SWIGNode N)) ∪ Z, ∀ d ∈ X,
¬ (M.fixSet X hX_obs hX_fixed).dag.isAncestor (SWIGNode.fixed d) v := by
intro v hv d hd hanc
-- A2-forward lifts `.fixed d`-ancestry in `fixSet X` to `.random d`-ancestry in `M`.
have hanc_base :
M.toSWIGGraph.dag.isAncestor (SWIGNode.random d) v :=
SCM.fixSet_isAncestor_fixed_forward M X hX_obs hX_fixed hd hanc
-- Unpack `v ∈ ∅ ∪ Z = Z` and contradict criterion (i).
rw [Finset.empty_union] at hv
exact h_crit_i v hv d hd hanc_base
-- Apply `do_rule3` with `Y_param := ∅`, `W_param := Z`. Rule 3's
-- conclusion projects along `union_subset (∅.empty_subset _) hZ`
-- (indexed by `∅ ∪ Z`); the goal projects along `hZ` (indexed by `Z`).
have _h := SCM.do_rule3 M X hX_obs hX_fixed
(∅ : Finset (SWIGNode N)) Z (empty_subset _) hZ hNoDesc s_post
-- Bridge `ValuesOn (∅ ∪ Z) ↦ ValuesOn Z` via `valuesEquivOfEq`.
-- Post-composing both sides of `_h` with `valuesEquivOfEq hU` and applying
-- `Measure.map_map` produces `valuesProjection` into `Z` on both sides
-- (the composition reduces definitionally).
have hU : (∅ : Finset (SWIGNode N)) ∪ Z = Z := Finset.empty_union _
have hmap := congrArg
(fun μ : Measure (ValuesOn (∅ ∪ Z) (swigΩ Ω)) =>
μ.map (valuesEquivOfEq (Ω := swigΩ Ω) hU)) _h
rw [MeasureTheory.Measure.map_map
(valuesEquivOfEq (Ω := swigΩ Ω) hU).measurable
(measurable_valuesProjection _),
MeasureTheory.Measure.map_map
(valuesEquivOfEq (Ω := swigΩ Ω) hU).measurable
(measurable_valuesProjection _)] at hmap
exact hmap
Backdoor 6 core · 5 supporting The kernel-equality backdoor_completeness is pointwise in the post-intervention slice, hence pointwise in the treatment value t. ★ backdoor_completeness_ae★ backdoor_identifiable_ae
Backdoor identification, a.e. in the treatment value
The kernel-equality backdoor_completeness is pointwise in the post-intervention slice, hence
pointwise in the treatment value t. For non-atomic (continuous) treatment that statement reads
the conditional obsCondKernel on the measure-zero {X = t} slice, where Mathlib's disintegration
representative is not pinned by the observational law — so the pointwise form is too strong.
This file states the honest, regime-uniform version: the identity holds for νX-almost-every
treatment value t, where νX is the observational treatment marginal, under a standard
positivity / overlap assumption P_X × P_Z ≪ P_{X,Z}. Discrete/atomic treatment is the special
case where νX is atomic, so "a.e. t" is "every positive-mass treatment value".
The proof vehicle is the joint identity νX ⊗ₘ Kdo = νX ⊗ₘ Kbd, from which the
a.e. statement follows by ProbabilityTheory.Kernel.ae_eq_of_compProd_eq.
Main declarations
* SCM.treatmentMarginal — observational treatment marginal νX.
* SCM.BackdoorPositivityAE — product-overlap condition P_X × P_Z ≪ P_{X,Z}.
* SCM.doKernelY and SCM.adjustmentKernelY — treatment-indexed do and
backdoor-adjustment kernels for the outcome block.
* SCM.doKernelY_disintegrate and SCM.doKernelY_marginal_const — chain-rule
and Rule-3 reductions used in the proof.
* SCM.backdoor_completeness_ae_compProd — primary joint-kernel completeness.
* SCM.backdoor_completeness_ae — almost-every treatment-value completeness.
* SCM.backdoor_identifiable_ae — cross-SCM almost-every identifiability.
def treatmentMarginal reviewed
⚑ flagged
Causalean.SCM
The observational treatment marginal νX = (M.obsKernel s₀).map π_{X.random}.
Definition (Lean source)
noncomputable def treatmentMarginal (M : SCM N Ω) (X : Finset N)
(hXr : X.image SWIGNode.random ⊆ M.observed) (s0 : M.FixedValues) :
Measure (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) :=
(M.obsKernel s0).map (valuesProjection hXr)
def BackdoorPositivityAE reviewed
⚑ flagged
Causalean.SCM
Joint (product) positivity / overlap at base s₀.
Definition (Lean source)
def BackdoorPositivityAE (M : SCM N Ω) (X : Finset N)
(Z : Finset (SWIGNode N))
(hZ : Z ⊆ M.observed)
(hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed)
(s0 : M.FixedValues) : Prop :=
(((M.treatmentMarginal X (Finset.subset_union_left.trans hXrZ) s0) ⊗ₘ
(const _
((M.obsKernel s0).map (valuesProjection hZ)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ ((M.obsKernel s0).map (valuesProjection hXrZ))
def doKernelY reviewed
⚑ flagged
Causalean.SCM
Post-intervention Y-marginal as a kernel in the treatment value t, at base s₀: t ↦ ((M.fixSet X).obsKernel (s_post s₀ t)).map π_Y.
Definition (Lean source)
noncomputable def doKernelY (M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (s0 : M.FixedValues) :
Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(((M.fixSet X hObs hFix).obsKernel.comap (M.fixSetExtend X hObs hFix s0)
(M.measurable_fixSetExtend X hObs hFix s0)).map
(valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY)))
def adjustmentKernelY reviewed
⚑ flagged
Causalean.SCM
Backdoor-adjustment Y-marginal as a kernel in the treatment value t, at base s₀.
Definition (Lean source)
noncomputable def adjustmentKernelY (M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed)
(s0 : M.FixedValues) :
Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.backdoorAdjustment X hObs hFix Y Z hY hZ).comap
(M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)
theorem backdoor_completeness_ae reviewed
⚑ flagged
Causalean.SCM
Backdoor completeness, a.e. in the treatment value. Fix a causal model M and a treatment set X whose random copy is observed and whose fixed copy is not already held fixed in M, and let Y, Z be observed outcome and adjustment sets, neither of which overlaps the treatment's random nodes, satisfying the backdoor criterion relative to (X,Y). Given a base configuration s0 at which overlap holds along every post-intervention slice and the product of the observational treatment and adjustment-set marginals is absolutely continuous with respect to their joint observational law, then for almost every treatment value t under the observational treatment marginal, the post-intervention outcome distribution at t equals the backdoor-adjustment functional evaluated at t.
Formal statement
hypotheses
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hZ :
Z ⊆ M.observed
h_bd :
M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z
hDisj_YXr :
Disjoint Y (X.image SWIGNode.random)
hDisj_XrZ :
Disjoint (X.image SWIGNode.random) Z
s0 :
M.FixedValues
hOverlap :
∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s
hPositivity :
M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0
conclusion
∀ᵐ t ∂(M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0),
M.doKernelY X hObs hFix Y hY s0 t = M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t
Proof (Lean source)
theorem backdoor_completeness_ae
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y Z : Finset (SWIGNode N))
(hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed)
(h_bd : M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z)
(hDisj_YXr : Disjoint Y (X.image SWIGNode.random))
(hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z)
(s0 : M.FixedValues)
(hOverlap : ∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix Z
(union_subset (Finset.image_subset_iff.mpr hObs) hZ) s)
(hPositivity : M.BackdoorPositivityAE X Z hZ
(union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0) :
∀ᵐ t ∂(M.treatmentMarginal X (Finset.subset_union_left.trans
(union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0),
M.doKernelY X hObs hFix Y hY s0 t
= M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t := by
have hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed :=
union_subset (Finset.image_subset_iff.mpr hObs) hZ
have hXr : X.image SWIGNode.random ⊆ M.observed :=
Finset.subset_union_left.trans hXrZ
haveI : IsFiniteMeasure (M.treatmentMarginal X hXr s0) := by
unfold treatmentMarginal
exact (M.obsKernel s0).isFiniteMeasure_map _
exact ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
(M.backdoor_completeness_ae_compProd X hObs hFix Y Z hY hZ h_bd
hDisj_YXr hDisj_XrZ s0 hOverlap hPositivity)
theorem backdoor_identifiable_ae reviewed
⚑ flagged
Causalean.SCM
Backdoor identifiability, a.e. in the treatment value (cross-SCM corollary). Fix two causal models M₁, M₂ that share the same SWIG graph and the same observational kernel, with base configurations that agree under this shared identification. Fix a treatment set X valid in both models and disjoint outcome/adjustment sets Y, Z that are observed in both models and disjoint from the treatment's random nodes, such that Z satisfies the backdoor criterion for (X,Y) in each model separately, with overlap holding along every post-intervention slice in each model and product positivity of the observational treatment and adjustment-set marginals holding in each model. Then for almost every treatment value t under the shared observational treatment marginal, the post-intervention outcome distribution computed in M₁ at t equals the one computed in M₂ at t, since each model individually satisfies backdoor completeness and the two share the same graph and observational kernel.
Formal statement
hypotheses
M₁ M₂ :
SCM N Ω
h_swig :
M₁.toSWIGGraph = M₂.toSWIGGraph
X :
Finset N
hObs₁ :
∀ D ∈ X, SWIGNode.random D ∈ M₁.observed
hFix₁ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed
hObs₂ :
∀ D ∈ X, SWIGNode.random D ∈ M₂.observed
hFix₂ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed
hY₁ :
Y ⊆ M₁.observed
hZ₁ :
Z ⊆ M₁.observed
hY₂ :
Y ⊆ M₂.observed
hZ₂ :
Z ⊆ M₂.observed
h_bd₁ :
M₁.toSWIGGraph.backdoorCriterion X hObs₁ hFix₁ Y Z
h_bd₂ :
M₂.toSWIGGraph.backdoorCriterion X hObs₂ hFix₂ Y Z
hDisj_YXr :
Disjoint Y (X.image SWIGNode.random)
hDisj_XrZ :
Disjoint (X.image SWIGNode.random) Z
s0₁ :
M₁.FixedValues
s0₂ :
M₂.FixedValues
hOverlap₁ :
∀ s : (M₁.fixSet X hObs₁ hFix₁).FixedValues,
Rule2JointOverlap M₁ X hObs₁ hFix₁ Z (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s
hOverlap₂ :
∀ s : (M₂.fixSet X hObs₂ hFix₂).FixedValues,
Rule2JointOverlap M₂ X hObs₂ hFix₂ Z (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s
hPositivity₁ :
M₁.BackdoorPositivityAE X Z hZ₁ (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s0₁
hPositivity₂ :
M₂.BackdoorPositivityAE X Z hZ₂ (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s0₂
h_obs :
HEq M₁.obsKernel M₂.obsKernel
h_s0 :
HEq s0₁ s0₂
conclusion
(M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁)
=ᵐ[M₁.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁)) s0₁] (M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂)
Proof (Lean source)
theorem backdoor_identifiable_ae
(M₁ M₂ : SCM N Ω)
(h_swig : M₁.toSWIGGraph = M₂.toSWIGGraph)
(X : Finset N) (Y Z : Finset (SWIGNode N))
(hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed)
(hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed)
(hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed)
(hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed)
(hY₁ : Y ⊆ M₁.observed) (hZ₁ : Z ⊆ M₁.observed)
(hY₂ : Y ⊆ M₂.observed) (hZ₂ : Z ⊆ M₂.observed)
(h_bd₁ : M₁.toSWIGGraph.backdoorCriterion X hObs₁ hFix₁ Y Z)
(h_bd₂ : M₂.toSWIGGraph.backdoorCriterion X hObs₂ hFix₂ Y Z)
(hDisj_YXr : Disjoint Y (X.image SWIGNode.random))
(hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z)
(s0₁ : M₁.FixedValues) (s0₂ : M₂.FixedValues)
(hOverlap₁ : ∀ s : (M₁.fixSet X hObs₁ hFix₁).FixedValues,
Rule2JointOverlap M₁ X hObs₁ hFix₁ Z
(union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s)
(hOverlap₂ : ∀ s : (M₂.fixSet X hObs₂ hFix₂).FixedValues,
Rule2JointOverlap M₂ X hObs₂ hFix₂ Z
(union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s)
(hPositivity₁ : M₁.BackdoorPositivityAE X Z hZ₁
(union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s0₁)
(hPositivity₂ : M₂.BackdoorPositivityAE X Z hZ₂
(union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s0₂)
(h_obs : HEq M₁.obsKernel M₂.obsKernel)
(h_s0 : HEq s0₁ s0₂) :
(M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁)
=ᵐ[M₁.treatmentMarginal X (Finset.subset_union_left.trans
(union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁)) s0₁]
(M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂) := by
-- Destructure both SCMs and `cases h_swig` to align the SWIGGraph-derived
-- type indices (FixedValues, observed, fixSet, treatmentMarginal); then the
-- base points `s0₁ s0₂` and obsKernels coincide.
obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁,
fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩,
eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁
obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂,
fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩,
eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂
cases h_swig
-- After `cases h_swig` the SWIGGraph fields agree definitionally, so the two
-- `FixedValues` types coincide and `h_s0` is an equality of base points.
-- The two SCMs still differ in their non-SWIGGraph fields, so we keep them as
-- distinct structure literals and use `h_obs` as a rewrite (obsKernel is a
-- *derived* def, not a structure field, hence not `cases`-able).
cases h_s0
have hXr₁ : X.image SWIGNode.random ⊆ observed₁ :=
Finset.image_subset_iff.mpr hObs₁
have hXr₂ : X.image SWIGNode.random ⊆ observed₁ :=
Finset.image_subset_iff.mpr hObs₂
-- Step 1: do-side ≡ adjustment-side on each SCM, a.e.
have hc1 := backdoor_completeness_ae
⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩
X hObs₁ hFix₁ Y Z hY₁ hZ₁ h_bd₁ hDisj_YXr hDisj_XrZ
s0₁ hOverlap₁ hPositivity₁
have hc2 := backdoor_completeness_ae
⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩
X hObs₂ hFix₂ Y Z hY₂ hZ₂ h_bd₂ hDisj_YXr hDisj_XrZ
s0₁ hOverlap₂ hPositivity₂
-- Step 2: cross-SCM invariance of the adjustment kernel.
have hinv :
(⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ :
SCM N Ω).adjustmentKernelY X hObs₁ hFix₁ Y Z hY₁ hZ₁ s0₁
= (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ :
SCM N Ω).adjustmentKernelY X hObs₂ hFix₂ Y Z hY₂ hZ₂ s0₁ := by
rw [adjustmentKernelY, adjustmentKernelY]
have hbd := backdoorAdjustment_invariant
(⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ :
SCM N Ω)
(⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ :
SCM N Ω)
rfl h_obs X hObs₁ hFix₁ hObs₂ hFix₂ Y Z hY₁ hZ₁ hY₂ hZ₂
rw [eq_of_heq hbd]
rfl
-- Step 3: the treatment marginals coincide (same obsKernel, same base, same
-- projection index).
have hνX :
(⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ :
SCM N Ω).treatmentMarginal X hXr₁ s0₁
= (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁,
foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ :
SCM N Ω).treatmentMarginal X hXr₂ s0₁ := by
rw [treatmentMarginal, treatmentMarginal, eq_of_heq h_obs]
-- Assemble: doKernelY M₁ ≡ adjY M₁ = adjY M₂ ≡ doKernelY M₂.
refine Filter.EventuallyEq.trans hc1 ?_
rw [hinv, hνX]
exact Filter.EventuallyEq.symm hc2
5 supporting declarations (lemmas, instances)
-
instIsFiniteKernelDoKernelYinstance — The treatment-indexed post-intervention Y-marginal kernel is finite.instance instIsFiniteKernelDoKernelY (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (s0 : M.FixedValues) : IsFiniteKernel (M.doKernelY X hObs hFix Y hY s0) := by rw [SCM.doKernelY]; infer_instance -
instIsFiniteKernelAdjustmentKernelYinstance — The treatment-indexed backdoor-adjustment Y-marginal kernel is finite.instance instIsFiniteKernelAdjustmentKernelY (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (s0 : M.FixedValues) : IsFiniteKernel (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) := by rw [SCM.adjustmentKernelY]; infer_instance -
doKernelY_disintegratetheorem — Treatment-indexed chain rule. At treatment value t, the post-do(X) Y-marginal kernel disintegrates through Z: it is the conditional Y ∣ Z (under do(X)) composed with the post-do(X) Z-marginal kernel. The doKernelY-level form of obsKernel_map_eq_obsCondKernel_comp.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhY :Y ⊆ M.observedhZ :Z ⊆ M.observeds0 :M.FixedValuesconclusionM.doKernelY X hObs hFix Y hY s0 t= ((M.fixSet X hObs hFix).obsCondKernel Y Z ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY) ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)).sectR (M.fixSetExtend X hObs hFix s0 t) ∘ₘ M.doKernelY X hObs hFix Z hZ s0 tProof (Lean source)
theorem doKernelY_disintegrate (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsCondKernel Y Z ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY) ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)).sectR (M.fixSetExtend X hObs hFix s0 t) ∘ₘ M.doKernelY X hObs hFix Z hZ s0 t := by have hY' : M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] have hZ' : M.doKernelY X hObs hFix Z hZ s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] rw [hY', hZ'] exact SCM.obsKernel_map_eq_obsCondKernel_comp (M.fixSet X hObs hFix) Y Z _ _ _ -
doKernelY_marginal_consttheorem — Treatment-indexed Rule 3 (marginal invariance). If no X-copy is an ancestor of any Z-node, the post-do(X) Z-marginal kernel is constant in the treatment value and equals the observational Z-marginal at base s₀. The doKernelY-level form of backdoor_rule3_Z_marginal.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhZ :Z ⊆ M.observedh_noanc :∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) zs0 :M.FixedValuesconclusionM.doKernelY X hObs hFix Z hZ s0 t = (M.obsKernel s0).map (valuesProjection hZ)Proof (Lean source)
theorem doKernelY_marginal_const (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Z : Finset (SWIGNode N)) (hZ : Z ⊆ M.observed) (h_noanc : ∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.doKernelY X hObs hFix Z hZ s0 t = (M.obsKernel s0).map (valuesProjection hZ) := by have hZ' : M.doKernelY X hObs hFix Z hZ s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] rw [hZ'] have hR3 := SCM.backdoor_rule3_Z_marginal M X hObs hFix Z hZ h_noanc (M.fixSetExtend X hObs hFix s0 t) rw [SCM.fixSetProj_fixSetExtend] at hR3 exact hR3 -
backdoor_completeness_ae_compProdtheorem — Joint (compProd) completeness — primary form.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhY :Y ⊆ M.observedhZ :Z ⊆ M.observed_h_bd :M.toSWIGGraph.backdoorCriterion X hObs hFix Y ZhDisj_YXr :Disjoint Y (X.image SWIGNode.random)hDisj_XrZ :Disjoint (X.image SWIGNode.random) Zs0 :M.FixedValueshOverlap :∀ s : (M.fixSet X hObs hFix).FixedValues,Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s_hPositivity :M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0conclusion(M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)= (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0)Proof (Lean source)
theorem backdoor_completeness_ae_compProd (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (_h_bd : M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z) (hDisj_YXr : Disjoint Y (X.image SWIGNode.random)) (hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z) (s0 : M.FixedValues) (hOverlap : ∀ s : (M.fixSet X hObs hFix).FixedValues, Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s) (_hPositivity : M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0) : (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0) = (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) := by have hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := union_subset (Finset.image_subset_iff.mpr hObs) hZ have hXr : X.image SWIGNode.random ⊆ M.observed := Finset.subset_union_left.trans hXrZ -- Abbreviations. set sT := fun t => M.fixSetExtend X hObs hFix s0 t with hsT set hZ_post : Z ⊆ (M.fixSet X hObs hFix).observed := (SCM.fixSet_observed M X hObs hFix).symm ▸ hZ with hZpost_def set hY_post : Y ⊆ (M.fixSet X hObs hFix).observed := (SCM.fixSet_observed M X hObs hFix).symm ▸ hY with hYpost_def -- μZ = (M.obsKernel s0).map projZ, the observational Z-marginal at base s0. set μZ := (M.obsKernel s0).map (valuesProjection hZ) with hμZ -- ============================================================ -- Reduction 1 (chain rule + Rule 3): the do-side Y-marginal kernel at t. -- doKernelY t = (sectR (fixSet X).obsCondKernel (sT t)) ∘ₘ μZ -- ============================================================ -- Reduction 1 (chain rule + Rule 3) is now packaged in the treatment-indexed -- do-calculus lemmas `doKernelY_disintegrate` and `doKernelY_marginal_const`. have hLHS : ∀ t, M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsCondKernel Y Z hY_post hZ_post).sectR (sT t) ∘ₘ μZ := by intro t rw [doKernelY_disintegrate M X hObs hFix Y Z hY hZ s0 t, doKernelY_marginal_const M X hObs hFix Z hZ _h_bd.2.2.2.1 s0 t] -- ============================================================ -- Reduction 2 (unfold backdoorAdjustment): the adjustment-side kernel at t. -- adjustmentKernelY t = (sectR condPost (sT t)) ∘ₘ μZ -- where condPost z = M.obsCondKernel Y (Xr∪Z) (s0, fillZrW (sT t) z). -- ============================================================ -- The `condPost` kernel appearing in `backdoorAdjustment`. set hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := hXrZ with hXZ_def set condPost : Kernel ((M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY hXZ).comap (fun p : (M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω) => (M.fixSetProj X hObs hFix p.1, M.fillZrW X hObs hFix Z p.1 p.2)) (prodMk ((M.measurable_fixSetProj X hObs hFix).comp measurable_fst) (M.measurable_fillZrW_prod X hObs hFix Z)) with hcondPost_def haveI : IsMarkovKernel (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY hXZ) := by unfold SCM.obsCondKernel; infer_instance haveI : IsMarkovKernel condPost := by rw [hcondPost_def]; infer_instance have hRHS : ∀ t, M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = condPost.sectR (sT t) ∘ₘ μZ := by intro t -- adjustmentKernelY t = backdoorAdjustment (sT t). have hadj : M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = M.backdoorAdjustment X hObs hFix Y Z hY hZ (sT t) := by rw [SCM.adjustmentKernelY, ProbabilityTheory.Kernel.comap_apply] rw [hadj] -- Unfold backdoorAdjustment body to ((zMarginalPost ⊗ₖ condPost).map snd) (sT t). change ((((M.obsKernel.map (valuesProjection hZ)).comap (M.fixSetProj X hObs hFix) (M.measurable_fixSetProj X hObs hFix)) ⊗ₖ condPost).map snd) (sT t) = condPost.sectR (sT t) ∘ₘ μZ rw [compProd_map_snd_apply, ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), SCM.fixSetProj_fixSetExtend, ← hμZ] -- ============================================================ -- a.e. Rule 2 on the product νX ⊗ₘ const μZ. -- ============================================================ -- νX = treatmentMarginal = (M.obsKernel s0).map projXr. set νX := M.treatmentMarginal X hXr s0 with hνX have hνX_eq : νX = (M.obsKernel s0).map (valuesProjection hXr) := by rw [hνX, SCM.treatmentMarginal] -- The product measure λ = νX ⊗ₘ const μZ. set lam := νX ⊗ₘ const _ μZ with hlam -- Finiteness instances. haveI : IsFiniteMeasure νX := by rw [hνX_eq]; exact (M.obsKernel s0).isFiniteMeasure_map _ haveI : IsFiniteMeasure μZ := by rw [hμZ]; exact (M.obsKernel s0).isFiniteMeasure_map _ -- Apply the a.e. Rule 2 with Z := X, W := Z. have hPos_ae : (((M.obsKernel s0).map (valuesProjection hXr) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M.obsKernel s0).map (valuesProjection hXrZ)) := _hPositivity -- Rule 2 straight from the backdoor criterion: the applicator derives the -- d-separation + non-descendance premises internally. have hR2 := SCM.backdoor_rule2_ae M X hObs hFix Y Z hY hZ hXr hXrZ hDisj_YXr hDisj_XrZ _h_bd s0 hOverlap hPos_ae haveI hdoKfin : IsFiniteKernel (M.doKernelY X hObs hFix Y hY s0) := by rw [SCM.doKernelY]; infer_instance haveI hadjSF : IsSFiniteKernel (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) := by rw [SCM.adjustmentKernelY, SCM.backdoorAdjustment]; infer_instance set liftTZ : ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω) → (M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω) := fun p => (sT p.1, p.2) with hliftTZ_def have hliftTZ_meas : Measurable liftTZ := by rw [hliftTZ_def, hsT] exact prodMk ((M.measurable_fixSetExtend X hObs hFix s0).comp measurable_fst) measurable_snd set fL : Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := ((M.fixSet X hObs hFix).obsCondKernel Y Z hY_post hZ_post).comap liftTZ hliftTZ_meas with hfL_def set fR : Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := condPost.comap liftTZ hliftTZ_meas with hfR_def have hL : ∀ t, M.doKernelY X hObs hFix Y hY s0 t = (fL.sectR t) ∘ₘ μZ := by intro t exact hLHS t have hR : ∀ t, M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = (fR.sectR t) ∘ₘ μZ := by intro t exact hRHS t have hae : ∀ᵐ p ∂(νX ⊗ₘ const (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) μZ), fL p = fR p := by rw [hνX_eq, hμZ] filter_upwards [hR2] with p hp simpa [hfL_def, hfR_def, hliftTZ_def, hcondPost_def, hsT, ProbabilityTheory.Kernel.comap_apply, SCM.fixSetProj_fixSetExtend, SCM.fillZrW_fixSetExtend] using hp exact compProd_eq_of_inner_ae νX μZ (M.doKernelY X hObs hFix Y hY s0) (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) fL fR hL hR hae
Query 8 core · 1 supporting This file contains the lightweight query-level API shared by ID soundness theorems. ★ interventionalQuery_eq_doKernelY_of_valid★ interventionalQueryValid_iff_of_toSWIGGraph_eq
Total interventional query API
This file contains the lightweight query-level API shared by ID soundness
theorems. It deliberately avoids importing the Tian/c-factor ID skeleton, so
modules can state and prove base cases for interventionalQuery without
depending on the full density recovery stack.
def swigValueNonempty reviewed
⚑ flagged
Causalean.SCM.ID
Every random or fixed SWIG-node value space is nonempty when every base-node value space is nonempty.
Definition (Lean source)
noncomputable def swigValueNonempty [∀ n, Nonempty (Ω n)]
(w : SWIGNode N) : Nonempty (swigΩ Ω w) := by
cases w <;> infer_instance
def valuesOnNonempty reviewed
⚑ flagged
Causalean.SCM.ID
A finite coordinate product of SWIG-node value spaces is nonempty when all base-node value spaces are nonempty.
Definition (Lean source)
noncomputable def valuesOnNonempty [∀ n, Nonempty (Ω n)]
(Y : Finset (SWIGNode N)) :
Nonempty (ValuesOn Y (swigΩ Ω)) :=
⟨fun y => Classical.choice (swigValueNonempty (Ω := Ω) y.val)⟩
def defaultInterventionalKernel reviewed
⚑ flagged
Causalean.SCM.ID
This fixed fallback kernel is used only outside the standard identification query domain.
Definition (Lean source)
noncomputable def defaultInterventionalKernel [∀ n, Nonempty (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) :
Kernel
(ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) := by
classical
letI : Nonempty (ValuesOn Y (swigΩ Ω)) :=
valuesOnNonempty (Ω := Ω) Y
exact const _
(dirac (Classical.choice inferInstance))
def standardFixedValues reviewed
⚑ flagged
Causalean.SCM.ID
A standard structural causal model has a canonical fixed-value assignment.
Definition (Lean source)
noncomputable def standardFixedValues (M : SCM N Ω)
(hM : M.isStandard) : M.FixedValues :=
fun d => elim (by
have hempty : M.fixed = ∅ := hM
have hd : d.val ∈ (∅ : Finset (SWIGNode N)) := by
simpa [hempty] using d.property
exact notMem_empty d.val hd)
def interventionalQueryValid reviewed
⚑ flagged
Causalean.SCM.ID
This predicate states when the interventional query is in its meaningful standard-model branch.
Definition (Lean source)
def interventionalQueryValid
(X : Finset N) (Y : Finset (SWIGNode N))
(M : SCM N Ω) : Prop :=
(∀ D ∈ X, SWIGNode.random D ∈ M.observed) ∧
(∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) ∧
(Y ⊆ M.observed) ∧ M.isStandard
def interventionalQuery reviewed
⚑ flagged
Causalean.SCM.ID
The interventional query returns the post-intervention outcome law as a kernel indexed by treatment values.
Definition (Lean source)
noncomputable def interventionalQuery [∀ n, Nonempty (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) :
CausalQuery N Ω
(Kernel
(ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω))) := by
classical
exact fun M =>
if h : (∀ D ∈ X, SWIGNode.random D ∈ M.observed) ∧
(∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) ∧
(Y ⊆ M.observed) ∧ M.isStandard then
M.doKernelY X h.1 h.2.1 Y h.2.2.1
(standardFixedValues M h.2.2.2)
else
defaultInterventionalKernel X Y
lemma interventionalQuery_eq_doKernelY_of_valid reviewed
⚑ flagged
Causalean.SCM.ID
For treatment nodes X and outcome nodes Y satisfying the well-formedness conditions for a valid interventional query in a model M, the total interventional query evaluated at M equals the post-intervention outcome-marginal kernel doKernelY.
Formal statement
hypotheses
conclusion
interventionalQuery (Ω := Ω) X Y M
= M.doKernelY X h.1 h.2.1 Y h.2.2.1 (standardFixedValues M h.2.2.2)
Proof (Lean source)
lemma interventionalQuery_eq_doKernelY_of_valid [∀ n, Nonempty (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) (M : SCM N Ω)
(h : interventionalQueryValid X Y M) :
interventionalQuery (Ω := Ω) X Y M =
M.doKernelY X h.1 h.2.1 Y h.2.2.1
(standardFixedValues M h.2.2.2) := by
classical
rw [interventionalQuery]
exact dif_pos (by simpa [interventionalQueryValid] using h)
theorem interventionalQueryValid_iff_of_toSWIGGraph_eq reviewed
⚑ flagged
Causalean.SCM.ID
Well-formedness invariance under matching SWIG graphs. For an intervention target set X and outcome set Y, if two structural causal models M₁, M₂ have the same SWIG graph, then they agree on whether the total interventional query for X, Y is well formed.
Formal statement
hypotheses
conclusion
interventionalQueryValid X Y M₁ ↔ interventionalQueryValid X Y M₂
Proof (Lean source)
theorem interventionalQueryValid_iff_of_toSWIGGraph_eq
(X : Finset N) (Y : Finset (SWIGNode N))
(M₁ M₂ : SCM N Ω)
(hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) :
interventionalQueryValid X Y M₁ ↔ interventionalQueryValid X Y M₂ := by
have ho : M₁.observed = M₂.observed := congrArg SWIGGraph.observed hsg
have hf : M₁.fixed = M₂.fixed := congrArg SWIGGraph.fixed hsg
unfold interventionalQueryValid isStandard
rw [ho, hf, hsg]
1 supporting declaration (lemmas, instances)
-
interventionalQuery_eq_default_of_not_validlemma — Outside the well-formed branch, the total interventional query is the fixed fallback kernel.hypothesesconclusioninterventionalQuery (Ω := Ω) X Y M = defaultInterventionalKernel (Ω := Ω) X YProof (Lean source)
lemma interventionalQuery_eq_default_of_not_valid [∀ n, Nonempty (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (M : SCM N Ω) (h : ¬ interventionalQueryValid X Y M) : interventionalQuery (Ω := Ω) X Y M = defaultInterventionalKernel (Ω := Ω) X Y := by classical rw [interventionalQuery] exact dif_neg (by simpa [interventionalQueryValid] using h)
DoLawTransport 2 core · 0 supporting The post-intervention Y-marginal kernel doKernelY is built from the do-observational law (M.fixSet X).obsKernel by a comap (extend the fixed slice by the treatment value) followed by a map (project to the outcomes Y): do ★ doKernelY_eq_of_doObsKernel_heq
Structural transport of the do-observational law to doKernelY
The post-intervention Y-marginal kernel doKernelY is built from the
do-observational law (M.fixSet X).obsKernel by a comap (extend the fixed
slice by the treatment value) followed by a map (project to the outcomes Y):
doKernelY M X … Y … s₀ = ((M.fixSet X).obsKernel.comap (fixSetExtend s₀)).map π_Y.
The comap/map data (fixSetExtend, the Y-projection) and the
intermediate value-space types depend on M only through its SWIG graph
(observed, fixed, which fixSet preserves/enlarges structurally) and the base
slice s₀. Therefore two models sharing a SWIG graph whose do-observational laws
agree produce the same doKernelY.
This isolates the genuine identification content — that the do-observational laws
agree — from the purely structural transport performed here. The identification
content is discharged elsewhere (the Tian g-formula in
GraphicalThms/DoGFormula and its recursive/discrete soundness layers); this file
is graph/measure bookkeeping only and makes no appeal to idSucceeds or any
reference measure.
def doObsKernelYMarginal reviewed
⚑ flagged
Causalean.SCM.ID
The Y-marginal of the do-observational law: push (M.fixSet X).obsKernel forward along the projection to the outcome coordinates Y. This is the only part of the do-law that the post-intervention Y-marginal kernel doKernelY depends on — doKernelY is this marginal, reindexed in the treatment value by the comap extension. Crucially this is the identifiable object: the full do-law over all observed nodes is not a functional of the observational law, but its Y-marginal (more precisely its An_{G_X}(Y)-marginal, of which this is a further projection) is.
Definition (Lean source)
noncomputable def doObsKernelYMarginal
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) :
Kernel (M.fixSet X hObs hFix).FixedValues
(ValuesOn Y (swigΩ Ω)) :=
(M.fixSet X hObs hFix).obsKernel.map
(valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY))
theorem doKernelY_eq_of_doObsKernel_heq reviewed
⚑ flagged
Causalean.SCM.ID
Structural transport. Fix two causal models that share the same underlying SWIG graph, together with a treatment set X that is a valid intervention in the first model — every node of X is observed and not already fixed there and likewise valid in the second model, and an outcome set Y that is observed in the first model and observed in the second. If the two models' base fixed-value slices coincide and their Y-marginals of the do-observational law agree, up to the type-level identification the shared graph provides, then the resulting post-intervention Y-marginal kernels doKernelY agree at that shared base slice.
Formal statement
hypotheses
X :
Finset N
M₁ M₂ :
SCM N Ω
hsg :
M₁.toSWIGGraph = M₂.toSWIGGraph
hObs₁ :
∀ D ∈ X, SWIGNode.random D ∈ M₁.observed
hFix₁ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed
hObs₂ :
∀ D ∈ X, SWIGNode.random D ∈ M₂.observed
hFix₂ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed
hY₁ :
Y ⊆ M₁.observed
hY₂ :
Y ⊆ M₂.observed
s0₁ :
M₁.FixedValues
s0₂ :
M₂.FixedValues
hs0 :
HEq s0₁ s0₂
hdoobsY :
conclusion
M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁ = M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂
Proof (Lean source)
theorem doKernelY_eq_of_doObsKernel_heq
(X : Finset N) (Y : Finset (SWIGNode N))
(M₁ M₂ : SCM N Ω)
(hsg : M₁.toSWIGGraph = M₂.toSWIGGraph)
(hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed)
(hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed)
(hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed)
(hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed)
(hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed)
(s0₁ : M₁.FixedValues) (s0₂ : M₂.FixedValues) (hs0 : HEq s0₁ s0₂)
(hdoobsY :
HEq (doObsKernelYMarginal M₁ X hObs₁ hFix₁ Y hY₁)
(doObsKernelYMarginal M₂ X hObs₂ hFix₂ Y hY₂)) :
M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁
= M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂ := by
obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁,
fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩,
eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁
obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂,
fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩,
eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂
cases hsg
have hs0_eq : s0₁ = s0₂ := eq_of_heq hs0
subst hs0_eq
have hmapY_eq : _ = _ := eq_of_heq hdoobsY
unfold SCM.doKernelY doObsKernelYMarginal at *
ext t A hA
-- Peel `map`/`comap` to the fibre, then fold the fibre back into `obsKernel.map π_Y`
-- so the marginal hypothesis `hmapY_eq` rewrites both sides to the same kernel.
rw [ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _),
ProbabilityTheory.Kernel.comap_apply,
ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _),
ProbabilityTheory.Kernel.comap_apply,
← ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _),
← ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _),
hmapY_eq]
-- Both sides are now the same `Y`-marginal kernel; the residual fibre arguments
-- differ only in proof-irrelevant SWIG-graph proof fields.
congr 1
Adjustment 4 core · 3 supporting This file defines graph-level adjustment functionals for backdoor and frontdoor identification. ★ backdoorAdjustment_invariant★ frontdoorAdjustment_invariant
Adjustment Functionals
This file defines graph-level adjustment functionals for backdoor and frontdoor identification. These functionals express post-intervention outcome distributions in terms of observational kernels, enabling single-model completeness arguments to be combined with cross-model invariance statements. It also proves finite-kernel instances and cross-SCM invariance for both adjustment functionals.
def backdoorAdjustment reviewed
⚑ flagged
Causalean.SCM
Backdoor adjustment functional.
Definition (Lean source)
noncomputable def backdoorAdjustment
(M : SCM N Ω) (X : Finset N)
(hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y Z : Finset (SWIGNode N))
(_hY : Y ⊆ M.observed)
(_hZ : Z ⊆ M.observed) :
Kernel
(M.fixSet X hX_obs hX_fixed).FixedValues
(ValuesOn Y (swigΩ Ω)) := by
-- X.image SWIGNode.random ∪ Z ⊆ M.observed, combining `hX_obs` and `_hZ`.
have hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := by
refine union_subset ?_ _hZ
intro v hv
rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩
exact hX_obs D hD
let zMarginal :
Kernel M.FixedValues (ValuesOn Z (swigΩ Ω)) :=
(M.obsKernel).map (valuesProjection _hZ)
let zMarginalPost :
Kernel
(M.fixSet X hX_obs hX_fixed).FixedValues
(ValuesOn Z (swigΩ Ω)) :=
zMarginal.comap (M.fixSetProj X hX_obs hX_fixed)
(M.measurable_fixSetProj X hX_obs hX_fixed)
let condPost :
Kernel
((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) _hY hXZ).comap
(fun p =>
(M.fixSetProj X hX_obs hX_fixed p.1,
M.fillZrW X hX_obs hX_fixed Z p.1 p.2))
(prodMk
((M.measurable_fixSetProj X hX_obs hX_fixed).comp measurable_fst)
(M.measurable_fillZrW_prod X hX_obs hX_fixed Z))
exact ((zMarginalPost ⊗ₖ condPost).map snd)
def frontdoorAdjustment reviewed
⚑ flagged
Causalean.SCM
Frontdoor adjustment functional.
Definition (Lean source)
noncomputable def frontdoorAdjustment
(M : SCM N Ω) (X : Finset N)
(hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y Z : Finset (SWIGNode N))
(_hY : Y ⊆ M.observed)
(_hZ : Z ⊆ M.observed) :
Kernel
(M.fixSet X hX_obs hX_fixed).FixedValues
(ValuesOn Y (swigΩ Ω)) := by
-- `X.image SWIGNode.random ⊆ M.observed` (from `hX_obs`).
have hXr : X.image SWIGNode.random ⊆ M.observed := by
intro v hv
rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩
exact hX_obs D hD
-- `X.image SWIGNode.random ∪ Z ⊆ M.observed`.
have hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed :=
union_subset hXr _hZ
-- **Frontdoor body** (Pearl's frontdoor functional). In informal notation,
-- frontdoorAdjustment M X Y Z (s_post)
-- = ∫_z ( ∫_{x'} P(Y | X = x', Z = z) dP(X' | s_orig) ) dP(Z | X = x_do)
-- where `s_orig := M.fixSetProj X _ _ s_post`, `x_do` is the *intervention*
-- treatment value read off `s_post`, and `x'` is an independent observational
-- copy of treatment integrated only inside the outcome leg. The split
-- between the intervention slice `x_do` in the mediator law `P(Z | X = x_do)`
-- and the observational marginal `dP(X')` in the outcome leg is the two-stage
-- structure of the frontdoor criterion.
--
-- `x_do` : the intervention treatment slice read off `s_post` — this is the
-- inner content of `fillZrW` (relabel the do-set fixed `X`-slice as random).
let xDo : (M.fixSet X hX_obs hX_fixed).FixedValues →
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) :=
fun s => zFixedAsRandom
(valuesProjection (fixSet_image_fixed_subset M X hX_obs hX_fixed) s)
have hxDo : Measurable xDo :=
measurable_zFixedAsRandom.comp
(measurable_valuesProjection (fixSet_image_fixed_subset M X hX_obs hX_fixed))
-- Mediator law `P(Z | X = x_do, s_orig)`, conditioned on the *intervention* X.
let zCondXdo :
Kernel (M.fixSet X hX_obs hX_fixed).FixedValues
(ValuesOn Z (swigΩ Ω)) :=
(M.obsCondKernel Z (X.image SWIGNode.random) _hZ hXr).comap
(fun s => (M.fixSetProj X hX_obs hX_fixed s, xDo s))
(prodMk (M.measurable_fixSetProj X hX_obs hX_fixed) hxDo)
-- Observational X'-marginal `P(X' | s_orig)` for the outcome leg.
let xMarginal :
Kernel (M.fixSet X hX_obs hX_fixed).FixedValues
(ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) :=
(M.obsKernel.map (valuesProjection hXr)).comap
(M.fixSetProj X hX_obs hX_fixed)
(M.measurable_fixSetProj X hX_obs hX_fixed)
-- Outcome law `P(Y | X' = x', Z = z, s_orig)`.
let yCondXZ :
Kernel
((M.fixSet X hX_obs hX_fixed).FixedValues ×
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) _hY hXZ).comap
(fun p =>
(M.fixSetProj X hX_obs hX_fixed p.1,
valuesUnionMk p.2.1 p.2.2))
(prodMk
((M.measurable_fixSetProj X hX_obs hX_fixed).comp measurable_fst)
(measurable_valuesUnionMk.comp
(prodMk
(measurable_fst.comp measurable_snd)
(measurable_snd.comp measurable_snd))))
-- Inner outcome leg `∫_{x'} P(Y | X' = x', Z = z) dP(X' | s_orig)`: a kernel
-- in `(s_post, z)` that integrates out the observational X' while holding `z`.
let innerY :
Kernel
((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
((xMarginal.comap fst measurable_fst) ⊗ₖ
(yCondXZ.comap
(fun q : ((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω)) ×
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) =>
(q.1.1, q.2, q.1.2))
(prodMk
(measurable_fst.comp measurable_fst)
(prodMk measurable_snd
(measurable_snd.comp measurable_fst))))).map snd
-- Outer mediator integration `∫_z innerY(·, z) dP(Z | X = x_do)`.
exact (zCondXdo ⊗ₖ innerY).map snd
theorem backdoorAdjustment_invariant reviewed
⚑ flagged
Causalean.SCM
Cross-SCM invariance of backdoorAdjustment. Fix two causal models M₁ and M₂ that share the same SWIG graph and the same observational kernel, and a treatment set X, an outcome set Y, and an adjustment set Z that are valid intervention data and observed variables in both models. Then the backdoor-adjustment kernel for Y given Z after intervening on X, computed within M₁, is the same as the one computed within M₂.
Formal statement
hypotheses
M₁ M₂ :
SCM N Ω
h_swig :
M₁.toSWIGGraph = M₂.toSWIGGraph
_h_obs :
HEq M₁.obsKernel M₂.obsKernel
X :
Finset N
hX_obs₁ :
∀ D ∈ X, SWIGNode.random D ∈ M₁.observed
hX_fixed₁ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed
hX_obs₂ :
∀ D ∈ X, SWIGNode.random D ∈ M₂.observed
hX_fixed₂ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed
hY₁ :
Y ⊆ M₁.observed
hZ₁ :
Z ⊆ M₁.observed
hY₂ :
Y ⊆ M₂.observed
hZ₂ :
Z ⊆ M₂.observed
conclusion
HEq (M₁.backdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁) (M₂.backdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂)
Proof (Lean source)
theorem backdoorAdjustment_invariant
(M₁ M₂ : SCM N Ω)
(h_swig : M₁.toSWIGGraph = M₂.toSWIGGraph)
(_h_obs : HEq M₁.obsKernel M₂.obsKernel)
(X : Finset N)
(hX_obs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed)
(hX_fixed₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed)
(hX_obs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed)
(hX_fixed₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed)
(Y Z : Finset (SWIGNode N))
(hY₁ : Y ⊆ M₁.observed) (hZ₁ : Z ⊆ M₁.observed)
(hY₂ : Y ⊆ M₂.observed) (hZ₂ : Z ⊆ M₂.observed) :
HEq (M₁.backdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁)
(M₂.backdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂) := by
-- Kernel-native transport: the remaining work is the HEq compatibility
-- of `obsCondKernel` (via `heq_obsKernel`/`heq_obsCondKernel` from
-- `EquivKernel.lean`) plus the `Kernel.comap`/`bind` reindexing along
-- `fixSetProj` and `fillZrW`.
obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁,
fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩,
eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁
obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂,
fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩,
eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂
cases h_swig
apply heq_of_eq
-- After `cases h_swig`, the SWIGGraph-level indices on both sides are unified
-- (proofs `fio/oi/od/...` are Prop-valued, hence definitionally equal by
-- proof irrelevance), while the non-SWIGGraph fields `eT/iota/sf/mf/lD/pL`
-- still differ. The `backdoorAdjustment` body uses only
-- `toSWIGGraph`-derived data (`fixSetProj`, `fillZrW`, `FixedValues`,
-- `observed`) plus `obsKernel` and `obsCondKernel`; the latter two agree
-- via `_h_obs` and its derived `obsCondKernel` consequence.
have h_ok : _ = _ := eq_of_heq _h_obs
unfold SCM.backdoorAdjustment
simp only
-- Peel off `.map snd`.
congr 1
-- Peel off `⊗ₖ` into zMarginalPost and condPost equalities.
congr 1
· -- zMarginalPost equality: `(obsKernel.map (valuesProjection hZ)).comap fixSetProj`
-- Only uses `obsKernel` (pointed from `h_ok`) and SWIG-level projections.
congr 1
· rw [h_ok]
· -- condPost equality: `(obsCondKernel Y CC hY hXZ).comap (fixSetProj, fillZrW)`
-- Uses `obsCondKernel` (unfolds to `(obsKernel.map _).condKernel`).
congr 1
unfold SCM.obsCondKernel SCM.obsCondPairKernel
congr 1
rw [h_ok]
theorem frontdoorAdjustment_invariant reviewed
⚑ flagged
Causalean.SCM
Cross-SCM invariance of frontdoorAdjustment. Fix two causal models M₁ and M₂ that share the same SWIG graph and the same observational kernel, and a treatment set X, an outcome set Y, and a mediator set Z that are valid intervention data and observed variables in both models. Then the frontdoor-adjustment kernel for Y through mediator Z after intervening on X, computed within M₁, is the same as the one computed within M₂.
Formal statement
hypotheses
M₁ M₂ :
SCM N Ω
h_swig :
M₁.toSWIGGraph = M₂.toSWIGGraph
_h_obs :
HEq M₁.obsKernel M₂.obsKernel
X :
Finset N
hX_obs₁ :
∀ D ∈ X, SWIGNode.random D ∈ M₁.observed
hX_fixed₁ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed
hX_obs₂ :
∀ D ∈ X, SWIGNode.random D ∈ M₂.observed
hX_fixed₂ :
∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed
hY₁ :
Y ⊆ M₁.observed
hZ₁ :
Z ⊆ M₁.observed
hY₂ :
Y ⊆ M₂.observed
hZ₂ :
Z ⊆ M₂.observed
conclusion
HEq (M₁.frontdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁) (M₂.frontdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂)
Proof (Lean source)
theorem frontdoorAdjustment_invariant
(M₁ M₂ : SCM N Ω)
(h_swig : M₁.toSWIGGraph = M₂.toSWIGGraph)
(_h_obs : HEq M₁.obsKernel M₂.obsKernel)
(X : Finset N)
(hX_obs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed)
(hX_fixed₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed)
(hX_obs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed)
(hX_fixed₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed)
(Y Z : Finset (SWIGNode N))
(hY₁ : Y ⊆ M₁.observed) (hZ₁ : Z ⊆ M₁.observed)
(hY₂ : Y ⊆ M₂.observed) (hZ₂ : Z ⊆ M₂.observed) :
HEq (M₁.frontdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁)
(M₂.frontdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂) := by
-- Mirror the `backdoorAdjustment_invariant` strategy: destructure both
-- SCMs, `cases h_swig` to align SWIGGraph indices, then `congr` through
-- the `⊗ₖ` / `.map` / `.comap` plumbing. Every leg uses only
-- `M.obsKernel` (transported via `_h_obs`) plus SWIGGraph-derived
-- projections.
obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁,
fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩,
eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁
obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂,
fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩,
eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂
cases h_swig
apply heq_of_eq
have h_ok : _ = _ := eq_of_heq _h_obs
unfold SCM.frontdoorAdjustment
simp only
-- The body is `((xMarginal ⊗ₖ zCondX) ⊗ₖ yCondXZ.comap …).map snd`.
-- Each leg either uses `obsKernel` directly (xMarginal) or `obsCondKernel`
-- (zCondX, yCondXZ). Unfolding `obsCondKernel` exposes the joint
-- `obsKernel.map (·, ·)` whose `condKernel` is taken. All legs reduce
-- to a single `obsKernel` argument that we rewrite via `h_ok`.
unfold SCM.obsCondKernel SCM.obsCondPairKernel
simp_rw [h_ok]
-- After `simp_rw [h_ok]` the obsKernel mentions are unified. The
-- remaining record-identity differences in `fixSetProj` etc. are
-- proof-irrelevance noise (only SWIGGraph fields are used, all unified
-- after `cases h_swig`); `rfl` closes the goal.
rfl
3 supporting declarations (lemmas, instances)
-
instIsMarkovKernelObsCondKernelinstance — The observational conditional kernel obsCondKernel Y CC is a Markov kernel (its values are probability measures), inherited from Mathlib's condKernel.instance instIsMarkovKernelObsCondKernel (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) : IsMarkovKernel (M.obsCondKernel Y CC hY hCC) := by unfold SCM.obsCondKernel; infer_instance -
instIsFiniteKernelBackdoorAdjustmentinstance — The backdoor-adjustment functional is a finite kernel (a compProd of finite kernels, pushed through Prod.snd).instance instIsFiniteKernelBackdoorAdjustment (M : SCM N Ω) (X : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) : IsFiniteKernel (M.backdoorAdjustment X hX_obs hX_fixed Y Z hY hZ) := by rw [SCM.backdoorAdjustment]; infer_instance -
instIsFiniteKernelFrontdoorAdjustmentinstance — The frontdoor-adjustment functional is a finite kernel (nested compProds of finite kernels, pushed through Prod.snd).instance instIsFiniteKernelFrontdoorAdjustment (M : SCM N Ω) (X : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) : IsFiniteKernel (M.frontdoorAdjustment X hX_obs hX_fixed Y Z hY hZ) := by rw [SCM.frontdoorAdjustment]; infer_instance
Frontdoor 4 core · 3 supporting This file states the frontdoor completeness / identification result tying the graph-level functional SCM.frontdoorAdjustment (defined in SCM/ID/Adjustment.lean) to the true post-intervention Y-marginal (M.fixSet X).obsKe ★ frontdoor_completeness_ae_compProd★ frontdoor_identifiable_ae
Frontdoor identification, a.e. in the treatment value
This file states the frontdoor completeness / identification result tying the
graph-level functional SCM.frontdoorAdjustment (defined in SCM/ID/Adjustment.lean)
to the true post-intervention Y-marginal (M.fixSet X).obsKernel.map π_Y, under the
three frontdoor graph clauses recorded by SWIGGraph.frontdoorCriterion.
It is the frontdoor analogue of SCM/ID/Backdoor.lean, and is stated in the same
regime-uniform a.e. style: the identity holds for νX-almost-every treatment value
t (where νX is the observational treatment marginal), via the version-safe joint
identity νX ⊗ₘ Kdo = νX ⊗ₘ Kfd (ProbabilityTheory.Kernel.ae_eq_of_compProd_eq).
Mediator representation
The mediator set is a base node set W : Finset N (so that it is intervenable
— the frontdoor derivation routes through do(W)). Wherever frontdoorAdjustment
expects a Finset (SWIGNode N) mediator it is instantiated at W.image SWIGNode.random.
Proof skeleton (for the main theorem; do-calculus Rules 2 and 3)
Pearl's derivation, in three legs, mirrored at the kernel level:
* Leg A — mediator (Rule 2, FD2). P(Z | do(X)) = P(Z | X): the Z-marginal of
the post-intervention kernel equals the observational conditional P(Z | X = x_do),
because there is no unblocked back-door path X → Z (the fd_no_backdoor_XZ clause).
State this leg νX-a.e. (or in compProd form), never pointwise in the treatment
slice — the pointwise conditional reads obsCondKernel on a νX-null {X = t}
slice and is too strong for continuous treatment (see SCM/ID/Backdoor.lean).
* Leg B — outcome (FD1 + FD3). Because Z intercepts every directed X → Y
path (criterion fd_intercept), P(Y | do(X), Z) = P(Y | do(Z)); and since X
is a valid back-door adjustment set for Z → Y (criterion fd_backdoor_ZY),
P(Y | do(Z)) = ∫_{x'} P(Y | X = x', Z) dP(x'). This leg is exactly
backdoor_completeness_ae_compProd instantiated with treatment := W,
adjustment set := X.image SWIGNode.random, outcome := Y.
* Composition. Chaining Leg A and Leg B reproduces the frontdoorAdjustment
body ∫_z (∫_{x'} P(Y | X=x', Z=z) dP(x')) dP(Z | X=x_do).
The FD1 bridge is exposed as an explicit compProd substrate hypothesis, keeping the theorem focused on assembling the frontdoor functional from Rule 2, Rule 3, and the backdoor marginal-invariance leg rather than re-deriving disintegration inside the final theorem.
def frontdoorCriterion reviewed
⚑ flagged
Causalean.SWIGGraph
frontdoorCriterion says that the base mediator set W satisfies Pearl's frontdoor criterion for treatment variables X and outcome nodes Y: the mediator random nodes intercept every directed treatment-outcome path, have no open back-door path from treatment, admit treatment adjustment for the mediator-outcome effect, and are excluded from the treatment and outcome sets.
Definition (Lean source)
def frontdoorCriterion
(X : Finset N)
(hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed)
(hX_fix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed)
(W : Finset N)
(hW_obs : ∀ D ∈ W, SWIGNode.random D ∈ G.observed)
(hW_fix : ∀ D ∈ W, SWIGNode.fixed D ∉ G.fixed)
(Y : Finset (SWIGNode N)) : Prop :=
-- (FD1) interception: Z = W.random intercepts all directed X → Y paths, i.e. the
-- intervention copies `X.fixed` (carrying X's causal outgoing edges; `random X` is a
-- sink) reach `Y` only through `Z`.
(G.splitMono X hX_obs hX_fix).dag.dSep Y (X.image SWIGNode.fixed)
(W.image SWIGNode.random) ∧
-- (FD2) no back-door X → Z (∅ is a backdoor adjustment set for (X, Z)).
G.backdoorCriterion X hX_obs hX_fix (W.image SWIGNode.random) ∅ ∧
-- (FD3) X.random is a backdoor adjustment set for the mediator effect (W → Y).
G.backdoorCriterion W hW_obs hW_fix Y (X.image SWIGNode.random) ∧
-- (FD4) mediator exclusions from treatment and outcome nodes.
Disjoint (W.image SWIGNode.random) (X.image SWIGNode.random) ∧
Disjoint (W.image SWIGNode.random) Y
def frontdoorKernelY reviewed
⚑ flagged
Causalean.SCM
Frontdoor-adjustment Y-marginal as a kernel in the treatment value t, at base s₀ — the frontdoor analogue of adjustmentKernelY. Reindexes the graph-level frontdoorAdjustment (with mediator Z := W.image SWIGNode.random) along fixSetExtend s₀, so its input is the treatment value t rather than the full post-intervention slice.
Definition (Lean source)
noncomputable def frontdoorKernelY (M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y W : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hW : W ⊆ M.observed)
(s0 : M.FixedValues) :
Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.frontdoorAdjustment X hObs hFix Y W hY hW).comap
(M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)
theorem frontdoor_completeness_ae_compProd reviewed
⚑ flagged
Causalean.SCM
Frontdoor completeness — joint (compProd), version-safe primary form. Let X be a valid intervention set — observed and not already fixed, and Wbase likewise a valid intervention set of mediators, with the outcome set Y observed, the random copies of Wbase observed, and the random copies of X observed. Suppose the frontdoor criterion holds for (X, Wbase, Y), that Y is disjoint from the random copies of Wbase and the random copies of Wbase are disjoint from those of X, and that each of the three legs of the frontdoor decomposition — the do(X) leg, the do(Wbase) leg adjusting for X, and the nested do(X)-then-do(Wbase) leg — satisfies the matching backdoor overlap and positivity conditions. Then the joint law of the treatment marginal with the post-intervention Y-marginal equals the joint law of the treatment marginal with the frontdoor-adjustment functional.
Formal statement
hypotheses
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hWr :
Wbase.image SWIGNode.random ⊆ M.observed
hXr :
X.image SWIGNode.random ⊆ M.observed
_hFD :
M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y
hDisj_YWr :
Disjoint Y (Wbase.image SWIGNode.random)
hDisj_WrXr :
Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)
s0 :
M.FixedValues
hOverlapA :
∀ s : (M.fixSet X hObs hFix).FixedValues,
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using hXr) s0
hOverlapB :
∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues,
Rule2JointOverlap M Wbase hWobs hWfix (X.image SWIGNode.random) (union_subset hWr hXr) s
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) hXr (union_subset hWr hXr) s0
hOverlapFD1 :
∀ s : ((M.fixSet X hObs hFix).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues,
Rule2JointOverlap (M.fixSet X hObs hFix) Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm)) (∅ : Finset (SWIGNode N)) (by simpa [union_empty, SCM.fixSet_observed] using hWr) s
hPositivityFD1 :
∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [union_empty, SCM.fixSet_observed] using hWr)))
conclusion
(M.treatmentMarginal X hXr s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X hXr s0) ⊗ₘ (M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0)
Proof (Lean source)
theorem frontdoor_completeness_ae_compProd
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hWr : Wbase.image SWIGNode.random ⊆ M.observed)
(hXr : X.image SWIGNode.random ⊆ M.observed)
(_hFD : M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y)
(hDisj_YWr : Disjoint Y (Wbase.image SWIGNode.random))
(hDisj_WrXr : Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random))
(s0 : M.FixedValues)
(hOverlapA : ∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix
(∅ : Finset (SWIGNode N)) (by simpa using hXr) s)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed) (by simpa using hXr) s0)
(hOverlapB : ∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues,
Rule2JointOverlap M Wbase hWobs hWfix
(X.image SWIGNode.random) (union_subset hWr hXr) s)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
hXr (union_subset hWr hXr) s0)
(hOverlapFD1 : ∀ s : ((M.fixSet X hObs hFix).fixSet Wbase
(by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD)
(fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix
((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues,
Rule2JointOverlap (M.fixSet X hObs hFix) Wbase
(by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD)
(fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix
((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))
(∅ : Finset (SWIGNode N))
(by
simpa [union_empty, SCM.fixSet_observed] using hWr)
s)
(hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection (empty_subset _)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ (((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [union_empty, SCM.fixSet_observed] using hWr)))) :
(M.treatmentMarginal X hXr s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X hXr s0) ⊗ₘ
(M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0) := by
exact frontdoor_fd1_interception_compProd M X hObs hFix Wbase hWobs hWfix Y hY hWr hXr
_hFD hDisj_YWr hDisj_WrXr s0 hOverlapA hPositivityA hOverlapB hPositivityB
hOverlapFD1 hPositivityFD1
theorem frontdoor_identifiable_ae reviewed
⚑ flagged
Causalean.SCM
Frontdoor identification, a.e. in the treatment value. Let X be a valid intervention set — observed and not already fixed, and Wbase likewise a valid intervention set of mediators, with the outcome set Y observed, the random copies of Wbase observed, and the random copies of X observed. Suppose the frontdoor criterion holds for (X, Wbase, Y), that Y is disjoint from the random copies of Wbase and the random copies of Wbase are disjoint from those of X, and that each of the three legs of the frontdoor decomposition — the do(X) leg, the do(Wbase) leg adjusting for X, and the nested do(X)-then-do(Wbase) leg — satisfies the matching backdoor overlap and positivity conditions. Then for treatmentMarginal-almost-every treatment value t, the post-intervention Y-marginal doKernelY at t equals the frontdoor-adjustment functional frontdoorKernelY at t.
Formal statement
hypotheses
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hWr :
Wbase.image SWIGNode.random ⊆ M.observed
hXr :
X.image SWIGNode.random ⊆ M.observed
_hFD :
M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y
hDisj_YWr :
Disjoint Y (Wbase.image SWIGNode.random)
hDisj_WrXr :
Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)
s0 :
M.FixedValues
hOverlapA :
∀ s : (M.fixSet X hObs hFix).FixedValues,
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using hXr) s0
hOverlapB :
∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues,
Rule2JointOverlap M Wbase hWobs hWfix (X.image SWIGNode.random) (union_subset hWr hXr) s
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) hXr (union_subset hWr hXr) s0
hOverlapFD1 :
∀ s : ((M.fixSet X hObs hFix).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues,
Rule2JointOverlap (M.fixSet X hObs hFix) Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm)) (∅ : Finset (SWIGNode N)) (by simpa [union_empty, SCM.fixSet_observed] using hWr) s
hPositivityFD1 :
∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [union_empty, SCM.fixSet_observed] using hWr)))
conclusion
∀ᵐ t ∂(M.treatmentMarginal X hXr s0),
M.doKernelY X hObs hFix Y hY s0 t
= M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0 t
Proof (Lean source)
theorem frontdoor_identifiable_ae
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hWr : Wbase.image SWIGNode.random ⊆ M.observed)
(hXr : X.image SWIGNode.random ⊆ M.observed)
(_hFD : M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y)
(hDisj_YWr : Disjoint Y (Wbase.image SWIGNode.random))
(hDisj_WrXr : Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random))
(s0 : M.FixedValues)
(hOverlapA : ∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix
(∅ : Finset (SWIGNode N)) (by simpa using hXr) s)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed) (by simpa using hXr) s0)
(hOverlapB : ∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues,
Rule2JointOverlap M Wbase hWobs hWfix
(X.image SWIGNode.random) (Finset.union_subset hWr hXr) s)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
hXr (Finset.union_subset hWr hXr) s0)
(hOverlapFD1 : ∀ s : ((M.fixSet X hObs hFix).fixSet Wbase
(by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD)
(fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix
((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues,
Rule2JointOverlap (M.fixSet X hObs hFix) Wbase
(by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD)
(fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix
((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))
(∅ : Finset (SWIGNode N))
(by
simpa [union_empty, SCM.fixSet_observed] using hWr)
s)
(hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection (empty_subset _)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ (((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [union_empty, SCM.fixSet_observed] using hWr)))) :
∀ᵐ t ∂(M.treatmentMarginal X hXr s0),
M.doKernelY X hObs hFix Y hY s0 t
= M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0 t := by
have hXrW : X.image SWIGNode.random ∪ Wbase.image SWIGNode.random ⊆ M.observed :=
Finset.union_subset hXr hWr
haveI : IsFiniteMeasure (M.treatmentMarginal X hXr s0) := by
unfold treatmentMarginal
exact (M.obsKernel s0).isFiniteMeasure_map _
exact ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
(M.frontdoor_completeness_ae_compProd X hObs hFix Wbase hWobs hWfix Y hY hWr hXr
_hFD hDisj_YWr hDisj_WrXr s0 hOverlapA hPositivityA hOverlapB hPositivityB
hOverlapFD1 hPositivityFD1)
3 supporting declarations (lemmas, instances)
-
instIsFiniteKernelFrontdoorKernelYinstance — The treatment-indexed frontdoor-adjustment Y-marginal kernel is finite.instance instIsFiniteKernelFrontdoorKernelY (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y W : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hW : W ⊆ M.observed) (s0 : M.FixedValues) : IsFiniteKernel (M.frontdoorKernelY X hObs hFix Y W hY hW s0) := by rw [SCM.frontdoorKernelY]; infer_instance -
obsKernel_map_proj_eq_of_equivlemma — Structurally equivalent structural causal models assign the same observational marginal law to a shared set of observed variables when their fixed-variable assignments correspond.hypothesesM₁ M₂ :SCM N Ωh :SCM.Equiv M₁ M₂hY₁ :Y ⊆ M₁.observedhY₂ :Y ⊆ M₂.observeds₁ :M₁.FixedValuess₂ :M₂.FixedValueshs :HEq s₁ s₂conclusion(M₁.obsKernel s₁).map (valuesProjection hY₁)= (M₂.obsKernel s₂).map (valuesProjection hY₂)Proof (Lean source)
lemma obsKernel_map_proj_eq_of_equiv {M₁ M₂ : SCM N Ω} (h : SCM.Equiv M₁ M₂) (Y : Finset (SWIGNode N)) (hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (s₁ : M₁.FixedValues) (s₂ : M₂.FixedValues) (hs : HEq s₁ s₂) : (M₁.obsKernel s₁).map (valuesProjection hY₁) = (M₂.obsKernel s₂).map (valuesProjection hY₂) := by -- Extract the `obsKernel` HEq while `h` still has its `Equiv` type. have hok0 : HEq M₁.obsKernel M₂.obsKernel := SCM.Equiv.heq_obsKernel h.1 h.2.2.1 h.2.2.2 obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ rcases h.1 with ⟨_hEdge, rfl, rfl, rfl⟩ -- After unifying `observed`/`fixed`/`unobserved`, the `FixedValues` and -- `ObservedValues` types coincide, so the `HEq`s collapse to `Eq`. have hs_eq : s₁ = s₂ := eq_of_heq hs subst hs_eq have hok := eq_of_heq hok0 rw [hok] -
adjustmentKernelY_empty_eqlemma — With an empty adjustment set, the outcome adjustment kernel equals the observed conditional kernel of the outcome variables given the treated variables at the same fixed values.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhWr :Wr ⊆ M.observedhXr :X.image SWIGNode.random ⊆ M.observeds0 :M.FixedValuesconclusion= M.obsCondKernel Wr (X.image SWIGNode.random) hWr hXr (s0, t)Proof (Lean source)
lemma adjustmentKernelY_empty_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Wr : Finset (SWIGNode N)) (hWr : Wr ⊆ M.observed) (hXr : X.image SWIGNode.random ⊆ M.observed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.adjustmentKernelY X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) s0 t = M.obsCondKernel Wr (X.image SWIGNode.random) hWr hXr (s0, t) := by let sTt := M.fixSetExtend X hObs hFix s0 t let zMarginalPost : Kernel (M.fixSet X hObs hFix).FixedValues (ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) := (M.obsKernel.map (valuesProjection (empty_subset M.observed))).comap (M.fixSetProj X hObs hFix) (M.measurable_fixSetProj X hObs hFix) haveI : IsMarkovKernel (M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed))) := by unfold SCM.obsCondKernel infer_instance let condPost : Kernel ((M.fixSet X hObs hFix).FixedValues × ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) (ValuesOn Wr (swigΩ Ω)) := (M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed))).comap (fun p => (M.fixSetProj X hObs hFix p.1, M.fillZrW X hObs hFix (∅ : Finset (SWIGNode N)) p.1 p.2)) (prodMk ((M.measurable_fixSetProj X hObs hFix).comp measurable_fst) (M.measurable_fillZrW_prod X hObs hFix (∅ : Finset (SWIGNode N)))) haveI : IsSFiniteKernel zMarginalPost := by dsimp [zMarginalPost] infer_instance haveI : IsSFiniteKernel condPost := by dsimp [condPost] infer_instance have hcollapse : ((zMarginalPost ⊗ₖ condPost).map snd) sTt = condPost (sTt, (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) := by rw [compProd_map_snd_apply] have hz : zMarginalPost sTt = dirac (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) := by ext S hS by_cases hempty : S = ∅ · simp [hempty] · have h_univ : S = univ := by apply Set.eq_univ_of_forall intro x by_contra hx apply hempty ext y constructor · intro hy have : y = x := Subsingleton.elim y x exact elim (hx (this ▸ hy)) · intro hy simp at hy rw [h_univ] dsimp [zMarginalPost] rw [ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _)] rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection _) MeasurableSet.univ] simp [M.obsKernel_apply_univ (M.fixSetProj X hObs hFix sTt)] rw [hz] simpa [sectR] using (MeasureTheory.Measure.dirac_bind (a := (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) (f := condPost.sectR sTt) (hf := by fun_prop)) have hadj : M.adjustmentKernelY X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) s0 t = ((zMarginalPost ⊗ₖ condPost).map snd) sTt := by rw [SCM.adjustmentKernelY, ProbabilityTheory.Kernel.comap_apply] change M.backdoorAdjustment X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) sTt = ((zMarginalPost ⊗ₖ condPost).map snd) sTt rw [SCM.backdoorAdjustment] rw [hadj, hcollapse] have hcond : condPost (sTt, (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) = M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed)) (s0, valuesUnionMk t (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) := by simp [condPost, sTt, SCM.fixSetProj_fixSetExtend, SCM.fillZrW_fixSetExtend] rw [hcond] apply obsCondKernel_congr_cc M Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) (X.image SWIGNode.random) (union_empty _) hWr (union_subset hXr (empty_subset M.observed)) hXr exact valuesOn_heq_of_coord (union_empty _) _ _ (fun v hvU hvX => valuesUnionMk_apply_left t (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) hvX)