SCM.ID.GraphicalThms
Graphical identification theorems: c-component factorization and related structure results.
DoGFormulaTian 7 core · 11 supporting · 3 submodules The density of the law of the ancestors of the outcome after an intervention do(X) factorizes as a product of one factor per c-component (district) of the post-intervention ancestral graph, each factor being the product IDAlgorithmRec 8 core · 7 supporting · 2 submodules Soundness of the Tian–Shpitser ID algorithm in its recursive form, for structural causal models with finitely many values per variable and positive observational probabilities.
DoGFormula 10 core · 15 supporting This file builds the graph-side objects over which the truncated g-formula for the do-law Y-marginal is assembled. ★ subset_fixObservedAncestralSet
Geometric foundation of the do-law g-formula (Tian, fixing route)
This file builds the graph-side objects over which the truncated g-formula for the
do-law Y-marginal is assembled. Intervening on a treatment set X mutilates the
SWIG graph to G_X = (M.fixSet X).toSWIGGraph (the monolithic split splitMono X).
Tian's identification of P(Y ∣ do(X)) only involves the part of the do-law lying
on the ancestors of the query in the mutilated graph, and factorizes that part
over the c-components of the induced ancestral subgraph.
* fixAncestralSet — the ancestors of Y (together with Y) in the mutilated
graph G_X; the support of the relevant do-law marginal.
* fixTruncCComponentSet — the c-components of G_X induced on that ancestral set;
the index set of the truncated product.
These are exactly the objects the success certificate idSucceeds ranges over
(∀ S ∈ (G_X.induce Ystar).cComponentSet, cFactorReachable G (containingCComponent G S) S),
named here for use in the measure-theoretic g-formula. The factorization itself —
the do-law Y-marginal equals the product over fixTruncCComponentSet of the
recovered full-district c-factors (each a functional of obsDensity via
condKernel_fixSet_identity_of_nonAncestor, with the truncation realized by the fixing operation M.fixSet Wn) —
is developed by the downstream Tian density and ID soundness layers.
def interventionValid reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables, an intervention set in a SWIG graph is valid exactly when every intervention variable's random node is observed and its fixed node is not already fixed.
def containingCComponent reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables, a SWIG graph, and a finite node set, the containing c-component is the c-component containing an arbitrary member of that set when it is nonempty, and is empty otherwise.
def cFactorReachable reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables, a SWIG graph, a proposed containing node set, and a target node set, structural c-factor reachability holds exactly when the target is nonempty, is contained in the proposed set, and is a c-component of the graph.
def idSucceeds reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables, an intervention set, an outcome-node set, and a SWIG graph, the no-additional-fixing ID success certificate holds when the intervention is valid, the outcome nodes are observed, no intervention variable's random node is an outcome node, and every c-component of the post-intervention ancestral induced graph is structurally c-factor reachable from its containing original c-component.
Definition (Lean source)
parameters
def
idSucceeds X Y G :
Prop
given by
∃ hX : interventionValid X G,
let GX := G.splitMono X hX.1 hX.2 let Ystar := GX.dag.ancestralSet Y Y ⊆ G.observed ∧
(∀ d ∈ X, SWIGNode.random d ∉ Y) ∧
def fixAncestralSet reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, and a query-node set, the post-intervention ancestral set is the query set together with all of its ancestors in the intervened graph.
def fixTruncCComponentSet reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, and a query-node set, the truncated c-component index set is the set of c-components of the intervened graph induced on the query's post-intervention ancestors.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
given by
((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).cComponentSet
def fixObservedAncestralSet reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, and a query-node set, the observed post-intervention ancestral set is the intersection of its post-intervention ancestors with the observed nodes of the intervened model.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
given by
fixAncestralSet M X hObs hFix Y ∩ (M.fixSet X hObs hFix).observed
def pinnedExtend reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with nonempty measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, a query-node set, and a fixed-value intervention slice, the pinned extension maps each assignment on the observed post-intervention ancestors to an assignment on all original observed nodes, using the slice's fixed value at intervened random coordinates, the supplied ancestral assignment at its remaining covered coordinates, and arbitrary values elsewhere.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
∀ n, Nonempty (Ω n)
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
sDo :
(M.fixSet X hObs hFix).FixedValues
def
pinnedExtend M X hObs hFix Y sDo :
given by
fun xD v
=> match v.val with | SWIGNode.random d => if hd : d ∈ X then sDo ⟨SWIGNode.fixed d, mem_union_right _ (Finset.mem_image.mpr ⟨d, hd, rfl⟩)⟩ else if hvD : SWIGNode.random d ∈ fixObservedAncestralSet M X hObs hFix Y then xD ⟨SWIGNode.random d, hvD⟩ else Classical.arbitrary _ | SWIGNode.fixed d => if hvD : SWIGNode.fixed d ∈ fixObservedAncestralSet M X hObs hFix Y then xD ⟨SWIGNode.fixed d, hvD⟩ else Classical.arbitrary _
def doObsKernelAncestralMarginal reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, and a query-node set, the post-intervention observed-ancestral marginal kernel maps fixed intervention values to the distribution of the observed ancestors of the query.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
def
doObsKernelAncestralMarginal M X hObs hFix Y :
Kernel (M.fixSet X hObs hFix).FixedValues (ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω))
given by
(M.fixSet X hObs hFix).obsKernel.map (valuesProjection inter_subset_right)
theorem subset_fixObservedAncestralSet reviewed
⚑ flagged
Causalean.SCM.ID
For a valid intervention set X (observed, not already fixed) and an outcome set Y contained in the observed nodes, Y is contained in its own post-intervention observed-ancestral closure: it lies in the post-intervention ancestral set (subset_fixAncestralSet) and in the observed nodes.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
conclusion
Y ⊆ fixObservedAncestralSet M X hObs hFix Y
Proof (Lean source)
theorem subset_fixObservedAncestralSet
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) :
Y ⊆ fixObservedAncestralSet M X hObs hFix Y :=
Finset.subset_inter (subset_fixAncestralSet M X hObs hFix Y)
((SCM.fixSet_observed M X hObs hFix).symm ▸ hY)
15 supporting declarations (lemmas, instances)
-
subset_fixAncestralSettheorem — The post-intervention ancestral set contains the query.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedconclusionY ⊆ fixAncestralSet M X hObs hFix YProof (Lean source)
theorem subset_fixAncestralSet (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) : Y ⊆ fixAncestralSet M X hObs hFix Y := (M.fixSet X hObs hFix).toSWIGGraph.dag.subset_ancestralSet Y -
splitMono_edge_from_unobserved_ifflemma — Under a valid monolithic intervention split, a directed edge from an unobserved node exists exactly when that edge existed in the original graph.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedu v :SWIGNode Nhu :u ∈ G.unobservedconclusion(G.splitMono X hObs hFix).dag.edge u v ↔ G.dag.edge u vProof (Lean source)
lemma splitMono_edge_from_unobserved_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {u v : SWIGNode N} (hu : u ∈ G.unobserved) : (G.splitMono X hObs hFix).dag.edge u v ↔ G.dag.edge u v := by obtain ⟨d, rfl⟩ := G.unobserved_is_random u hu have hdX : d ∉ X := by intro hd exact (Finset.disjoint_left.mp G.obs_unobs_disjoint (hObs d hd)) hu simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel, hdX] -
splitMono_directlyConfounded_ifflemma — Under a valid monolithic intervention split, two nodes are directly confounded exactly when they were directly confounded in the original graph.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv₁ v₂ :SWIGNode Nconclusion(G.splitMono X hObs hFix).directlyConfounded v₁ v₂ ↔ G.directlyConfounded v₁ v₂Proof (Lean source)
lemma splitMono_directlyConfounded_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v₁ v₂ : SWIGNode N) : (G.splitMono X hObs hFix).directlyConfounded v₁ v₂ ↔ G.directlyConfounded v₁ v₂ := by constructor · rintro ⟨hne, u, hu, hu₁, hu₂⟩ exact ⟨hne, u, hu, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mp hu₁, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mp hu₂⟩ · rintro ⟨hne, u, hu, hu₁, hu₂⟩ exact ⟨hne, u, hu, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mpr hu₁, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mpr hu₂⟩ -
splitMono_bidirectedReachable_ifflemma — A valid monolithic intervention split leaves bidirected reachability between any two SWIG nodes unchanged.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv w :SWIGNode Nconclusion(G.splitMono X hObs hFix).bidirectedReachable v w ↔ G.bidirectedReachable v wProof (Lean source)
lemma splitMono_bidirectedReachable_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v w : SWIGNode N) : (G.splitMono X hObs hFix).bidirectedReachable v w ↔ G.bidirectedReachable v w := by constructor · intro h induction h with | refl hv => exact SWIGGraph.bidirectedReachable.refl hv | step hreach hconf ih => exact SWIGGraph.bidirectedReachable.step ih ((splitMono_directlyConfounded_iff G X hObs hFix _ _).mp hconf) · intro h induction h with | refl hv => exact SWIGGraph.bidirectedReachable.refl hv | step hreach hconf ih => exact SWIGGraph.bidirectedReachable.step ih ((splitMono_directlyConfounded_iff G X hObs hFix _ _).mpr hconf) -
splitMono_cComponentOf_eqlemma — Under a valid monolithic intervention split, the bidirected component containing any SWIG node is the same as it was before intervention.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode Nconclusion(G.splitMono X hObs hFix).cComponentOf v = G.cComponentOf vProof (Lean source)
lemma splitMono_cComponentOf_eq (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v : SWIGNode N) : (G.splitMono X hObs hFix).cComponentOf v = G.cComponentOf v := by by_cases hv : v ∈ G.observed · apply Finset.Subset.antisymm · intro w hw rw [G.mem_cComponentOf_iff_reachable hv] exact (splitMono_bidirectedReachable_iff G X hObs hFix v w).mp (((G.splitMono X hObs hFix).mem_cComponentOf_iff_reachable hv).mp hw) · intro w hw rw [(G.splitMono X hObs hFix).mem_cComponentOf_iff_reachable hv] exact (splitMono_bidirectedReachable_iff G X hObs hFix v w).mpr ((G.mem_cComponentOf_iff_reachable hv).mp hw) · simp [SWIGGraph.cComponentOf, SWIGGraph.bidirectedBFS, hv] -
splitMono_cComponentSet_eqlemma — Splitting a graph under a valid monolithic intervention leaves its partition into bidirected connected components unchanged.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusion(G.splitMono X hObs hFix).cComponentSet = G.cComponentSetProof (Lean source)
lemma splitMono_cComponentSet_eq (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : (G.splitMono X hObs hFix).cComponentSet = G.cComponentSet := by ext C simp [SWIGGraph.cComponentSet, splitMono_cComponentOf_eq G X hObs hFix] -
splitMono_no_edge_from_intervened_randomlemma — Under a valid monolithic intervention split, the random copy of an intervened variable has no outgoing directed edge.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedd :Nhd :d ∈ Xv :SWIGNode Nconclusion¬ (G.splitMono X hObs hFix).dag.edge (SWIGNode.random d) vProof (Lean source)
lemma splitMono_no_edge_from_intervened_random (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {d : N} (hd : d ∈ X) (v : SWIGNode N) : ¬ (G.splitMono X hObs hFix).dag.edge (SWIGNode.random d) v := by simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel, hd] -
splitMono_not_isAncestor_from_intervened_randomlemma — After a valid monolithic intervention split, the random copy of an intervened variable is not an ancestor of any node.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedd :Nhd :d ∈ Xv :SWIGNode Nconclusion¬ (G.splitMono X hObs hFix).dag.isAncestor (SWIGNode.random d) vProof (Lean source)
lemma splitMono_not_isAncestor_from_intervened_random (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {d : N} (hd : d ∈ X) (v : SWIGNode N) : ¬ (G.splitMono X hObs hFix).dag.isAncestor (SWIGNode.random d) v := by intro h induction h with | edge he => exact splitMono_no_edge_from_intervened_random G X hObs hFix hd _ he | trans _ _ ih => exact ih -
random_intervened_mem_fixAncestralSet_iff_mem_Ylemma — For an intervened variable, its random copy is a post-intervention ancestor of the query exactly when it is explicitly queried.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedd :Nhd :d ∈ XconclusionSWIGNode.random d ∈ fixAncestralSet M X hObs hFix Y ↔ SWIGNode.random d ∈ YProof (Lean source)
lemma random_intervened_mem_fixAncestralSet_iff_mem_Y (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) {d : N} (hd : d ∈ X) : SWIGNode.random d ∈ fixAncestralSet M X hObs hFix Y ↔ SWIGNode.random d ∈ Y := by constructor · intro h unfold fixAncestralSet at h rcases Finset.mem_union.mp h with hY | hAnc · exact hY · simp only [DAG.ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hAnc obtain ⟨v, hvY, hanc⟩ := hAnc have hno := splitMono_not_isAncestor_from_intervened_random (M.toSWIGGraph) X hObs hFix hd v have hno' : ¬ (M.fixSet X hObs hFix).toSWIGGraph.dag.isAncestor (SWIGNode.random d) v := by simpa [SCM.fixSet, SCM.fixMono] using hno exact False.elim (hno' hanc) · intro hY exact (M.fixSet X hObs hFix).toSWIGGraph.dag.subset_ancestralSet Y hY -
pinnedExtend_projection_eqlemma — The pinned extension projects back to the ancestral assignment when natural intervened coordinates are excluded from the query.hypothesesN :sharedType u_1N → Type u_2∀ n, Nonempty (Ω n)M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedsDo :(M.fixSet X hObs hFix).FixedValueshYX :∀ D ∈ X, SWIGNode.random D ∉ YxD :conclusionvaluesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (pinnedExtend M X hObs hFix Y sDo xD)= xDProof (Lean source)
lemma pinnedExtend_projection_eq [∀ n, Nonempty (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (sDo : (M.fixSet X hObs hFix).FixedValues) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (pinnedExtend M X hObs hFix Y sDo xD) = xD := by intro xD funext v rcases v with ⟨v, hv⟩ cases v with | random d => have hvD : SWIGNode.random d ∈ fixObservedAncestralSet M X hObs hFix Y := hv have hnotX : d ∉ X := by intro hd have hAnc : SWIGNode.random d ∈ fixAncestralSet M X hObs hFix Y := (Finset.mem_inter.mp hvD).1 have hYd : SWIGNode.random d ∈ Y := (random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hd).mp hAnc exact hYX d hd hYd simp [valuesProjection, pinnedExtend, hnotX, hvD] | fixed d => have hvD : SWIGNode.fixed d ∈ fixObservedAncestralSet M X hObs hFix Y := hv simp [valuesProjection, pinnedExtend, hvD] -
pinnedExtend_pin_eqlemma — The pinned extension reads intervened random coordinates from the matching fixed coordinate of the do-slice.hypothesesN :sharedType u_1N → Type u_2∀ n, Nonempty (Ω n)M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedsDo :(M.fixSet X hObs hFix).FixedValuesxD (D : N) (hD : D ∈ X) :conclusionpinnedExtend M X hObs hFix Y sDo xD ⟨SWIGNode.random D, hObs D hD⟩= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩Proof (Lean source)
lemma pinnedExtend_pin_eq [∀ n, Nonempty (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (sDo : (M.fixSet X hObs hFix).FixedValues) : ∀ xD (D : N) (hD : D ∈ X), pinnedExtend M X hObs hFix Y sDo xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ := by intro xD D hD simp [pinnedExtend, hD] -
fixSet_cComponentSet_eqlemma — Intervening does not change the full c-component partition.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedconclusion(M.fixSet X hObs hFix).toSWIGGraph.cComponentSet = M.toSWIGGraph.cComponentSetProof (Lean source)
lemma fixSet_cComponentSet_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) : (M.fixSet X hObs hFix).toSWIGGraph.cComponentSet = M.toSWIGGraph.cComponentSet := by simpa [SCM.fixSet, SCM.fixMono] using (splitMono_cComponentSet_eq (M.toSWIGGraph) X hObs hFix) -
fixSet_cComponentSet_memlemma — Membership in the full c-component partition transports across fixSet.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedconclusionS ∈ (M.fixSet X hObs hFix).toSWIGGraph.cComponentSet ↔ S ∈ M.toSWIGGraph.cComponentSetProof (Lean source)
lemma fixSet_cComponentSet_mem (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (S : Finset (SWIGNode N)) : S ∈ (M.fixSet X hObs hFix).toSWIGGraph.cComponentSet ↔ S ∈ M.toSWIGGraph.cComponentSet := by rw [fixSet_cComponentSet_eq M X hObs hFix] -
fixObservedAncestralSet_obsParent_closedlemma — The observed post-intervention ancestral support is closed under observed parents in the do-model.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedconclusion(M.fixSet X hObs hFix).ObsParentClosed (fixObservedAncestralSet M X hObs hFix Y)Proof (Lean source)
lemma fixObservedAncestralSet_obsParent_closed (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) : (M.fixSet X hObs hFix).ObsParentClosed (fixObservedAncestralSet M X hObs hFix Y) := by refine ⟨Finset.inter_subset_right, ?_⟩ intro v hv w hw hEdge have hvAnc : v ∈ fixAncestralSet M X hObs hFix Y := (Finset.mem_inter.mp hv).1 have hwAnc : w ∈ fixAncestralSet M X hObs hFix Y := by unfold fixAncestralSet at hvAnc ⊢ exact DAG.mem_ancestralSet_of_edge_to_mem (M.fixSet X hObs hFix).toSWIGGraph.dag hEdge hvAnc exact Finset.mem_inter.mpr ⟨hwAnc, hw⟩ -
instIsMarkovKernel_doObsKernelAncestralMarginalinstance — For a finite collection of distinguishable node labels, measurable node-value spaces, a structural causal model, an intervention set whose random intervention nodes are observed and whose fixed intervention nodes are not already fixed, and a query-node set, the observed-ancestral post-intervention marginal is a Markov kernel.parametersN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedinstanceinstIsMarkovKernel_doObsKernelAncestralMarginal M X hObs hFix Y :IsMarkovKernel (doObsKernelAncestralMarginal M X hObs hFix Y)given byby unfold doObsKernelAncestralMarginal exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (measurable_valuesProjection inter_subset_right)
DoGFormulaRec 5 core · 3 supporting The no-fixing certificate cFactorReachable (in DoGFormula) only handles the case where a required district is already a full c-component of the original graph. ★ cFactorReachable_base_toRec★ idSucceeds_toRec
A recursive IDENTIFY soundness certificate
The no-fixing certificate cFactorReachable (in DoGFormula) only handles the
case where a required district is already a full c-component of the original
graph. The recursive IDENTIFY success branch recovers a target c-factor Q[C] from the c-factor
Q[T] of its containing district T by Tian's IDENTIFY subroutine
(Shpitser–Pearl, Fig. 5; Tian–Pearl, Fig. 7): repeatedly restrict to the ancestral set of C and
descend into the c-component of C in that restriction.
This file encodes successful IDENTIFY derivations as an inductive reachability predicate
CFactorReachableRec G T C. It is used only in the soundness direction here;
no converse or formal failure/hedge certificate is claimed. Using an inductive predicate (rather than a
termination_by recursion) makes the downstream soundness proof a clean
induction on the derivation, and makes well-foundedness structural.
* inducedAncestral G T C — the observed ancestors of C within the subgraph of
G induced on T (Tian's An(C)_{G_T}, the observed part).
* CFactorReachableRec G T C — the IDENTIFY success predicate.
* cFactorReachable_base_toRec / idSucceeds_toRec — the no-fixing certificate is
the base case, so idSucceedsRec generalizes idSucceeds (and the recursive
soundness id_sound_rec will subsume the no-fixing id_sound).
def inducedAncestral reviewed
⚑ flagged
Causalean.SCM.ID
For a finite collection of distinguishable node labels, a SWIG graph, a node set on which to induce a subgraph, and a target node set, the induced ancestral set is the observed part of the ancestors of the target set in the graph induced on the first set.
inductive CFactorReachableRec reviewed
⚑ flagged
Causalean.SCM.ID
For a finite collection of distinguishable node labels and a SWIG graph, the recursive c-factor reachability relation relates any source node set to any target node set when either the target is nonempty, is contained in the source, and its observed ancestral set in the source-induced graph is exactly the target, or the target is nonempty and contained in the source, that ancestral set is neither the target nor the source, and the target is recursively reachable from its containing c-component in the ancestral induced graph.
Definition (Lean source)
parameters
N :
Type u_1
G :
constructors
base :
{T C : Finset (SWIGNode N)} (hne : C.Nonempty) (hCT : C ⊆ T) (hproject : inducedAncestral G T C = C) : CFactorReachableRec G T C
step :
{T C : Finset (SWIGNode N)} (hne : C.Nonempty) (hCT : C ⊆ T) (hnotC : inducedAncestral G T C ≠ C) (hnotT : inducedAncestral G T C ≠ T) (hrec : CFactorReachableRec G (containingCComponent (G.induce (inducedAncestral G T C)) C) C) : CFactorReachableRec G T C
def idSucceedsRec reviewed
⚑ flagged
Causalean.SCM.ID
For a finite collection of distinguishable node labels, an intervention variable set, an outcome-node set, and a SWIG graph, the recursive ID soundness certificate holds exactly when the intervention set is valid for the graph, the outcome nodes are observed, no random counterpart of an intervention variable is an outcome node, and every district of the post-intervention ancestral graph is recursively reachable from its containing district in the original graph.
Definition (Lean source)
parameters
def
idSucceedsRec X Y G :
Prop
given by
∃ hX : interventionValid X G,
let GX := G.splitMono X hX.1 hX.2 let Ystar := GX.dag.ancestralSet Y Y ⊆ G.observed ∧
(∀ d ∈ X, SWIGNode.random d ∉ Y) ∧
theorem cFactorReachable_base_toRec reviewed
⚑ flagged
Causalean.SCM.ID
The no-fixing certificate is the base case of the recursive one. For a SWIG graph G and a district S, if S is already reachable from its containing district under the plain no-fixing certificate, then S is recursively reachable from its containing district — which, since S is a full c-component, is S itself.
Formal statement
hypotheses
conclusion
CFactorReachableRec G (containingCComponent G S) S
Proof (Lean source)
theorem cFactorReachable_base_toRec
(G : SWIGGraph N) (S : Finset (SWIGNode N))
(h : cFactorReachable G (containingCComponent G S) S) :
CFactorReachableRec G (containingCComponent G S) S := by
obtain ⟨hne, _hsub, hmem⟩ := h
rw [containingCComponent_of_mem_cComponentSet G S hmem]
exact CFactorReachableRec.base hne (refl _)
(inducedAncestral_self_of_mem_cComponentSet G S hmem)
theorem idSucceeds_toRec reviewed
⚑ flagged
Causalean.SCM.ID
idSucceedsRec generalizes idSucceeds. For an intervention target set X, an outcome node set Y, and a SWIG graph G, if the plain no-fixing ID certificate succeeds for X, Y on G, then the recursive ID soundness certificate also succeeds for X, Y on G, so soundness proved for idSucceedsRec subsumes the no-fixing headline.
Formal statement
hypotheses
conclusion
idSucceedsRec X Y G
Proof (Lean source)
theorem idSucceeds_toRec
(X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N)
(h : idSucceeds X Y G) : idSucceedsRec X Y G := by
obtain ⟨hX, hYobs, hdisj, hreach⟩ := h
refine ⟨hX, hYobs, hdisj, ?_⟩
intro S hS
exact cFactorReachable_base_toRec G S (hreach S hS)
3 supporting declarations (lemmas, instances)
-
inducedAncestral_parent_closedtheorem — The induced ancestral set is closed under observed parents inside the ambient district T.hypothesesN :sharedType u_1G :hT :T ⊆ G.observedv ∈ T :w ∈ inducedAncestral G T C :G.dag.edge v wconclusionv ∈ inducedAncestral G T CProof (Lean source)
theorem inducedAncestral_parent_closed (G : SWIGGraph N) {T C : Finset (SWIGNode N)} (hT : T ⊆ G.observed) : ∀ v ∈ T, ∀ w ∈ inducedAncestral G T C, G.dag.edge v w → v ∈ inducedAncestral G T C := by classical intro v hvT w hw hEdge unfold inducedAncestral at hw ⊢ rcases Finset.mem_inter.mp hw with ⟨hwAnc, hwIndObs⟩ have hvIndObs : v ∈ (G.induce T).observed := by simp [SWIGGraph.induce, hvT, hT hvT] have hwIndObs' : w ∈ T ∩ G.observed := by simpa [SWIGGraph.induce] using hwIndObs have hEdgeInd : (G.induce T).dag.edge v w := by rw [SWIGGraph.induce] rw [SWIGGraph.inducedDag_edge_iff] refine ⟨hEdge, ?_, ?_⟩ · simp [hvT, hT hvT] · simp [(Finset.mem_inter.mp hwIndObs').1, (Finset.mem_inter.mp hwIndObs').2] have hvAnc : v ∈ (G.induce T).dag.ancestralSet C := by rcases Finset.mem_union.mp hwAnc with hwC | hwA · exact (G.induce T).dag.mem_ancestralSet_of_isAncestor hwC (DAG.isAncestor.edge hEdgeInd) · apply mem_union_right simp only [DAG.ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hwA ⊢ obtain ⟨c, hcC, hwc⟩ := hwA exact ⟨c, hcC, (G.induce T).dag.isAncestor_trans (DAG.isAncestor.edge hEdgeInd) hwc⟩ exact Finset.mem_inter.mpr ⟨hvAnc, hvIndObs⟩ -
containingCComponent_of_mem_cComponentSettheorem — When S is a full c-component of G, its containing district is S itself.hypothesesconclusioncontainingCComponent G S = SProof (Lean source)
theorem containingCComponent_of_mem_cComponentSet (G : SWIGGraph N) (S : Finset (SWIGNode N)) (hS : S ∈ G.cComponentSet) : containingCComponent G S = S := by simp only [SWIGGraph.cComponentSet] at hS obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp hS have hne : (G.cComponentOf v).Nonempty := ⟨v, G.mem_cComponentOf_self hv⟩ simp only [containingCComponent, dif_pos hne] have hreach : G.bidirectedReachable v hne.choose := (G.mem_cComponentOf_iff_reachable hv).mp hne.choose_spec exact (G.cComponentOf_eq_of_reachable hreach).symm -
inducedAncestral_self_of_mem_cComponentSettheorem — The observed ancestors of a full c-component S within G_S are S itself.hypothesesconclusioninducedAncestral G S S = SProof (Lean source)
theorem inducedAncestral_self_of_mem_cComponentSet (G : SWIGGraph N) (S : Finset (SWIGNode N)) (hS : S ∈ G.cComponentSet) : inducedAncestral G S S = S := by have hSobs : S ⊆ G.observed := G.cComponentSet_subset_observed S hS have hobs : (G.induce S).observed = S := by change S ∩ G.observed = S exact Finset.inter_eq_left.mpr hSobs rw [inducedAncestral, hobs] apply Finset.Subset.antisymm · exact inter_subset_right · intro x hx exact Finset.mem_inter.mpr ⟨(G.induce S).dag.subset_ancestralSet S hx, hx⟩
ChainRuleFactorization 3 core · 1 supporting This file supplies an ordinary topological chain-rule factorization for an SCM's observational kernel, plus a conditional-kernel construction for an arbitrary observed vertex set. ★ obsKernel_eq_chainRuleProduct
Observational Chain-Rule Factorization
This file supplies an ordinary topological chain-rule factorization for an SCM's observational kernel, plus a conditional-kernel construction for an arbitrary observed vertex set. Neither declaration establishes a c-component factorization: the construction is a conditional law given a chosen predecessor-derived coordinate set, and the theorem is the per-node observational chain rule.
For genuine Tian c-component content, see
SCM/ID/Density/CComponentDensity.lean, SCM/ID/Density/MechCFactor/, and
SCM/ID/Density/QFactor/TianRecovery.lean.
def qFactorParents reviewed
⚑ flagged
Causalean.Graph.SWIGGraph
For a SWIG graph and a finite set of its vertices, the conditioning-parent set is the union of the graph's observed predecessors of the vertices in that set, with the set itself removed.
def condKernelFactor reviewed
⚑ flagged
Causalean.SCM
For a structural causal model, a finite set of observed SWIG vertices, and a fixed-value assignment, provided that the vertex set is contained in the observed-node set and that the value space of that vertex set is standard Borel and nonempty, every observational distribution at a fixed-value assignment is finite, and either the fixed-value space is countable or the conditioning-value space has a countably generated σ-algebra, the conditional-kernel factor is the conditional law of the values on the vertex set given the values on its conditioning-parent set under the model's observational law at that fixed-value assignment.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
hC :
C ⊆ M.observed
s :
M.FixedValues
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
def
given by
(M.obsCondKernel C (M.toSWIGGraph.qFactorParents C) hC (M.toSWIGGraph.qFactorParents_subset_observed C)).comap (fun c => (s, c)) (prodMk measurable_const measurable_id)
theorem obsKernel_eq_chainRuleProduct reviewed
⚑ flagged
Causalean.SCM
For a structural causal model M and a fixed assignment s, its observational kernel equals the full chain-rule product of one-node conditional kernels along the topological order of observed nodes. This is the ordinary iterated-disintegration factorization; it does not use graphical Markov or do-calculus reasoning and does not group factors into c-components.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
s :
M.FixedValues
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
conclusion
M.obsKernel s = M.qFactorProduct s
Proof (Lean source)
theorem obsKernel_eq_chainRuleProduct
(M : SCM N Ω) (s : M.FixedValues)
[∀ (k : ℕ) (hk : k < M.observed.card),
StandardBorelSpace
(ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < M.observed.card),
Nonempty
(ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
[∀ k : ℕ,
CountableOrCountablyGenerated
(M.FixedValues) (ValuesOn (M.prefixNodes k) (swigΩ Ω))] :
M.obsKernel s = M.qFactorProduct s :=
M.obsKernel_eq_qFactorProduct s
1 supporting declaration (lemmas, instances)
-
qFactorParents_subset_observedlemma — qFactorParents C consists of observed nodes outside C.hypothesesconclusionG.qFactorParents C ⊆ G.observedProof (Lean source)
lemma qFactorParents_subset_observed (C : Finset (SWIGNode N)) : G.qFactorParents C ⊆ G.observed := by intro w hw rcases Finset.mem_sdiff.mp hw with ⟨hw_union, _⟩ rcases Finset.mem_biUnion.mp hw_union with ⟨v, _, hw_pred⟩ exact G.observedPredecessors_subset_observed v hw_pred
IDAlgorithm 2 core · 8 supporting This file records the graph-side success certificate for the ID algorithm and states that the certificate identifies the interventional outcome kernel when the admissible model class is inhabited. ★ doKernelY_eq_cfactor_decomposition★ id_sound
ID Algorithm Soundness for the No-Fixing Fragment
This file records the graph-side success certificate for the ID algorithm and states that the certificate identifies the interventional outcome kernel when the admissible model class is inhabited. The proved soundness theorem combines branch alignment for the total query's well-formedness predicate with the Tian c-factor decomposition for the valid branch.
The success predicate is structural. It computes the ancestors of the requested outcomes after splitting the treatment variables in the SWIG, induces the ancestral subgraph, and checks its c-components against c-components already available in the original graph. This is the no-additional-fixing case of the Tian/Shpitser reachability condition; the general fixing-sequence predicate is deferred here rather than encoded as a circular appeal to identifiability.
theorem doKernelY_eq_cfactor_decomposition reviewed
⚑ flagged
Causalean.SCM.ID
Valid-branch kernel equality under a successful no-fixing ID certificate. For two finite structural causal models M₁, M₂ that share the same SWIG graph G, are each dominated by a reference-measure family ref that is faithful to the graph, satisfy discrete positivity of their observational kernels, and have heterogeneously equal observational kernels, if the total interventional query on outcome set Y under intervention X is well formed in both models and X, Y have a successful no-fixing ID certificate on G, then the two models' post-intervention outcome kernels for Y are equal at their chosen default fixed-value assignments.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, StandardBorelSpace (Ω n)
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
X :
Finset N
G :
ref :
href :
_hID :
idSucceeds X Y G
M₁ M₂ :
SCM N Ω
_hsg₁ :
M₁.toSWIGGraph = G
_hsg₂ :
M₂.toSWIGGraph = G
_hdom₁ :
DominatedObs M₁ ref
_hdom₂ :
DominatedObs M₂ ref
hpos₁ :
DiscreteID.DiscretePositive M₁
hpos₂ :
DiscreteID.DiscretePositive M₂
_hobs :
HEq M₁.obsKernel M₂.obsKernel
hvalid₁ :
interventionalQueryValid X Y M₁
hvalid₂ :
interventionalQueryValid X Y M₂
conclusion
M₁.doKernelY X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1 (standardFixedValues M₁ hvalid₁.2.2.2)
= M₂.doKernelY X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1 (standardFixedValues M₂ hvalid₂.2.2.2)
Proof (Lean source)
theorem doKernelY_eq_cfactor_decomposition
[∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N)
(ref : ReferenceMeasures Ω)
(href : ReferenceFaithful ref)
(_hID : idSucceeds X Y G)
(M₁ M₂ : SCM N Ω)
(_hsg₁ : M₁.toSWIGGraph = G) (_hsg₂ : M₂.toSWIGGraph = G)
(_hdom₁ : DominatedObs M₁ ref) (_hdom₂ : DominatedObs M₂ ref)
(hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂)
(_hobs : HEq M₁.obsKernel M₂.obsKernel)
(hvalid₁ : interventionalQueryValid X Y M₁)
(hvalid₂ : interventionalQueryValid X Y M₂) :
M₁.doKernelY X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1
(standardFixedValues M₁ hvalid₁.2.2.2)
=
M₂.doKernelY X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1
(standardFixedValues M₂ hvalid₂.2.2.2) := by
have hsg : M₁.toSWIGGraph = M₂.toSWIGGraph := _hsg₁.trans _hsg₂.symm
exact doKernelY_eq_of_doObsKernel_heq X Y M₁ M₂ hsg
hvalid₁.1 hvalid₁.2.1 hvalid₂.1 hvalid₂.2.1 hvalid₁.2.2.1 hvalid₂.2.2.1
(standardFixedValues M₁ hvalid₁.2.2.2) (standardFixedValues M₂ hvalid₂.2.2.2)
(standardFixedValues_heq M₁ M₂ (congrArg SWIGGraph.fixed hsg) hvalid₁.2.2.2)
(doObsKernelYMarginal_heq_of_obsKernel_heq X Y G ref href _hID M₁ M₂ _hsg₁ _hsg₂
_hdom₁ _hdom₂ hpos₁ hpos₂ _hobs hvalid₁ hvalid₂)
theorem id_sound reviewed
⚑ flagged
Causalean.SCM.ID
Soundness of the no-fixing ID algorithm. Fix targets, outcomes, a standard graph, and a faithful reference family, and assume an inhabited compatible dominated-positive class. Then certificate success guarantees query identification within that class.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, StandardBorelSpace (Ω n)
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
X :
Finset N
G :
ref :
href :
hG :
G.isStandard
hNonempty :
∃ M : SCM N Ω,
M.toSWIGGraph = G ∧ DominatedObs M ref ∧ DiscreteID.DiscretePositive M
idSucceeds X Y G
conclusion
IdentifiableUnder (Ω := Ω) G (fun _ => True) (fun M => DominatedObs M ref ∧ DiscreteID.DiscretePositive M) (interventionalQuery (Ω := Ω) X Y)
Proof (Lean source)
theorem id_sound [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N)
(ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (hG : G.isStandard)
(hNonempty : ∃ M : SCM N Ω,
M.toSWIGGraph = G ∧ DominatedObs M ref ∧ DiscreteID.DiscretePositive M) :
idSucceeds X Y G →
IdentifiableUnder (Ω := Ω) G (fun _ => True)
(fun M => DominatedObs M ref ∧ DiscreteID.DiscretePositive M)
(interventionalQuery (Ω := Ω) X Y) := by
classical
intro hID M₁ M₂ hsg₁ hsg₂ _ _ hM₁ hM₂ hobs
have hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y := by
rcases hID with ⟨_hX, hIDrest⟩
exact hIDrest.2.1
have hvalid_iff :
interventionalQueryValid X Y M₁ ↔ interventionalQueryValid X Y M₂ :=
interventionalQueryValid_iff_of_toSWIGGraph_eq
(Ω := Ω) X Y M₁ M₂ (hsg₁.trans hsg₂.symm)
by_cases hvalid₁ : interventionalQueryValid X Y M₁
· have hvalid₂ : interventionalQueryValid X Y M₂ := hvalid_iff.mp hvalid₁
rw [interventionalQuery_eq_doKernelY_of_valid (Ω := Ω) X Y M₁ hvalid₁,
interventionalQuery_eq_doKernelY_of_valid (Ω := Ω) X Y M₂ hvalid₂]
exact doKernelY_eq_cfactor_decomposition
(Ω := Ω) X Y G ref href hID M₁ M₂ hsg₁ hsg₂ hM₁.1 hM₂.1 hM₁.2 hM₂.2
hobs hvalid₁ hvalid₂
· have hvalid₂ : ¬ interventionalQueryValid X Y M₂ := by
intro h
exact hvalid₁ (hvalid_iff.mpr h)
rw [interventionalQuery_eq_default_of_not_valid (Ω := Ω) X Y M₁ hvalid₁,
interventionalQuery_eq_default_of_not_valid (Ω := Ω) X Y M₂ hvalid₂]
8 supporting declarations (lemmas, instances)
-
standardFixedValues_heqtheorem — Given two finite structural causal models with equal fixed-node sets, if the first model is standard, then their canonical fixed-value assignments are equal after type transport.hypothesesconclusionHEq (standardFixedValues M₁ h₁) (standardFixedValues M₂ (by change M₂.fixed = ∅ rw [← hf] exact h₁))Proof (Lean source)
theorem standardFixedValues_heq (M₁ M₂ : SCM N Ω) (hf : M₁.fixed = M₂.fixed) (h₁ : M₁.isStandard) : HEq (standardFixedValues M₁ h₁) (standardFixedValues M₂ (by change M₂.fixed = ∅ rw [← hf] exact h₁)) := by have h₁' : M₁.fixed = (∅ : Finset (SWIGNode N)) := h₁ haveI hempty : IsEmpty {v // v ∈ M₁.fixed} := ⟨fun i => absurd (h₁' ▸ i.property) (notMem_empty i.val)⟩ haveI hsub₁ : Subsingleton M₁.FixedValues := ⟨fun a b => funext fun i => isEmptyElim i⟩ exact Subsingleton.helim (congrArg (fun S => ValuesOn S (swigΩ Ω)) hf) _ _ -
doObsKernelYMarginal_eq_ancestralMarginal_maptheorem — The outcome marginal of the do-law is the projection of the observed-ancestral do-law marginal to the outcome coordinates.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhY :Y ⊆ M.observedconclusiondoObsKernelYMarginal M X hObs hFix Y hY= (doObsKernelAncestralMarginal M X hObs hFix Y).map (valuesProjection (subset_fixObservedAncestralSet M X hObs hFix Y hY))Proof (Lean source)
theorem doObsKernelYMarginal_eq_ancestralMarginal_map (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) : doObsKernelYMarginal M X hObs hFix Y hY = (doObsKernelAncestralMarginal M X hObs hFix Y).map (valuesProjection (subset_fixObservedAncestralSet M X hObs hFix Y hY)) := by -- Name both inclusions with their *folded* types: the auto-generated proof -- inside `doObsKernelAncestralMarginal` records the unfolded intersection type, -- which blocks `rw` after `unfold` (defeq only at default transparency). have hJI : fixObservedAncestralSet M X hObs hFix Y ⊆ (M.fixSet X hObs hFix).observed := Finset.inter_subset_right have hKJ : Y ⊆ fixObservedAncestralSet M X hObs hFix Y := subset_fixObservedAncestralSet M X hObs hFix Y hY show (M.fixSet X hObs hFix).obsKernel.map (valuesProjection (hKJ.trans hJI)) = ((M.fixSet X hObs hFix).obsKernel.map (valuesProjection hJI)).map (valuesProjection hKJ) rw [← ProbabilityTheory.Kernel.map_comp_right _ (measurable_valuesProjection hJI) (measurable_valuesProjection hKJ), valuesProjection_comp hKJ hJI] -
doObsKernelYMarginal_heq_of_ancestralMarginal_heqtheorem — If two models with the same SWIG graph have equal observed-ancestral do-law marginals, then their outcome marginals agree.hypothesesN :sharedType u_1N → Type u_2X :Finset NM₁ M₂ :SCM N Ωhsg :M₁.toSWIGGraph = M₂.toSWIGGraphhObs₁ :∀ D ∈ X, SWIGNode.random D ∈ M₁.observedhFix₁ :∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixedhObs₂ :∀ D ∈ X, SWIGNode.random D ∈ M₂.observedhFix₂ :∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixedhY₁ :Y ⊆ M₁.observedhY₂ :Y ⊆ M₂.observedhAnc :HEq (doObsKernelAncestralMarginal M₁ X hObs₁ hFix₁ Y) (doObsKernelAncestralMarginal M₂ X hObs₂ hFix₂ Y)conclusionProof (Lean source)
theorem doObsKernelYMarginal_heq_of_ancestralMarginal_heq (X : Finset N) (Y : Finset (SWIGNode N)) (M₁ M₂ : SCM N Ω) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) (hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed) (hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed) (hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (hAnc : HEq (doObsKernelAncestralMarginal M₁ X hObs₁ hFix₁ Y) (doObsKernelAncestralMarginal M₂ X hObs₂ hFix₂ Y)) : HEq (doObsKernelYMarginal M₁ X hObs₁ hFix₁ Y hY₁) (doObsKernelYMarginal M₂ X hObs₂ hFix₂ Y hY₂) := by rw [doObsKernelYMarginal_eq_ancestralMarginal_map M₁ X hObs₁ hFix₁ Y hY₁, doObsKernelYMarginal_eq_ancestralMarginal_map M₂ X hObs₂ hFix₂ Y hY₂] obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg apply heq_of_eq congr 1 exact eq_of_heq hAnc -
instIsFiniteMeasure_doObsKernelAncestralMarginalinstance — For a finite collection of distinguishable node labels, measurable node-value spaces, a structural causal model, an intervention set whose random intervention nodes are observed and whose fixed intervention nodes are not already fixed, a query-node set, and fixed intervention values, the observed-ancestral post-intervention marginal measure has finite total mass.parametersN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixeds :(M.fixSet X hObs hFix).FixedValuesinstanceinstIsFiniteMeasure_doObsKernelAncestralMarginal M X hObs hFix Y s :IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y s)given byby unfold doObsKernelAncestralMarginal rw [ProbabilityTheory.Kernel.map_apply] · exact ((M.fixSet X hObs hFix).obsKernel s).isFiniteMeasure_map (valuesProjection (Finset.inter_subset_right : fixObservedAncestralSet M X hObs hFix Y ⊆ (M.fixSet X hObs hFix).observed)) · exact measurable_valuesProjection _ -
doObsKernelAncestralMarginal_dominatedtheorem — A faithful finite product reference dominates the post-intervention observed-ancestral marginal.hypothesesN :sharedType u_1N → Type u_2∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedref :href :s :(M.fixSet X hObs hFix).FixedValuesconclusiondoObsKernelAncestralMarginal M X hObs hFix Y s ≪ jointRef ref (fixObservedAncestralSet M X hObs hFix Y)Proof (Lean source)
theorem doObsKernelAncestralMarginal_dominated [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (s : (M.fixSet X hObs hFix).FixedValues) : doObsKernelAncestralMarginal M X hObs hFix Y s ≪ jointRef ref (fixObservedAncestralSet M X hObs hFix Y) := by exact absolutelyContinuous_jointRef_of_faithful ref href (fixObservedAncestralSet M X hObs hFix Y) (doObsKernelAncestralMarginal M X hObs hFix Y s) -
doObsKernelAncestralMarginal_heq_of_obsDensity_heqtheorem — Two dominated models with the same SWIG graph and observational density have the same post-intervention law on the observed ancestors selected by a successful ID certificate.hypothesesN :sharedType u_1N → Type u_2∀ n, StandardBorelSpace (Ω n)∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)X :Finset NG :ref :href :_hID :idSucceeds X Y GM₁ M₂ :SCM N Ω_hsg₁ :M₁.toSWIGGraph = G_hsg₂ :M₂.toSWIGGraph = G_hdom₁ :DominatedObs M₁ ref_hdom₂ :DominatedObs M₂ refhpos₁ :DiscreteID.DiscretePositive M₁hpos₂ :DiscreteID.DiscretePositive M₂_hden :HEq (M₁.obsDensity ref) (M₂.obsDensity ref)hvalid₁ :interventionalQueryValid X Y M₁hvalid₂ :interventionalQueryValid X Y M₂conclusionHEq (doObsKernelAncestralMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y) (doObsKernelAncestralMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y)Proof (Lean source)
theorem doObsKernelAncestralMarginal_heq_of_obsDensity_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (_hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (_hsg₁ : M₁.toSWIGGraph = G) (_hsg₂ : M₂.toSWIGGraph = G) (_hdom₁ : DominatedObs M₁ ref) (_hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (_hden : HEq (M₁.obsDensity ref) (M₂.obsDensity ref)) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelAncestralMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y) (doObsKernelAncestralMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y) := by classical have hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y := by rcases _hID with ⟨_, hIDrest⟩ exact hIDrest.2.1 have hobs : HEq M₁.obsKernel M₂.obsKernel := obsKernel_heq_of_obsDensity_heq M₁ M₂ ref (_hsg₁.trans _hsg₂.symm) _hdom₁ _hdom₂ _hden have hsg : M₁.toSWIGGraph = M₂.toSWIGGraph := _hsg₁.trans _hsg₂.symm -- Materialize the marginals' finiteness as local instances while the models are -- still named; they survive the structural `obtain` below, where the global -- instance no longer matches the constructor form. haveI hfin1 : ∀ s, IsFiniteMeasure ((doObsKernelAncestralMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y) s) := fun s => inferInstance haveI hfin2 : ∀ s, IsFiniteMeasure ((doObsKernelAncestralMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y) s) := fun s => inferInstance haveI hobsfin1 : ∀ s, IsFiniteMeasure (M₁.obsKernel s) := fun s => inferInstance haveI hobsfin2 : ∀ s, IsFiniteMeasure (M₂.obsKernel s) := fun s => inferInstance obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg have hfio : fio₂ = fio₁ := Subsingleton.elim _ _ subst fio₂ have hoi : oi₂ = oi₁ := Subsingleton.elim _ _ subst oi₂ have hod : od₂ = od₁ := Subsingleton.elim _ _ subst od₂ have hoou : oou₂ = oou₁ := Subsingleton.elim _ _ subst oou₂ have hfoi : foi₂ = foi₁ := Subsingleton.elim _ _ subst foi₂ have hfou : fou₂ = fou₁ := Subsingleton.elim _ _ subst fou₂ have haic : aic₂ = aic₁ := Subsingleton.elim _ _ subst aic₂ have hdc : dc₂ = dc₁ := Subsingleton.elim _ _ subst dc₂ have hfoff : foff₂ = foff₁ := Subsingleton.elim _ _ subst foff₂ have haco : aco₂ = aco₁ := Subsingleton.elim _ _ subst aco₂ apply heq_of_eq refine ProbabilityTheory.Kernel.ext (fun s => ?_) -- `s` is typed against the *first* model's fixed-value space, so the `∀ s` -- instances above are only usable after one application at default -- transparency; instance synthesis alone cannot bridge the two (definitionally -- equal) fixed-value types. Specialize them here so the shapes match -- syntactically at every later call site. haveI hfin1s := hfin1 s haveI hfin2s := hfin2 s -- The two ancestral marginals share the coordinate reference `jointRef ref D` -- (`D = fixObservedAncestralSet` reads only the shared SWIG graph, so the two -- syntactic copies are definitionally equal), and both are dominated by it -- (`doObsKernelAncestralMarginal_dominated`). A measure is determined by its -- density against a fixed reference (`Measure.eq_of_rnDeriv_eq`), so it suffices -- to show the two Radon–Nikodym derivatives agree a.e. Applying the lemma as a -- term (not by `rw`) lets unification absorb the definitional `D₁ = D₂` gap that -- previously made the rewrite route brittle. refine eq_of_rnDeriv_eq (doObsKernelAncestralMarginal_dominated _ X hvalid₁.1 hvalid₁.2.1 Y ref href s) (doObsKernelAncestralMarginal_dominated _ X hvalid₂.1 hvalid₂.2.1 Y ref href s) ?_ -- Remaining density (rnDeriv) transport. By the Tian wrapper each side's density -- is the product over the districts of `G_X[D]` of the district factors -- (`doObsKernelAncestralMarginal_tian_cfactorization_density`); by T2 each district -- factor equals a recovered full-graph c-factor -- (`doAncestralDistrictDensity_recovered_from_obs`); and equal observational kernels -- give equal recovered factors (`cComponentDensityFactor_heq_of_obsKernel_heq`), -- so the two products — hence the two densities — agree a.e. have w1 := doObsKernelAncestralMarginal_tian_cfactorization_density _ X hvalid₁.1 hvalid₁.2.1 Y ref s (doObsKernelAncestralMarginal_dominated _ X hvalid₁.1 hvalid₁.2.1 Y ref href s) have w2 := doObsKernelAncestralMarginal_tian_cfactorization_density _ X hvalid₂.1 hvalid₂.2.1 Y ref s (doObsKernelAncestralMarginal_dominated _ X hvalid₂.1 hvalid₂.2.1 Y ref href s) refine w1.trans (Filter.EventuallyEq.trans ?_ w2.symm) let M₁' : SCM N Ω := { dag := dag₁, fixed := fixed₁, observed := observed₁, unobserved := unobserved₁, fixed_is_fixed := fio₁, observed_is_random := oi₁, unobserved_is_random := od₁, obs_unobs_disjoint := oou₁, dag_edges_classified := foi₁, fixed_image_in_observed := fou₁, fixed_are_roots := aic₁, unobs_are_roots := dc₁, fixed_outside_fixed_isolated := foff₁, all_children_in_observed := aco₁, edgeTypes := eT₁, iota_valueSpace := iota₁, structFun := sf₁, structFun_measurable := mf₁, latentDist := lD₁, isProbability_latent := pL₁ } let M₂' : SCM N Ω := { dag := dag₁, fixed := fixed₁, observed := observed₁, unobserved := unobserved₁, fixed_is_fixed := fio₁, observed_is_random := oi₁, unobserved_is_random := od₁, obs_unobs_disjoint := oou₁, dag_edges_classified := foi₁, fixed_image_in_observed := fou₁, fixed_are_roots := aic₁, unobs_are_roots := dc₁, fixed_outside_fixed_isolated := foff₁, all_children_in_observed := aco₁, edgeTypes := eT₂, iota_valueSpace := iota₂, structFun := sf₂, structFun_measurable := mf₂, latentDist := lD₂, isProbability_latent := pL₂ } let D := fixObservedAncestralSet M₁' X hvalid₁.1 hvalid₁.2.1 Y let H := (M₁'.fixSet X hvalid₁.1 hvalid₁.2.1).toSWIGGraph.induce (fixAncestralSet M₁' X hvalid₁.1 hvalid₁.2.1 Y) haveI hν₁ : IsFiniteMeasure ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) := hfin1 s haveI hν₂ : IsFiniteMeasure ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) := hfin2 s haveI hν₂D : IsFiniteMeasure (show Measure (ValuesOn D (swigΩ Ω)) from ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s)) := by change IsFiniteMeasure ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) exact hfin2 s change (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S x) =ᵐ[jointRef ref D] (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S x) have hfac : ∀ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S =ᵐ[jointRef ref D] tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S := by intro S hS have hIDM : idSucceeds X Y M₁'.toSWIGGraph := by rw [_hsg₁] exact _hID rcases hIDM with ⟨hX, hIDrest⟩ have hSreach : S ∈ ((M₁'.toSWIGGraph.splitMono X hX.1 hX.2).induce ((M₁'.toSWIGGraph.splitMono X hX.1 hX.2).dag.ancestralSet Y)).cComponentSet := by exact hS let C := containingCComponent M₁'.toSWIGGraph S have hReach : cFactorReachable M₁'.toSWIGGraph C S := by simpa [C] using hIDrest.2.2 S hSreach have hCmem : C ∈ M₁'.toSWIGGraph.cComponentSet := by have hSne : S.Nonempty := hReach.1 have hSobs : S ⊆ M₁'.toSWIGGraph.observed := M₁'.toSWIGGraph.cComponentSet_subset_observed S hReach.2.2 have hchoose : hSne.choose ∈ M₁'.toSWIGGraph.observed := hSobs hSne.choose_spec simp only [C, containingCComponent, dif_pos hSne, SWIGGraph.cComponentSet] exact Finset.mem_image.mpr ⟨hSne.choose, hchoose, rfl⟩ let extend : ValuesOn D (swigΩ Ω) → ValuesOn M₁'.observed (swigΩ Ω) := pinnedExtend M₁' X hvalid₁.1 hvalid₁.2.1 Y s have hExtend : ∀ xD, valuesProjection (show D ⊆ M₁'.observed from inter_subset_right) (extend xD) = xD := pinnedExtend_projection_eq M₁' X hvalid₁.1 hvalid₁.2.1 Y s hYX have hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hvalid₁.1 D hD⟩ = s ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ := pinnedExtend_pin_eq M₁' X hvalid₁.1 hvalid₁.2.1 Y s have hpos₁' : ∀ s' : M₁'.FixedValues, DiscreteID.PositiveMass (M₁'.obsKernel s') := hpos₁ have hpos₂' : ∀ s' : M₂'.FixedValues, DiscreteID.PositiveMass (M₂'.obsKernel s') := hpos₂ haveI hobsfin₁ : ∀ s' : M₁'.FixedValues, IsFiniteMeasure (M₁'.obsKernel s') := hobsfin1 haveI hobsfin₂ : ∀ s' : M₂'.FixedValues, IsFiniteMeasure (M₂'.obsKernel s') := hobsfin2 have t1 := doAncestralDistrictDensity_recovered_from_obs M₁' X hvalid₁.2.2.2 hvalid₁.1 hvalid₁.2.1 Y ref href s S C (by simpa [H, fixTruncCComponentSet] using hS) hReach hCmem hpos₁' hYX extend hExtend hExtendX have t2 := doAncestralDistrictDensity_recovered_from_obs M₂' X hvalid₂.2.2.2 hvalid₂.1 hvalid₂.2.1 Y ref href s S C (by exact hS) (by simpa [M₁', M₂'] using hReach) (by simpa [M₁', M₂'] using hCmem) hpos₂' hYX extend (by exact hExtend) (by exact hExtendX) have hrec := cComponentDensityFactor_heq_of_obsKernel_heq M₁' M₂' ref C rfl hobs have hrec_fun : (fun s' => M₁'.cComponentDensityFactor ref s' C) = (fun s' => M₂'.cComponentDensityFactor ref s' C) := eq_of_heq hrec have hrec_s := congrFun hrec_fun (M₁'.fixSetProj X hvalid₁.1 hvalid₁.2.1 s) refine t1.trans ?_ filter_upwards [t2.symm] with x hx exact hrec_s ▸ hx clear w1 w2 have hprod : ∀ I : Finset (Finset (SWIGNode N)), (∀ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S =ᵐ[jointRef ref D] tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S) → (fun x => ∏ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S x) =ᵐ[jointRef ref D] (fun x => ∏ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S x) := by intro I hIall induction I using Finset.induction_on with | empty => -- … truncated; follow the source link for the rest … -
doObsKernelYMarginal_heq_of_obsDensity_heqtheorem — Two dominated models with the same SWIG graph and observational density have the same post-intervention outcome marginal under a successful ID certificate.hypothesesN :sharedType u_1N → Type u_2∀ n, StandardBorelSpace (Ω n)∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)X :Finset NG :ref :href :_hID :idSucceeds X Y GM₁ M₂ :SCM N Ω_hsg₁ :M₁.toSWIGGraph = G_hsg₂ :M₂.toSWIGGraph = G_hdom₁ :DominatedObs M₁ ref_hdom₂ :DominatedObs M₂ refhpos₁ :DiscreteID.DiscretePositive M₁hpos₂ :DiscreteID.DiscretePositive M₂_hden :HEq (M₁.obsDensity ref) (M₂.obsDensity ref)hvalid₁ :interventionalQueryValid X Y M₁hvalid₂ :interventionalQueryValid X Y M₂conclusionHEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1)Proof (Lean source)
theorem doObsKernelYMarginal_heq_of_obsDensity_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (_hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (_hsg₁ : M₁.toSWIGGraph = G) (_hsg₂ : M₂.toSWIGGraph = G) (_hdom₁ : DominatedObs M₁ ref) (_hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (_hden : HEq (M₁.obsDensity ref) (M₂.obsDensity ref)) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1) := by -- Split off the easy `Y ← (Ystar ∩ observed)` projection; the genuine content -- is the observed-ancestral marginal identification. have hsg : M₁.toSWIGGraph = M₂.toSWIGGraph := _hsg₁.trans _hsg₂.symm exact doObsKernelYMarginal_heq_of_ancestralMarginal_heq X Y M₁ M₂ hsg hvalid₁.1 hvalid₁.2.1 hvalid₂.1 hvalid₂.2.1 hvalid₁.2.2.1 hvalid₂.2.2.1 (doObsKernelAncestralMarginal_heq_of_obsDensity_heq X Y G ref href _hID M₁ M₂ _hsg₁ _hsg₂ _hdom₁ _hdom₂ hpos₁ hpos₂ _hden hvalid₁ hvalid₂) -
doObsKernelYMarginal_heq_of_obsKernel_heqtheorem — Two dominated models with the same SWIG graph and observational law have the same post-intervention outcome marginal under a successful ID certificate.hypothesesN :sharedType u_1N → Type u_2∀ n, StandardBorelSpace (Ω n)∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)X :Finset NG :ref :href :hID :idSucceeds X Y GM₁ M₂ :SCM N Ωhsg₁ :M₁.toSWIGGraph = Ghsg₂ :M₂.toSWIGGraph = Ghdom₁ :DominatedObs M₁ refhdom₂ :DominatedObs M₂ refhpos₁ :DiscreteID.DiscretePositive M₁hpos₂ :DiscreteID.DiscretePositive M₂hobs :HEq M₁.obsKernel M₂.obsKernelhvalid₁ :interventionalQueryValid X Y M₁hvalid₂ :interventionalQueryValid X Y M₂conclusionHEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1)Proof (Lean source)
theorem doObsKernelYMarginal_heq_of_obsKernel_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (hsg₁ : M₁.toSWIGGraph = G) (hsg₂ : M₂.toSWIGGraph = G) (hdom₁ : DominatedObs M₁ ref) (hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (hobs : HEq M₁.obsKernel M₂.obsKernel) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1) := -- The observational law enters the do-law `Y`-marginal *only* through its -- density: equal `obsKernel` gives equal `obsDensity` (`obsDensity_heq_of_obsKernel_heq`), -- and the g-formula core consumes that density. doObsKernelYMarginal_heq_of_obsDensity_heq X Y G ref href hID M₁ M₂ hsg₁ hsg₂ hdom₁ hdom₂ hpos₁ hpos₂ (obsDensity_heq_of_obsKernel_heq M₁ M₂ ref (hsg₁.trans hsg₂.symm) hobs) hvalid₁ hvalid₂
IDSoundDiscrete 1 core · 0 supporting GraphicalThms.IDAlgorithm.id_sound concludes over the model class fun M => DominatedObs M ref ∧ DiscretePositive M on a standard graph, parameterised by an arbitrary faithful reference family. ★ id_sound_discrete
On-contract discrete soundness of the graphical ID assembly
GraphicalThms.IDAlgorithm.id_sound concludes over the model class
fun M => DominatedObs M ref ∧ DiscretePositive M on a standard graph,
parameterised by an arbitrary faithful reference family. Instantiating that reference at the
counting measure and using that the counting reference dominates every model
(dominatedObs_countingRef), the model class collapses to the frozen
discrete-positive class StandardDiscretePositive. The explicit standard-graph
guard excludes nonstandard graphs, while the explicit inhabitation premise in
the soundness theorem rules out an empty compatible model class.
theorem id_sound_discrete reviewed
⚑ flagged
Causalean.SCM.ID
Discrete soundness of the ID assembly for the no-additional-fixing (full-district) fragment (on-contract). For treatments, outcomes, a standard graph, an inhabited compatible positive class, and a successful no-fixing certificate, the query is identifiable from the observational law within that class.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, StandardBorelSpace (Ω n)
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
X :
Finset N
G :
hG :
G.isStandard
hNonempty :
∃ M : SCM N Ω, M.toSWIGGraph = G ∧ StandardDiscretePositive M
h :
idSucceeds X Y G
conclusion
Proof (Lean source)
theorem id_sound_discrete
[∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N)
(hG : G.isStandard)
(hNonempty : ∃ M : SCM N Ω,
M.toSWIGGraph = G ∧ StandardDiscretePositive M)
(h : idSucceeds X Y G) :
IdentifiableUnder G (fun _ => True) StandardDiscretePositive
(interventionalQuery (Ω := Ω) X Y) := by
have hdom :=
id_sound X Y G (countingRef (Ω := Ω)) referenceFaithful_countingRef hG
(by
rcases hNonempty with ⟨M, hMG, hM⟩
exact ⟨M, hMG, dominatedObs_countingRef M, hM.2⟩)
h
exact identifiableUnder_mono G (fun _ => True) (fun _ => True)
(fun M => DominatedObs M (countingRef (Ω := Ω)) ∧ DiscretePositive M)
StandardDiscretePositive (interventionalQuery (Ω := Ω) X Y)
(fun _ h => h) (fun M hM => ⟨dominatedObs_countingRef M, hM.2⟩) hdom
InducedSubgraph 5 core · 7 supporting This file provides graph-level utilities for restricting a SWIG to selected observed nodes in graphical identification arguments. ★ properDescIn_union_nonDescIn_eq_erase
Induced Subgraphs for Identification
This file provides graph-level utilities for restricting a SWIG to selected
observed nodes in graphical identification arguments. It defines
SWIGGraph.isAncestrallyClosed, the InducedFrom abbreviation for G.induce R,
and the descendant/non-descendant sets properDescIn and nonDescIn used in
Tian-style fixing arguments, together with their basic disjointness and coverage
lemmas.
def isAncestrallyClosed reviewed
⚑ flagged
Causalean.Graph.SWIGGraph
For a single-world intervention graph, ancestral closure holds exactly when every observed node's parent that is a random node is itself observed.
Definition (Lean source)
parameters
N :
Type u_1
v ∈ G.observed :
u ∈ G.dag.parents v :
(∃ n : N, u = SWIGNode.random n)
def
isAncestrallyClosed G :
Prop
given by
u ∈ G.observed
abbrev InducedFrom reviewed
⚑ flagged
Causalean
For a single-world intervention graph and a selected finite set of nodes, the induced subgraph is the graph obtained by restricting the original graph to those selected nodes.
def properDescIn reviewed
⚑ flagged
Causalean.Graph.SWIGGraph
For a single-world intervention graph, a selected finite node set, and a target node, the proper-descendant set within the induced graph is the finite set of descendants of the target in the graph induced by the selected nodes.
def nonDescIn reviewed
⚑ flagged
Causalean.Graph.SWIGGraph
For a single-world intervention graph, a selected finite node set, and a target node, the induced non-descendant set is the selected set with the target and all of its proper descendants in the induced graph removed.
lemma properDescIn_union_nonDescIn_eq_erase reviewed
⚑ flagged
Causalean.Graph.SWIGGraph
Within a selected node set R of a SWIG graph G, the proper descendants of a node v₀ together with its non-descendants exhaust the selected nodes other than v₀ itself.
Formal statement
Proof (Lean source)
lemma properDescIn_union_nonDescIn_eq_erase
(G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) :
G.properDescIn R v₀ ∪ G.nonDescIn R v₀ = R.erase v₀ := by
ext x
simp only [mem_union, Finset.mem_erase, properDescIn, nonDescIn,
DAG.mem_descendants, mem_sdiff]
constructor
· -- (⊆): both parts are subsets of R.erase v₀
intro hx
rcases hx with hx | ⟨⟨hne, hxR⟩, _⟩
· exact ⟨fun heq => DAG.isAncestor_irrefl _ v₀ (heq ▸ hx),
(Finset.mem_inter.mp (G.induce_isAncestor_mem_R R hx)).1⟩
· exact ⟨hne, hxR⟩
· -- (⊇): x ∈ R.erase v₀ → in properDescIn or nonDescIn
intro ⟨hne, hxR⟩
by_cases hdesc : (G.induce R).dag.isAncestor v₀ x
· left; exact hdesc
· right
exact ⟨⟨hne, hxR⟩, hdesc⟩
7 supporting declarations (lemmas, instances)
-
decIsAncestrallyClosedinstance — For a finite single-world intervention graph, the decision procedure for ancestral closure determines whether every parent of an observed node that is itself a random node is also observed. -
v₀_not_mem_properDescInlemma — A node is not a proper descendant of itself inside the induced subgraph.hypothesesconclusionv₀ ∉ G.properDescIn R v₀Proof (Lean source)
lemma v₀_not_mem_properDescIn (G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) : v₀ ∉ G.properDescIn R v₀ := by simp only [properDescIn, DAG.mem_descendants] exact DAG.isAncestor_irrefl _ _ -
v₀_not_mem_nonDescInlemma — The target node is not in its induced non-descendant set because it is explicitly removed.hypothesesconclusionv₀ ∉ G.nonDescIn R v₀ -
properDescIn_subset_eraselemma — Proper descendants lie in the selected set with the target node removed.hypothesesconclusionG.properDescIn R v₀ ⊆ R.erase v₀Proof (Lean source)
lemma properDescIn_subset_erase (G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) : G.properDescIn R v₀ ⊆ R.erase v₀ := by intro w hw simp only [properDescIn, DAG.mem_descendants] at hw rw [Finset.mem_erase] exact ⟨fun heq => DAG.isAncestor_irrefl _ v₀ (heq ▸ hw), (Finset.mem_inter.mp (G.induce_isAncestor_mem_R R hw)).1⟩ -
nonDescIn_subset_eraselemma — Every induced non-descendant lies in the selected set with the target node removed.hypothesesconclusionG.nonDescIn R v₀ ⊆ R.erase v₀Proof (Lean source)
lemma nonDescIn_subset_erase (G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) : G.nonDescIn R v₀ ⊆ R.erase v₀ := sdiff_subset -
nonDescIn_subsetlemma — Every induced non-descendant lies in the selected set.hypothesesconclusionG.nonDescIn R v₀ ⊆ RProof (Lean source)
lemma nonDescIn_subset (G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) : G.nonDescIn R v₀ ⊆ R := (G.nonDescIn_subset_erase R v₀).trans (R.erase_subset v₀) -
properDescIn_disjoint_nonDescInlemma — The proper-descendant set and non-descendant set are disjoint inside the selected nodes.hypothesesconclusionDisjoint (G.properDescIn R v₀) (G.nonDescIn R v₀)Proof (Lean source)
lemma properDescIn_disjoint_nonDescIn (G : SWIGGraph N) (R : Finset (SWIGNode N)) (v₀ : SWIGNode N) : Disjoint (G.properDescIn R v₀) (G.nonDescIn R v₀) := by simp only [properDescIn, nonDescIn] rw [Finset.disjoint_left] intro x hx hx' rw [mem_sdiff] at hx' exact hx'.2 hx
NonAncestorKernelTransport 6 core · 3 supporting This file transports observed conditional kernels between an induced SCM and a fixed SCM under an ancestral-closure and Rule-3-style non-ancestry condition. ★ condKernel_transport_of_nonAncestor★ condKernel_fixSet_identity_of_nonAncestor
Non-Ancestor Kernel Transport
This file transports observed conditional kernels between an induced SCM and a fixed SCM under an ancestral-closure and Rule-3-style non-ancestry condition. The results apply to an arbitrary observed node set; they neither assume that the set is a c-component nor establish Tian's c-component factorization. The file also provides intervention-target simplification.
For genuine Tian c-component content, see
SCM/ID/Density/CComponentDensity.lean, SCM/ID/Density/MechCFactor/, and
SCM/ID/Density/QFactor/TianRecovery.lean.
def QFactorMarginalFixingConclusion reviewed
⚑ flagged
Causalean.SCM.ID
For a finite node-label set, measurable node-value spaces, a structural causal model, a node set, a second node set, and an intervention target set, the non-ancestor marginal-transport conclusion asserts the following. Whenever the first node set is ancestrally closed, the second lies among the observed nodes of the induced model, the intervention targets are observed random nodes not already fixed and have no descendants in the second set after intervention, and a fixed-value slice is chosen, the two specified marginal observational measures on that second set are equal.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
Wn :
Finset N
hR_ac :
M.isAncestrallyClosedSCM R
hT_induce :
T ⊆ (M.induce R hR_ac).observed
_hWn_obs :
∀ D ∈ Wn, SWIGNode.random D ∈ M.observed
_hWn_fixed :
∀ D ∈ Wn, SWIGNode.fixed D ∉ M.fixed
_hNoDesc :
∀ z ∈ Wn, ∀ v ∈ T, ¬ (M.fixSet Wn _hWn_obs _hWn_fixed).dag.isAncestor (SWIGNode.fixed z) v
s' :
(M.fixSet Wn _hWn_obs _hWn_fixed).FixedValues
def
QFactorMarginalFixingConclusion M R T Wn :
Prop
given by
((M.fixSet Wn _hWn_obs _hWn_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M Wn _hWn_obs _hWn_fixed).symm ▸ (show T ⊆ M.observed from fun v hv => (Finset.mem_inter.mp (show v ∈ R ∩ M.observed from hT_induce hv)).2)))
= ((M.induce R hR_ac).obsKernel (valuesProjection (filter_subset _ _) (M.fixSetProj Wn _hWn_obs _hWn_fixed s'))).map (valuesProjection hT_induce)
def QFactorIdentityConclusion reviewed
⚑ flagged
Causalean.SCM.ID
For a finite node-label set, measurable node-value spaces, a structural causal model, a node set, a second node set, and an intervention target set, the conditional-kernel transport conclusion asserts that, whenever the first node set is ancestrally closed, the second lies among the observed nodes of the induced model, and the targets are observed random nodes not already fixed with no descendants in the second set or its induced conditioning-parent set after intervention, the indicated induced and post-intervention conditional kernels are almost everywhere equal under the induced parent marginal at every fixed-value slice, provided their stated finite-measure, standard-Borel, nonemptiness, and countable-generation conditions hold. It uses the induced model, the post-intervention model, and the induced conditioning-parent set.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
Wn :
Finset N
hR_ac :
M.isAncestrallyClosedSCM R
hT_induce :
T ⊆ (M.induce R hR_ac).observed
_hWn_obs :
∀ D ∈ Wn, SWIGNode.random D ∈ M.observed
_hWn_fixed :
∀ D ∈ Wn, SWIGNode.fixed D ∉ M.fixed
_hNoDesc :
∀ z ∈ Wn,
∀ v ∈ T ∪ (M.induce R hR_ac).toSWIGGraph.qFactorParents T,
¬ (M.fixSet Wn _hWn_obs _hWn_fixed).dag.isAncestor (SWIGNode.fixed z) v
def
QFactorIdentityConclusion M R T Wn :
Prop
given by
MI :
M.induce R hR_ac (: SCM N Ω)
Mdo :
M.fixSet Wn _hWn_obs _hWn_fixed (: SCM N Ω)
∀ sI : MI.FixedValues, IsFiniteMeasure (MI.obsKernel sI)
∀ sD : Mdo.FixedValues, IsFiniteMeasure (Mdo.obsKernel sD)
s' :
Mdo.FixedValues
sInduce :
valuesProjection (filter_subset _ _) (M.fixSetProj Wn _hWn_obs _hWn_fixed s') (: MI.FixedValues)
∀ᵐ c ∂((MI.obsKernel sInduce).map (valuesProjection (MI.toSWIGGraph.qFactorParents_subset_observed T))), (MI.condKernelFactor T hT_induce sInduce) c
= (((Mdo.obsCondKernel T P (show T ⊆ Mdo.observed from by intro v hv have hvM : v ∈ M.observed := by exact (Finset.mem_inter.mp (show v ∈ R ∩ M.observed from hT_induce hv)).2 simpa [Mdo, fixSet_observed] using hvM) (show P ⊆ Mdo.observed from by intro v hv have hvMI : v ∈ MI.observed := MI.toSWIGGraph.qFactorParents_subset_observed T hv have hvM : v ∈ M.observed := by exact (Finset.mem_inter.mp (show v ∈ R ∩ M.observed from hvMI)).2 simpa [Mdo, fixSet_observed] using hvM)).comap (fun c => (s', c)) (prodMk measurable_const measurable_id)) c)
theorem condKernel_transport_of_nonAncestor reviewed
⚑ flagged
Causalean.SCM.ID
For a structural causal model M, an ancestrally closed node set R, an observed node set T of the induced model, and an intervention target set Wn, the induced conditional-kernel factor agrees almost everywhere with the corresponding conditional kernel of the fixed model, provided the stated Rule-3-style non-ancestor, finite-measure, standard-Borel, and countable-generation assumptions hold. No c-component assumption is present.
Formal statement
Proof (Lean source)
theorem condKernel_transport_of_nonAncestor
(M : SCM N Ω)
(R : Finset (SWIGNode N))
(T : Finset (SWIGNode N))
(Wn : Finset N) :
QFactorIdentityConclusion M R T Wn := by
classical
intro hR_ac hT_induce hWn_obs hWn_fixed hNoDesc
dsimp only
intro _ _ _ _ _ _ s'
-- The conditional-kernel uniqueness argument first proves the joint identity on
-- `T ∪ qFactorParents T` by combining the marginal helper with Rule 3 at that
-- larger target, then applies `Kernel.disintegrate`/`condKernel` uniqueness to
-- identify the two conditional kernels a.e. under the common parent marginal.
have hMarginal :
QFactorMarginalFixingConclusion M R T Wn :=
q_factor_marginal_fixing M R T Wn
have _hT_marginal :=
hMarginal hR_ac hT_induce hWn_obs hWn_fixed
(by
intro z hz v hv
exact hNoDesc z hz v (Finset.mem_union_left _ hv))
s'
let MI : SCM N Ω := M.induce R hR_ac
let Mdo : SCM N Ω := M.fixSet Wn hWn_obs hWn_fixed
let P : Finset (SWIGNode N) := MI.toSWIGGraph.qFactorParents T
let sInduce : MI.FixedValues :=
valuesProjection (filter_subset _ _)
(M.fixSetProj Wn hWn_obs hWn_fixed s')
have hP_induce : P ⊆ MI.observed := by
simpa [P, MI] using
(MI.toSWIGGraph.qFactorParents_subset_observed T)
have hT_base : T ⊆ M.observed := by
intro v hv
exact (Finset.mem_inter.mp
(show v ∈ R ∩ M.observed from hT_induce hv)).2
have hP_base : P ⊆ M.observed := by
intro v hv
have hvMI : v ∈ MI.observed := hP_induce hv
exact (Finset.mem_inter.mp
(show v ∈ R ∩ M.observed from hvMI)).2
have hT_do : T ⊆ Mdo.observed := by
simpa [Mdo, fixSet_observed] using hT_base
have hP_do : P ⊆ Mdo.observed := by
simpa [Mdo, fixSet_observed] using hP_base
let U : Finset (SWIGNode N) := T ∪ P
have hU_induce : U ⊆ MI.observed := by
intro v hv
rcases Finset.mem_union.mp hv with hvT | hvP
· exact hT_induce hvT
· exact hP_induce hvP
have hU_base : U ⊆ M.observed := by
intro v hv
rcases Finset.mem_union.mp hv with hvT | hvP
· exact hT_base hvT
· exact hP_base hvP
have hU_do : U ⊆ Mdo.observed := by
simpa [Mdo, fixSet_observed] using hU_base
have hMI_obs_base : MI.observed ⊆ M.observed := by
exact Finset.inter_subset_right
have hRule3U :
(Mdo.obsKernel s').map (valuesProjection hU_do)
=
(M.obsKernel (M.fixSetProj Wn hWn_obs hWn_fixed s')).map
(valuesProjection hU_base) := by
simpa [Mdo, U] using
condDistrib_intervention_ancestral_eq
M Wn hWn_obs hWn_fixed U hU_base
(by
intro z hz v hv
exact hNoDesc z hz v (by simpa [U, P, MI] using hv))
s'
have hInduced :
MI.obsKernel sInduce =
(M.obsKernel (M.fixSetProj Wn hWn_obs hWn_fixed s')).map
(valuesProjection hMI_obs_base) := by
simpa [MI, sInduce] using
induce_marginal_compat M R hR_ac
(M.fixSetProj Wn hWn_obs hWn_fixed s')
have hJointU :
(Mdo.obsKernel s').map (valuesProjection hU_do)
=
(MI.obsKernel sInduce).map (valuesProjection hU_induce) := by
rw [hRule3U, hInduced]
rw [MeasureTheory.Measure.map_map
(measurable_valuesProjection hU_induce)
(measurable_valuesProjection hMI_obs_base)]
rw [← valuesProjection_comp hU_induce hMI_obs_base]
have hP_U : P ⊆ U := by
intro v hv
exact Finset.mem_union_right T hv
have hT_U : T ⊆ U := by
intro v hv
exact Finset.mem_union_left P hv
let pairU : ValuesOn U (swigΩ Ω) →
ValuesOn P (swigΩ Ω) × ValuesOn T (swigΩ Ω) :=
fun ω => (valuesProjection hP_U ω, valuesProjection hT_U ω)
have hpairU_meas : Measurable pairU := by
exact (measurable_valuesProjection hP_U).prodMk
(measurable_valuesProjection hT_U)
have hPair_do_comp :
pairU ∘ valuesProjection hU_do =
(fun ω : Mdo.ObservedValues =>
(valuesProjection hP_do ω, valuesProjection hT_do ω)) := by
funext ω
apply Prod.ext
· exact congrFun (valuesProjection_comp hP_U hU_do).symm ω
· exact congrFun (valuesProjection_comp hT_U hU_do).symm ω
have hPair_induce_comp :
pairU ∘ valuesProjection hU_induce =
(fun ω : MI.ObservedValues =>
(valuesProjection hP_induce ω, valuesProjection hT_induce ω)) := by
funext ω
apply Prod.ext
· exact congrFun (valuesProjection_comp hP_U hU_induce).symm ω
· exact congrFun (valuesProjection_comp hT_U hU_induce).symm ω
have hPairMeasure :
MI.obsCondPairKernel T P hT_induce hP_induce sInduce =
Mdo.obsCondPairKernel T P hT_do hP_do s' := by
unfold SCM.obsCondPairKernel
rw [ProbabilityTheory.Kernel.map_apply _
((measurable_valuesProjection hP_induce).prodMk
(measurable_valuesProjection hT_induce))]
rw [ProbabilityTheory.Kernel.map_apply _
((measurable_valuesProjection hP_do).prodMk
(measurable_valuesProjection hT_do))]
rw [← hPair_induce_comp, ← hPair_do_comp]
rw [← MeasureTheory.Measure.map_map hpairU_meas
(measurable_valuesProjection hU_induce)]
rw [← MeasureTheory.Measure.map_map hpairU_meas
(measurable_valuesProjection hU_do)]
exact congrArg (map pairU) hJointU.symm
have hAE :=
obsCondKernel_slice_ae_eq_of_pairMeasure_eq
MI Mdo T P hT_induce hP_induce hT_do hP_do
sInduce s' hPairMeasure
exact hAE
def InterventionTargetSimpConclusion reviewed
⚑ flagged
Causalean.SCM.ID
For a finite node-label set, measurable node-value spaces, a structural causal model, a first intervention target set, and a second intervention target set, the intervention-target simplification conclusion asserts that the two target sets are disjoint, that each listed intervention is well formed, and that intervening first on the first set and then on the second produces a structurally equivalent model to intervening once on their union.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
Dn Yn :
Finset N
hD_obs :
∀ D ∈ Dn, SWIGNode.random D ∈ M.observed
hD_fixed :
∀ D ∈ Dn, SWIGNode.fixed D ∉ M.fixed
hY_obs :
∀ D ∈ Yn, SWIGNode.random D ∈ (M.fixSet Dn hD_obs hD_fixed).observed
hY_fixed :
∀ D ∈ Yn, SWIGNode.fixed D ∉ (M.fixSet Dn hD_obs hD_fixed).fixed
hUnion_obs :
∀ D ∈ Dn ∪ Yn, SWIGNode.random D ∈ M.observed
hUnion_fixed :
∀ D ∈ Dn ∪ Yn, SWIGNode.fixed D ∉ M.fixed
_hDY_disjoint :
Disjoint Dn Yn
def
InterventionTargetSimpConclusion M Dn Yn :
Prop
given by
SCM.Equiv ((M.fixSet Dn hD_obs hD_fixed).fixSet Yn hY_obs hY_fixed) (M.fixSet (Dn ∪ Yn) hUnion_obs hUnion_fixed)
def DistrictIdConclusion reviewed
⚑ flagged
Causalean.SCM.ID
For a finite node-label set, measurable node-value spaces, a structural causal model, a node set, and an intervention target set, the full-observed transport conclusion is the conditional-kernel transport conclusion obtained by taking the ancestral node set to be all observed nodes of the model.
Definition (Lean source)
parameters
def
DistrictIdConclusion M T Wn :
Prop
given by
QFactorIdentityConclusion M M.observed T Wn
theorem condKernel_fixSet_identity_of_nonAncestor reviewed
⚑ flagged
Causalean.SCM.ID
For a structural causal model M, an observed node set T, and an intervention set Wn, the fixed-model conditional kernel equals almost everywhere the corresponding kernel of the induced full-observed model, under the non-ancestor assumptions of QFactorIdentityConclusion.
Formal statement
hypotheses
conclusion
DistrictIdConclusion M T Wn
Proof (Lean source)
theorem condKernel_fixSet_identity_of_nonAncestor
(M : SCM N Ω)
(T : Finset (SWIGNode N))
(Wn : Finset N) :
DistrictIdConclusion M T Wn :=
condKernel_transport_of_nonAncestor M M.observed T Wn
3 supporting declarations (lemmas, instances)
-
q_factor_marginal_fixingtheorem — The marginal non-ancestor transport identity.hypothesesconclusionQFactorMarginalFixingConclusion M R T WnProof (Lean source)
theorem q_factor_marginal_fixing (M : SCM N Ω) (R : Finset (SWIGNode N)) (T : Finset (SWIGNode N)) (Wn : Finset N) : QFactorMarginalFixingConclusion M R T Wn := by classical intro hR_ac hT_induce hWn_obs hWn_fixed hNoDesc s' let sTilde : M.FixedValues := M.fixSetProj Wn hWn_obs hWn_fixed s' let MI : SCM N Ω := M.induce R hR_ac have hT_base : T ⊆ M.observed := by intro v hv exact (Finset.mem_inter.mp (show v ∈ R ∩ M.observed from hT_induce hv)).2 have hMI_obs_base : MI.observed ⊆ M.observed := by exact Finset.inter_subset_right have hRule3 : ((M.fixSet Wn hWn_obs hWn_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M Wn hWn_obs hWn_fixed).symm ▸ hT_base)) = (M.obsKernel sTilde).map (valuesProjection hT_base) := by simpa [sTilde] using condDistrib_intervention_ancestral_eq M Wn hWn_obs hWn_fixed T hT_base hNoDesc s' have hInduced : MI.obsKernel (valuesProjection (filter_subset _ _) sTilde) = (M.obsKernel sTilde).map (valuesProjection hMI_obs_base) := by simpa [MI] using induce_marginal_compat M R hR_ac sTilde rw [hRule3, hInduced] rw [MeasureTheory.Measure.map_map (measurable_valuesProjection hT_induce) (measurable_valuesProjection hMI_obs_base)] rw [← valuesProjection_comp hT_induce hMI_obs_base] -
obsCondKernel_slice_ae_eq_of_pairMeasure_eqtheorem — Equal pair laws give equal conditional-kernel slices a.e.hypothesesN :sharedType u_1N → Type u_2M₁ M₂ :SCM N ΩhY₁ :Y ⊆ M₁.observedhCC₁ :CC ⊆ M₁.observedhY₂ :Y ⊆ M₂.observedhCC₂ :CC ⊆ M₂.observed∀ s : M₁.FixedValues, IsFiniteMeasure (M₁.obsKernel s)∀ s : M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s)s₁ :M₁.FixedValuess₂ :M₂.FixedValueshPair :M₁.obsCondPairKernel Y CC hY₁ hCC₁ s₁ = M₂.obsCondPairKernel Y CC hY₂ hCC₂ s₂conclusion(fun c => (M₁.obsCondKernel Y CC hY₁ hCC₁).sectR s₁ c)=ᵐ[(M₁.obsKernel s₁).map (valuesProjection hCC₁)] fun c => (M₂.obsCondKernel Y CC hY₂ hCC₂).sectR s₂ cProof (Lean source)
theorem obsCondKernel_slice_ae_eq_of_pairMeasure_eq (M₁ M₂ : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY₁ : Y ⊆ M₁.observed) (hCC₁ : CC ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (hCC₂ : CC ⊆ M₂.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [∀ s : M₁.FixedValues, IsFiniteMeasure (M₁.obsKernel s)] [∀ s : M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s)] [CountableOrCountablyGenerated M₁.FixedValues (ValuesOn CC (swigΩ Ω))] [CountableOrCountablyGenerated M₂.FixedValues (ValuesOn CC (swigΩ Ω))] (s₁ : M₁.FixedValues) (s₂ : M₂.FixedValues) (hPair : M₁.obsCondPairKernel Y CC hY₁ hCC₁ s₁ = M₂.obsCondPairKernel Y CC hY₂ hCC₂ s₂) : (fun c => (M₁.obsCondKernel Y CC hY₁ hCC₁).sectR s₁ c) =ᵐ[(M₁.obsKernel s₁).map (valuesProjection hCC₁)] fun c => (M₂.obsCondKernel Y CC hY₂ hCC₂).sectR s₂ c := by classical let μ₁ : Measure (ValuesOn CC (swigΩ Ω)) := (M₁.obsKernel s₁).map (valuesProjection hCC₁) let μ₂ : Measure (ValuesOn CC (swigΩ Ω)) := (M₂.obsKernel s₂).map (valuesProjection hCC₂) let κ₁ : Kernel (ValuesOn CC (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M₁.obsCondKernel Y CC hY₁ hCC₁).sectR s₁ let κ₂ : Kernel (ValuesOn CC (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M₂.obsCondKernel Y CC hY₂ hCC₂).sectR s₂ haveI : IsMarkovKernel (M₁.obsCondKernel Y CC hY₁ hCC₁) := by unfold SCM.obsCondKernel infer_instance haveI : IsMarkovKernel (M₂.obsCondKernel Y CC hY₂ hCC₂) := by unfold SCM.obsCondKernel infer_instance haveI : IsMarkovKernel κ₁ := by dsimp [κ₁] infer_instance haveI : IsMarkovKernel κ₂ := by dsimp [κ₂] infer_instance have h₁ : M₁.obsCondPairKernel Y CC hY₁ hCC₁ s₁ = μ₁ ⊗ₘ κ₁ := by simpa [μ₁, κ₁] using SCM.obsCondPairKernel_apply_eq_compProd M₁ Y CC hY₁ hCC₁ s₁ have h₂ : M₂.obsCondPairKernel Y CC hY₂ hCC₂ s₂ = μ₂ ⊗ₘ κ₂ := by simpa [μ₂, κ₂] using SCM.obsCondPairKernel_apply_eq_compProd M₂ Y CC hY₂ hCC₂ s₂ have hComp : μ₁ ⊗ₘ κ₁ = μ₂ ⊗ₘ κ₂ := by rw [← h₁, ← h₂] exact hPair have hμ : μ₁ = μ₂ := by have hfst := congrArg fst hComp simpa [MeasureTheory.Measure.fst_compProd] using hfst have hComp' : μ₁ ⊗ₘ κ₁ = μ₁ ⊗ₘ κ₂ := by simpa [hμ] using hComp exact ProbabilityTheory.Kernel.ae_eq_of_compProd_eq hComp' -
intervention_target_simptheorem — Proposition (fact4 — intervention target simplification).hypothesesconclusionInterventionTargetSimpConclusion M Dn YnProof (Lean source)
theorem intervention_target_simp (M : SCM N Ω) (Dn Yn : Finset N) : InterventionTargetSimpConclusion M Dn Yn := by classical refine Finset.induction_on Yn ?_ ?_ · intro hD_obs hD_fixed hY_obs hY_fixed hUnion_obs hUnion_fixed _hDY_disjoint have hEmpty : SCM.Equiv ((M.fixSet Dn hD_obs hD_fixed).fixSet ∅ hY_obs hY_fixed) (M.fixSet Dn hD_obs hD_fixed) := fixSet_empty_equiv (M.fixSet Dn hD_obs hD_fixed) have hRhs : SCM.Equiv (M.fixSet Dn hD_obs hD_fixed) (M.fixSet (Dn ∪ ∅) hUnion_obs hUnion_fixed) := by simpa [union_empty] using fixSet_equiv_congr (SCM.Equiv.refl M) Dn hD_obs hD_fixed exact SCM.Equiv.trans hEmpty hRhs · intro y Ys hyYs ih hD_obs hD_fixed hY_obs hY_fixed hUnion_obs hUnion_fixed hDY_disjoint let M₀ : SCM N Ω := M.fixSet Dn hD_obs hD_fixed have hYs_obs : ∀ D ∈ Ys, SWIGNode.random D ∈ M₀.observed := by intro D hD exact hY_obs D (Finset.mem_insert_of_mem hD) have hYs_fixed : ∀ D ∈ Ys, SWIGNode.fixed D ∉ M₀.fixed := by intro D hD exact hY_fixed D (Finset.mem_insert_of_mem hD) have hUnionYs_obs : ∀ D ∈ Dn ∪ Ys, SWIGNode.random D ∈ M.observed := by intro D hD exact hUnion_obs D (by rcases Finset.mem_union.mp hD with hD | hD · exact mem_union_left _ hD · exact mem_union_right _ (Finset.mem_insert_of_mem hD)) have hUnionYs_fixed : ∀ D ∈ Dn ∪ Ys, SWIGNode.fixed D ∉ M.fixed := by intro D hD exact hUnion_fixed D (by rcases Finset.mem_union.mp hD with hD | hD · exact mem_union_left _ hD · exact mem_union_right _ (Finset.mem_insert_of_mem hD)) have hDYs_disjoint : Disjoint Dn Ys := by exact hDY_disjoint.mono_right (by intro D hD; exact Finset.mem_insert_of_mem hD) have hyDn : y ∉ Dn := by intro hyD have hyMeet : y ∈ Dn ∩ insert y Ys := Finset.mem_inter.mpr ⟨hyD, Finset.mem_insert_self y Ys⟩ have hyBot : y ∈ (⊥ : Finset N) := hDY_disjoint.le_bot hyMeet simp at hyBot have hIH : SCM.Equiv (M₀.fixSet Ys hYs_obs hYs_fixed) (M.fixSet (Dn ∪ Ys) hUnionYs_obs hUnionYs_fixed) := ih hD_obs hD_fixed hYs_obs hYs_fixed hUnionYs_obs hUnionYs_fixed hDYs_disjoint have hy_single_obs₀ : ∀ D ∈ ({y} : Finset N), SWIGNode.random D ∈ (M₀.fixSet Ys hYs_obs hYs_fixed).observed := by intro D hD have hDy : D = y := by simpa using hD rw [hDy] simpa [M₀, fixSet_observed] using hY_obs y (Finset.mem_insert_self y Ys) have hy_single_fixed₀ : ∀ D ∈ ({y} : Finset N), SWIGNode.fixed D ∉ (M₀.fixSet Ys hYs_obs hYs_fixed).fixed := by intro D hD hmem have hDy : D = y := by simpa using hD rw [hDy] at hmem rw [fixSet_fixed] at hmem rcases Finset.mem_union.mp hmem with hM | hImg · exact hY_fixed y (Finset.mem_insert_self y Ys) hM · rcases Finset.mem_image.mp hImg with ⟨z, hz, hzy⟩ have hzy' : z = y := SWIGNode.fixed.inj hzy exact hyYs (by simpa [hzy'] using hz) have hStepL : SCM.Equiv (M₀.fixSet (insert y Ys) hY_obs hY_fixed) ((M₀.fixSet Ys hYs_obs hYs_fixed).fixSet ({y} : Finset N) hy_single_obs₀ hy_single_fixed₀) := (swigInterventionSet_insert_equiv M₀ Ys y hyYs hY_obs hY_fixed).symm have hy_single_obs₁ : ∀ D ∈ ({y} : Finset N), SWIGNode.random D ∈ (M.fixSet (Dn ∪ Ys) hUnionYs_obs hUnionYs_fixed).observed := by intro D hD have hDy : D = y := by simpa using hD rw [hDy] simpa [fixSet_observed] using hUnion_obs y (mem_union_right _ (Finset.mem_insert_self y Ys)) have hy_single_fixed₁ : ∀ D ∈ ({y} : Finset N), SWIGNode.fixed D ∉ (M.fixSet (Dn ∪ Ys) hUnionYs_obs hUnionYs_fixed).fixed := by intro D hD hmem have hDy : D = y := by simpa using hD rw [hDy] at hmem rw [fixSet_fixed] at hmem rcases Finset.mem_union.mp hmem with hM | hImg · exact hUnion_fixed y (mem_union_right _ (Finset.mem_insert_self y Ys)) hM · rcases Finset.mem_image.mp hImg with ⟨z, hz, hzy⟩ have hzy' : z = y := SWIGNode.fixed.inj hzy rcases Finset.mem_union.mp hz with hyD | hyY · exact hyDn (by simpa [hzy'] using hyD) · exact hyYs (by simpa [hzy'] using hyY) have hStepMid : SCM.Equiv ((M₀.fixSet Ys hYs_obs hYs_fixed).fixSet ({y} : Finset N) hy_single_obs₀ hy_single_fixed₀) ((M.fixSet (Dn ∪ Ys) hUnionYs_obs hUnionYs_fixed).fixSet ({y} : Finset N) hy_single_obs₁ hy_single_fixed₁) := fixSet_equiv_congr hIH ({y} : Finset N) hy_single_obs₀ hy_single_fixed₀ have hInsertUnion_obs : ∀ D ∈ insert y (Dn ∪ Ys), SWIGNode.random D ∈ M.observed := by intro D hD rcases Finset.mem_insert.mp hD with hEq | hD · rw [hEq] exact hUnion_obs y (mem_union_right _ (Finset.mem_insert_self y Ys)) · exact hUnion_obs D (by rcases Finset.mem_union.mp hD with hD | hD · exact mem_union_left _ hD · exact mem_union_right _ (Finset.mem_insert_of_mem hD)) have hInsertUnion_fixed : ∀ D ∈ insert y (Dn ∪ Ys), SWIGNode.fixed D ∉ M.fixed := by intro D hD rcases Finset.mem_insert.mp hD with hEq | hD · rw [hEq] exact hUnion_fixed y (mem_union_right _ (Finset.mem_insert_self y Ys)) · exact hUnion_fixed D (by rcases Finset.mem_union.mp hD with hD | hD · exact mem_union_left _ hD · exact mem_union_right _ (Finset.mem_insert_of_mem hD)) have hStepR : SCM.Equiv ((M.fixSet (Dn ∪ Ys) hUnionYs_obs hUnionYs_fixed).fixSet ({y} : Finset N) hy_single_obs₁ hy_single_fixed₁) (M.fixSet (insert y (Dn ∪ Ys)) hInsertUnion_obs hInsertUnion_fixed) := swigInterventionSet_insert_equiv M (Dn ∪ Ys) y (by intro hyUnion rcases Finset.mem_union.mp hyUnion with hyD | hyY · exact hyDn hyD · exact hyYs hyY) hInsertUnion_obs hInsertUnion_fixed have hAll := SCM.Equiv.trans hStepL (SCM.Equiv.trans hStepMid hStepR) simpa [M₀, Finset.insert_union, Finset.union_insert, Finset.union_assoc, union_comm, Finset.union_left_comm] using hAll