SCM.ID.Toolkit · Causalean Library

Derivation 1 core · 4 supporting Graphical-side helpers that turn a backdoorCriterion into the d-separation / non-descendance facts that the kernel-level do-calculus rules consume, plus the Rule-2 *applicator* that hides the whole plumbing. ★ backdoorCriterion_dSep_fixSet

Do-calculus derivation helpers (identification toolkit, Layer 2)

Graphical-side helpers that turn a backdoorCriterion into the d-separation / non-descendance facts that the kernel-level do-calculus rules consume, plus the Rule-2 applicator that hides the whole plumbing. These are the lemmas that the backdoor and frontdoor identification proofs previously rebuilt inline (≈40 lines of have blocks each). Factoring them out lets an identification proof name the criterion and read off the graphical premises — or the entire Rule-2 conclusion — in one call.

* disjoint_fixed_observed — a standing structural fact: an SCM's fixed and observed node sets are disjoint. * backdoorCriterion_dSep_fixSet — criterion (ii) extended to the post-intervention fixed nodes (the conditioning set Rule 2 wants). * backdoorCriterion_W_nonDesc / backdoorCriterion_W_nonDescM1 — criterion (i) in the two non-ancestry forms the Rule-2 witness transfer consumes. * backdoor_rule2_ae_of_positivity — the Rule-2 applicator: from a backdoorCriterion plus product positivity it produces the a.e. obsCondKernel do/obs identity directly, deriving the three graphical premises internally. This is the one-call replacement for the criterion→premises→do_rule2_kernel_of_nondescendant_product_ae sequence.

theorem backdoorCriterion_dSep_fixSet reviewed

Causalean.SCM

Backdoor criterion (ii), extended to the post-intervention fixed nodes. Fix a structural causal model M and an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed, an outcome set Y and a conditioning set Z with Y contained in the observed nodes and the randomized image of X contained in the observed nodes. If M's DAG satisfies the backdoor criterion for X, Y given Z, then in the post-intervention graph obtained by fixing X, Y is d-separated from the randomized image of X given Z together with the post-intervention fixed node set.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

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

hXr :

X.image SWIGNode.random ⊆ M.observed

h_bd :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

conclusion

(M.fixSet X hObs hFix).dag.dSep Y (X.image SWIGNode.random) (Z ∪ (M.fixSet X hObs hFix).fixed)

Proof (Lean source)

theorem backdoorCriterion_dSep_fixSet (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) (hXr : X.image SWIGNode.random ⊆ M.observed) (h_bd : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) : (M.fixSet X hObs hFix).dag.dSep Y (X.image SWIGNode.random) (Z ∪ (M.fixSet X hObs hFix).fixed) := by have h_step1 : (M.fixSet X hObs hFix).dag.dSep Y (X.image SWIGNode.random) (Z ∪ X.image SWIGNode.fixed) := h_bd.2.2.2.2 have h_disj_obs_fixed : Disjoint M.fixed M.observed := disjoint_fixed_observed M have h_disj_mfixed_Y : Disjoint M.fixed Y := h_disj_obs_fixed.mono_right hY have h_disj_mfixed_Xr : Disjoint M.fixed (X.image SWIGNode.random) := h_disj_obs_fixed.mono_right hXr have hRoots : ∀ r ∈ M.fixed, ∀ u, ¬ (M.fixSet X hObs hFix).dag.edge u r := by intro r hr u he have hs_ds : r ∈ (M.fixSet X hObs hFix).fixed := SCM.fixSet_fixed_subset M X hObs hFix hr have hroot := (M.fixSet X hObs hFix).fixed_are_roots r hs_ds have hmem : u ∈ (M.fixSet X hObs hFix).dag.parents r := (M.fixSet X hObs hFix).dag.mem_parents.mpr he rw [hroot] at hmem exact absurd hmem (notMem_empty _) have h_step2 : (M.fixSet X hObs hFix).dag.dSep Y (X.image SWIGNode.random) ((Z ∪ X.image SWIGNode.fixed) ∪ M.fixed) := DAG.dSep_union_roots_right _ h_step1 hRoots h_disj_mfixed_Y h_disj_mfixed_Xr have h_cond_rewrite : (Z ∪ X.image SWIGNode.fixed) ∪ M.fixed = Z ∪ (M.fixSet X hObs hFix).fixed := by rw [SCM.fixSet_fixed]; ext x; simp only [mem_union]; tauto rw [← h_cond_rewrite]; exact h_step2

Causalean.SCM.backdoorCriterion_dSep_fixSet · Causalean/SCM/ID/Toolkit/Derivation.lean:65 · uses dSep , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , SCM , fixSet , backdoorCriterion

4 supporting declarations (lemmas, instances)

disjoint_fixed_observed theorem — Fixed and observed node sets of an SCM are disjoint.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

conclusion

Disjoint M.fixed M.observed

Proof (Lean source)

theorem disjoint_fixed_observed (M : SCM N Ω) : Disjoint M.fixed M.observed := by rw [Finset.disjoint_left] intro x hxF hxO obtain ⟨n, rfl⟩ := M.fixed_is_fixed x hxF obtain ⟨m, hm⟩ := M.observed_is_random _ hxO cases hm

Causalean.SCM.disjoint_fixed_observed · Causalean/SCM/ID/Toolkit/Derivation.lean:54
backdoorCriterion_W_nonDesc theorem — Backdoor criterion (i), post-intervention non-descendance form.

hypotheses

N :

Type u_1
N → Type u_2
shared

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)

h_bd :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

x ∈ X :

v ∈ Z :

conclusion

¬ (M.fixSet X hObs hFix).dag.isAncestor (SWIGNode.fixed x) v

Proof (Lean source)

theorem backdoorCriterion_W_nonDesc (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)) (h_bd : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) : ∀ x ∈ X, ∀ v ∈ Z, ¬ (M.fixSet X hObs hFix).dag.isAncestor (SWIGNode.fixed x) v := by intro x hx v hv hanc have hanc_base : M.toSWIGGraph.dag.isAncestor (SWIGNode.random x) v := SCM.fixSet_isAncestor_fixed_forward M X hObs hFix hx hanc exact h_bd.2.2.2.1 v hv x hx hanc_base

