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 — the Rule-2 applicator: from a backdoorCriterion (plus overlap + 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 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

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 :

M.toSWIGGraph.backdoorCriterion 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 : M.toSWIGGraph.backdoorCriterion 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:55 · uses dSep , SCM , fixSet , backdoorCriterion , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

4 supporting declarations (lemmas, instances)

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

hypotheses

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:44
backdoorCriterion_W_nonDesc theorem — Backdoor criterion (i), post-intervention non-descendance form.

hypotheses

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 :

M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z

conclusion

∀ x ∈ X, ∀ v ∈ Z, ¬ (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 : M.toSWIGGraph.backdoorCriterion 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:107
backdoorCriterion_W_nonDescM1 theorem — Backdoor criterion (i), base-graph non-descendance form.

hypotheses

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 :

M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z

conclusion

∀ D ∈ X, ∀ w ∈ Z, ¬ 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 : M.toSWIGGraph.backdoorCriterion 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:124
backdoor_rule2_ae theorem — Rule-2 applicator (backdoor form).

hypotheses

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

hXr :

X.image SWIGNode.random ⊆ M.observed

hXrZ :

X.image SWIGNode.random ∪ Z ⊆ M.observed

hDisj_YXr :

Disjoint Y (X.image SWIGNode.random)

hDisj_XrZ :

Disjoint (X.image SWIGNode.random) Z

h_bd :

M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z

s0 :

M.FixedValues

hOverlap :

∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix Z hXrZ s

hPositivity_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))

conclusion

∀ᵐ p ∂((M.obsKernel s0).map (valuesProjection hXr) ⊗ₘ 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 hXrZ (s0, valuesUnionMk p.1 p.2)

Proof (Lean source)

theorem backdoor_rule2_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) (hXr : X.image SWIGNode.random ⊆ M.observed) (hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed) (hDisj_YXr : Disjoint Y (X.image SWIGNode.random)) (hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z) (h_bd : M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z) (s0 : M.FixedValues) (hOverlap : ∀ s : (M.fixSet X hObs hFix).FixedValues, Rule2JointOverlap M X hObs hFix Z hXrZ s) (hPositivity_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))) : ∀ᵐ p ∂((M.obsKernel s0).map (valuesProjection hXr) ⊗ₘ 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 hXrZ (s0, valuesUnionMk p.1 p.2) := SCM.obsCondKernel_fixSet_eq_ae_witness M X hObs hFix Y Z hY hZ hXr hXrZ (backdoorCriterion_dSep_fixSet M X hObs hFix Y Z hY hXr 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 · Causalean/SCM/ID/Toolkit/Derivation.lean:138

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

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 :

M.toSWIGGraph.backdoorCriterion 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 : M.toSWIGGraph.backdoorCriterion 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_activePath] 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_activePath] 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 · have hadjR := hadjD (i + 1) (by omega) -- … truncated; follow the source link for the rest …

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

7 supporting declarations (lemmas, instances)

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

hypotheses

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:41
fixSet_fixed_not_mem_of_disjoint lemma — Fixing one intervention block does not add fixed copies from a disjoint block.

hypotheses

hX_fixed :

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

hDisj :

Disjoint W X

conclusion

∀ D ∈ X, 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:47
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

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:60
isAncestorAvoiding_of_sinks lemma

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:102
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

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

conclusion

∀ D ∈ W, 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 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 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 elim ((notMem_empty _) hpar) · intro ha exact 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:116
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

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:173
frontdoor_fd1_rule3_nonDesc theorem — G2: corrected-FD1 Rule-3 non-ancestry premise.

hypotheses

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)

conclusion

∀ 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

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.IsActivePath (Wbase.image SWIGNode.random) p := (M.fixSet X hX_obs hX_fixed).dag.isActivePath_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_activePath] 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:217

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

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:40 · uses SCM , FixedValues , ObservedValues , obsCondKernel , obsKernel , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection

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

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 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:124
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

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:155