SCM.ID.GraphicalThms
Graphical identification theorems: c-component factorization and related structure results.
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
district_id, 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.
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 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
The recursive IDENTIFY certificate (full Tian–Shpitser ID success)
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 full ID algorithm 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. 3): repeatedly restrict to the ancestral set of C and
descend into the c-component of C in that restriction.
This file encodes IDENTIFY as an inductive reachability predicate
CFactorReachableRec G T C — a derivation exists iff identify(C, T, ·) returns
successfully (no hedge). 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 full recursive ID success 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 full recursive ID 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⟩
CComponentFactor 3 core · 1 supporting This file develops Tian's c-component factor setup for structural causal models and connects it to the per-node observational chain-rule product. ★ c_component_factorization
C-Component Factorization
This file develops Tian's c-component factor setup for structural causal models and connects it to the per-node observational chain-rule product.
The public API names the conditioning set for a component factor,
SWIGGraph.qFactorParents C = (⋃ v ∈ C, Pa⁺_G(v)) \ C, proves that these
conditioning coordinates are observed, and defines SCM.qFactor M C s as the
conditional-kernel proxy for Q[C] at a fixed slice. The theorem
c_component_factorization records the continuous-safe foundation: the
observational kernel is the chain-rule product of one-node conditional kernels
along the topological order of observed nodes.
Grouping that chain-rule product into Tian c-component factors is theorem
content supplied by downstream density and q-factor identity files; it is not a
definitional property of qFactor.
def qFactorParents reviewed
⚑ flagged
Causalean.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 qFactor 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 c-component conditional kernel 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 c_component_factorization reviewed
⚑ flagged
Causalean.SCM
Theorem (Tian 2002, per-node chain-rule factorization). For a structural causal model M, at 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. Tian's Pa⁺(V) is interpreted as the full observed history before V, so this statement is the ordinary iterated-disintegration factorization and does not use graphical Markov or do-calculus reasoning.
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 c_component_factorization
(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
DoGFormulaTian 6 core · 22 supporting This file states the Tian density factorization used by the graphical ID algorithm: the post-intervention law on the observed ancestors of the query is identified by a product of district factors recovered from the obser ★ markov_tian_cfactorization_density★ doAncestralDistrictDensity_recovered_from_obs★ doObsKernelAncestralMarginal_tian_cfactorization_density
Tian density assembly for the ID do-law g-formula
This file states the Tian density factorization used by the graphical ID algorithm: the post-intervention law on the observed ancestors of the query is identified by a product of district factors recovered from the observational density.
The statements avoid SCM.induce for the post-intervention ancestral law: all
district factors of the do-law marginal are defined from the marginal measure
itself, using Tian's prefix-ratio/conditional construction on
D = An_{G_X}(Y) ∩ observed.
The main results are:
* rnDeriv_eq_tianDensityProduct, a measure-only chain rule expressing a
dominated finite law's density as a product of one-coordinate conditional
densities in graph order.
* markov_tian_cfactorization_density, which regroups that product into Tian
district factors for a globally Markov finite law.
* doObsKernelAncestralMarginal_globalMarkovOn, the SCM-to-measure Markov bridge
for the ancestral do-law marginal.
* doAncestralDistrictDensity_recovered_from_obs and
doObsKernelAncestralMarginal_tian_cfactorization_density, the ID-specific
recovery and factorization statements used by the discrete soundness layer.
def extendTianPrefix reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a SWIG graph, a finite node set, and an index strictly below its cardinality, the prefix-extension map combines an assignment on the first indexed nodes with an assignment on the next node into an assignment on the one-node-longer prefix.
Definition (Lean source)
parameters
def
given by
fun p
def tianPrefixDensityProductInPrefix reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a SWIG graph, a finite node set, a finite measure on its joint value space, and reference measures, assuming every graph-ordered singleton node value space is standard Borel and nonempty, the Tian prefix density product at a prefix length and an assignment on that prefix is one at length zero and otherwise the preceding product times the next conditional-density factor, or one when that next index is outside the node set.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
H :
ref :
∀ (k : ℕ) (hk : k < D.card),
k :
ℕ
given by
clause 1
| 0, _ => 1
clause 2
| k + 1, z
=> tianPrefixDensityProductInPrefix H D μ ref k (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z) * if hk : k < D.card then ((condDistrib (valuesProjection (show ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hk⟩).property)) (valuesProjection (H.prefixIn_subset D k)) μ) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z)).rnDeriv (jointRef ref ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N))) (valuesProjection (show ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D (k + 1) from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨k, hk⟩] exact Nat.lt_succ_self k) z) else 1
def tianPrefixStepDensityInPrefix reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a SWIG graph, a finite node set, a finite measure on its joint value space, reference measures, assuming every graph-ordered singleton node value space is standard Borel and nonempty, a prefix length, an assignment on that prefix, and a node index, the one-step Tian density is the conditional-density factor for that indexed node when it lies in both the prefix and the node set, and is one otherwise.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
H :
ref :
∀ (i : ℕ) (hi : i < D.card),
k :
ℕ
i :
ℕ
def
given by
if hi : i < k then if hcard : i < D.card then ((condDistrib (valuesProjection (show ({(H.nodesAt D ⟨i, hcard⟩).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨i, hcard⟩).property)) (valuesProjection (H.prefixIn_subset D i)) μ) (valuesProjection (prefixIn_mono H D (le_of_lt hi)) z)).rnDeriv (jointRef ref ({(H.nodesAt D ⟨i, hcard⟩).val} : Finset (SWIGNode N))) (valuesProjection (show ({(H.nodesAt D ⟨i, hcard⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D k from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D k ⟨i, hcard⟩] exact hi) z) else 1 else 1
theorem markov_tian_cfactorization_density reviewed
⚑ flagged
Causalean.SCM.ID
Density form of the Markov-to-c-factorization theorem. Let H be a pure SWIG graph, D a finite set of SWIG nodes, μ a finite (probability) measure on the assignments to D, and ref a family of reference measures. If D is exactly the observed-node set of H and μ is absolutely continuous with respect to the product reference measure on D, then the Radon–Nikodym density of μ against that product reference equals, almost everywhere, the product over the c-components of H of their Tian district-density factors.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
H :
hD :
H.observed = D
ref :
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
∀ (k : ℕ) (hk : k < D.card),
hdom :
μ ≪ jointRef ref D
conclusion
μ.rnDeriv (jointRef ref D)
=ᵐ[jointRef ref D] fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x
Proof (Lean source)
theorem markov_tian_cfactorization_density
(H : SWIGGraph N) (D : Finset (SWIGNode N))
(hD : H.observed = D)
(μ : Measure (ValuesOn D (swigΩ Ω)))
(ref : ReferenceMeasures Ω)
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
[StandardBorelSpace (ValuesOn D (swigΩ Ω))]
[IsProbabilityMeasure μ]
[∀ (k : ℕ) (hk : k < D.card),
StandardBorelSpace
(ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < D.card),
Nonempty
(ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))]
(hdom : μ ≪ jointRef ref D) :
μ.rnDeriv (jointRef ref D)
=ᵐ[jointRef ref D]
fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x := by
exact (rnDeriv_eq_tianDensityProduct H D μ ref hdom).trans
(Filter.EventuallyEq.of_eq
(prod_tianDistrictDensity_eq_tianDensityProduct H D hD μ ref).symm)
theorem doAncestralDistrictDensity_recovered_from_obs reviewed
⚑ flagged
Causalean.SCM.ID
T2, abstract density recovery statement. Fix a standard structural causal model M and an intervention target set X for which every targeted node is currently a random observed node and none of its fixed copies is already fixed, an output set Y, and a reference-measure family faithful to the graph. For a district S of the truncated c-component set of the post-intervention ancestral graph and a c-component C of the base graph that is factor-reachable from S, assume every fixed-value assignment gives an observational kernel with everywhere-positive point masses, no intervention target's random form lies in Y, and that an extension map from ancestral assignments to full observed assignments restricts back to the identity and agrees with the intervention values sDo on the targeted coordinates. Then the district factor of S computed from the density of the do-law's ancestral marginal equals, almost everywhere, the full-graph c-component density factor of C evaluated at the extension of the ancestral assignment.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
X :
Finset N
hStd :
M.isStandard
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
ref :
href :
sDo :
(M.fixSet X hObs hFix).FixedValues
hS :
S ∈ fixTruncCComponentSet M X hObs hFix Y
hReach :
cFactorReachable M.toSWIGGraph C S
hCmem :
C ∈ M.toSWIGGraph.cComponentSet
IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
hpos :
∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')
hYX :
∀ D ∈ X, SWIGNode.random D ∉ Y
extend :
hExtend :
∀ xD,
valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)
= xD
hExtendX :
∀ xD (D : N) (hD : D ∈ X),
extend xD ⟨SWIGNode.random D, hObs D hD⟩
= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩
conclusion
D :
fixObservedAncestralSet M X hObs hFix Y
H :
(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)
tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S
=ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) C (extend xD)
Proof (Lean source)
theorem doAncestralDistrictDensity_recovered_from_obs
[∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(M : SCM N Ω) (X : Finset N)
(hStd : M.isStandard)
(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)
(sDo : (M.fixSet X hObs hFix).FixedValues)
(S C : Finset (SWIGNode N))
(hS : S ∈ fixTruncCComponentSet M X hObs hFix Y)
(hReach : cFactorReachable M.toSWIGGraph C S)
(hCmem : C ∈ M.toSWIGGraph.cComponentSet)
[IsFiniteMeasure
(doObsKernelAncestralMarginal M X hObs hFix Y sDo)]
[∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (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Ω Ω))]
(hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s'))
(hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y)
(extend :
ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) →
ValuesOn M.observed (swigΩ Ω))
(hExtend : ∀ xD, valuesProjection
(show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from
inter_subset_right) (extend xD) = xD)
(hExtendX : ∀ xD (D : N) (hD : D ∈ X),
extend xD ⟨SWIGNode.random D, hObs D hD⟩ =
sDo ⟨SWIGNode.fixed D,
mem_union_right _
(Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) :
let D := fixObservedAncestralSet M X hObs hFix Y
let H := (M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)
tianDistrictDensity H D
(doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S
=ᵐ[jointRef ref D]
fun xD =>
M.cComponentDensityFactor ref
(M.fixSetProj X hObs hFix sDo) C (extend xD) := by
exact doAncestralDistrictDensity_recovered_from_obs_core
M X hStd hObs hFix Y ref href sDo S C hS hReach hCmem hpos hYX extend hExtend
hExtendX
theorem doObsKernelAncestralMarginal_tian_cfactorization_density reviewed
⚑ flagged
Causalean.SCM.ID
ID-specific T1 wrapper. For an intervention target set X where every targeted node is currently a random observed node with no fixed copy already fixed, if the ancestral marginal of the do-law ν_M = (M.fixSet X).obsKernel.map π_D is absolutely continuous with respect to the product reference measure on the ancestral observed set, then its Radon–Nikodym density equals, almost everywhere, the product over the c-components of the induced post-intervention ancestral graph G_X[D] of their Tian district-density factors.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
∀ n, Fintype (Ω n)
∀ 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
ref :
s :
(M.fixSet X hObs hFix).FixedValues
StandardBorelSpace (M.fixSet X hObs hFix).RandomValues
StandardBorelSpace (M.fixSet X hObs hFix).ObservedValues
∀ s' : (M.fixSet X hObs hFix).FixedValues,
IsFiniteMeasure ((M.fixSet X hObs hFix).jointKernel s')
∀ s' : (M.fixSet X hObs hFix).FixedValues,
IsFiniteMeasure ((M.fixSet X hObs hFix).obsKernel s')
IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y s)
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
hdomD :
doObsKernelAncestralMarginal M X hObs hFix Y s ≪ jointRef ref (fixObservedAncestralSet M X hObs hFix Y)
conclusion
D :
fixObservedAncestralSet M X hObs hFix Y
H :
(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)
(doObsKernelAncestralMarginal M X hObs hFix Y s).rnDeriv (jointRef ref D)
=ᵐ[jointRef ref D] fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y s) ref S x
Proof (Lean source)
theorem doObsKernelAncestralMarginal_tian_cfactorization_density
[∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)]
[∀ n, Fintype (Ω n)] [∀ 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 Ω)
(s : (M.fixSet X hObs hFix).FixedValues)
[StandardBorelSpace
(ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω))]
[StandardBorelSpace (M.fixSet X hObs hFix).RandomValues]
[StandardBorelSpace (M.fixSet X hObs hFix).ObservedValues]
[∀ s' : (M.fixSet X hObs hFix).FixedValues,
IsFiniteMeasure ((M.fixSet X hObs hFix).jointKernel s')]
[∀ s' : (M.fixSet X hObs hFix).FixedValues,
IsFiniteMeasure ((M.fixSet X hObs hFix).obsKernel s')]
[IsFiniteMeasure
(doObsKernelAncestralMarginal M X hObs hFix Y s)]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
(hdomD :
doObsKernelAncestralMarginal M X hObs hFix Y s ≪
jointRef ref (fixObservedAncestralSet M X hObs hFix Y)) :
let D := fixObservedAncestralSet M X hObs hFix Y
let H := (M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)
(doObsKernelAncestralMarginal M X hObs hFix Y s).rnDeriv
(jointRef ref D)
=ᵐ[jointRef ref D]
fun x => ∏ S ∈ H.cComponentSet,
tianDistrictDensity H D
(doObsKernelAncestralMarginal M X hObs hFix Y s) ref S x := by
intro D H
exact markov_tian_cfactorization_density H D rfl
(doObsKernelAncestralMarginal M X hObs hFix Y s) ref hdomD
22 supporting declarations (lemmas, instances)
-
mem_prefixIn_ifflemma — Membership in a graph-ordered prefix of D is exactly index membership below the prefix length.hypothesesconclusionv ∈ H.prefixIn D n ↔ ∃ h : v ∈ D, (H.nodeIndex D ⟨v, h⟩).val < nProof (Lean source)
lemma mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (v : SWIGNode N) : v ∈ H.prefixIn D n ↔ ∃ h : v ∈ D, (H.nodeIndex D ⟨v, h⟩).val < n := by unfold SWIGGraph.prefixIn constructor · intro hv rcases Finset.mem_filter.mp hv with ⟨hD, hltif⟩ exact ⟨hD, by simpa [hD] using hltif⟩ · rintro ⟨hD, hlt⟩ exact Finset.mem_filter.mpr ⟨hD, by simpa [hD] using hlt⟩ -
prefixIn_zerolemma — The D-prefix of length zero is empty.hypothesesconclusionH.prefixIn D 0 = ∅Proof (Lean source)
lemma prefixIn_zero (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D 0 = ∅ := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D 0 v).mp hv with ⟨_, hlt⟩ omega · simp -
nodesAt_mem_prefixIn_ifflemma — The node at index i belongs to the first n D-nodes iff i < n.hypothesesconclusion(H.nodesAt D i).val ∈ H.prefixIn D n ↔ i.val < nProof (Lean source)
lemma nodesAt_mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (i : Fin D.card) : (H.nodesAt D i).val ∈ H.prefixIn D n ↔ i.val < n := by rw [mem_prefixIn_iff] constructor · rintro ⟨hD, hlt⟩ have hidx : H.nodeIndex D ⟨(H.nodesAt D i).val, hD⟩ = i := by have hsub : (⟨(H.nodesAt D i).val, hD⟩ : {v // v ∈ D}) = H.nodesAt D i := Subtype.ext rfl rw [hsub] simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rwa [hidx] at hlt · intro hlt exact ⟨(H.nodesAt D i).property, by have hidx : H.nodeIndex D (H.nodesAt D i) = i := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] simpa [hidx] using hlt⟩ -
prefixIn_cardlemma — The full D-prefix is D.hypothesesconclusionH.prefixIn D D.card = DProof (Lean source)
lemma prefixIn_card (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D D.card = D := by ext v constructor · exact fun hv => H.prefixIn_subset D D.card hv · intro hv exact (mem_prefixIn_iff H D D.card v).mpr ⟨hv, (H.nodeIndex D ⟨v, hv⟩).isLt⟩ -
prefixIn_monolemma — Prefix sets are monotone in the prefix length.hypothesesconclusionH.prefixIn D m ⊆ H.prefixIn D kProof (Lean source)
lemma prefixIn_mono (H : SWIGGraph N) (D : Finset (SWIGNode N)) {m k : ℕ} (h : m ≤ k) : H.prefixIn D m ⊆ H.prefixIn D k := by intro v hv rcases (mem_prefixIn_iff H D m v).mp hv with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D k v).mpr ⟨hD, lt_of_lt_of_le hlt h⟩ -
nodesAt_not_mem_prefixInlemma — The next D-node is not in the previous D-prefix.hypothesesconclusion(H.nodesAt D ⟨n, hn⟩).val ∉ H.prefixIn D nProof (Lean source)
lemma nodesAt_not_mem_prefixIn (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : (H.nodesAt D ⟨n, hn⟩).val ∉ H.prefixIn D n := by rw [nodesAt_mem_prefixIn_iff H D n ⟨n, hn⟩] exact Nat.lt_irrefl n -
prefixIn_succlemma — The successor D-prefix is obtained by adjoining the next D-node.hypothesesconclusionH.prefixIn D (n + 1) = H.prefixIn D n ∪ {(H.nodesAt D ⟨n, hn⟩).val}Proof (Lean source)
lemma prefixIn_succ (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : H.prefixIn D (n + 1) = H.prefixIn D n ∪ {(H.nodesAt D ⟨n, hn⟩).val} := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D (n + 1) v).mp hv with ⟨hD, hlt⟩ by_cases hlt_n : (H.nodeIndex D ⟨v, hD⟩).val < n · exact mem_union_left _ ((mem_prefixIn_iff H D n v).mpr ⟨hD, hlt_n⟩) · have hidx_val : (H.nodeIndex D ⟨v, hD⟩).val = n := by omega have hidx : H.nodeIndex D ⟨v, hD⟩ = ⟨n, hn⟩ := Fin.ext hidx_val have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by have hround : H.nodesAt D (H.nodeIndex D ⟨v, hD⟩) = ⟨v, hD⟩ := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rw [hidx] at hround exact congrArg val hround.symm exact mem_union_right _ (by simp [hv_eq]) · intro hv rcases Finset.mem_union.mp hv with hvpre | hvlast · rcases (mem_prefixIn_iff H D n v).mp hvpre with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D (n + 1) v).mpr ⟨hD, by omega⟩ · have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by simpa using hvlast subst hv_eq rw [nodesAt_mem_prefixIn_iff H D (n + 1) ⟨n, hn⟩] exact Nat.lt_succ_self n -
prefixIn_disjoint_singleton_nextlemma — The previous D-prefix is disjoint from the singleton next node.hypothesesProof (Lean source)
lemma prefixIn_disjoint_singleton_next (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : Disjoint (H.prefixIn D n) ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N)) := by rw [Finset.disjoint_singleton_right] exact nodesAt_not_mem_prefixIn H D hn -
measurable_extendTianPrefixlemma — Prefix extension is measurable.hypothesesconclusionMeasurable (extendTianPrefix (Ω := Ω) H D hn)Proof (Lean source)
@[fun_prop] lemma measurable_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : Measurable (extendTianPrefix (Ω := Ω) H D hn) := by unfold extendTianPrefix exact (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hn).symm).measurable.comp (measurable_valuesUnionMk (Ω := swigΩ Ω)) -
valuesUnionEquiv_extendTianPrefixlemma — The successor-prefix extension is inverse to the union-equivalence view of the successor prefix.hypothesesN :sharedType u_1N → Type u_2H :n :ℕhn :n < D.cardconclusionvaluesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hn)) (extendTianPrefix (Ω := Ω) H D hn p))= pProof (Lean source)
lemma valuesUnionEquiv_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) (p : ValuesOn (H.prefixIn D n) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) : valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hn)) (extendTianPrefix (Ω := Ω) H D hn p)) = p := by unfold extendTianPrefix exact valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk (prefixIn_disjoint_singleton_next H D hn) (prefixIn_succ H D hn) p -
jointRef_extendTianPrefixlemma — The successor prefix extension carries the product of the old-prefix reference and the next singleton reference to the successor-prefix reference.hypothesesN :sharedType u_1N → Type u_2H :ref :k :ℕhk :k < D.cardProof (Lean source)
lemma jointRef_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) {k : ℕ} (hk : k < D.card) : ((jointRef ref (H.prefixIn D k)).prod (jointRef ref ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)))).map (extendTianPrefix (Ω := Ω) H D hk) = jointRef ref (H.prefixIn D (k + 1)) := by classical let v : SWIGNode N := (H.nodesAt D ⟨k, hk⟩).val let A : Finset (SWIGNode N) := H.prefixIn D k let B : Finset (SWIGNode N) := ({v} : Finset (SWIGNode N)) let hDisj : Disjoint A B := by simpa [A, B, v] using prefixIn_disjoint_singleton_next H D hk have hunion : ((jointRef ref A).prod (jointRef ref B)).map ((valuesUnionEquiv (Ω := Ω) hDisj).symm) = jointRef ref (A ∪ B) := by have hmp := (measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ).symm (valuesUnionEquiv (Ω := Ω) hDisj) simpa [jointRef] using hmp.map_eq unfold extendTianPrefix change (((jointRef ref A).prod (jointRef ref B)).map ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hk).symm) ∘ (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk p.1 p.2))) = jointRef ref (H.prefixIn D (k + 1)) rw [← MeasureTheory.Measure.map_map] · have hinner : (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk p.1 p.2) = ((valuesUnionEquiv (Ω := Ω) hDisj).symm) := by rfl rw [hinner, hunion] rw [jointRef, map_pi_valuesEquivOfEq] rfl · exact (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hk).symm).measurable · exact measurable_valuesUnionMk (Ω := swigΩ Ω) -
jointRef_map_prefixIn_absolutelyContinuouslemma — The reference marginal of any D-prefix is absolutely continuous with respect to the corresponding product reference.hypothesesN :sharedType u_1N → Type u_2H :ref :k :ℕconclusionProof (Lean source)
lemma jointRef_map_prefixIn_absolutelyContinuous (H : SWIGGraph N) (D : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (k : ℕ) : (jointRef ref D).map (valuesProjection (H.prefixIn_subset D k)) ≪ jointRef ref (H.prefixIn D k) := by classical have hsubset : H.prefixIn D k ⊆ D := H.prefixIn_subset D k have hDisj : Disjoint (H.prefixIn D k) (D \ H.prefixIn D k) := disjoint_sdiff_self_right have hAB : H.prefixIn D k ∪ (D \ H.prefixIn D k) = D := Finset.union_sdiff_of_subset hsubset have hfun : (valuesProjection (Ω := swigΩ Ω) hsubset) = fst ∘ (valuesUnionEquiv (Ω := Ω) hDisj) ∘ (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm) := by funext ω i rfl have hmarg : (jointRef ref D).map (valuesProjection hsubset) = (jointRef ref (D \ H.prefixIn D k) univ) • jointRef ref (H.prefixIn D k) := by rw [hfun] rw [← MeasureTheory.Measure.map_map measurable_fst ((valuesUnionEquiv (Ω := Ω) hDisj).measurable.comp (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable)] rw [← MeasureTheory.Measure.map_map (valuesUnionEquiv (Ω := Ω) hDisj).measurable (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable] rw [jointRef, map_pi_valuesEquivOfEq hAB.symm (fun i : {i // i ∈ D} => ref.μ i.val)] have hsplit : (pi (fun j : {j // j ∈ H.prefixIn D k ∪ (D \ H.prefixIn D k)} => ref.μ j.val)).map (valuesUnionEquiv (Ω := Ω) hDisj) = (jointRef ref (H.prefixIn D k)).prod (jointRef ref (D \ H.prefixIn D k)) := by have hmp := measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ simpa [jointRef] using hmp.map_eq rw [hsplit, MeasureTheory.Measure.map_fst_prod] rw [hmarg] intro t ht simp [MeasureTheory.Measure.smul_apply, ht] -
measure_map_prefixIn_absolutelyContinuous_jointReflemma — Domination of a dominated law's prefix marginal by the prefix reference.hypothesesconclusionμ.map (valuesProjection (H.prefixIn_subset D k)) ≪ jointRef ref (H.prefixIn D k)Proof (Lean source)
lemma measure_map_prefixIn_absolutelyContinuous_jointRef (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) (hdom : μ ≪ jointRef ref D) (k : ℕ) : μ.map (valuesProjection (H.prefixIn_subset D k)) ≪ jointRef ref (H.prefixIn D k) := by exact ((hdom.map (measurable_valuesProjection (H.prefixIn_subset D k))).trans (jointRef_map_prefixIn_absolutelyContinuous H D ref k)) -
tianPrefixDensityProductInPrefix_eq_range_productlemma — The recursive prefix density product is the range product of its one-step factors.hypothesesN :sharedType u_1N → Type u_2H :ref :∀ (k : ℕ) (hk : k < D.card),k :ℕhk :k ≤ D.cardconclusiontianPrefixDensityProductInPrefix H D μ ref k z= ∏ i ∈ range k, tianPrefixStepDensityInPrefix H D μ ref k z iProof (Lean source)
lemma tianPrefixDensityProductInPrefix_eq_range_product (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [IsFiniteMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (k : ℕ) (hk : k ≤ D.card) (z : ValuesOn (H.prefixIn D k) (swigΩ Ω)) : tianPrefixDensityProductInPrefix H D μ ref k z = ∏ i ∈ range k, tianPrefixStepDensityInPrefix H D μ ref k z i := by induction k with | zero => simp [tianPrefixDensityProductInPrefix] | succ k ih => have hkcard : k < D.card := Nat.lt_of_succ_le hk rw [tianPrefixDensityProductInPrefix] rw [ih (le_of_succ_le hk) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z)] rw [Finset.prod_range_succ] congr 1 · refine Finset.prod_congr rfl ?_ intro i hi have hik : i < k := Finset.mem_range.mp hi have hisucc : i < k + 1 := Nat.lt_succ_of_lt hik have hicard : i < D.card := lt_of_lt_of_le hik (le_of_succ_le hk) have hproj : valuesProjection (prefixIn_mono H D (le_of_lt hik)) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z) = valuesProjection (prefixIn_mono H D (le_of_lt hisucc)) z := by funext a rfl have hnode : valuesProjection (show ({(H.nodesAt D ⟨i, hicard⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D k from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D k ⟨i, hicard⟩] exact hik) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z) = valuesProjection (show ({(H.nodesAt D ⟨i, hicard⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D (k + 1) from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨i, hicard⟩] exact hisucc) z := by funext a rfl simp [tianPrefixStepDensityInPrefix, hik, hisucc, hicard, hproj, hnode] · simp [tianPrefixStepDensityInPrefix, hkcard] -
tianPrefixDensityProductInPrefix_card_eq_tianDensityProductlemma — At the full D prefix, the recursive prefix density product is Tian's finite product over all D indices.hypothesesN :sharedType u_1N → Type u_2H :ref :∀ (k : ℕ) (hk : k < D.card),conclusiontianPrefixDensityProductInPrefix H D μ ref D.card yProof (Lean source)
lemma tianPrefixDensityProductInPrefix_card_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [IsFiniteMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (y : ValuesOn (H.prefixIn D D.card) (swigΩ Ω)) : tianPrefixDensityProductInPrefix H D μ ref D.card y = tianDensityProduct H D μ ref ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_card H D)) y) := by rw [tianPrefixDensityProductInPrefix_eq_range_product H D μ ref D.card (le_refl _) y] rw [Finset.prod_range] simp only [tianDensityProduct, tianPrefixStepDensity, tianPrefixStepDensityInPrefix, coe_valuesEquivOfEq] refine Finset.prod_congr rfl ?_ intro i _hi have hproj : valuesProjection (H.prefixIn_subset D i.val) (valuesProjection (le_of_eq (prefixIn_card H D).symm) y) = valuesProjection (prefixIn_mono H D (le_of_lt i.isLt)) y := by funext a rfl have hnode : valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) (valuesProjection (le_of_eq (prefixIn_card H D).symm) y) = valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D D.card from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D D.card i] exact i.isLt) y := by funext a rfl simp [i.isLt, hproj, hnode] -
measure_prefixIn_rnDeriv_eq_tianPrefixDensityProductInPrefixlemma — Prefix-level Radon--Nikodym chain rule for Tian's arbitrary-measure conditional density product.hypothesesN :sharedType u_1N → Type u_2H :ref :∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)∀ (k : ℕ) (hk : k < D.card),hdom :μ ≪ jointRef ref Dk :ℕ_hk :k ≤ D.cardconclusion(μ.map (valuesProjection (H.prefixIn_subset D k))).rnDeriv (jointRef ref (H.prefixIn D k))=ᵐ[jointRef ref (H.prefixIn D k)] tianPrefixDensityProductInPrefix H D μ ref kProof (Lean source)
lemma measure_prefixIn_rnDeriv_eq_tianPrefixDensityProductInPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] [StandardBorelSpace (ValuesOn D (swigΩ Ω))] [IsProbabilityMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (hdom : μ ≪ Causalean.SCM.jointRef ref D) : ∀ (k : ℕ) (_hk : k ≤ D.card), (μ.map (valuesProjection (H.prefixIn_subset D k))).rnDeriv (Causalean.SCM.jointRef ref (H.prefixIn D k)) =ᵐ[Causalean.SCM.jointRef ref (H.prefixIn D k)] tianPrefixDensityProductInPrefix H D μ ref k := by intro k induction k with | zero => intro _hk have hsub : Subsingleton (ValuesOn (H.prefixIn D 0) (swigΩ Ω)) := ⟨fun a b => funext fun i => absurd (prefixIn_zero H D ▸ i.property) (notMem_empty i.val)⟩ have heq : μ.map (valuesProjection (H.prefixIn_subset D 0)) = Causalean.SCM.jointRef ref (H.prefixIn D 0) := by refine MeasureTheory.Measure.ext fun A _ => ?_ rcases Set.eq_empty_or_nonempty A with rfl | hA · simp · obtain ⟨a, ha⟩ := hA have hAuniv : A = univ := Set.eq_univ_of_forall fun x => (hsub.elim x a) ▸ ha subst hAuniv rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection (H.prefixIn_subset D 0)) MeasurableSet.univ] simp only [Set.preimage_univ] rw [MeasureTheory.measure_univ, Causalean.SCM.jointRef, MeasureTheory.Measure.pi_univ] symm apply Finset.prod_eq_one intro i hi have : i.val ∈ (∅ : Finset (SWIGNode N)) := by simpa [prefixIn_zero H D] using i.property simp at this rw [heq] have h1 : tianPrefixDensityProductInPrefix H D μ ref 0 = (fun _ => (1 : ENNReal)) := rfl rw [h1] exact MeasureTheory.Measure.rnDeriv_self _ | succ k ih => intro hk classical have hkc : k < D.card := Nat.lt_of_succ_le hk have hkprev : k ≤ D.card := Nat.le_of_succ_le hk let node : SWIGNode N := (H.nodesAt D ⟨k, hkc⟩).val let A : Finset (SWIGNode N) := H.prefixIn D k let B : Finset (SWIGNode N) := ({node} : Finset (SWIGNode N)) let νk : Measure (ValuesOn A (swigΩ Ω)) := Causalean.SCM.jointRef ref A let ρ : Measure (ValuesOn B (swigΩ Ω)) := Causalean.SCM.jointRef ref B let prefixMap : ValuesOn D (swigΩ Ω) → ValuesOn A (swigΩ Ω) := valuesProjection (H.prefixIn_subset D k) let nodeMap : ValuesOn D (swigΩ Ω) → ValuesOn B (swigΩ Ω) := valuesProjection (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property) let succMap : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D (k + 1)) (swigΩ Ω) := valuesProjection (H.prefixIn_subset D (k + 1)) let chain : Measure (ValuesOn A (swigΩ Ω)) := μ.map prefixMap let stepK : Kernel (ValuesOn A (swigΩ Ω)) (ValuesOn B (swigΩ Ω)) := ProbabilityTheory.condDistrib nodeMap prefixMap μ let ext : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) → ValuesOn (H.prefixIn D (k + 1)) (swigΩ Ω) := extendTianPrefix (Ω := Ω) H D hkc have hcomp_ext : ext ∘ (fun x : ValuesOn D (swigΩ Ω) => (prefixMap x, nodeMap x)) = succMap := by funext x ext a by_cases hmem : a.val ∈ H.prefixIn D k · simp [ext, prefixMap, nodeMap, succMap, A, B, node, extendTianPrefix, coe_valuesEquivOfEq, valuesProjection, valuesUnionMk, hmem] · simp [ext, prefixMap, nodeMap, succMap, A, B, node, extendTianPrefix, coe_valuesEquivOfEq, valuesProjection, valuesUnionMk, hmem] have hchainSucc : μ.map succMap = (chain ⊗ₘ stepK).map ext := by have hpair : chain ⊗ₘ stepK = μ.map (fun x : ValuesOn D (swigΩ Ω) => (prefixMap x, nodeMap x)) := by dsimp [chain, stepK] exact ProbabilityTheory.compProd_map_condDistrib ((measurable_valuesProjection (Ω' := swigΩ Ω) (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property)).aemeasurable) rw [hpair] rw [MeasureTheory.Measure.map_map] · rw [hcomp_ext] · exact measurable_extendTianPrefix (Ω := Ω) H D hkc · exact (measurable_valuesProjection (Ω' := swigΩ Ω) (H.prefixIn_subset D k)).prod (measurable_valuesProjection (Ω' := swigΩ Ω) (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property)) have hrefSucc : Causalean.SCM.jointRef ref (H.prefixIn D (k + 1)) = (νk.prod ρ).map ext := by dsimp [νk, ρ, A, B, node, ext] exact (jointRef_extendTianPrefix H D ref hkc).symm have hext_emb : MeasurableEmbedding ext := by dsimp [ext, A, B, node] unfold extendTianPrefix refine (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hkc).symm).measurableEmbedding.comp ?_ change MeasurableEmbedding (fun p : ValuesOn (H.prefixIn D k) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk p.1 p.2) have hfun : (fun p : ValuesOn (H.prefixIn D k) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk p.1 p.2) = ((valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hkc)).symm) := by rfl rw [hfun] exact ((valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hkc)).symm.measurableEmbedding) have hcore : (chain ⊗ₘ stepK).rnDeriv (νk.prod ρ) =ᵐ[νk.prod ρ] fun p => tianPrefixDensityProductInPrefix H D μ ref k p.1 * (stepK p.1).rnDeriv ρ p.2 := by have hchain_ac : chain ≪ νk := by dsimp [chain, νk, prefixMap, A] exact measure_map_prefixIn_absolutelyContinuous_jointRef H D μ ref hdom k have hsucc_ac : μ.map succMap ≪ Causalean.SCM.jointRef ref (H.prefixIn D (k + 1)) := by dsimp [succMap] exact measure_map_prefixIn_absolutelyContinuous_jointRef H D μ ref hdom (k + 1) have hjoint_map : (chain ⊗ₘ stepK).map ext ≪ (νk.prod ρ).map ext := by simpa [hchainSucc, hrefSucc] using hsucc_ac have hjoint : chain ⊗ₘ stepK ≪ νk.prod ρ := absolutelyContinuous_of_map_measurableEmbedding hext_emb hjoint_map -- In this finite/discrete setting `ρ` is finite, so `Kernel.const _ ρ` is a -- finite kernel and fibre domination follows from joint domination. have hfiber : ∀ᵐ a ∂chain, stepK a ≪ ρ := by have hjoint_const : chain ⊗ₘ stepK ≪ νk ⊗ₘ const _ ρ := by rwa [MeasureTheory.Measure.compProd_const] filter_upwards [hjoint_const.kernel_of_compProd] with a ha simpa [ProbabilityTheory.Kernel.const_apply] using ha have hfiber_meas : AEMeasurable (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => (stepK p.1).rnDeriv ρ p.2) (νk.prod ρ) := aemeasurable_fiber_rnDeriv_of_finite (νk.prod ρ) ρ stepK exact rnDeriv_compProd_prod_sigmaFinite chain νk ρ stepK (tianPrefixDensityProductInPrefix H D μ ref k) hchain_ac hfiber hfiber_meas (ih hkprev) rw [hchainSucc, hrefSucc, EventuallyEq, hext_emb.ae_map_iff] filter_upwards [hext_emb.rnDeriv_map (chain ⊗ₘ stepK) (νk.prod ρ), hcore] with p hmap hp rw [hmap, hp] dsimp [ext, stepK, ρ, B, node] have hpair := valuesUnionEquiv_extendTianPrefix H D hkc p have hproj_ext : valuesProjection (prefixIn_mono H D (Nat.le_succ k)) (extendTianPrefix (Ω := Ω) H D hkc p) = p.1 := by funext i have hi := congrArg (fun q => q.1 i) hpair simpa [valuesUnionEquiv, valuesProjection, coe_valuesEquivOfEq] using hi have hnode_ext : valuesProjection (show ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D (k + 1) from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨k, hkc⟩] exact Nat.lt_succ_self k) (extendTianPrefix (Ω := Ω) H D hkc p) = p.2 := by funext i have hi := congrArg (fun q => q.2 i) hpair simpa [valuesUnionEquiv, valuesProjection, coe_valuesEquivOfEq] using hi rw [tianPrefixDensityProductInPrefix] simp [hkc, hproj_ext, hnode_ext, A, B, node, prefixMap, nodeMap] -
rnDeriv_eq_tianDensityProducttheorem — The density of any dominated finite law on a finite coordinate set factors as the product of its one-coordinate conditional densities along the chosen topological order. The conditional density at each coordinate is computed from Mathlib's regular conditional distribution given the preceding prefix.hypothesesN :sharedType u_1N → Type u_2H :ref :∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)∀ (k : ℕ) (hk : k < D.card),hdom :μ ≪ jointRef ref Dconclusionμ.rnDeriv (jointRef ref D)=ᵐ[jointRef ref D] tianDensityProduct H D μ refProof (Lean source)
theorem rnDeriv_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] [StandardBorelSpace (ValuesOn D (swigΩ Ω))] [IsProbabilityMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (hdom : μ ≪ jointRef ref D) : μ.rnDeriv (jointRef ref D) =ᵐ[jointRef ref D] tianDensityProduct H D μ ref := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_card H D) with he have hf : MeasurableEmbedding (e : ValuesOn (H.prefixIn D D.card) (swigΩ Ω) → ValuesOn D (swigΩ Ω)) := e.measurableEmbedding have hμe : (μ.map e.symm).map e = μ := by rw [MeasureTheory.Measure.map_map e.measurable e.symm.measurable] have hcomp : (e : ValuesOn (H.prefixIn D D.card) (swigΩ Ω) → ValuesOn D (swigΩ Ω)) ∘ e.symm = id := by funext x exact e.right_inv x rw [hcomp, MeasureTheory.Measure.map_id] have href : (jointRef ref (H.prefixIn D D.card)).map e = jointRef ref D := by rw [jointRef, jointRef, map_pi_valuesEquivOfEq] have hprefixMap : valuesProjection (H.prefixIn_subset D D.card) = (e.symm : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D D.card) (swigΩ Ω)) := by funext x i rfl have hprefix : (μ.map e.symm).rnDeriv (jointRef ref (H.prefixIn D D.card)) =ᵐ[jointRef ref (H.prefixIn D D.card)] tianPrefixDensityProductInPrefix H D μ ref D.card := by simpa [hprefixMap] using (measure_prefixIn_rnDeriv_eq_tianPrefixDensityProductInPrefix H D μ ref hdom D.card (le_refl _)) have hmap : μ.rnDeriv (jointRef ref D) =ᵐ[jointRef ref D] fun x => ((μ.map e.symm).rnDeriv (jointRef ref (H.prefixIn D D.card))) (e.symm x) := by rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hf.rnDeriv_map (μ.map e.symm) (jointRef ref (H.prefixIn D D.card))] with y hy simpa [hμe] using hy refine hmap.trans ?_ rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hprefix] with y hy have hleft : e.symm (e y) = y := e.left_inv y rw [hleft, hy] simpa using tianPrefixDensityProductInPrefix_card_eq_tianDensityProduct H D μ ref y -
doObsKernelAncestralMarginal_globalMarkovOntheorem — The do-law ancestral marginal is globally Markov with respect to the pure ancestral graph G_X[D]. This is the SCM-to-measure bridge for T1; it does not assert that D is an ancestrally closed SCM support.hypothesesN :sharedType u_1N → Type u_2∀ n, StandardBorelSpace (swigΩ Ω n)∀ n, Nonempty (swigΩ Ω n)M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedStandardBorelSpace (M.fixSet X hObs hFix).RandomValuesStandardBorelSpace (M.fixSet X hObs hFix).ObservedValues∀ s : (M.fixSet X hObs hFix).FixedValues,IsFiniteMeasure ((M.fixSet X hObs hFix).jointKernel s)∀ s : (M.fixSet X hObs hFix).FixedValues,IsFiniteMeasure ((M.fixSet X hObs hFix).obsKernel s)s :(M.fixSet X hObs hFix).FixedValuesIsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y s)conclusionA :fixAncestralSet M X hObs hFix YD :fixObservedAncestralSet M X hObs hFix YH :(M.fixSet X hObs hFix).toSWIGGraph.induce AKernelGlobalMarkovOn H D (doObsKernelAncestralMarginal M X hObs hFix Y s)Proof (Lean source)
theorem doObsKernelAncestralMarginal_globalMarkovOn [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω 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)) [StandardBorelSpace (M.fixSet X hObs hFix).RandomValues] [StandardBorelSpace (M.fixSet X hObs hFix).ObservedValues] [∀ s : (M.fixSet X hObs hFix).FixedValues, IsFiniteMeasure ((M.fixSet X hObs hFix).jointKernel s)] [∀ s : (M.fixSet X hObs hFix).FixedValues, IsFiniteMeasure ((M.fixSet X hObs hFix).obsKernel s)] (s : (M.fixSet X hObs hFix).FixedValues) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y s)] : let A := fixAncestralSet M X hObs hFix Y let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce A KernelGlobalMarkovOn H D (doObsKernelAncestralMarginal M X hObs hFix Y s) := by classical let M' := M.fixSet X hObs hFix let A := fixAncestralSet M X hObs hFix Y let D := fixObservedAncestralSet M X hObs hFix Y change KernelGlobalMarkovOn (M'.toSWIGGraph.induce A) D ((doObsKernelAncestralMarginal M X hObs hFix Y) s) dsimp [KernelGlobalMarkovOn] intro X' Y' Z' hX hY hZ hXY hXZ hYZ hdSep have hD_obs : D ⊆ M'.observed := by intro v hv exact (Finset.mem_inter.mp hv).2 have hX_obs : X' ⊆ M'.observed := fun v hv => hD_obs (hX hv) have hY_obs : Y' ⊆ M'.observed := fun v hv => hD_obs (hY hv) have hZ_obs : Z' ⊆ M'.observed := fun v hv => hD_obs (hZ hv) have hA_closed : M'.dag.ancestralSet A = A := by simpa [A, fixAncestralSet, M'] using (M'.dag.ancestralSet_idem Y) have hdSep_fixed : M'.dag.dSep X' Y' (Z' ∪ M'.fixed) := by simpa [A, D, M'] using (M'.toSWIGGraph.dSep_union_fixed_of_induce_dSep A X' Y' Z' hX hY hZ (by simp [hA_closed]) hdSep) have hCI_obs : SCM.ObsCondIndep M' X' Y' Z' hX_obs hY_obs hZ_obs (M'.obsKernel s) := SCM.globalMarkov_with_fixed M' X' Y' Z' M'.fixed hX_obs hY_obs hZ_obs (by intro v hv; exact hv) hdSep_fixed s unfold KernelObsCondIndepOn unfold SCM.ObsCondIndep at hCI_obs have hCI_pre : CondIndepFun (comap (valuesProjection hZ ∘ valuesProjection hD_obs) inferInstance) (comap_le ((measurable_valuesProjection hZ).comp (measurable_valuesProjection hD_obs))) (valuesProjection hX ∘ valuesProjection hD_obs) (valuesProjection hY ∘ valuesProjection hD_obs) (M'.obsKernel s) := by convert hCI_obs using 2 <;> rfl have hCI_map : CondIndepFun (comap (valuesProjection hZ) inferInstance) (comap_valuesProjection_le hZ) (valuesProjection hX) (valuesProjection hY) ((M'.obsKernel s).map (valuesProjection hD_obs)) := condIndepFun_of_map (φ := valuesProjection hD_obs) (measurable_valuesProjection hD_obs) (measurable_valuesProjection hX) (measurable_valuesProjection hY) (measurable_valuesProjection hZ) hCI_pre convert hCI_map using 2 rw [doObsKernelAncestralMarginal, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection hD_obs)] -
nodesAt_toSWIGGraph_observed_eq_observedAtlemma — The graph-level topological enumeration agrees definitionally with the SCM-level observed-node enumeration.hypothesesconclusionM.toSWIGGraph.nodesAt M.observed i = M.observedAt iProof (Lean source)
lemma nodesAt_toSWIGGraph_observed_eq_observedAt (M : SCM N Ω) (i : Fin M.observed.card) : M.toSWIGGraph.nodesAt M.observed i = M.observedAt i := by rfl -
tian_full_cComponent_density_recovery_corelemma — Core Tian c-factor recovery for a full observational c-component.hypothesesN :sharedType u_1N → Type u_2∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩX :Finset NhStd :M.isStandardhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedref :href :sDo :(M.fixSet X hObs hFix).FixedValueshS :S ∈ fixTruncCComponentSet M X hObs hFix YhSfull :S ∈ M.toSWIGGraph.cComponentSetIsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hpos :∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')hYX :∀ D ∈ X, SWIGNode.random D ∉ Yextend :hExtend :∀ xD,valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)= xDhExtendX :∀ xD (D : N) (hD : D ∈ X),extend xD ⟨SWIGNode.random D, hObs D hD⟩= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩conclusionD :fixObservedAncestralSet M X hObs hFix YH :(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S=ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD)Proof (Lean source)
lemma tian_full_cComponent_density_recovery_core [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (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) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (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Ω Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by exact tian_full_cComponent_density_recovery_core_direct M X hStd hObs hFix Y ref href sDo S hS hSfull hpos hYX extend hExtend hExtendX -
doAncestralDistrictDensity_recovered_from_obs_core_selflemma — Finite same-district recovery: the do-law's S-district density factor equals S's observational c-component density factor (after extension), for a district S that is already a full observational c-component.hypothesesN :sharedType u_1N → Type u_2∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩX :Finset NhStd :M.isStandardhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedref :href :sDo :(M.fixSet X hObs hFix).FixedValueshS :S ∈ fixTruncCComponentSet M X hObs hFix YhSfull :S ∈ M.toSWIGGraph.cComponentSetIsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hpos :∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')hYX :∀ D ∈ X, SWIGNode.random D ∉ Yextend :hExtend :∀ xD,valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)= xDhExtendX :∀ xD (D : N) (hD : D ∈ X),extend xD ⟨SWIGNode.random D, hObs D hD⟩= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩conclusionD :fixObservedAncestralSet M X hObs hFix YH :(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S=ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD)Proof (Lean source)
lemma doAncestralDistrictDensity_recovered_from_obs_core_self [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (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) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (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Ω Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by exact tian_full_cComponent_density_recovery_core M X hStd hObs hFix Y ref href sDo S hS hSfull hpos hYX extend hExtend hExtendX -
doAncestralDistrictDensity_recovered_from_obs_corelemma — T2 density-recovery core.hypothesesN :sharedType u_1N → Type u_2∀ n, Nonempty (Ω n)∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩX :Finset NhStd :M.isStandardhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedref :href :sDo :(M.fixSet X hObs hFix).FixedValueshS :S ∈ fixTruncCComponentSet M X hObs hFix YhReach :cFactorReachable M.toSWIGGraph C ShCmem :C ∈ M.toSWIGGraph.cComponentSetIsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))∀ (k : ℕ) (hk : k < M.observed.card),∀ k : ℕ,hpos :∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')hYX :∀ D ∈ X, SWIGNode.random D ∉ Yextend :hExtend :∀ xD,valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)= xDhExtendX :∀ xD (D : N) (hD : D ∈ X),extend xD ⟨SWIGNode.random D, hObs D hD⟩= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩conclusionD :fixObservedAncestralSet M X hObs hFix YH :(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S=ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) C (extend xD)Proof (Lean source)
lemma doAncestralDistrictDensity_recovered_from_obs_core [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (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) (sDo : (M.fixSet X hObs hFix).FixedValues) (S C : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hReach : cFactorReachable M.toSWIGGraph C S) (hCmem : C ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (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Ω Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) C (extend xD) := by classical rcases hReach with ⟨hSnonempty, hSsubC, hSmem⟩ have hCS : C = S := by by_contra hne rcases hSnonempty with ⟨v, hvS⟩ have hvC : v ∈ C := hSsubC hvS have hdisj := M.toSWIGGraph.cComponentSet_pairwise_disjoint hCmem hSmem hne exact (Finset.disjoint_left.mp hdisj) hvC hvS subst C exact doAncestralDistrictDensity_recovered_from_obs_core_self M X hStd hObs hFix Y ref href sDo S hS hSmem hpos hYX extend hExtend hExtendX
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. ★ 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. 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 admit a successful no-fixing ID certificate on G, then the two models' post-intervention outcome kernels for Y are heterogeneously equal.
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 an intervention target set X, an outcome node set Y, a SWIG graph G, and a reference-measure family ref that is faithful to the graph. Then whenever the no-fixing ID certificate succeeds for X, Y on G, the interventional query mapping X to Y is identifiable within the class of models dominated by ref with discretely positive observational kernels: any two such models that share graph G and observational kernel agree on the query.
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 :
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) :
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 — Two standard models with the same SWIG graph have the same canonical fixed-value assignment 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₂
IDAlgorithmRec 8 core · 7 supporting id_sound (in GraphicalThms.IDAlgorithm) proves soundness for the *no-fixing* certificate idSucceeds, where every post-intervention ancestral district is already a full c-component of the original graph. ★ doAncestralDistrictDensity_recovered_from_obs_rec★ doKernelY_eq_cfactor_decomposition_rec★ id_sound_rec★ id_sound_rec_discrete
Soundness of the full (recursive) Tian–Shpitser ID algorithm
id_sound (in GraphicalThms.IDAlgorithm) proves soundness for the no-fixing
certificate idSucceeds, where every post-intervention ancestral district is
already a full c-component of the original graph. This file lifts soundness to
the full recursive certificate idSucceedsRec: each district need only be
recursively reachable (CFactorReachableRec) from its containing district via
Tian's IDENTIFY fixing sequence.
Since idSucceeds → idSucceedsRec (idSucceeds_toRec), id_sound_rec subsumes
id_sound, and id_sound_rec_discrete subsumes the frozen id_sound_discrete.
Proof architecture for id_sound_rec
The assembly mirrors id_sound: the do-law Y-marginal factorizes over the
c-components of the post-intervention ancestral graph H, and it suffices to
show each district factor tianDistrictDensity H D (do-law marginal) ref S is a
functional of the observational kernel. The ONLY change from id_sound is the
per-district recovery step (id_sound uses
doAncestralDistrictDensity_recovered_from_obs, which needs S to be a full
c-component). The recursive version is:
* M4a (per-step Lemma 12). For W ancestrally closed inside a district T,
the W-marginal of the Q[T]-density equals the Q[W]-density. At the
measure level this is q_factor_marginal_fixing applied inside
M_T := M.fixSet (observed ∖ T); transport to densities via the
DoLawMarginal / FiniteReference bridges used by id_sound's base recovery.
* M4b (recursive recovery). By induction on the CFactorReachableRec C S
derivation: the base case (inducedAncestral G C S = S) is a marginalization
of the full-district obs-side factor cComponentDensityFactor ref C (whose
recovery is the existing doAncestralDistrictDensity_recovered_from_obs at the
containing full c-component C); each step composes one M4a fixing step. The
recovered value is a functional of obsKernel, so equal observational kernels
give equal district factors — exactly as in id_sound's
cComponentDensityFactor_heq_of_obsKernel_heq step.
* M4c (assembly). Feed the recursive per-district equality into the same
Finset.prod induction as id_sound.
Everything downstream of the per-district recovery is verbatim id_sound.
def marginalizeOnObserved reviewed
⚑ flagged
Causalean.SCM.ID
For a population of variables with finite value spaces, an observed-node set, a node subset to be marginalized contained in that observed set, and a nonnegative mass function on observed assignments, the observed-set marginalization functional assigns to each observed assignment the sum of that mass function over all replacements on the specified subset.
def extractDistrictObserved reviewed
⚑ flagged
Causalean.SCM.ID
For a population of variables with finite value spaces, an observed-node set, a SWIG graph, an ancestral node set, a target district contained in the observed set, and a nonnegative mass function on observed assignments, the observed-set district-extraction functional is the product of the successive marginal-ratio factors indexed by the graph order of nodes in the target district.
Definition (Lean source)
parameters
given by
fun x
=> ∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (G'.nodesAt A i).val ∈ C'), marginalizeOnObserved O (A \ G'.prefixIn A (i.val + 1)) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) q x / marginalizeOnObserved O (A \ G'.prefixIn A i.val) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) q x
def identifyMassRecObserved reviewed
⚑ flagged
Causalean.SCM.ID
For a population of variables with finite value spaces, an observed-node set, a SWIG graph, a containing node set, a target district contained in the observed set, and a nonnegative mass function on observed assignments, the recursive observed-set mass identification functional first [forms the induced ancestral set and records that it is observed](step:1,step:2), then returns the appropriate marginal, original mass, or recursively extracted district mass according to its ancestral-set cases.
Definition (Lean source)
parameters
given by
| T, C, hT, q
=> let A := inducedAncestral G T C let hA : A ⊆ O := fun _ hv => hT (inducedAncestral_subset_left G T C hv) if _hAC : A = C then marginalizeOnObserved O (T \ C) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) q else if _hAT : A = T then q else let C₁ := containingCComponent (G.induce A) C let hC₁ : C₁ ⊆ O := fun _ hv => hT (inducedAncestral_subset_left G T C (containingCComponent_induce_subset G A C hv)) identifyMassRecObserved O G C₁ C hC₁ (extractDistrictObserved O (G.induce A) A C₁ hA (marginalizeOnObserved O (T \ A) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) q)) termination_by T _ _ _ => T.card decreasing_by classical have hAsubT : A ⊆ T := inducedAncestral_subset_left G T C have hAssubT : A ⊂ T := Finset.ssubset_iff_subset_ne.mpr ⟨hAsubT, _hAT⟩ have hC₁subA : C₁ ⊆ A := containingCComponent_induce_subset G A C exact Nat.lt_of_le_of_lt (Finset.card_le_card hC₁subA) (Finset.card_lt_card hAssubT)
def recoveredFactorRec reviewed
⚑ flagged
Causalean.SCM.ID
For a finite population of variables with measurable value spaces, a structural causal model, reference measures, a fixed-value assignment, a containing c-component, and a target district, assuming finite value spaces, finite observational-kernel slices, standard-Borel and nonempty one-node observed value spaces, and countably generated prefix value spaces, the recursively recovered factor assigns to every observed-data realization the recursive identification mass for the target divided by its reference atom, and is zero when either named node set is not observed.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
ref :
s :
M.FixedValues
hfin :
∀ n, Fintype (Ω n)
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
given by
fun x
=> if hC : C ⊆ M.observed then if hSobs : S ⊆ M.observed then SCM.identifyMassRec M.observed M.toSWIGGraph C S hC (fun x' => (∏ i ∈ Finset.univ.filter (fun i : Fin M.observed.card => (M.observedAt i).val ∈ C), M.obsStepCondDensity ref s i x') * jointRef ref C ({valuesProjection hC x'} : Set (ValuesOn C (swigΩ Ω)))) x / jointRef ref S ({valuesProjection hSobs x} : Set (ValuesOn S (swigΩ Ω))) else 0 else 0
theorem doAncestralDistrictDensity_recovered_from_obs_rec reviewed
⚑ flagged
Causalean.SCM.ID
Recursive district-density recovery from the observational kernel. Fix a standard structural causal model M and an intervention target set X for which every targeted node is currently a random observed node and none of its fixed copies is already fixed, an output set Y, and a reference-measure family faithful to the graph. For a district S of the truncated c-component set of the post-intervention ancestral graph and a c-component C of the base graph that is recursively factor-reachable from S, assume every fixed-value assignment gives an observational kernel with everywhere-positive point masses, no intervention target's random form lies in Y, and that an extension map from ancestral assignments to full observed assignments restricts back to the identity and agrees with the intervention values sDo on the targeted coordinates. Then the district factor of S computed from the density of the do-law's ancestral marginal equals, almost everywhere, the full-graph c-component density factor of C evaluated at the extension of the ancestral assignment.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
∀ n, Nonempty (Ω n)
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
X :
Finset N
hStd :
M.isStandard
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
ref :
href :
sDo :
(M.fixSet X hObs hFix).FixedValues
hS :
S ∈ fixTruncCComponentSet M X hObs hFix Y
hReach :
CFactorReachableRec M.toSWIGGraph C S
hCmem :
C ∈ M.toSWIGGraph.cComponentSet
IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)
∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < M.observed.card),
∀ k : ℕ,
hpos :
∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')
hYX :
∀ D ∈ X, SWIGNode.random D ∉ Y
extend :
hExtend :
∀ xD,
valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)
= xD
hExtendX :
∀ xD (D : N) (hD : D ∈ X),
extend xD ⟨SWIGNode.random D, hObs D hD⟩
= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩
conclusion
D :
fixObservedAncestralSet M X hObs hFix Y
H :
(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)
tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S
=ᵐ[jointRef ref D] fun xD => recoveredFactorRec M ref (M.fixSetProj X hObs hFix sDo) C S (extend xD)
Proof (Lean source)
theorem doAncestralDistrictDensity_recovered_from_obs_rec
[∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(M : SCM N Ω) (X : Finset N)
(hStd : M.isStandard)
(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)
(sDo : (M.fixSet X hObs hFix).FixedValues)
(S C : Finset (SWIGNode N))
(hS : S ∈ fixTruncCComponentSet M X hObs hFix Y)
(hReach : CFactorReachableRec M.toSWIGGraph C S)
(hCmem : C ∈ M.toSWIGGraph.cComponentSet)
[IsFiniteMeasure
(doObsKernelAncestralMarginal M X hObs hFix Y sDo)]
[∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
StandardBorelSpace
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),
Nonempty
(ValuesOn
({(((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).nodesAt
(fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} :
Finset (SWIGNode N)) (swigΩ Ω))]
[∀ (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Ω Ω))]
(hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s'))
(hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y)
(extend :
ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) →
ValuesOn M.observed (swigΩ Ω))
(hExtend : ∀ xD, valuesProjection
(show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from
inter_subset_right) (extend xD) = xD)
(hExtendX : ∀ xD (D : N) (hD : D ∈ X),
extend xD ⟨SWIGNode.random D, hObs D hD⟩ =
sDo ⟨SWIGNode.fixed D,
mem_union_right _
(Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) :
let D := fixObservedAncestralSet M X hObs hFix Y
let H := (M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)
tianDistrictDensity H D
(doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S
=ᵐ[jointRef ref D]
fun xD =>
recoveredFactorRec M ref
(M.fixSetProj X hObs hFix sDo) C S (extend xD) := by
classical
let MX := M.fixSet X hObs hFix
let D := fixObservedAncestralSet M X hObs hFix Y
let H := MX.toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)
let sObs := M.fixSetProj X hObs hFix sDo
have hCobs : C ⊆ M.observed := by
simpa using M.toSWIGGraph.cComponentSet_subset_observed C hCmem
have hSobs : S ⊆ M.observed := fun _ hv => hCobs (hReach.target_subset hv)
have hSD : S ⊆ D := by
have hScomp : S ∈ H.cComponentSet := by
change S ∈
((M.fixSet X hObs hFix).toSWIGGraph.induce
(fixAncestralSet M X hObs hFix Y)).cComponentSet
simpa [fixTruncCComponentSet] using hS
have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S hScomp
-- `H.observed` is `fixAncestralSet … ∩ MX.observed` only after delta-unfolding
-- `SWIGGraph.induce`, whose body is `let`-structured: simp will not do it, and
-- the folded/unfolded pair is defeq only at default transparency.
exact hSHobs
have hSX : ∀ n ∈ X, SWIGNode.random n ∉ S := by
intro n hn hnS
have hnD : SWIGNode.random n ∈ D := hSD hnS
have hnA : SWIGNode.random n ∈ fixAncestralSet M X hObs hFix Y := by
simpa [D, fixObservedAncestralSet] using (Finset.mem_inter.mp hnD).1
exact hYX n hn
((random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hn).mp hnA)
filter_upwards with xD
have hproj :
valuesProjection hSobs (extend xD) =
valuesProjection hSD xD := by
ext v
have h := congrFun (hExtend xD) ⟨v.val, hSD v.property⟩
simpa [valuesProjection] using h
have hdo :
MX.qLocalMass sDo S (by simpa [MX, SCM.fixSet_observed] using hSobs)
(extend xD) =
M.qLocalMass sObs S hSobs (extend xD) := by
simpa [MX, sObs] using
qLocalMass_fixSet_invariant M X hObs hFix sDo S hSobs hSX
(extend xD) (fun D hD => hExtendX xD D hD)
have hseed :
(fun x' =>
(∏ i ∈ Finset.univ.filter
(fun i : Fin M.observed.card => (M.observedAt i).val ∈ C),
M.obsStepCondDensity ref sObs i x') *
jointRef ref C
({valuesProjection hCobs x'} : Set (ValuesOn C (swigΩ Ω)))) =
M.qLocalMass sObs C hCobs := by
funext x'
have hprod :
(∏ i ∈ Finset.univ.filter
(fun i : Fin M.observed.card => (M.observedAt i).val ∈ C),
M.obsStepCondDensity ref sObs i x') =
M.cComponentDensityFactor ref sObs C x' := by
unfold cComponentDensityFactor
refine Finset.prod_congr ?_ ?_
· ext i
simp only [mem_filter, Finset.mem_univ, true_and]
exact
(mem_cComponent_iff_cComponentOf_eq M.toSWIGGraph
(M.observedAt i).property hCmem)
· intro i _hi
rfl
let atom :=
jointRef ref C ({valuesProjection hCobs x'} :
Set (ValuesOn C (swigΩ Ω)))
have hatom0 : atom ≠ 0 := by
exact jointRef_singleton_ne_zero ref href C (valuesProjection hCobs x')
have hatomtop : atom ≠ (⊤ : ENNReal) := by
exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref C)
({valuesProjection hCobs x'} : Set (ValuesOn C (swigΩ Ω))))
have hmech :
M.mechCFactor ref C hCobs sObs x' =
M.qLocalMass sObs C hCobs x' / atom := by
simpa [atom] using
mechCFactor_eq_qLocalMass_div_jointRef M ref sObs C hCobs href
(standard_fixed_random_edgeless M hStd) x'
calc
(∏ i ∈ Finset.univ.filter
(fun i : Fin M.observed.card => (M.observedAt i).val ∈ C),
M.obsStepCondDensity ref sObs i x') *
jointRef ref C
({valuesProjection hCobs x'} : Set (ValuesOn C (swigΩ Ω)))
= M.cComponentDensityFactor ref sObs C x' * atom := by
rw [hprod]
_ = M.mechCFactor ref C hCobs sObs x' * atom := by
rw [cComponentDensityFactor_eq_mechCFactor
M ref sObs hStd C hCobs hCmem href (hpos sObs) x']
_ = (M.qLocalMass sObs C hCobs x' / atom) * atom := by
rw [hmech]
_ = M.qLocalMass sObs C hCobs x' := by
exact ENNReal.div_mul_cancel hatom0 hatomtop
have hidentify :
SCM.identifyMassRec M.observed M.toSWIGGraph C S hCobs
(fun x' =>
(∏ i ∈ Finset.univ.filter
(fun i : Fin M.observed.card => (M.observedAt i).val ∈ C),
M.obsStepCondDensity ref sObs i x') *
jointRef ref C
({valuesProjection hCobs x'} : Set (ValuesOn C (swigΩ Ω))))
(extend xD) =
M.qLocalMass sObs S hSobs (extend xD) := by
rw [hseed]
exact identifyMassRec_qLocalMass M sObs (hpos sObs) C S hCobs hReach (extend xD)
have hkey :=
tianDistrictDensity_eq_qLocalMass_div_jointRef_district
M X hObs hFix Y ref href sDo hpos hYX S hS extend hExtend xD
calc
tianDistrictDensity H D
(doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD
=
MX.qLocalMass sDo S
(show S ⊆ MX.observed from by
simpa [MX, SCM.fixSet_observed] using hSobs)
(extend xD) /
jointRef ref S
({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by
simpa [H, D, MX] using hkey
_ =
M.qLocalMass sObs S hSobs (extend xD) /
jointRef ref S
({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by
rw [hdo]
_ =
M.qLocalMass sObs S hSobs (extend xD) /
jointRef ref S
({valuesProjection hSobs (extend xD)} : Set (ValuesOn S (swigΩ Ω))) := by
rw [hproj]
_ =
recoveredFactorRec M ref sObs C S (extend xD) := by
unfold recoveredFactorRec
rw [dif_pos hCobs, dif_pos hSobs, hidentify]
theorem doKernelY_eq_cfactor_decomposition_rec reviewed
⚑ flagged
Causalean.SCM.ID
Recursive valid-branch kernel equality. 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 admit a successful full recursive ID certificate on G, then the two models' post-intervention outcome kernels for Y are heterogeneously equal. This is the same transport as doKernelY_eq_cfactor_decomposition, with the recursive Y-marginal wrapper in place of the no-fixing one.
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 :
idSucceedsRec 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_rec
[∀ 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 : idSucceedsRec 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_rec X Y G ref href _hID M₁ M₂ _hsg₁ _hsg₂
_hdom₁ _hdom₂ hpos₁ hpos₂ _hobs hvalid₁ hvalid₂)
theorem id_sound_rec reviewed
⚑ flagged
Causalean.SCM.ID
Soundness of the full recursive ID algorithm for finite discrete-positive models. Fix an intervention target set X, an outcome node set Y, a SWIG graph G, and a reference-measure family ref that is faithful to the graph. Then whenever the full recursive Tian–Shpitser IDENTIFY certificate succeeds for X, Y on G, the interventional query mapping X to Y is identifiable within the class of models dominated by ref with discretely positive observational kernels: any two such models that share graph G and observational kernel agree on the query. This generalizes id_sound from the no-fixing fragment to the full Tian-Shpitser IDENTIFY recursion; see the module docstring for the proof architecture.
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 :
idSucceedsRec 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_rec [∀ 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) :
idSucceedsRec 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 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_rec
(Ω := Ω) 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₂]
theorem id_sound_rec_discrete reviewed
⚑ flagged
Causalean.SCM.ID
Discrete soundness of the full recursive ID algorithm (on-contract). For an intervention target set X, an outcome node set Y, and a SWIG graph G, if the full recursive Tian–Shpitser IDENTIFY certificate succeeds for X, Y on G, then the interventional query mapping X to Y is identifiable within the standard discrete positive model class. Obtained from id_sound_rec at the counting reference by collapsing DominatedObs · countingRef to StandardDiscretePositive, exactly as id_sound_discrete is obtained from id_sound. This subsumes id_sound_discrete (via idSucceeds_toRec).
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 :
h :
idSucceedsRec X Y G
conclusion
Proof (Lean source)
theorem id_sound_rec_discrete
[∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)]
[∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)]
(X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N)
(h : idSucceedsRec X Y G) :
IdentifiableUnder G (fun _ => True) StandardDiscretePositive
(interventionalQuery (Ω := Ω) X Y) := by
have hdom :=
id_sound_rec X Y G (countingRef (Ω := Ω)) referenceFaithful_countingRef 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
7 supporting declarations (lemmas, instances)
-
marginalizeOnObserved_eq_marginalizeOnlemmahypothesesconclusionmarginalizeOnObserved M.observed W hW q = SCM.marginalizeOn M.observed W hW qProof (Lean source)
@[simp] lemma marginalizeOnObserved_eq_marginalizeOn [∀ n, Fintype (Ω n)] (M : SCM N Ω) (W : Finset (SWIGNode N)) (hW : W ⊆ M.observed) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal) : marginalizeOnObserved M.observed W hW q = SCM.marginalizeOn M.observed W hW q := by rfl -
extractDistrictObserved_eq_extractDistrictlemmahypothesesconclusionextractDistrictObserved M.observed G' A C' hA q= SCM.extractDistrict M.observed G' A C' hA qProof (Lean source)
@[simp] lemma extractDistrictObserved_eq_extractDistrict [∀ n, Fintype (Ω n)] (M : SCM N Ω) (G' : SWIGGraph N) (A C' : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal) : extractDistrictObserved M.observed G' A C' hA q = SCM.extractDistrict M.observed G' A C' hA q := by funext x unfold extractDistrictObserved SCM.extractDistrict rfl -
identifyMassRecObserved_eq_identifyMassReclemmahypothesesconclusionidentifyMassRecObserved M.observed G T C hT q = SCM.identifyMassRec M.observed G T C hT qProof (Lean source)
lemma identifyMassRecObserved_eq_identifyMassRec [∀ n, Fintype (Ω n)] (M : SCM N Ω) (G : SWIGGraph N) (T C : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal) : identifyMassRecObserved M.observed G T C hT q = SCM.identifyMassRec M.observed G T C hT q := by classical let P : ℕ → Prop := fun n => ∀ (T C : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal), T.card = n → identifyMassRecObserved M.observed G T C hT q = SCM.identifyMassRec M.observed G T C hT q have hP : ∀ n, P n := by intro n induction n using Nat.strong_induction_on with | h n ih => intro T C hT q hcard rw [identifyMassRecObserved, SCM.identifyMassRec] by_cases hAC : inducedAncestral G T C = C · simp [hAC] · by_cases hAT : inducedAncestral G T C = T · simp [hAT] · simp only [hAC, hAT, marginalizeOnObserved_eq_marginalizeOn, extractDistrictObserved_eq_extractDistrict, dite_eq_ite] let A := inducedAncestral G T C let C₁ := containingCComponent (G.induce A) C have hAsubT : A ⊆ T := inducedAncestral_subset_left G T C have hAssubT : A ⊂ T := Finset.ssubset_iff_subset_ne.mpr ⟨hAsubT, hAT⟩ have hC₁subA : C₁ ⊆ A := containingCComponent_induce_subset G A C have hlt : C₁.card < n := by rw [← hcard] exact Nat.lt_of_le_of_lt (Finset.card_le_card hC₁subA) (Finset.card_lt_card hAssubT) exact ih C₁.card hlt C₁ C _ _ rfl exact hP T.card T C hT q rfl -
recoveredFactorRec_heq_of_obsKernel_heqlemma — Equal observational kernels transport the recursive recovered factor.hypothesesN :sharedType u_1N → Type u_2M₁ M₂ :SCM N Ωref :hsg :M₁.toSWIGGraph = M₂.toSWIGGraphhobs :HEq M₁.obsKernel M₂.obsKernelhfin :∀ n, Fintype (Ω n)∀ s' : M₁.FixedValues, IsFiniteMeasure (M₁.obsKernel s')∀ (k : ℕ) (hk : k < M₁.observed.card),∀ k : ℕ,∀ s' : M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s')∀ (k : ℕ) (hk : k < M₂.observed.card),∀ k : ℕ,conclusionProof (Lean source)
lemma recoveredFactorRec_heq_of_obsKernel_heq (M₁ M₂ : SCM N Ω) (ref : ReferenceMeasures Ω) (C S : Finset (SWIGNode N)) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) (hobs : HEq M₁.obsKernel M₂.obsKernel) [hfin : ∀ n, Fintype (Ω n)] [∀ s' : M₁.FixedValues, IsFiniteMeasure (M₁.obsKernel s')] [∀ (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Ω Ω))] [∀ s' : M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s')] [∀ (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Ω Ω))] : HEq (fun s => recoveredFactorRec M₁ ref s C S) (fun s => recoveredFactorRec M₂ ref s C S) := by obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg have 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₂ 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₂ } have hk : _ = _ := eq_of_heq hobs apply heq_of_eq funext s x unfold recoveredFactorRec by_cases hC : C ⊆ observed₁ · by_cases hSobs : S ⊆ observed₁ · rw [dif_pos hC, dif_pos hSobs, dif_pos hC, dif_pos hSobs] change SCM.identifyMassRec M₁'.observed M₁'.toSWIGGraph C S hC _ x / _ = SCM.identifyMassRec M₂'.observed M₂'.toSWIGGraph C S hC _ x / _ rw [← identifyMassRecObserved_eq_identifyMassRec M₁' M₁'.toSWIGGraph C S hC] rw [← identifyMassRecObserved_eq_identifyMassRec M₂' M₂'.toSWIGGraph C S hC] have hseed : (fun x' => (∏ i ∈ Finset.univ.filter (fun i : Fin observed₁.card => (M₁'.observedAt i).val ∈ C), M₁'.obsStepCondDensity ref s i x') * jointRef ref C ({valuesProjection hC x'} : Set (ValuesOn C (swigΩ Ω)))) = (fun x' => (∏ i ∈ Finset.univ.filter (fun i : Fin observed₁.card => (M₂'.observedAt i).val ∈ C), M₂'.obsStepCondDensity ref s i x') * jointRef ref C ({valuesProjection hC x'} : Set (ValuesOn C (swigΩ Ω)))) := by funext x' congr 1 apply Finset.prod_congr rfl intro i _hi unfold obsStepCondDensity obsStepCondKernel SCM.obsCondKernel SCM.obsCondPairKernel repeat' congr rw [hseed] · rw [dif_pos hC, dif_neg hSobs, dif_pos hC, dif_neg hSobs] · rw [dif_neg hC, dif_neg hC] -
doObsKernelAncestralMarginal_heq_of_obsDensity_heq_rectheorem — Recursive Tian–Shpitser density core for the observed-ancestral do-law.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 :idSucceedsRec 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_rec [∀ 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 : idSucceedsRec 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 ⟨_hX, 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 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 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) ?_ 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 : idSucceedsRec 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 : CFactorReachableRec M₁'.toSWIGGraph C S := by simpa [C] using hIDrest.2.2 S hSreach have hSne : S.Nonempty := by simp only [SWIGGraph.cComponentSet] at hS rcases Finset.mem_image.mp hS with ⟨v, hv, rfl⟩ exact ⟨v, H.mem_cComponentOf_self hv⟩ have hSobs : S ⊆ M₁'.toSWIGGraph.observed := by have hSobsH : S ⊆ H.observed := H.cComponentSet_subset_observed S hS intro v hv have hvD : v ∈ D := by simpa [H, D, fixObservedAncestralSet, SCM.fixSet_observed, SWIGGraph.induce] using hSobsH hv exact (Finset.mem_inter.mp hvD).2 have hCmem : C ∈ M₁'.toSWIGGraph.cComponentSet := by 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_rec 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_rec 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 := recoveredFactorRec_heq_of_obsKernel_heq M₁' M₂' ref C S rfl hobs have hrec_fun : (fun s' => recoveredFactorRec M₁' ref s' C S) = (fun s' => recoveredFactorRec M₂' ref s' C S) := 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 => simp | insert S I hSnot ih => have hS : 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 := hIall S (mem_insert_self S I) have hI : (fun x => ∏ T ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref T x) =ᵐ[jointRef ref D] (fun x => ∏ T ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref T x) := ih (by intro T hT exact hIall T (mem_insert_of_mem hT)) filter_upwards [hS, hI] with x hxS hxI simp [Finset.prod_insert hSnot, hxS, hxI] exact hprod H.cComponentSet hfac -
doObsKernelYMarginal_heq_of_obsDensity_heq_rectheorem — Recursive density-to-Y-marginal wrapper. The projection from the observed-ancestral marginal to the query coordinates is identical to the no-fixing proof; only the ancestral density core changes.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 :idSucceedsRec 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_rec [∀ 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 : idSucceedsRec 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 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_rec X Y G ref href _hID M₁ M₂ _hsg₁ _hsg₂ _hdom₁ _hdom₂ hpos₁ hpos₂ _hden hvalid₁ hvalid₂) -
doObsKernelYMarginal_heq_of_obsKernel_heq_rectheorem — Recursive observational-kernel wrapper. Equal observational kernels give equal observational densities, which feed the recursive density core.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 :idSucceedsRec 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_rec [∀ 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 : idSucceedsRec 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) := doObsKernelYMarginal_heq_of_obsDensity_heq_rec 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, 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, 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 with no graph side conditions
— this is the discrete identification headline the checker soundness theorem
will wrap.
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 treatment nodes X, outcome nodes Y, and a SWIG graph G, a successful idSucceeds certificate implies that the interventional query is identified from the observational distribution within the standard discrete positive model 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 :
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)
(h : idSucceeds X Y G) :
IdentifiableUnder G (fun _ => True) StandardDiscretePositive
(interventionalQuery (Ω := Ω) X Y) := by
have hdom :=
id_sound X Y G (countingRef (Ω := Ω)) referenceFaithful_countingRef 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.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.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.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.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
QFactorIdentity 6 core · 3 supporting This file proves the structural identities behind district-based identification in the Tian-Pearl style. ★ q_factor_identity★ district_id
Q-Factor Identity
This file proves the structural identities behind district-based identification
in the Tian-Pearl style. The main results are the marginal fixing helper
q_factor_marginal_fixing, Tian's conditional q_factor_identity, the
intervention-order simplification intervention_target_simp, and the full-SCM
district specialization district_id. These relate c-component factors, induced
subgraphs, and post-fixing kernels so later ID soundness proofs can reuse a
common theorem frame.
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 Q-factor marginal-fixing 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 Q-factor identity 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 Q-factor parents after intervention, the indicated induced and post-intervention conditional kernels are equal 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 Q-factor 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.qFactor 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 q_factor_identity reviewed
⚑ flagged
Causalean.SCM.ID
Proposition 2.19 (Q-factor identity / Tian's lemma). For an ancestrally-closed node set R and a c-component T of the induced subgraph on R in a structural causal model M, after intervening on a node set Wn, the structurally-defined c-factor on T equals, almost everywhere, the conditional of T given its q-factor parents extracted from that intervention. See QFactorIdentityConclusion for the precise hypothesis frame.
Formal statement
Proof (Lean source)
theorem q_factor_identity
(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 district-identification conclusion is the Q-factor identity 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 district_id reviewed
⚑ flagged
Causalean.SCM.ID
Corollary (District identification). For a structural causal model M, a c-component T of M's full graph, and an intervention set Wn, the c-factor of T equals, almost everywhere, the observational conditional obtained by intervening on Wn.
Formal statement
hypotheses
conclusion
DistrictIdConclusion M T Wn
Proof (Lean source)
theorem district_id
(M : SCM N Ω)
(T : Finset (SWIGNode N))
(Wn : Finset N) :
DistrictIdConclusion M T Wn :=
q_factor_identity M M.observed T Wn
3 supporting declarations (lemmas, instances)
-
q_factor_marginal_fixingtheorem — Marginal fixing form of Tian's Q-factor 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 (mem_insert_of_mem hD) have hYs_fixed : ∀ D ∈ Ys, SWIGNode.fixed D ∉ M₀.fixed := by intro D hD exact hY_fixed D (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 _ (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 _ (mem_insert_of_mem hD)) have hDYs_disjoint : Disjoint Dn Ys := by exact hDY_disjoint.mono_right (by intro D hD; exact 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 _ (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 _ (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, union_assoc, union_comm, Finset.union_left_comm] using hAll