Causalean.SCM.backdoorCriterion_W_nonDesc · Causalean/SCM/ID/Toolkit/Derivation.lean:118
backdoorCriterion_W_nonDescM1 theorem — Backdoor criterion (i), base-graph non-descendance form.

hypotheses

N :

Type u_1
N → Type u_2
shared

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)

h_bd :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

D ∈ X :

w ∈ Z :

conclusion

¬ M.dag.isAncestor (SWIGNode.random D) w

Proof (Lean source)

theorem backdoorCriterion_W_nonDescM1 (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)) (h_bd : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) : ∀ D ∈ X, ∀ w ∈ Z, ¬ M.dag.isAncestor (SWIGNode.random D) w := fun D hD w hw => h_bd.2.2.2.1 w hw D hD

Causalean.SCM.backdoorCriterion_W_nonDescM1 · Causalean/SCM/ID/Toolkit/Derivation.lean:135
backdoor_rule2_ae_of_positivity theorem — For a finite node population with measurable, standard-Borel, nonempty value spaces, a structural causal model, a treatment set whose random copies are observed and whose fixed copies are not already fixed, observed outcome and adjustment sets, a backdoor criterion, a fixed-node assignment, and product-level positivity, the post-intervention and observational conditional kernels agree for almost every treatment/adjustment pair.

hypotheses

N :

Type u_1
N → Type u_2
shared

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 :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

s0 :

M.FixedValues

hPositivity_ae :

(((M.obsKernel s0).map (valuesProjection (Finset.image_subset_iff.mpr hObs)) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M.obsKernel s0).map (valuesProjection (union_subset (Finset.image_subset_iff.mpr hObs) hZ)))

conclusion

∀ᵐ p ∂((M.obsKernel s0).map (valuesProjection (Finset.image_subset_iff.mpr hObs)) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))), (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) (M.fixSetExtend X hObs hFix s0 p.1, p.2)
= M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY (union_subset (Finset.image_subset_iff.mpr hObs) hZ) (s0, valuesUnionMk p.1 p.2)

Proof (Lean source)

theorem backdoor_rule2_ae_of_positivity (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 : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) (s0 : M.FixedValues) (hPositivity_ae : (((M.obsKernel s0).map (valuesProjection (Finset.image_subset_iff.mpr hObs)) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M.obsKernel s0).map (valuesProjection (union_subset (Finset.image_subset_iff.mpr hObs) hZ)))) : ∀ᵐ p ∂((M.obsKernel s0).map (valuesProjection (Finset.image_subset_iff.mpr hObs)) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))), (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) (M.fixSetExtend X hObs hFix s0 p.1, p.2) = M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY (union_subset (Finset.image_subset_iff.mpr hObs) hZ) (s0, valuesUnionMk p.1 p.2) := SCM.do_rule2_kernel_of_nondescendant_product_ae M X hObs hFix Y Z hY hZ (Finset.image_subset_iff.mpr hObs) (union_subset (Finset.image_subset_iff.mpr hObs) hZ) (backdoorCriterion_dSep_fixSet M X hObs hFix Y Z hY (Finset.image_subset_iff.mpr hObs) h_bd) (backdoorCriterion_W_nonDesc M X hObs hFix Y Z h_bd) (backdoorCriterion_W_nonDescM1 M X hObs hFix Y Z h_bd) s0 hPositivity_ae

Causalean.SCM.backdoor_rule2_ae_of_positivity · Causalean/SCM/ID/Toolkit/Derivation.lean:149

FrontdoorGraph 1 core · 7 supporting This file contains the graph-only premises needed by the frontdoor identification derivation after the first intervention has already been applied. ★ frontdoor_fd3_rule2_dSep

Frontdoor double-intervention graph lemmas

This file contains the graph-only premises needed by the frontdoor identification derivation after the first intervention has already been applied.

* frontdoor_fd1_rule3_nonDesc is the Rule-3 non-ancestry premise: after intervening on the mediator block and on the treatment block, no treatment intervention copy can still be an ancestor of an outcome node, provided the corrected FD1 interception d-separation holds in the do(X) graph. * frontdoor_fd3_rule2_dSep is the Rule-2 d-separation premise in the double-intervention graph, transported from the FD3 backdoor d-separation.

theorem frontdoor_fd3_rule2_dSep reviewed

Causalean.SCM

Rule-2 d-separation premise for the frontdoor third condition. Fix a structural causal model M and two intervention target sets X, Wbase such that every node of X is currently a random observed node with no fixed copy already fixed, and likewise every node of Wbase, and an outcome set Y with Y contained in the observed nodes, such that the base graph satisfies the backdoor criterion for Wbase, Y given the randomized image of X and the randomized images of Wbase and X are disjoint. Then in the graph obtained by first fixing X and then fixing Wbase, Y is d-separated from the randomized image of Wbase given exactly that double-intervention graph's fixed node set.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X Wbase :

Finset N

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

hW_obs :

∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed

hW_fixed :

∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed

Y :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hFD3 :

backdoorCriterion M.toSWIGGraph Wbase hW_obs hW_fixed Y (X.image SWIGNode.random)

hDisj_WX :

Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)

conclusion

((M.fixSet X hX_obs hX_fixed).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hX_obs hX_fixed hW_fixed ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WX).symm))).dag.dSep Y (Wbase.image SWIGNode.random) ((∅ : Finset (SWIGNode N)) ∪ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hX_obs hX_fixed hW_fixed ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WX).symm))).fixed)

Proof (Lean source)

theorem frontdoor_fd3_rule2_dSep (M : SCM N Ω) (X Wbase : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (hW_obs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed) (hW_fixed : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hFD3 : backdoorCriterion M.toSWIGGraph Wbase hW_obs hW_fixed Y (X.image SWIGNode.random)) (hDisj_WX : Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)) : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hX_obs hX_fixed hW_fixed ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WX).symm))).dag.dSep Y (Wbase.image SWIGNode.random) ((∅ : Finset (SWIGNode N)) ∪ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hX_obs hX_fixed hW_fixed ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WX).symm))).fixed) := by classical have hDisjBaseWX : Disjoint Wbase X := disjoint_base_of_disjoint_random_image X Wbase hDisj_WX have hDisjBaseXW : Disjoint X Wbase := hDisjBaseWX.symm let hW_obs_X : ∀ D ∈ Wbase, SWIGNode.random D ∈ (M.fixSet X hX_obs hX_fixed).observed := by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD let hW_fixed_X : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ (M.fixSet X hX_obs hX_fixed).fixed := fixSet_fixed_not_mem_of_disjoint M Wbase X hX_obs hX_fixed hW_fixed hDisjBaseXW let Gdouble := ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag let Cdouble := (∅ : Finset (SWIGNode N)) ∪ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed refine ⟨hFD3.2.2.2.2.1, ?_, ?_, ?_⟩ · have hY_double : Y ⊆ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).observed := by intro v hv simpa [SCM.fixSet_observed] using hY hv rw [Finset.disjoint_left] intro v hvY hvC simp only [Cdouble, Finset.empty_union] at hvC exact (not_fixed_of_obs ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).toSWIGGraph (hY_double hvY)) hvC · have hW_double : Wbase.image SWIGNode.random ⊆ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).observed := by intro v hv rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩ simpa [SCM.fixSet_observed] using hW_obs D hD rw [Finset.disjoint_left] intro v hvW hvC simp only [Cdouble, Finset.empty_union] at hvC exact (not_fixed_of_obs ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).toSWIGGraph (hW_double hvW)) hvC · rw [Finset.disjoint_left] intro v hvReach hvW rw [((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.bbReachableVertices_iff_activeWalk] at hvReach obtain ⟨y, hyY, p, hlen, hact, hhead, hlast⟩ := hvReach have hReach_doW : v ∈ (M.fixSet Wbase hW_obs hW_fixed).dag.bbReachableVertices (X.image SWIGNode.random ∪ Wbase.image SWIGNode.fixed) Y := by rw [(M.fixSet Wbase hW_obs hW_fixed).dag.bbReachableVertices_iff_activeWalk] refine ⟨y, hyY, p, hlen, ?_, hhead, hlast⟩ obtain ⟨hadjD, hcollD⟩ := hact have hNoFixedInterior : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ ∉ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed := by intro i hi hmfix have hroot : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.parents (p.get ⟨i + 1, by omega⟩) = ∅ := ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed_are_roots _ hmfix have hval := hcollD i hi simp only at hval set l := p.get ⟨i, by omega⟩ set m := p.get ⟨i + 1, by omega⟩ set r := p.get ⟨i + 2, hi⟩ have hnotColl : ¬ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.IsCollider l m r := by intro hc have hpar : l ∈ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.parents m := ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.mem_parents.mpr hc.1 rw [show m = p.get ⟨i + 1, by omega⟩ from rfl] at hpar rw [hroot] at hpar exact (notMem_empty _) hpar rw [if_neg hnotColl] at hval exact hval (by simpa [Finset.empty_union] using hmfix) have hY_not_fixed : ∀ D ∈ X, y ≠ SWIGNode.fixed D := by intro D hD hyfix have hyObs : y ∈ M.observed := hY hyY obtain ⟨n, hn⟩ := M.observed_is_random y hyObs rw [hn] at hyfix cases hyfix have hV_not_fixed : ∀ D ∈ X, v ≠ SWIGNode.fixed D := by intro D hD hvfix rcases Finset.mem_image.mp hvW with ⟨E, hE, hv⟩ rw [← hv] at hvfix cases hvfix have hNotFixedAt : ∀ (k : ℕ) (hk : k < p.length), ∀ D ∈ X, p.get ⟨k, hk⟩ ≠ SWIGNode.fixed D := by intro k hk D hD hEq by_cases hk0 : k = 0 · subst hk0 have hp0 : p.get ⟨0, hk⟩ = y := by cases p with | nil => simp at hlen | cons a t => simp only [List.head?_cons] at hhead exact Option.some.inj hhead rw [hp0] at hEq exact hY_not_fixed D hD hEq · by_cases hklast : k + 1 = p.length · have hpLast : p.get ⟨k, hk⟩ = v := by have hp_ne : p ≠ [] := by intro hpnil rw [hpnil] at hlen simp at hlen rw [getLast?_eq_some_getLast hp_ne] at hlast have hgetLast : p.getLast hp_ne = v := Option.some.inj hlast rw [← hgetLast] rw [List.getLast_eq_getElem] congr omega rw [hpLast] at hEq exact hV_not_fixed D hD hEq · have hkpos : 0 < k := Nat.pos_of_ne_zero hk0 have hmid := hNoFixedInterior (k - 1) (by omega) have hfixedD : SWIGNode.fixed D ∈ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed := by exact SCM.fixSet_fixed_subset (M.fixSet X hX_obs hX_fixed) Wbase hW_obs_X hW_fixed_X (SCM.fixed_mem_fixSet M X hX_obs hX_fixed hD) have hidx : k - 1 + 1 = k := by omega rw [show p.get ⟨k - 1 + 1, by omega⟩ = p.get ⟨k, hk⟩ by congr 1; exact Fin.ext hidx] at hmid exact hmid (by rw [hEq]; exact hfixedD) have hNoXrInterior : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ ∉ X.image SWIGNode.random := by intro i hi hmX rcases Finset.mem_image.mp hmX with ⟨D, hD, hmEq⟩ set m := p.get ⟨i + 1, by omega⟩ have hmEq' : m = SWIGNode.random D := by simpa [m] using hmEq.symm have hNoOut : ∀ z, ¬ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.edge (SWIGNode.random D) z := by intro z he have hDnotW : D ∉ Wbase := by intro hDW exact (Finset.disjoint_left.mp hDisjBaseWX) hDW hD have h_eqrel : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.edge (SWIGNode.random D) z ↔ SWIGGraph.splitMonoEdgeRel (M.fixSet X hX_obs hX_fixed).dag.edge Wbase (SWIGNode.random D) z := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [h_eqrel] at he simp only [SWIGGraph.splitMonoEdgeRel, if_neg hDnotW] at he exact SCM.fixSet_random_no_children M X hX_obs hX_fixed hD z he have hadjL := hadjD i (by omega) have hadjR := hadjD (i + 1) (by omega) have hleft : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.edge (p.get ⟨i, by omega⟩) m := by rcases hadjL with h | h · simpa [m] using h · exfalso rw [show p.get ⟨i + 1, by omega⟩ = SWIGNode.random D from by simpa [m] using hmEq'] at h exact hNoOut (p.get ⟨i, by omega⟩) h have hright : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.edge (p.get ⟨i + 2, hi⟩) m := by rcases hadjR with h | h · exfalso rw [show p.get ⟨i + 1, by omega⟩ = SWIGNode.random D from by simpa [m] using hmEq'] at h exact hNoOut (p.get ⟨i + 2, hi⟩) h · simpa [m] using h have hCollD : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.IsCollider (p.get ⟨i, by omega⟩) m (p.get ⟨i + 2, hi⟩) := ⟨hleft, hright⟩ have hval := hcollD i hi simp only at hval rw [show p.get ⟨i + 1, by omega⟩ = m from rfl] at hval rw [if_pos hCollD] at hval have hm_notC : m ∉ (∅ : Finset (SWIGNode N)) ∪ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed := by intro hmC rw [Finset.empty_union] at hmC obtain ⟨n, hn⟩ := ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).fixed_is_fixed m hmC rw [hmEq'] at hn cases hn have hnotAnc : ∀ c, ¬ ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.isAncestor m c := by intro c hanc rcases ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.isAncestor_child hanc with hE | ⟨c0, hE, _⟩ · exact hNoOut c (by simpa [hmEq'] using hE) · exact hNoOut c0 (by simpa [hmEq'] using hE) simp only [DAG.bbZAncestors, DAG.ancestralSet, DAG.ancestorsSet, mem_union, mem_filter, Finset.mem_univ, true_and] at hval rcases hval with hmC | ⟨c, hcC, hmc⟩ · exact hm_notC (Finset.mem_union.mpr hmC) · exact hnotAnc c hmc refine ⟨?_, ?_⟩ · intro i hi have hdAdj := hadjD i hi rcases hdAdj with he | he · exact inl (double_edge_to_doW_of_not_fixedX M X Wbase hX_obs hX_fixed hW_obs hW_fixed hDisjBaseXW (fun D hD => hNotFixedAt i (by omega) D hD) he) · exact inr (double_edge_to_doW_of_not_fixedX M X Wbase hX_obs hX_fixed hW_obs hW_fixed hDisjBaseXW (fun D hD => hNotFixedAt (i + 1) hi D hD) he) · intro i hi have hvalD := hcollD i hi simp only at hvalD by_cases hCollW : (M.fixSet Wbase hW_obs hW_fixed).dag.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) · rw [if_pos hCollW] have hCollD : ((M.fixSet X hX_obs hX_fixed).fixSet Wbase hW_obs_X hW_fixed_X).dag.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by constructor · have hadjL := hadjD i (by omega) rcases hadjL with h | h · exact h · exfalso have hmw : (M.fixSet Wbase hW_obs hW_fixed).dag.edge (p.get ⟨i + 1, by omega⟩) (p.get ⟨i, by omega⟩) := double_edge_to_doW_of_not_fixedX M X Wbase hX_obs hX_fixed hW_obs hW_fixed hDisjBaseXW (fun D hD => hNotFixedAt (i + 1) (by omega) D hD) h exact (M.fixSet Wbase hW_obs hW_fixed).dag.asymm hmw hCollW.1 -- … truncated; follow the source link for the rest …

Causalean.SCM.frontdoor_fd3_rule2_dSep · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:326 · uses dSep , SWIGNode , instFintype , instDecidableEqSWIGNode , SCM , disjoint_base_of_disjoint_random_image , fixSet , fixSet_fixed_not_mem_of_disjoint , backdoorCriterion

7 supporting declarations (lemmas, instances)

disjoint_base_of_disjoint_random_image lemma — Disjoint random-node images have disjoint underlying base-variable sets.

hypotheses

N :

Type u_1
shared

X :

Finset N
shared

W :

Finset N
shared

hDisj :

Disjoint (W.image SWIGNode.random) (X.image SWIGNode.random)

conclusion

Disjoint W X

Proof (Lean source)

lemma disjoint_base_of_disjoint_random_image (hDisj : Disjoint (W.image SWIGNode.random) (X.image SWIGNode.random)) : Disjoint W X := (Finset.disjoint_image SWIGNode.random_injective).mp hDisj

Causalean.SCM.disjoint_base_of_disjoint_random_image · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:48
fixSet_fixed_not_mem_of_disjoint lemma — Fixing one intervention block does not add fixed copies from a disjoint block.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω
shared

X :

Finset N
shared

W :

Finset N
shared

hW_obs :

∀ D ∈ W, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hW_fixed :

∀ D ∈ W, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

hDisj :

Disjoint W X

D ∈ X :

conclusion

SWIGNode.fixed D ∉ (M.fixSet W hW_obs hW_fixed).fixed

Proof (Lean source)

lemma fixSet_fixed_not_mem_of_disjoint (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (hDisj : Disjoint W X) : ∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet W hW_obs hW_fixed).fixed := by intro D hD hmem rw [SCM.fixSet_fixed] at hmem rcases Finset.mem_union.mp hmem with hM | hWF · exact hX_fixed D hD hM · rcases Finset.mem_image.mp hWF with ⟨D0, hD0W, hEq⟩ cases hEq exact (Finset.disjoint_left.mp hDisj) hD0W hD

Causalean.SCM.fixSet_fixed_not_mem_of_disjoint · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:54
double_edge_to_doX_of_not_fixedW lemma — For two disjoint intervention blocks, an edge remaining after first fixing the W block and then the X block also remains after fixing X alone when its source is not a fixed copy from W.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω
shared

X :

Finset N
shared

W :

Finset N
shared

hX_obs :

∀ D ∈ X, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hX_fixed :

∀ D ∈ X, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hW_obs :

∀ D ∈ W, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hW_fixed :

∀ D ∈ W, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hDisj :

Disjoint W X

u v :

SWIGNode N

huW :

∀ D ∈ W, u ≠ SWIGNode.fixed D

he :

((M.fixSet W hW_obs hW_fixed).fixSet X (by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD) (fixSet_fixed_not_mem_of_disjoint M X W hW_obs hW_fixed hX_fixed hDisj)).dag.edge u v

conclusion

(M.fixSet X hX_obs hX_fixed).dag.edge u v

Proof (Lean source)

lemma double_edge_to_doX_of_not_fixedW (hDisj : Disjoint W X) {u v : SWIGNode N} (huW : ∀ D ∈ W, u ≠ SWIGNode.fixed D) (he : ((M.fixSet W hW_obs hW_fixed).fixSet X (by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD) (fixSet_fixed_not_mem_of_disjoint M X W hW_obs hW_fixed hX_fixed hDisj)).dag.edge u v) : (M.fixSet X hX_obs hX_fixed).dag.edge u v := by have hWXedge : ((M.fixSet W hW_obs hW_fixed).fixSet X (by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD) (fixSet_fixed_not_mem_of_disjoint M X W hW_obs hW_fixed hX_fixed hDisj)).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel (SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge W) X u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] have hXedge : (M.fixSet X hX_obs hX_fixed).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge X u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [hWXedge] at he rw [hXedge] cases u with | random d => by_cases hdX : d ∈ X · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdX] at he · simp only [SWIGGraph.splitMonoEdgeRel, if_neg hdX] at he ⊢ by_cases hdW : d ∈ W · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdW] at he · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdW] using he | fixed d => by_cases hdX : d ∈ X · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdX] at he ⊢ have hdW : d ∉ W := by intro hdW exact (Finset.disjoint_left.mp hDisj) hdW hdX simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdW] using he · simp only [SWIGGraph.splitMonoEdgeRel, if_neg hdX] at he ⊢ by_cases hdW : d ∈ W · exact (huW d hdW rfl).elim · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdW] using he

Causalean.SCM.double_edge_to_doX_of_not_fixedW · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:67
isAncestorAvoiding_of_sinks lemma — In a finite directed acyclic graph, if every vertex of a designated set is a sink, then every ancestral path witnessed between two vertices can be chosen with all internal vertices outside that set.

hypotheses

V :

Type*
DecidableEq V
Fintype V

G :

DAG V

C :

Finset V

hSink :

∀ c ∈ C, ∀ v, ¬ G.edge c v

u v :

V

h :

G.isAncestor u v

conclusion

G.isAncestorAvoiding C u v

Proof (Lean source)

lemma isAncestorAvoiding_of_sinks {V : Type*} [DecidableEq V] [Fintype V] (G : DAG V) (C : Finset V) (hSink : ∀ c ∈ C, ∀ v, ¬ G.edge c v) {u v : V} (h : G.isAncestor u v) : G.isAncestorAvoiding C u v := by induction h with | edge he => exact DAG.isAncestorAvoiding.edge he | @trans w v hprev he ih => exact DAG.isAncestorAvoiding.trans ih (by intro hwC exact hSink w hwC v he) he

Causalean.SCM.isAncestorAvoiding_of_sinks · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:109
not_fixedW_of_incoming_doX lemma — If fixed copies of the W block are absent in the original model, no edge after fixing X can end at a fixed copy from W.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω
shared

X :

Finset N
shared

W :

Finset N
shared

hX_obs :

∀ D ∈ X, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hX_fixed :

∀ D ∈ X, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hW_fixed :

∀ D ∈ W, SWIGNode.fixed D ∉ M.fixed

u w :

SWIGNode N

he :

(M.fixSet X hX_obs hX_fixed).dag.edge u w

D ∈ W :

conclusion

w ≠ SWIGNode.fixed D

Proof (Lean source)

lemma not_fixedW_of_incoming_doX (hW_fixed : ∀ D ∈ W, SWIGNode.fixed D ∉ M.fixed) {u w : SWIGNode N} (he : (M.fixSet X hX_obs hX_fixed).dag.edge u w) : ∀ D ∈ W, w ≠ SWIGNode.fixed D := by intro D hD hEq have hmem : u ∈ (M.fixSet X hX_obs hX_fixed).dag.parents w := (M.fixSet X hX_obs hX_fixed).dag.mem_parents.mpr he have hroot : (M.fixSet X hX_obs hX_fixed).dag.parents (SWIGNode.fixed D) = ∅ := by by_cases hDX : D ∈ X · exact (M.fixSet X hX_obs hX_fixed).fixed_are_roots _ (SCM.fixed_mem_fixSet M X hX_obs hX_fixed hDX) · -- If `D ∉ X`, the fixed node is not a target of `do(X)` and is not fixed in -- `M`; its incoming edges remain absent by `fixed_outside_fixed_isolated`. ext a constructor · intro ha have haEdge : (M.fixSet X hX_obs hX_fixed).dag.edge a (SWIGNode.fixed D) := (M.fixSet X hX_obs hX_fixed).dag.mem_parents.mp ha have h_eqrel : (M.fixSet X hX_obs hX_fixed).dag.edge a (SWIGNode.fixed D) ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge X a (SWIGNode.fixed D) := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [h_eqrel] at haEdge have hrootM : M.dag.parents (SWIGNode.fixed D) = ∅ := (M.fixed_outside_fixed_isolated D (hW_fixed D hD)).1 cases a with | random aD => by_cases haX : aD ∈ X · simp only [SWIGGraph.splitMonoEdgeRel, if_pos haX] at haEdge · simp only [SWIGGraph.splitMonoEdgeRel, if_neg haX] at haEdge have hpar : SWIGNode.random aD ∈ M.dag.parents (SWIGNode.fixed D) := M.dag.mem_parents.mpr haEdge rw [hrootM] at hpar exact False.elim ((notMem_empty _) hpar) | fixed aD => by_cases haX : aD ∈ X · simp only [SWIGGraph.splitMonoEdgeRel, if_pos haX] at haEdge have hpar : SWIGNode.random aD ∈ M.dag.parents (SWIGNode.fixed D) := M.dag.mem_parents.mpr haEdge rw [hrootM] at hpar exact False.elim ((notMem_empty _) hpar) · simp only [SWIGGraph.splitMonoEdgeRel, if_neg haX] at haEdge have hpar : SWIGNode.fixed aD ∈ M.dag.parents (SWIGNode.fixed D) := M.dag.mem_parents.mpr haEdge rw [hrootM] at hpar exact False.elim ((notMem_empty _) hpar) · intro ha exact False.elim ((notMem_empty _) ha) rw [hEq, hroot] at hmem exact (notMem_empty _) hmem

Causalean.SCM.not_fixedW_of_incoming_doX · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:126
double_edge_to_doW_of_not_fixedX lemma — For two disjoint intervention blocks, an edge remaining after first fixing the X block and then the W block also remains after fixing W alone when its source is not a fixed copy from X.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω
shared

X :

Finset N
shared

W :

Finset N
shared

hX_obs :

∀ D ∈ X, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hX_fixed :

∀ D ∈ X, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hW_obs :

∀ D ∈ W, Causalean.Graph.SWIGNode.random D ∈ M.observed
shared

hW_fixed :

∀ D ∈ W, Causalean.Graph.SWIGNode.fixed D ∉ M.fixed
shared

hDisj :

Disjoint X W

u v :

SWIGNode N

huX :

∀ D ∈ X, u ≠ SWIGNode.fixed D

he :

((M.fixSet X hX_obs hX_fixed).fixSet W (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M W X hX_obs hX_fixed hW_fixed hDisj)).dag.edge u v

conclusion

(M.fixSet W hW_obs hW_fixed).dag.edge u v

Proof (Lean source)

lemma double_edge_to_doW_of_not_fixedX (hDisj : Disjoint X W) {u v : SWIGNode N} (huX : ∀ D ∈ X, u ≠ SWIGNode.fixed D) (he : ((M.fixSet X hX_obs hX_fixed).fixSet W (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M W X hX_obs hX_fixed hW_fixed hDisj)).dag.edge u v) : (M.fixSet W hW_obs hW_fixed).dag.edge u v := by have hXWedge : ((M.fixSet X hX_obs hX_fixed).fixSet W (by intro D hD; simpa [SCM.fixSet_observed] using hW_obs D hD) (fixSet_fixed_not_mem_of_disjoint M W X hX_obs hX_fixed hW_fixed hDisj)).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel (SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge X) W u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] have hWedge : (M.fixSet W hW_obs hW_fixed).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge W u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [hXWedge] at he rw [hWedge] cases u with | random d => by_cases hdW : d ∈ W · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdW] at he · simp only [SWIGGraph.splitMonoEdgeRel, if_neg hdW] at he ⊢ by_cases hdX : d ∈ X · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdX] at he · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdX] using he | fixed d => by_cases hdW : d ∈ W · simp only [SWIGGraph.splitMonoEdgeRel, if_pos hdW] at he ⊢ have hdX : d ∉ X := by intro hdX exact (Finset.disjoint_left.mp hDisj) hdX hdW simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdX] using he · simp only [SWIGGraph.splitMonoEdgeRel, if_neg hdW] at he ⊢ by_cases hdX : d ∈ X · exact (huX d hdX rfl).elim · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg hdX] using he

Causalean.SCM.double_edge_to_doW_of_not_fixedX · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:183
frontdoor_fd1_rule3_nonDesc theorem — Given a finite structural causal model, treatment and mediator sets with valid intervention copies, and an outcome set, if the outcome is d-separated from the fixed treatment copies after intervening on treatment and conditioning on the random mediator copies, and the random mediator and treatment copies are disjoint, then for any outcome node and treatment node, the fixed treatment copy is not an ancestor of the outcome after the two interventions.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X Wbase :

Finset N

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

hW_obs :

∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed

hW_fixed :

∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed

Y :

Finset (SWIGNode N)

hFD1 :

(M.fixSet X hX_obs hX_fixed).dag.dSep Y (X.image SWIGNode.fixed) (Wbase.image SWIGNode.random)

hDisj_WX :

Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)

v ∈ Y :

d ∈ X :

conclusion

¬ ((M.fixSet Wbase hW_obs hW_fixed).fixSet X (by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD) (fixSet_fixed_not_mem_of_disjoint M X Wbase hW_obs hW_fixed hX_fixed (disjoint_base_of_disjoint_random_image X Wbase hDisj_WX))).dag.isAncestor (SWIGNode.fixed d) v

Proof (Lean source)

theorem frontdoor_fd1_rule3_nonDesc (M : SCM N Ω) (X Wbase : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (hW_obs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed) (hW_fixed : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hFD1 : (M.fixSet X hX_obs hX_fixed).dag.dSep Y (X.image SWIGNode.fixed) (Wbase.image SWIGNode.random)) (hDisj_WX : Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)) : ∀ v ∈ Y, ∀ d ∈ X, ¬ ((M.fixSet Wbase hW_obs hW_fixed).fixSet X (by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD) (fixSet_fixed_not_mem_of_disjoint M X Wbase hW_obs hW_fixed hX_fixed (disjoint_base_of_disjoint_random_image X Wbase hDisj_WX))).dag.isAncestor (SWIGNode.fixed d) v := by classical intro v hv d hd hanc have hDisjBase : Disjoint Wbase X := disjoint_base_of_disjoint_random_image X Wbase hDisj_WX let hX_obs_W : ∀ D ∈ X, SWIGNode.random D ∈ (M.fixSet Wbase hW_obs hW_fixed).observed := by intro D hD; simpa [SCM.fixSet_observed] using hX_obs D hD let hX_fixed_W : ∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet Wbase hW_obs hW_fixed).fixed := fixSet_fixed_not_mem_of_disjoint M X Wbase hW_obs hW_fixed hX_fixed hDisjBase let Gdouble := ((M.fixSet Wbase hW_obs hW_fixed).fixSet X hX_obs_W hX_fixed_W).dag have hAvoid : Gdouble.isAncestorAvoiding (Wbase.image SWIGNode.random) (SWIGNode.fixed d) v := by refine isAncestorAvoiding_of_sinks Gdouble (Wbase.image SWIGNode.random) ?_ hanc intro c hc z he rcases Finset.mem_image.mp hc with ⟨D, hD, rfl⟩ have hDnotX : D ∉ X := by intro hDX exact (Finset.disjoint_left.mp hDisjBase) hD hDX have h_eqrel : Gdouble.edge (SWIGNode.random D) z ↔ SWIGGraph.splitMonoEdgeRel (M.fixSet Wbase hW_obs hW_fixed).dag.edge X (SWIGNode.random D) z := by simp only [Gdouble, SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [h_eqrel] at he simp only [SWIGGraph.splitMonoEdgeRel, if_neg hDnotX] at he exact SCM.fixSet_random_no_children M Wbase hW_obs hW_fixed hD z he obtain ⟨p, hplen, hphead, hplast, hpedge_double, hpintW⟩ := hAvoid.exists_path have hpedge_doX : ∀ (i : ℕ) (hi : i + 1 < p.length), (M.fixSet X hX_obs hX_fixed).dag.edge (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, hi⟩) := by intro i hi refine double_edge_to_doX_of_not_fixedW M X Wbase hX_obs hX_fixed hW_obs hW_fixed hDisjBase ?_ (hpedge_double i hi) intro D hD hEq rcases Nat.eq_zero_or_pos i with hi0 | hi0 · subst hi0 have : d = D := by have hp0 : p.get ⟨0, by omega⟩ = SWIGNode.fixed d := by cases p with | nil => simp at hplen | cons a t => simp only [List.head?_cons] at hphead exact Option.some.inj hphead rw [hp0] at hEq cases hEq rfl cases this exact (Finset.disjoint_left.mp hDisjBase) hD hd · have hprevDouble : Gdouble.edge (p.get ⟨i - 1, by omega⟩) (p.get ⟨i, by omega⟩) := by have hprev0 := hpedge_double (i - 1) (by omega) have hidx : i - 1 + 1 = i := by omega simpa [Gdouble, hidx] using hprev0 have hmem : p.get ⟨i - 1, by omega⟩ ∈ Gdouble.parents (p.get ⟨i, by omega⟩) := Gdouble.mem_parents.mpr hprevDouble have hfixedW_double : SWIGNode.fixed D ∈ ((M.fixSet Wbase hW_obs hW_fixed).fixSet X hX_obs_W hX_fixed_W).fixed := by exact SCM.fixSet_fixed_subset (M.fixSet Wbase hW_obs hW_fixed) X hX_obs_W hX_fixed_W (SCM.fixed_mem_fixSet M Wbase hW_obs hW_fixed hD) have hroot : Gdouble.parents (SWIGNode.fixed D) = ∅ := ((M.fixSet Wbase hW_obs hW_fixed).fixSet X hX_obs_W hX_fixed_W).fixed_are_roots _ hfixedW_double rw [hEq, hroot] at hmem exact (notMem_empty _) hmem have hpact : (M.fixSet X hX_obs hX_fixed).dag.IsActiveWalk (Wbase.image SWIGNode.random) p := (M.fixSet X hX_obs hX_fixed).dag.isActiveWalk_of_directed hpedge_doX hpintW have hvReach : v ∈ (M.fixSet X hX_obs hX_fixed).dag.bbReachableVertices (Wbase.image SWIGNode.random) (X.image SWIGNode.fixed) := by rw [(M.fixSet X hX_obs hX_fixed).dag.bbReachableVertices_iff_activeWalk] refine ⟨SWIGNode.fixed d, Finset.mem_image.mpr ⟨d, hd, rfl⟩, p, hplen, hpact, ?_, ?_⟩ · exact hphead · exact hplast have hSepSymm := (M.fixSet X hX_obs hX_fixed).dag.dSep_symm _ _ _ hFD1 exact (Finset.disjoint_left.mp hSepSymm.2.2.2) hvReach hv

Causalean.SCM.frontdoor_fd1_rule3_nonDesc · Causalean/SCM/ID/Toolkit/FrontdoorGraph.lean:227

ObsChainRule 1 core · 2 supporting A single reusable disintegration lemma: the Y-marginal of an SCM's observational kernel factors as the conditional kernel Y | CC composed with the CC-marginal. ★ obsKernel_map_eq_obsCondKernel_comp

Observational chain rule (do-calculus identification toolkit, Layer 3)

A single reusable disintegration lemma: the Y-marginal of an SCM's observational kernel factors as the conditional kernel Y | CC composed with the CC-marginal. In probability notation, at a fixed parameter slice s,

P(Y | s) = ∫_{cc} P(Y | CC = cc, s) dP(CC | s).

Both the do-side reduction and the adjustment-side reduction of every backdoor/frontdoor identification proof are instances of this lemma; previously each proof re-derived it by hand from obsCondPairKernel.disintegrate (≈40 lines, twice in SCM/ID/Backdoor.lean). Factoring it out is the keystone of the identification toolkit.

The only genuinely-supplied typeclass is finiteness of M.obsKernel; every ValuesOn-product instance (standard-Borel, nonempty, countably-generated) infers from the per-node primitives because ValuesOn I Ω is a finite product.

theorem obsKernel_map_eq_obsCondKernel_comp reviewed

Causalean.SCM

Observational chain rule. Fix a structural causal model M, a target node set Y and a conditioning node set CC with Y contained in the observed nodes and CC contained in the observed nodes. Then, at a fixed parameter slice s, the observational distribution of Y equals the observational conditional law of Y given CC composed with the observational marginal law of CC.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

Y CC :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hCC :

CC ⊆ M.observed

StandardBorelSpace (ValuesOn Y (swigΩ Ω))

Nonempty (ValuesOn Y (swigΩ Ω))

CountableOrCountablyGenerated (M.FixedValues) (ValuesOn CC (swigΩ Ω))

s :

M.FixedValues

conclusion

(M.obsKernel s).map (valuesProjection hY)

= (M.obsCondKernel Y CC hY hCC).sectR s ∘ₘ ((M.obsKernel s).map (valuesProjection hCC))

Proof (Lean source)

theorem obsKernel_map_eq_obsCondKernel_comp (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated (M.FixedValues) (ValuesOn CC (swigΩ Ω))] (s : M.FixedValues) : (M.obsKernel s).map (valuesProjection hY) = (M.obsCondKernel Y CC hY hCC).sectR s ∘ₘ ((M.obsKernel s).map (valuesProjection hCC)) := by haveI : IsMarkovKernel (M.obsCondKernel Y CC hY hCC) := by unfold SCM.obsCondKernel; infer_instance haveI hPairFin : IsFiniteKernel (M.obsCondPairKernel Y CC hY hCC) := by haveI : IsMarkovKernel (M.obsCondPairKernel Y CC hY hCC) := by unfold SCM.obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY)) infer_instance have hDisint : (M.obsCondPairKernel Y CC hY hCC).fst ⊗ₖ M.obsCondKernel Y CC hY hCC = M.obsCondPairKernel Y CC hY hCC := by change (M.obsCondPairKernel Y CC hY hCC).fst ⊗ₖ (M.obsCondPairKernel Y CC hY hCC).condKernel = M.obsCondPairKernel Y CC hY hCC exact ProbabilityTheory.Kernel.disintegrate _ _ have hAt : ((M.obsCondPairKernel Y CC hY hCC).fst ⊗ₖ M.obsCondKernel Y CC hY hCC) s = M.obsCondPairKernel Y CC hY hCC s := by rw [hDisint] rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] at hAt have hFst : (M.obsCondPairKernel Y CC hY hCC).fst s = (M.obsKernel s).map (valuesProjection hCC) := by rw [ProbabilityTheory.Kernel.fst_apply, SCM.obsCondPairKernel, ProbabilityTheory.Kernel.map_apply _ (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY)), MeasureTheory.Measure.map_map measurable_fst (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY))] rfl have hSnd : (M.obsCondPairKernel Y CC hY hCC s).snd = (M.obsKernel s).map (valuesProjection hY) := by rw [MeasureTheory.Measure.snd, SCM.obsCondPairKernel, ProbabilityTheory.Kernel.map_apply _ (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY)), MeasureTheory.Measure.map_map measurable_snd (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY))] rfl have hAtSnd := congrArg MeasureTheory.Measure.snd hAt rw [hFst, MeasureTheory.Measure.snd_compProd, hSnd] at hAtSnd exact hAtSnd.symm

Causalean.SCM.obsKernel_map_eq_obsCondKernel_comp · Causalean/SCM/ID/Toolkit/ObsChainRule.lean:49 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , ObservedValues , obsCondKernel , obsKernel

2 supporting declarations (lemmas, instances)

obsKernel_empty_projection_eq_dirac lemma — Empty-projection collapse. Projecting the observational kernel onto the empty node set yields a Dirac measure: ValuesOn ∅ is a subsingleton, so the projected Markov kernel is the point mass at its unique value. The base case of any conditioning set shrinking to ∅ in a fixing/adjustment step.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

hEmpty :

(∅ : Finset (SWIGNode N)) ⊆ M.observed

s :

M.FixedValues

c :

ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)

conclusion

(M.obsKernel s).map (valuesProjection hEmpty) = dirac c

Proof (Lean source)

lemma obsKernel_empty_projection_eq_dirac (M : SCM N Ω) (hEmpty : (∅ : Finset (SWIGNode N)) ⊆ M.observed) (s : M.FixedValues) (c : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) : (M.obsKernel s).map (valuesProjection hEmpty) = dirac c := by ext S hS by_cases hSEmpty : S = ∅ · simp [hSEmpty] · have hUniv : S = univ := by apply Set.eq_univ_of_forall intro x by_contra hx apply hSEmpty ext y constructor · intro hy have : y = x := Subsingleton.elim y x exact False.elim (hx (this ▸ hy)) · intro hy simp at hy rw [hUniv] rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection _) MeasurableSet.univ] rw [show (valuesProjection hEmpty) ⁻¹' univ = univ by ext x simp] simp [M.obsKernel_apply_univ s]

Causalean.SCM.obsKernel_empty_projection_eq_dirac · Causalean/SCM/ID/Toolkit/ObsChainRule.lean:133
obsCondKernel_empty_eq_marginal lemma — Empty-conditioning collapse. Conditioning obsCondKernel Y on the empty set collapses to the plain Y-marginal (M.obsKernel s).map π_Y. This is the reusable step every do-calculus factorization performs when a conditioning block becomes empty (e.g. the first node of a fixing sequence); it is graph-agnostic in M, so it applies verbatim to any stacked-intervention model M.fixSet ….

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

Y :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

StandardBorelSpace (ValuesOn Y (swigΩ Ω))

Nonempty (ValuesOn Y (swigΩ Ω))

s :

M.FixedValues

c :

ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)

conclusion

M.obsCondKernel Y (∅ : Finset (SWIGNode N)) hY (empty_subset M.observed) (s, c)
= (M.obsKernel s).map (valuesProjection hY)

Proof (Lean source)

lemma obsCondKernel_empty_eq_marginal (M : SCM N Ω) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] (s : M.FixedValues) (c : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) : M.obsCondKernel Y (∅ : Finset (SWIGNode N)) hY (Finset.empty_subset M.observed) (s, c) = (M.obsKernel s).map (valuesProjection hY) := by have hChain := SCM.obsKernel_map_eq_obsCondKernel_comp M Y (∅ : Finset (SWIGNode N)) hY (Finset.empty_subset M.observed) s have hEmpty : (M.obsKernel s).map (valuesProjection (Finset.empty_subset M.observed : (∅ : Finset (SWIGNode N)) ⊆ M.observed)) = dirac c := obsKernel_empty_projection_eq_dirac M (Finset.empty_subset M.observed) s c calc M.obsCondKernel Y (∅ : Finset (SWIGNode N)) hY (Finset.empty_subset M.observed) (s, c) = (M.obsCondKernel Y (∅ : Finset (SWIGNode N)) hY (Finset.empty_subset M.observed)).sectR s ∘ₘ dirac c := by rw [MeasureTheory.Measure.dirac_bind] · rfl · fun_prop _ = (M.obsCondKernel Y (∅ : Finset (SWIGNode N)) hY (Finset.empty_subset M.observed)).sectR s ∘ₘ ((M.obsKernel s).map (valuesProjection (Finset.empty_subset M.observed : (∅ : Finset (SWIGNode N)) ⊆ M.observed))) := by rw [hEmpty] _ = (M.obsKernel s).map (valuesProjection hY) := hChain.symm

Causalean.SCM.obsCondKernel_empty_eq_marginal · Causalean/SCM/ID/Toolkit/ObsChainRule.lean:164