SCM.Model
The structural-causal-model substrate: causal models, edge types, mechanisms, interventions, and evaluation under overrides.
SCM 16 core · 9 supporting This file defines the core measure-theoretic structural causal model object used by the single-world intervention graph framework. ★ observed_parent_index_lt★ trans
Structural causal models
This file defines the core measure-theoretic structural causal model object used by the
single-world intervention graph framework. It provides the SCM structure itself,
aliases for fixed, observed, latent, and random value assignments, the latent product
measure, canonical topological-order indexing of observed nodes, and structural equivalence
of models. The underlying value-space bookkeeping (ValuesOn, valuesProjection, and the
coordinate-restriction measurability lemmas) lives in
Causalean.Mathlib.MeasureTheory.FinsetValues.
An SCM consists of a SWIG graph, value spaces, deterministic measurable structural
functions for observed variables, edge labels, and one probability measure for each latent
root. Later evaluation and kernel files build the joint and observational laws from these
primitive ingredients.
A generalized structural causal model bundles a SWIG graph together with an edge-type assignment recording functional restrictions on each edge, the requirement that each fixed parameter and its corresponding random node share the same value space, a deterministic structural function for each observed node mapping its parents' values to its own, and an independent probability law on each latent root node.
Definition (Lean source)
For a single-world intervention graph, its random-node set is the union of its observed nodes and its unobserved latent nodes.
For a finite node population with measurable value spaces and a structural causal model, the fixed-value assignments assign one value to every fixed intervention node of the model.
For a finite node population with measurable value spaces and a structural causal model, the observed-value assignments assign one value to every observed node of the model.
For a finite node population with measurable value spaces and a structural causal model, the latent-value assignments assign one value to every unobserved latent root node of the model.
For a finite node population with measurable value spaces and a structural causal model, the unobserved-value assignments are exactly the model's latent-value assignments.
Definition (Lean source)
For a finite node population with measurable value spaces and a structural causal model, standardness holds exactly when the model has no fixed intervention nodes.
Definition (Lean source)
For a finite node population with measurable value spaces and a structural causal model, its random-node set is the union of its observed nodes and its unobserved latent nodes.
For a finite node population with measurable value spaces and a structural causal model, the random-value assignments assign one value to every observed or unobserved latent node of the model.
For a finite node population with measurable value spaces and a structural causal model, the latent product measure is the product of the model's probability laws over all unobserved latent root nodes.
For a finite node population with measurable value spaces and a structural causal model, the canonical linear order on graph nodes ranks nodes by the model graph's topological ordering.
Definition (Lean source)
For a finite node population with measurable value spaces, a structural causal model, and a valid position among its observed nodes, the observed-node enumeration returns the observed node at that position in canonical topological order.
For a finite node population with measurable value spaces, a structural causal model, and an observed node, the observed-node index is that node's position in canonical topological order.
For a structural causal model M, fix a valid position n among the observed nodes, and let p be a node such that there is an edge from p to the n-th node in the canonical observed order and p itself is observed; then the canonical index of p among the observed nodes is strictly less than n — an observed parent always precedes its child in the canonical observed topological order.
Formal statement
Proof (Lean source)
For a finite node population with measurable value spaces and two structural causal models, structural equivalence holds exactly when their single-world intervention graphs are equivalent, their edge-type labels agree on every directed edge, and their structural functions and latent-root probability laws agree.
Definition (Lean source)
Structural equivalence is transitive: if M₁ and M₂ are structurally equivalent and M₂ and M₃ are structurally equivalent, then M₁ and M₃ are structurally equivalent.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
not_unobs_of_obstheorem — An observed node cannot also be an unobserved node.hypothesesconclusionn ∉ G.unobservedProof (Lean source)
theorem not_unobs_of_obs (G : SWIGGraph N) {n : SWIGNode N} (h : n ∈ G.observed) : n ∉ G.unobserved := Finset.disjoint_left.mp G.obs_unobs_disjoint h -
not_obs_of_unobstheorem — An unobserved node cannot also be an observed node.hypothesesconclusionn ∉ G.observedProof (Lean source)
theorem not_obs_of_unobs (G : SWIGGraph N) {n : SWIGNode N} (h : n ∈ G.unobserved) : n ∉ G.observed := Finset.disjoint_right.mp G.obs_unobs_disjoint h -
not_fixed_of_obstheorem — An observed node cannot also be a fixed node.hypothesesconclusionn ∉ G.fixedProof (Lean source)
theorem not_fixed_of_obs (G : SWIGGraph N) {n : SWIGNode N} (h : n ∈ G.observed) : n ∉ G.fixed := by intro hfix obtain ⟨m, hm⟩ := G.fixed_is_fixed n hfix obtain ⟨k, hk⟩ := G.observed_is_random n h rw [hm] at hk cases hk -
instProbabilityLatentProductinstance — For a finite node population with measurable value spaces and a structural causal model, the probability-measure structure for the model's latent product measure asserts that this measure assigns total mass one to the joint space of latent-root values.parametersN :sharedType uNN → Type uΩM :SCM N Ωinstancegiven byby letI := M.isProbability_latent change IsProbabilityMeasure (pi (fun u => M.latentDist u)) infer_instance -
observedAt_observedIndextheorem — Looking up an observed node by its canonical index recovers the same node.hypothesesconclusion(M.observedAt (M.observedIndex v)).val = v.valProof (Lean source)
@[simp] theorem observedAt_observedIndex (M : SCM N Ω) (v : {v // v ∈ M.observed}) : (M.observedAt (M.observedIndex v)).val = v.val := by classical letI := M.topoLinearOrder simp [SCM.observedAt, SCM.observedIndex] -
observedIndex_observedAttheorem — Looking up the canonical index of the observed node at a position recovers that position.hypothesesconclusionM.observedIndex (M.observedAt k) = kProof (Lean source)
@[simp] theorem observedIndex_observedAt (M : SCM N Ω) (k : Fin M.observed.card) : M.observedIndex (M.observedAt k) = k := by classical letI := M.topoLinearOrder simp [SCM.observedAt, SCM.observedIndex] -
symmlemma — Structural equivalence is symmetric. -
instSetoidSCMinstance — For a finite node population with measurable value spaces, the setoid structure on structural causal models uses structural equivalence as its equivalence relation and certifies that this relation is reflexive, symmetric, and transitive.
Evaluation 4 core · 12 supporting This file defines the evaluation map that sends fixed intervention values and a latent realization to the values of all random nodes in a structural causal model. ★ ancestralFactorization
Evaluation Map
This file defines the evaluation map that sends fixed intervention values and a latent realization to the values of all random nodes in a structural causal model. It proves the measurability and ancestral factorization facts that support the joint-kernel, Markov, and do-calculus layers, using the model's stored topological order of observed nodes.
Main definitions and results
* SCM.parentMap assembles the fixed, latent, and recursive observed parent
values for one observed node.
* SCM.evalObservedAux evaluates observed nodes by strong recursion over the
stored topological order.
* SCM.evalMap evaluates all random nodes, projecting latent roots directly and
computing observed nodes through evalObservedAux.
* SCM.evalMap_observed_unfold exposes the structural-function form of
evaluation at an observed node.
* SCM.evalMap_measurable and SCM.ancestralFactorization provide the
measurability and ancestor-agreement interfaces used by the kernel and Markov
developments.
For a structural causal model, an assignment of its fixed values, a realization of its latent values, an index strictly below the number of observed nodes, values already supplied for every earlier observed index, and a parent of the observed node at that index, the parent-value assignment gives that parent's value: it reads an unobserved parent from the latent realization, a fixed parent from the fixed assignment, and any observed parent from the earlier supplied values.
Definition (Lean source)
For a structural causal model, an assignment of its fixed values, a realization of its latent values, and an observed-node index, the auxiliary observed-node evaluator assigns, for every proof that the index is valid, the value of that observed node by recursively applying its structural function to its parent values in topological order.
Definition (Lean source)
For a structural causal model, the evaluation map maps each fixed-value assignment and latent realization to the resulting assignment of all random-node values, using the recursive structural evaluation for observed nodes and the supplied latent realization for unobserved nodes.
Definition (Lean source)
Ancestral factorization (Lemma lem:scm-ancestral-factor). Fix a structural causal model M, a target node set T, two fixed-value assignments s, s', two latent assignments ℓ, ℓ', and a node v with v belonging to T and v an observed node. If s and s' agree on every fixed node that equals or is an ancestor of some node of T and ℓ and ℓ' agree on every unobserved node that equals or is an ancestor of some node of T, then the evaluation of M at v with (s, ℓ) equals the evaluation with (s', ℓ').
Formal statement
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
parentMap_unobservedlemma — The parent-value tuple reads a latent parent directly from the latent assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}huo :w.val ∈ M.unobservedconclusionparentMap M s ℓ hn prev w = ℓ ⟨w.val, huo⟩Proof (Lean source)
lemma parentMap_unobserved (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (huo : w.val ∈ M.unobserved) : parentMap M s ℓ hn prev w = ℓ ⟨w.val, huo⟩ := by unfold parentMap rw [dif_pos huo] -
parentMap_fixedlemma — The parent-value tuple reads a fixed parent directly from the fixed-value assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}hfix :w.val ∈ M.fixedconclusionparentMap M s ℓ hn prev w = s ⟨w.val, hfix⟩Proof (Lean source)
lemma parentMap_fixed (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (hfix : w.val ∈ M.fixed) : parentMap M s ℓ hn prev w = s ⟨w.val, hfix⟩ := by unfold parentMap have huo : w.val ∉ M.unobserved := by intro h obtain ⟨m, hm⟩ := M.unobserved_is_random _ h obtain ⟨k, hk⟩ := M.fixed_is_fixed _ hfix rw [hk] at hm exact absurd hm (by simp) rw [dif_neg huo, dif_pos hfix] -
parentMap_observedlemma — The parent-value tuple reads an observed parent from the previously computed observed values.hypothesesProof (Lean source)
lemma parentMap_observed (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (hobs : w.val ∈ M.observed) : parentMap M s ℓ hn prev w = (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ prev (M.observedIndex ⟨w.val, hobs⟩).val (M.observed_parent_index_lt hn (M.dag.mem_parents.mp w.property) hobs) (M.observedIndex ⟨w.val, hobs⟩).isLt := by unfold parentMap have huo : w.val ∉ M.unobserved := not_unobs_of_obs M.toSWIGGraph hobs have hfix : w.val ∉ M.fixed := not_fixed_of_obs M.toSWIGGraph hobs rw [dif_neg huo, dif_neg hfix] -
evalObservedAux_eqlemma — The auxiliary evaluator unfolds to its structural function applied to the parent tuple.hypothesesconclusionevalObservedAux M s ℓ n hn= M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMap M s ℓ hn (fun m _ hm_card => evalObservedAux M s ℓ m hm_card) w)Proof (Lean source)
lemma evalObservedAux_eq (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) (n : ℕ) (hn : n < M.observed.card) : evalObservedAux M s ℓ n hn = M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMap M s ℓ hn (fun m _ hm_card => evalObservedAux M s ℓ m hm_card) w) := by unfold evalObservedAux rw [Nat.strongRec_eq] -
evalMap_observedlemma — On an observed node, the evaluation map is the auxiliary topological-order evaluation transported to that node.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :ℓ :w :{w // w ∈ M.randomVars}hobs :w.val ∈ M.observedconclusionM.evalMap s ℓ w= (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨w.val, hobs⟩).val (M.observedIndex ⟨w.val, hobs⟩).isLtProof (Lean source)
lemma evalMap_observed (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) (w : {w // w ∈ M.randomVars}) (hobs : w.val ∈ M.observed) : M.evalMap s ℓ w = (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨w.val, hobs⟩).val (M.observedIndex ⟨w.val, hobs⟩).isLt := by unfold evalMap rw [dif_pos hobs] -
evalMap_unobservedlemma — On a latent node, the evaluation map is direct projection from the latent assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :ℓ :w :{w // w ∈ M.randomVars}huo :w.val ∈ M.unobservedconclusionM.evalMap s ℓ w = ℓ ⟨w.val, huo⟩Proof (Lean source)
lemma evalMap_unobserved (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) (w : {w // w ∈ M.randomVars}) (huo : w.val ∈ M.unobserved) : M.evalMap s ℓ w = ℓ ⟨w.val, huo⟩ := by unfold evalMap rw [dif_neg (not_obs_of_unobs M.toSWIGGraph huo)] -
evalMap_observed_unfoldlemma — At an observed node, the evaluation map unfolds to the structural function applied to fixed, latent, or recursively evaluated parent values.hypothesesconclusionM.evalMap s ℓ ⟨v.val, mem_union_left _ v.property⟩= M.structFun v (fun w : {w // w ∈ M.dag.parents v.val} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v.val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M.evalMap s ℓ ⟨w.val, mem_union_left _ hobs⟩)Proof (Lean source)
lemma evalMap_observed_unfold (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) (v : {v // v ∈ M.observed}) : M.evalMap s ℓ ⟨v.val, mem_union_left _ v.property⟩ = M.structFun v (fun w : {w // w ∈ M.dag.parents v.val} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v.val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M.evalMap s ℓ ⟨w.val, mem_union_left _ hobs⟩) := by -- Reduce to the `parentDispatch` form via a helper that takes the Subtype witness -- `hw : M.observedAt j = w` as a parameter. `subst hw` inside the helper eliminates -- the circular dependency between `v` and `M.observedIndex v`. suffices h : ∀ (j : Fin M.observed.card) (w : {v // v ∈ M.observed}) (_ : M.observedAt j = w), M.evalMap s ℓ ⟨w.val, mem_union_left _ w.property⟩ = M.structFun w (parentDispatch M s ℓ w) by have key := h (M.observedIndex ⟨v.val, v.property⟩) v (Subtype.ext (M.observedAt_observedIndex ⟨v.val, v.property⟩)) rw [key] rfl intro j w hw subst hw -- `w` eliminated. Goal mentions `M.observedAt j` only. -- `rw` cannot key on `M.evalMap s ℓ ⟨_, _⟩` here: `M.randomVars` is semireducible, so -- the membership witness (typed at `M.observed ∪ M.unobserved`) is not accepted at -- `implicit` transparency. Chain the rewrite at term level instead. refine (evalMap_observed M s ℓ ⟨(M.observedAt j).val, mem_union_left _ (M.observedAt j).property⟩ (M.observedAt j).property).trans ?_ -- Apply the cast helper: the Fin index `M.observedIndex ⟨(M.observedAt j).val, _⟩` -- reduces to `j` via `observedIndex_observedAt` (after Subtype eta), and the cast -- proof is discharged via proof irrelevance inside the helper. exact evalObservedAux_cast_eq_structFunAt M s ℓ (M.observedIndex_observedAt j) (M.observedAt_observedIndex ⟨(M.observedAt j).val, (M.observedAt j).property⟩) -
evalObservedAux_measurablelemma — At every position in a causal model's topological ordering of observed variables, the recursively evaluated observed value is measurable as a function of the model's fixed and latent inputs.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma evalObservedAux_measurable (M : SCM N Ω) : ∀ (n : ℕ) (hn : n < M.observed.card), Measurable (fun p : FixedValues M × LatentValues M => evalObservedAux M p.1 p.2 n hn) := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn have hrw : (fun p : FixedValues M × LatentValues M => evalObservedAux M p.1 p.2 n hn) = (fun p => M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMap M p.1 p.2 hn (fun m _ hm_card => evalObservedAux M p.1 p.2 m hm_card) w)) := by funext p exact evalObservedAux_eq M p.1 p.2 n hn rw [hrw] refine (M.structFun_measurable _).comp ?_ refine measurable_pi_lambda _ (fun w => ?_) by_cases huo : w.val ∈ M.unobserved · have hfun : (fun p : FixedValues M × LatentValues M => parentMap M p.1 p.2 hn (fun m _ hm_card => evalObservedAux M p.1 p.2 m hm_card) w) = (fun p => p.2 ⟨w.val, huo⟩) := by funext p exact parentMap_unobserved M p.1 p.2 hn _ w huo rw [hfun] exact (measurable_pi_apply _).comp measurable_snd · by_cases hfix : w.val ∈ M.fixed · have hfun : (fun p : FixedValues M × LatentValues M => parentMap M p.1 p.2 hn (fun m _ hm_card => evalObservedAux M p.1 p.2 m hm_card) w) = (fun p => p.1 ⟨w.val, hfix⟩) := by funext p exact parentMap_fixed M p.1 p.2 hn _ w hfix rw [hfun] exact (measurable_pi_apply _).comp measurable_fst · have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by have hcls := (M.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hcls with hfo | huo' · rcases Finset.mem_union.mp hfo with hf | ho · exact absurd hf hfix · exact ho · exact absurd huo' huo have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs have hfun : (fun p : FixedValues M × LatentValues M => parentMap M p.1 p.2 hn (fun m _ hm_card => evalObservedAux M p.1 p.2 m hm_card) w) = (fun p => (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ evalObservedAux M p.1 p.2 (M.observedIndex ⟨w.val, hobs⟩).val (M.observedIndex ⟨w.val, hobs⟩).isLt) := by funext p exact parentMap_observed M p.1 p.2 hn _ w hobs rw [hfun] exact measurable_family_cast _ (ih _ hj _) -
evalMap_measurabletheorem — The evaluation map is jointly measurable in the fixed-value assignment and latent realization.Proof (Lean source)
theorem evalMap_measurable (M : SCM N Ω) : Measurable (uncurry M.evalMap) := by refine measurable_pi_iff.mpr (fun w => ?_) by_cases hobs : w.val ∈ M.observed · have hfun : (fun p : FixedValues M × LatentValues M => uncurry M.evalMap p w) = (fun p => (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ evalObservedAux M p.1 p.2 (M.observedIndex ⟨w.val, hobs⟩).val (M.observedIndex ⟨w.val, hobs⟩).isLt) := by funext p exact evalMap_observed M p.1 p.2 w hobs rw [hfun] exact measurable_family_cast _ (evalObservedAux_measurable M _ _) · have hrand : w.val ∈ M.observed ∪ M.unobserved := by have hw := w.property change w.val ∈ M.observed ∪ M.unobserved at hw exact hw have huo : w.val ∈ M.unobserved := (Finset.mem_union.mp hrand).elim (fun ho => absurd ho hobs) id have hfun : (fun p : FixedValues M × LatentValues M => uncurry M.evalMap p w) = (fun p => p.2 ⟨w.val, huo⟩) := by funext p exact evalMap_unobserved M p.1 p.2 w huo rw [hfun] exact (measurable_pi_apply _).comp measurable_snd -
measurable_evalMap_prodtheorem — The evaluation map, read as a function of the pair (s, ℓ) rather than as a curried map, is measurable.Proof (Lean source)
@[fun_prop] theorem measurable_evalMap_prod (M : SCM N Ω) : Measurable (fun p : FixedValues M × LatentValues M => M.evalMap p.1 p.2) := M.evalMap_measurable -
measurable_evalMap_applytheorem — For each fixed assignment to the intervened variables, the evaluation map is measurable as a function of the latent realization alone.hypothesesconclusionMeasurable (M.evalMap s)Proof (Lean source)
@[fun_prop] theorem measurable_evalMap_apply (M : SCM N Ω) (s : FixedValues M) : Measurable (M.evalMap s) := M.evalMap_measurable.comp (measurable_const.prodMk measurable_id) -
evalObservedAux_agree_anclemma — An observed variable has the same recursively evaluated value under two inputs when those inputs agree on every fixed and latent cause that can affect the target variables. This expresses the local ancestral dependence of a structural causal model.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs s' :ℓ ℓ' :hs :∀ (d : SWIGNode N) (hd : d ∈ M.fixed)if(∃ v ∈ T, d = v ∨ M.dag.isAncestor d v)thens ⟨d, hd⟩ = s' ⟨d, hd⟩hℓ :∀ (u : SWIGNode N) (hu : u ∈ M.unobserved)if(∃ v ∈ T, u = v ∨ M.dag.isAncestor u v)thenℓ ⟨u, hu⟩ = ℓ' ⟨u, hu⟩n :ℕhn :n < M.observed.card_ :∃ v ∈ T, (M.observedAt ⟨n, hn⟩).val = v ∨ M.dag.isAncestor (M.observedAt ⟨n, hn⟩).val vconclusionevalObservedAux M s ℓ n hn = evalObservedAux M s' ℓ' n hnProof (Lean source)
lemma evalObservedAux_agree_anc (M : SCM N Ω) (T : Finset (SWIGNode N)) {s s' : FixedValues M} {ℓ ℓ' : LatentValues M} (hs : ∀ (d : SWIGNode N) (hd : d ∈ M.fixed), (∃ v ∈ T, d = v ∨ M.dag.isAncestor d v) → s ⟨d, hd⟩ = s' ⟨d, hd⟩) (hℓ : ∀ (u : SWIGNode N) (hu : u ∈ M.unobserved), (∃ v ∈ T, u = v ∨ M.dag.isAncestor u v) → ℓ ⟨u, hu⟩ = ℓ' ⟨u, hu⟩) : ∀ (n : ℕ) (hn : n < M.observed.card) (_ : ∃ v ∈ T, (M.observedAt ⟨n, hn⟩).val = v ∨ M.dag.isAncestor (M.observedAt ⟨n, hn⟩).val v), evalObservedAux M s ℓ n hn = evalObservedAux M s' ℓ' n hn := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn hAnc rw [evalObservedAux_eq M s ℓ n hn, evalObservedAux_eq M s' ℓ' n hn] congr 1 funext w have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property have hw_anc_obs : M.dag.isAncestor w.val (M.observedAt ⟨n, hn⟩).val := DAG.isAncestor.edge hedge -- Chain the ancestor witness from `observedAt n` through `w`. have hAncW : ∃ v ∈ T, w.val = v ∨ M.dag.isAncestor w.val v := by rcases hAnc with ⟨v, hv, hOrAnc⟩ refine ⟨v, hv, ?_⟩ rcases hOrAnc with hEq | hAncToV · -- `observedAt n = v`, so `w` is a direct ancestor of `v`. exact inr (hEq ▸ hw_anc_obs) · -- `observedAt n` ancestor of `v`: transit through `w`. exact inr (M.dag.isAncestor_trans hw_anc_obs hAncToV) by_cases huo : w.val ∈ M.unobserved · rw [parentMap_unobserved M s ℓ hn _ w huo, parentMap_unobserved M s' ℓ' hn _ w huo] exact hℓ w.val huo hAncW · by_cases hfix : w.val ∈ M.fixed · rw [parentMap_fixed M s ℓ hn _ w hfix, parentMap_fixed M s' ℓ' hn _ w hfix] exact hs w.val hfix hAncW · -- `w` is observed: apply IH at its smaller topological index. have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs rw [parentMap_observed M s ℓ hn _ w hobs, parentMap_observed M s' ℓ' hn _ w hobs] congr 1 apply ih _ hj -- Re-cast the ancestor witness at `observedAt (observedIndex w) = w`. rcases hAncW with ⟨v, hv, hwv⟩ refine ⟨v, hv, ?_⟩ have h_at : (M.observedAt ⟨(M.observedIndex ⟨w.val, hobs⟩).val, (M.observedIndex ⟨w.val, hobs⟩).isLt⟩).val = w.val := M.observedAt_observedIndex ⟨w.val, hobs⟩ rw [h_at] exact hwv
Kernel 7 core · 7 supporting This file constructs the joint kernel induced by a structural causal model from its latent distribution and evaluation map, and then obtains the observational kernel by projecting to observed coordinates. ★ jointKernel_apply_eq★ obsCondKernel_ae_eq_condDistrib
Kernels Generated by Structural Causal Models
This file constructs the joint kernel induced by a structural causal model from its latent distribution and evaluation map, and then obtains the observational kernel by projecting to observed coordinates. It also provides the conditional kernels used to state kernel-level do-calculus rules.
Do-calculus Rule 2 and Rule 3 kernel statements and their value-space helpers live in the dedicated do-calculus files rather than in this core kernel file.
Main definitions and results
* SCM.jointKernel is the law of SCM.evalMap under the latent product,
parameterized by fixed values.
* SCM.randomToObserved and SCM.obsKernel project the joint law to observed
coordinates.
* SCM.jointKernel_apply_eq and SCM.jointKernel_map_commute expose
pushforward forms used by downstream measure proofs.
* SCM.obsCondPairKernel and SCM.obsCondKernel construct jointly measurable
conditional laws of target coordinates given conditioning coordinates.
* SCM.obsCondKernel_ae_eq_condDistrib connects the kernel-native conditional
object to the measure-level conditional distribution.
For a finite node population with measurable node-value spaces and a structural causal model, the joint conditional law of all random-node values given fixed-node values assigns each fixed-value assignment the distribution obtained by evaluating the model under its product distribution of latent variables. It is defined by combining that latent distribution with the deterministic evaluation rule and projecting to evaluated random values.
Definition (Lean source)
For a finite node population with measurable node-value spaces and a structural causal model, the projection from all random-node values to observed-node values retains exactly the coordinates belonging to observed nodes. It is defined coordinate by coordinate.
Definition (Lean source)
For a structural causal model M and a fixed-node assignment s, the joint kernel evaluated at s equals the pushforward of the latent-variable product measure through the evaluation map at s.
Formal statement
Proof (Lean source)
For a finite node population with measurable node-value spaces and a structural causal model, the conditional law of observed-node values given fixed-node values is obtained by mapping the joint conditional law to its observed coordinates. It is defined by that observed-coordinate projection.
For a finite node population with measurable node-value spaces, a structural causal model, a target-node set, a conditioning-node set, the requirement that every target node is observed, and the requirement that every conditioning node is observed, the joint conditional law of the conditioning and target coordinates given fixed-node values maps each observational law to the ordered pair of its conditioning-coordinate and target-coordinate restrictions. It is defined by that paired coordinate projection.
Definition (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, a target-node set, a conditioning-node set, the requirement that every target node is observed, the requirement that every conditioning node is observed, a nonempty standard-Borel target-value space, and a conditioning-value space satisfying the stipulated countable-generation condition, the jointly measurable conditional law of target coordinates given fixed-node and conditioning-coordinate values is obtained as a conditional law from the paired observational distribution.
Definition (Lean source)
At a fixed value s of the intervention-free (fixed) coordinates, provided the target coordinates Y are observed and the conditioning coordinates CC are observed, the jointly-measurable conditional kernel obsCondKernel built from Y and CC, evaluated at s, agrees almost everywhere — under the pushforward of the observational kernel onto CC — with the measure-theoretic conditional distribution of Y given CC under the observational kernel at s.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
measurable_randomToObservedtheorem — The observed-coordinate projection is measurable.Proof (Lean source)
@[fun_prop] theorem measurable_randomToObserved (M : SCM N Ω) : Measurable (M.randomToObserved) := by refine measurable_pi_lambda _ ?_ intro v exact measurable_pi_apply (a := (⟨v.val, Finset.mem_union_left _ v.property⟩ : {i // i ∈ M.randomVars})) -
instIsMarkovKernelJointKernelinstance — For a finite, distinguishable node population with measurable node-value spaces and a structural causal model, the joint conditional law of random-node values given fixed-node values is a Markov kernel: every conditional law is a probability measure.parametersN :sharedType u_1N → Type u_2M :SCM N Ωinstancegiven byby unfold jointKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ measurable_snd -
instIsMarkovKernelObsKernelinstance — For a finite, distinguishable node population with measurable node-value spaces and a structural causal model, the conditional law of observed-node values given fixed-node values is a Markov kernel: every conditional law is a probability measure. -
kernel_apply_univtheorem — Every slice of a Markov kernel has total mass one.hypothesesconclusionκ a univ = 1Proof (Lean source)
theorem kernel_apply_univ {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) [IsMarkovKernel κ] (a : α) : κ a univ = 1 := MeasureTheory.measure_univ -
obsKernel_apply_univtheorem — Each observational-kernel slice has total mass one.hypothesesconclusionM.obsKernel s univ = 1Proof (Lean source)
theorem obsKernel_apply_univ (M : SCM N Ω) (s : FixedValues M) : M.obsKernel s univ = 1 := kernel_apply_univ M.obsKernel s -
jointKernel_map_commutetheorem — The observational kernel can be written as one pushforward that evaluates the model and then projects to observed coordinates.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩconclusionM.obsKernel= ((const (FixedValues M) M.latentProduct) ⊗ₖ (deterministic (uncurry M.evalMap) M.evalMap_measurable)).map (M.randomToObserved ∘ snd)Proof (Lean source)
theorem jointKernel_map_commute (M : SCM N Ω) : M.obsKernel = ((const (FixedValues M) M.latentProduct) ⊗ₖ (deterministic (uncurry M.evalMap) M.evalMap_measurable)).map (M.randomToObserved ∘ snd) := by unfold obsKernel jointKernel exact (ProbabilityTheory.Kernel.map_comp_right _ measurable_snd M.measurable_randomToObserved).symm -
obsCondPairKernel_eqlemma — The conditional-pair kernel is the observational kernel pushed forward along the map that records the conditioning coordinates paired with the target coordinates.hypothesesconclusionM.obsCondPairKernel Y CC hY hCCProof (Lean source)
@[causal_defs_simps] lemma obsCondPairKernel_eq (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) : M.obsCondPairKernel Y CC hY hCC = (M.obsKernel).map (fun ω => (valuesProjection hCC ω, valuesProjection hY ω)) := rfl
EdgeType 9 core · 7 supporting This file records functional restrictions that may be attached to directed edges in a causal graph, including nonparametric, monotone, linear, and parametric cases. ★ refines_nonparametric
Edge Type Hierarchy
This file records functional restrictions that may be attached to directed edges in a causal graph, including nonparametric, monotone, linear, and parametric cases. The hierarchy is separate from the probabilistic semantics of structural causal models and is used to track functional assumptions.
Main definitions
* MonotonicityKind records the four monotonicity directions.
* EdgeType classifies an edge as nonparametric, monotone, linear, or
parametrically restricted.
* EdgeType.refinesBool and EdgeType.refines encode the assumption-refinement
order in which every edge type refines the nonparametric top element.
* EdgeTypeAssignment attaches an EdgeType label to each ordered edge slot of
a directed acyclic graph, with EdgeTypeAssignment.allNonparametric as the
default assignment.
A monotonicity classification is one of nondecreasing, nonincreasing, strictly increasing, or strictly decreasing.
Definition (Lean source)
An edge-type classification is either nonparametric, monotonic with a specified monotonicity classification, linear, or parametric.
Definition (Lean source)
For two edge-type assumptions, the Boolean refinement indicator is true exactly when the first assumption is at least as restrictive as the second: every assumption refines the nonparametric class, matching monotonicity kinds refine one another, and linear or parametric classes refine only their respective matching classes.
For two edge-type assumptions, the refinement relation holds exactly when their Boolean refinement indicator is true; thus the first assumption is at least as restrictive as the second.
Every edge-type functional-form assumption e refines the nonparametric assumption: nonparametric is the weakest assumption in the refinement order, so every other assumption is at least as specific as it.
Formal statement
Proof (Lean source)
An edge type assignment attaches a functional-assumption label to each directed edge of a graph.
For a directed acyclic graph, the all-nonparametric edge-type assignment labels every ordered pair of its vertices as nonparametric.
Definition (Lean source)
For an edge-type assignment and a vertex in its graph, the incoming edge-type set is the finite set of labels assigned to all parents of that vertex.
Definition (Lean source)
For an edge-type assignment, full nonparametricity holds exactly when, for every ordered pair of vertices joined by a directed edge, the assigned label is nonparametric.
Definition (Lean source)
7 supporting declarations (lemmas, instances)
-
instDecidableEqMonotonicityKindinstancederiving DecidableEq, Repr -
instReprMonotonicityKindinstancederiving DecidableEq, Repr -
instDecidableEqEdgeTypeinstancederiving DecidableEq, Repr -
instReprEdgeTypeinstancederiving DecidableEq, Repr -
decRefinesinstance — For each first edge-type assumption and each second edge-type assumption, a decision procedure for whether the first refines the second is provided. -
refines_refltheorem — Every edge-type assumption refines itself.hypotheses -
decIsFullyNonparametricinstance — For a finite vertex set whose members can be compared for equality and a directed acyclic graph on it and an edge-type assignment on that graph, a decision procedure for whether every directed edge has the nonparametric label is provided.
InterventionSet 5 core · 17 supporting This file exposes the public interface for set-valued interventions on structural causal models. ★ fixSet_empty_equiv★ fixSet_equiv_congr
Multi-Target Intervention Interface
This file exposes the public interface for set-valued interventions on structural causal models. It packages the monolithic intervention construction with preservation lemmas and the fixed-value projections used by the do-calculus kernel statements.
Main definitions and results
* SCM.fixSet is the public multi-target do-operation, implemented as the
monolithic intervention SCM.fixMono.
* SCM.fixSet_empty_equiv shows that intervening on the empty set is
structurally equivalent to the original model.
* SCM.fixSet_equiv_congr transports SCM.Equiv through a common intervention
target set.
* SCM.swigInterventionSet_insert_equiv relates iterative singleton insertion
to the one-shot intervention on insert y X.
* SCM.fixSetProj and SCM.fixSetZSlice provide the fixed-coordinate
projections used by kernel-level do-calculus statements.
For a finite node population with measurable node-value spaces, a structural causal model, and a finite set of intervention targets whose random copies are observed and whose fixed copies are not already fixed, the standard multi-target intervention is the model obtained by simultaneously splitting all targets. It is defined as the monolithic intervention.
For a structural causal model M, intervening on the empty set of nodes yields a structural causal model that is equivalent to M.
Formal statement
Proof (Lean source)
fixSet preserves SCM.Equiv. Given a structural equivalence h between M₁ and M₂ and a finite set of nodes X whose members are, in M₁, observed in their random coordinate and not already held fixed, intervening on X in both models produces two structurally equivalent post-intervention models — the analogous observed/not-fixed conditions transfer automatically to M₂ via h.
Formal statement
Proof (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, a finite intervention-target set whose random copies are observed and whose fixed copies are not already fixed, the projection from post-intervention fixed-value assignments to original fixed-value assignments restricts an assignment to the model's original fixed coordinates. It is defined by coordinate projection.
Definition (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, an initial intervention-target set whose random copies are observed and whose fixed copies are not already fixed, and a second intervention-target set whose random copies are observed after the first intervention and whose fixed copies are not already fixed after the first intervention, the second-intervention fixed-slice extractor maps every fixed-value assignment after both interventions to its coordinates for the fixed copies of the second targets. It is defined by coordinate projection.
Definition (Lean source)
17 supporting declarations (lemmas, instances)
-
fixSet_observedlemma — fixSet preserves observed.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).observed = M.observedProof (Lean source)
@[simp] lemma fixSet_observed (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).observed = M.observed := rfl -
fixSet_unobservedlemma — fixSet preserves unobserved.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).unobserved = M.unobservedProof (Lean source)
@[simp] lemma fixSet_unobserved (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).unobserved = M.unobserved := rfl -
fixSet_fixedlemma — fixSet enlarges fixed by exactly X.image SWIGNode.fixed.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).fixed = M.fixed ∪ X.image SWIGNode.fixedProof (Lean source)
@[simp] lemma fixSet_fixed (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).fixed = M.fixed ∪ X.image SWIGNode.fixed := rfl -
fixSet_latentDistlemma — fixSet inherits latentDist verbatim. Both sides have the same type ((M.fixSet X _ _).unobserved = M.unobserved by rfl) and equal body.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.fixedu :{u // u ∈ (M.fixSet X hObs hFix).unobserved}conclusion(M.fixSet X hObs hFix).latentDist u = M.latentDist uProof (Lean source)
@[simp] lemma fixSet_latentDist (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (u : {u // u ∈ (M.fixSet X hObs hFix).unobserved}) : (M.fixSet X hObs hFix).latentDist u = M.latentDist u := rfl -
fixSet_fixed_subsetlemma — fixSet only enlarges the fixed set.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.fixedconclusionM.fixed ⊆ (M.fixSet X hObs hFix).fixedProof (Lean source)
lemma fixSet_fixed_subset (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) : M.fixed ⊆ (M.fixSet X hObs hFix).fixed := fixMono_fixed_subset M.toSWIGGraph X hObs hFix -
fixSet_image_fixed_subsetlemma — X.image SWIGNode.fixed ⊆ (M.fixSet X _ _).fixed.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.fixedconclusionX.image SWIGNode.fixed ⊆ (M.fixSet X hObs hFix).fixedProof (Lean source)
lemma fixSet_image_fixed_subset (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) : X.image SWIGNode.fixed ⊆ (M.fixSet X hObs hFix).fixed := fixMono_image_fixed_subset M.toSWIGGraph X hObs hFix -
fixed_mem_fixSetlemma — Every SWIGNode.fixed D with D ∈ X is in the fixed set of fixSet X.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.fixed D ∈ (M.fixSet X hObs hFix).fixedProof (Lean source)
lemma fixed_mem_fixSet (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) {D : N} (hD : D ∈ X) : SWIGNode.fixed D ∈ (M.fixSet X hObs hFix).fixed := fixSet_image_fixed_subset M X hObs hFix (Finset.mem_image.mpr ⟨D, hD, rfl⟩) -
fixSet_parents_eq_of_no_fixed_parentlemma — SCM-level parent-set coincidence at non-.fixed-targeted vertices.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.fixedv :SWIGNode NhNoFP :∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet X hObs hFix).dag.parents vconclusion(M.fixSet X hObs hFix).dag.parents v = M.dag.parents vProof (Lean source)
lemma fixSet_parents_eq_of_no_fixed_parent (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) {v : SWIGNode N} (hNoFP : ∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet X hObs hFix).dag.parents v) : (M.fixSet X hObs hFix).dag.parents v = M.dag.parents v := fixMono_parents_eq_of_no_fixed_parent M X hObs hFix hNoFP -
splitMono_empty_parentslemma — Splitting no variables leaves every parent set unchanged.hypothesesconclusion(G.splitMono ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.parents v= G.dag.parents vProof (Lean source)
lemma splitMono_empty_parents (G : SWIGGraph N) (v : SWIGNode N) : (G.splitMono ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.parents v = G.dag.parents v := splitMono_parents_eq_of_no_fixed_parent G ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _)) v (fun _ hD => absurd hD (notMem_empty _)) -
fixSet_empty_parentslemma — Parent set of fixSet ∅ coincides with the base.hypothesesconclusion(M.fixSet ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.parents v= M.dag.parents vProof (Lean source)
lemma fixSet_empty_parents (M : SCM N Ω) (v : SWIGNode N) : (M.fixSet ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.parents v = M.dag.parents v := SWIGGraph.splitMono_empty_parents M.toSWIGGraph v -
fixSet_empty_edgelemma — Edges of fixSet ∅ coincide with the base.hypothesesconclusion(G.splitMono ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.edge u v↔ G.dag.edge u vProof (Lean source)
lemma fixSet_empty_edge (G : SWIGGraph N) (u v : SWIGNode N) : (G.splitMono ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).dag.edge u v ↔ G.dag.edge u v := by -- `splitMono ∅ .dag.edge = splitMonoEdgeRel G.dag.edge ∅`, which reduces to -- `G.dag.edge` by simp. cases u with | random u => simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel] | fixed d => simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel] -
fixSet_edgeType_random_eqlemma — After intervening on a set of variables, the label of every edge leaving a random-coordinate node is unchanged from the original causal 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.fixedu :Nv :SWIGNode Nconclusion(M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.random u) v= M.edgeTypes.edgeType (SWIGNode.random u) vProof (Lean source)
lemma fixSet_edgeType_random_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (u : N) (v : SWIGNode N) : (M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.random u) v = M.edgeTypes.edgeType (SWIGNode.random u) v := by change (if h : ∃ D ∈ X, SWIGNode.random u = SWIGNode.fixed D then M.edgeTypes.edgeType (SWIGNode.random (choose h)) v else M.edgeTypes.edgeType (SWIGNode.random u) v) = M.edgeTypes.edgeType (SWIGNode.random u) v rw [dif_neg] rintro ⟨D, _hD, hEq⟩ cases hEq -
fixSet_edgeType_fixed_mem_eqlemma — For a variable included in the intervention set, the edge label from its fixed-coordinate node equals the original label from its random-coordinate node.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 :Nv :SWIGNode Nhd :d ∈ Xconclusion(M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.fixed d) v= M.edgeTypes.edgeType (SWIGNode.random d) vProof (Lean source)
lemma fixSet_edgeType_fixed_mem_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (d : N) (v : SWIGNode N) (hd : d ∈ X) : (M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.fixed d) v = M.edgeTypes.edgeType (SWIGNode.random d) v := by change (if h : ∃ D ∈ X, SWIGNode.fixed d = SWIGNode.fixed D then M.edgeTypes.edgeType (SWIGNode.random (choose h)) v else M.edgeTypes.edgeType (SWIGNode.fixed d) v) = M.edgeTypes.edgeType (SWIGNode.random d) v let hmem : ∃ D ∈ X, SWIGNode.fixed d = SWIGNode.fixed D := ⟨d, hd, rfl⟩ rw [dif_pos hmem] have hchoose : choose hmem = d := by exact (SWIGNode.fixed.inj (Classical.choose_spec hmem).2).symm rw [hchoose] -
fixSet_edgeType_fixed_notMem_eqlemma — For a variable outside the intervention set, the edge label from its fixed-coordinate node is unchanged by the intervention.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 :Nv :SWIGNode Nhd :d ∉ Xconclusion(M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.fixed d) v= M.edgeTypes.edgeType (SWIGNode.fixed d) vProof (Lean source)
lemma fixSet_edgeType_fixed_notMem_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (d : N) (v : SWIGNode N) (hd : d ∉ X) : (M.fixSet X hObs hFix).edgeTypes.edgeType (SWIGNode.fixed d) v = M.edgeTypes.edgeType (SWIGNode.fixed d) v := by change (if h : ∃ D ∈ X, SWIGNode.fixed d = SWIGNode.fixed D then M.edgeTypes.edgeType (SWIGNode.random (choose h)) v else M.edgeTypes.edgeType (SWIGNode.fixed d) v) = M.edgeTypes.edgeType (SWIGNode.fixed d) v rw [dif_neg] rintro ⟨D, hD, hEq⟩ exact hd ((SWIGNode.fixed.inj hEq) ▸ hD) -
swigInterventionSet_insert_equivtheorem — Insert form of monolithic intervention composition.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset Ny :NhyX :y ∉ XhInsert_obs :∀ D ∈ insert y X, SWIGNode.random D ∈ M.observedhInsert_fixed :∀ D ∈ insert y X, SWIGNode.fixed D ∉ M.fixedconclusionhX_obs :by intro D hD exact hInsert_obs D (mem_insert_of_mem hD) (: ∀ D ∈ X, SWIGNode.random D ∈ M.observed)hX_fixed :by intro D hD exact hInsert_fixed D (mem_insert_of_mem hD) (: ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)hy_obs :by intro D hD have hDy : D= y := Finset.mem_singleton.mp hD subst D simpa only [fixSet_observed] using hInsert_obs y (mem_insert_self y X) (: ∀ D ∈ ({y} : Finset N), SWIGNode.random D ∈ (M.fixSet X hX_obs hX_fixed).observed)hy_fixed :by intro D hD hDfixed have hDy : D= y := Finset.mem_singleton.mp hD subst D rw [fixSet_fixed] at hDfixed rcases Finset.mem_union.mp hDfixed with hyfixed | hyimage · exact hInsert_fixed y (mem_insert_self y X) hyfixed · rcases Finset.mem_image.mp hyimage with ⟨z, hz, hzy⟩ exact hyX ((SWIGNode.fixed.inj hzy).symm ▸ hz) (: ∀ D ∈ ({y} : Finset N), SWIGNode.fixed D ∉ (M.fixSet X hX_obs hX_fixed).fixed)Proof (Lean source)
theorem swigInterventionSet_insert_equiv (M : SCM N Ω) (X : Finset N) (y : N) (hyX : y ∉ X) (hInsert_obs : ∀ D ∈ insert y X, SWIGNode.random D ∈ M.observed) (hInsert_fixed : ∀ D ∈ insert y X, SWIGNode.fixed D ∉ M.fixed) : let hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed := by intro D hD exact hInsert_obs D (mem_insert_of_mem hD) let hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed := by intro D hD exact hInsert_fixed D (mem_insert_of_mem hD) let hy_obs : ∀ D ∈ ({y} : Finset N), SWIGNode.random D ∈ (M.fixSet X hX_obs hX_fixed).observed := by intro D hD have hDy : D = y := Finset.mem_singleton.mp hD subst D simpa only [fixSet_observed] using hInsert_obs y (mem_insert_self y X) let hy_fixed : ∀ D ∈ ({y} : Finset N), SWIGNode.fixed D ∉ (M.fixSet X hX_obs hX_fixed).fixed := by intro D hD hDfixed have hDy : D = y := Finset.mem_singleton.mp hD subst D rw [fixSet_fixed] at hDfixed rcases Finset.mem_union.mp hDfixed with hyfixed | hyimage · exact hInsert_fixed y (mem_insert_self y X) hyfixed · rcases Finset.mem_image.mp hyimage with ⟨z, hz, hzy⟩ exact hyX ((SWIGNode.fixed.inj hzy).symm ▸ hz) SCM.Equiv ((M.fixSet X hX_obs hX_fixed).fixSet ({y} : Finset N) hy_obs hy_fixed) (M.fixSet (insert y X) hInsert_obs hInsert_fixed) := by dsimp apply swigInterventionSet_insert_equiv_aux M X y hyX (fun D hD => hInsert_obs D (mem_insert_of_mem hD)) (fun D hD => hInsert_fixed D (mem_insert_of_mem hD)) (hInsert_obs := hInsert_obs) (hInsert_fixed := hInsert_fixed) -
measurable_fixSetProjtheorem — fixSetProj is measurable.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.fixedconclusionMeasurable (M.fixSetProj X hObs hFix)Proof (Lean source)
@[fun_prop] theorem measurable_fixSetProj (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) : Measurable (M.fixSetProj X hObs hFix) := measurable_valuesProjection _ -
measurable_fixSetZSlicetheorem — fixSetZSlice is measurable.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX Z :Finset NhX_obs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhX_fixed :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ (M.fixSet X hX_obs hX_fixed).observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ (M.fixSet X hX_obs hX_fixed).fixedconclusionMeasurable (M.fixSetZSlice X Z hX_obs hX_fixed hZ_obs hZ_fixed)Proof (Lean source)
@[fun_prop] theorem measurable_fixSetZSlice (M : SCM N Ω) (X Z : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ (M.fixSet X hX_obs hX_fixed).observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ (M.fixSet X hX_obs hX_fixed).fixed) : Measurable (M.fixSetZSlice X Z hX_obs hX_fixed hZ_obs hZ_fixed) := measurable_valuesProjection _
EvalOverrideC 4 core · 12 supporting This file defines and analyzes a structural-model evaluation rule that holds a chosen set of observed variables fixed while evaluating the rest of the model, supporting conditional kernels aligned with single-world inter ★ evalMap_overrideC_at_self
This file defines and analyzes a structural-model evaluation rule that holds a chosen set of observed variables fixed while evaluating the rest of the model, supporting conditional kernels aligned with single-world intervention graphs.
The override evaluation short-circuits the chosen observed block and is proved measurable jointly in the fixed values, override values, and latent realization.
Main definitions and results
* SCM.parentMapOverride and SCM.evalObservedAuxOverride are the overridden
parent-tuple assembly and topological-order evaluator.
* SCM.evalMap_overrideC returns values on a target set while short-circuiting
every coordinate in the override block.
* SCM.evalMap_overrideC_apply_of_mem_C and
SCM.evalMap_overrideC_apply_of_not_mem_C are the two public unfold rules for
target nodes inside and outside the override block.
* SCM.evalMap_overrideC_at_self shows that overriding by the model's own
evaluated values leaves the target evaluation unchanged.
* SCM.measurable_evalMap_overrideC proves joint measurability of the override
evaluation.
For a structural causal model, an override block, an assignment of fixed values, an override assignment on that block, a latent realization, an index strictly below the number of observed nodes, values supplied for every earlier observed index, and a parent of the observed node at that index, the override parent-value assignment gives that parent's value, reading an overridden observed parent from the override assignment and otherwise following the fixed, latent, or earlier-observed source appropriate to that parent.
Definition (Lean source)
For a structural causal model, an override block contained in its observed nodes, an assignment of fixed values, an assignment on the override block, a latent realization, and an observed-node index, the override auxiliary evaluator gives, for every proof that the index is valid, the node's override value when it lies in the override block and otherwise its structural-function value computed recursively from overridden parent values.
Definition (Lean source)
For a structural causal model, a target set contained in its observed nodes, an override block contained in its observed nodes, an assignment of fixed values, an assignment on the override block, and a latent realization, the overridden evaluation map returns the values of every target node, holding every node in the override block to its assigned override value.
Definition (Lean source)
Cornerstone: overriding by the model's own values changes nothing. Fix a structural causal model M, a target set Y and an override set C with Y contained in the observed nodes and C contained in the observed nodes, a fixed-value assignment s, and a latent assignment ℓ. Then overriding C with the values that evalMap s ℓ would itself have produced there leaves the resulting evaluation on Y equal to the plain evaluation evalMap s ℓ on Y. No d-separation hypothesis is needed.
Formal statement
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
parentMapOverride_unobservedlemma — The override parent-value tuple reads a latent parent directly from the latent assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}huo :w.val ∈ M.unobservedconclusionparentMapOverride M s c ℓ hn prev w = ℓ ⟨w.val, huo⟩Proof (Lean source)
lemma parentMapOverride_unobserved (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (huo : w.val ∈ M.unobserved) : parentMapOverride M s c ℓ hn prev w = ℓ ⟨w.val, huo⟩ := by unfold parentMapOverride rw [dif_pos huo] -
parentMapOverride_fixedlemma — The override parent-value tuple reads a fixed parent directly from the fixed-value assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}hfix :w.val ∈ M.fixedconclusionparentMapOverride M s c ℓ hn prev w = s ⟨w.val, hfix⟩Proof (Lean source)
lemma parentMapOverride_fixed (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (hfix : w.val ∈ M.fixed) : parentMapOverride M s c ℓ hn prev w = s ⟨w.val, hfix⟩ := by unfold parentMapOverride have huo : w.val ∉ M.unobserved := by intro h obtain ⟨m, hm⟩ := M.unobserved_is_random _ h obtain ⟨k, hk⟩ := M.fixed_is_fixed _ hfix rw [hk] at hm exact absurd hm (by simp) rw [dif_neg huo, dif_pos hfix] -
parentMapOverride_Clemma — The override parent-value tuple reads an overridden observed parent directly from the override assignment.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}hc :w.val ∈ CconclusionparentMapOverride M s c ℓ hn prev w = c ⟨w.val, hc⟩Proof (Lean source)
lemma parentMapOverride_C (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (hc : w.val ∈ C) : parentMapOverride M s c ℓ hn prev w = c ⟨w.val, hc⟩ := by unfold parentMapOverride have hobs : w.val ∈ M.observed := hC hc have huo : w.val ∉ M.unobserved := not_unobs_of_obs M.toSWIGGraph hobs have hfix : w.val ∉ M.fixed := not_fixed_of_obs M.toSWIGGraph hobs rw [dif_neg huo, dif_neg hfix, dif_pos hc] -
parentMapOverride_observedlemma — The override parent-value tuple reads a non-overridden observed parent from the previous recursive values.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardprev :∀ m : ℕifm < nthen∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).valw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}hobs :w.val ∈ M.observedhc :w.val ∉ CconclusionparentMapOverride M s c ℓ hn prev w= (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ prev (M.observedIndex ⟨w.val, hobs⟩).val (M.observed_parent_index_lt hn (M.dag.mem_parents.mp w.property) hobs) (M.observedIndex ⟨w.val, hobs⟩).isLtProof (Lean source)
lemma parentMapOverride_observed (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) {n : ℕ} (hn : n < M.observed.card) (prev : ∀ m : ℕ, m < n → ∀ hm : m < M.observed.card, swigΩ Ω (M.observedAt ⟨m, hm⟩).val) (w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}) (hobs : w.val ∈ M.observed) (hc : w.val ∉ C) : parentMapOverride M s c ℓ hn prev w = (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ prev (M.observedIndex ⟨w.val, hobs⟩).val (M.observed_parent_index_lt hn (M.dag.mem_parents.mp w.property) hobs) (M.observedIndex ⟨w.val, hobs⟩).isLt := by unfold parentMapOverride have huo : w.val ∉ M.unobserved := not_unobs_of_obs M.toSWIGGraph hobs have hfix : w.val ∉ M.fixed := not_fixed_of_obs M.toSWIGGraph hobs rw [dif_neg huo, dif_neg hfix, dif_neg hc] -
evalObservedAuxOverride_eqlemma — The override auxiliary evaluator unfolds to either the override value or the structural function applied to overridden parents.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardconclusionevalObservedAuxOverride M hC s c ℓ n hn= (if hcSelf : (M.observedAt ⟨n, hn⟩).val ∈ C then c ⟨(M.observedAt ⟨n, hn⟩).val, hcSelf⟩ else M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMapOverride M s c ℓ hn (fun m _ hm_card => evalObservedAuxOverride M hC s c ℓ m hm_card) w))Proof (Lean source)
lemma evalObservedAuxOverride_eq (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ : LatentValues M) (n : ℕ) (hn : n < M.observed.card) : evalObservedAuxOverride M hC s c ℓ n hn = (if hcSelf : (M.observedAt ⟨n, hn⟩).val ∈ C then c ⟨(M.observedAt ⟨n, hn⟩).val, hcSelf⟩ else M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMapOverride M s c ℓ hn (fun m _ hm_card => evalObservedAuxOverride M hC s c ℓ m hm_card) w)) := by unfold evalObservedAuxOverride rw [Nat.strongRec_eq] -
evalMap_overrideC_eqlemma — At any target node, the overridden evaluation map is the transported override auxiliary value at that node's topological index.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhY :Y ⊆ M.observedhC :C ⊆ M.observeds :M.FixedValuesℓ :M.LatentValuesv :{v // v ∈ Y}conclusionM.evalMap_overrideC hY hC s c ℓ v= (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ evalObservedAuxOverride M hC s c ℓ (M.observedIndex ⟨v.val, hY v.property⟩).val (M.observedIndex ⟨v.val, hY v.property⟩).isLtProof (Lean source)
lemma evalMap_overrideC_eq (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : M.FixedValues) (c : ValuesOn C (swigΩ Ω)) (ℓ : M.LatentValues) (v : {v // v ∈ Y}) : M.evalMap_overrideC hY hC s c ℓ v = (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ evalObservedAuxOverride M hC s c ℓ (M.observedIndex ⟨v.val, hY v.property⟩).val (M.observedIndex ⟨v.val, hY v.property⟩).isLt := rfl -
evalMap_overrideC_apply_of_mem_Ctheorem — At a target node inside the override block, the overridden evaluation returns the assigned override value.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhY :Y ⊆ M.observedhC :C ⊆ M.observeds :M.FixedValuesℓ :M.LatentValuesv :{v // v ∈ Y}hvC :v.val ∈ CconclusionM.evalMap_overrideC hY hC s c ℓ v = c ⟨v.val, hvC⟩Proof (Lean source)
theorem evalMap_overrideC_apply_of_mem_C (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : M.FixedValues) (c : ValuesOn C (swigΩ Ω)) (ℓ : M.LatentValues) (v : {v // v ∈ Y}) (hvC : v.val ∈ C) : M.evalMap_overrideC hY hC s c ℓ v = c ⟨v.val, hvC⟩ := by rw [evalMap_overrideC_eq] set j : Fin M.observed.card := M.observedIndex ⟨v.val, hY v.property⟩ with hj_def rw [evalObservedAuxOverride_eq] have hAtJ : M.observedAt ⟨j.val, j.isLt⟩ = M.observedAt j := rfl have hcSelf : (M.observedAt ⟨j.val, j.isLt⟩).val ∈ C := by rw [hAtJ] rw [show M.observedAt j = ⟨v.val, hY v.property⟩ from observedAt_observedIndex_subtype M (hY v.property)] exact hvC rw [dif_pos hcSelf] -- Goal: transport ▸ c ⟨(M.observedAt ⟨j.val, j.isLt⟩).val, hcSelf⟩ = c ⟨v.val, hvC⟩ -- The transport is along `(M.observedAt j).val = v.val`. -- Reduce by `c_at_observedAt_eq_c_at_self`, with j ≡ M.observedIndex ⟨v.val, hY v.property⟩. -- First: rewrite ⟨j.val, j.isLt⟩ as j using Fin eta. have hFinEta : (⟨j.val, j.isLt⟩ : Fin M.observed.card) = j := Fin.ext rfl -- Now use a direct calculation. -- The expression `(M.observedAt ⟨j.val, j.isLt⟩).val` is defeq to `(M.observedAt j).val`. -- The cast proof on the LHS is `M.observedAt_observedIndex ⟨v.val, hY v.property⟩`. change (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ c ⟨(M.observedAt ⟨j.val, j.isLt⟩).val, hcSelf⟩ = c ⟨v.val, hvC⟩ -- Reduce to the helper form. exact c_at_observedAt_eq_c_at_self M c (hY v.property) hvC hcSelf -
evalMap_overrideC_apply_of_not_mem_Ctheorem — At a target node outside the override block, the overridden evaluation applies the structural function to overridden parent values.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhY :Y ⊆ M.observedhC :C ⊆ M.observeds :M.FixedValuesℓ :M.LatentValuesv :{v // v ∈ Y}hvC :v.val ∉ CconclusionM.evalMap_overrideC hY hC s c ℓ v= (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v.val, hY v.property⟩)) (fun w => parentMapOverride M s c ℓ (M.observedIndex ⟨v.val, hY v.property⟩).isLt (fun m _ hm_card => evalObservedAuxOverride M hC s c ℓ m hm_card) w)Proof (Lean source)
theorem evalMap_overrideC_apply_of_not_mem_C (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : M.FixedValues) (c : ValuesOn C (swigΩ Ω)) (ℓ : M.LatentValues) (v : {v // v ∈ Y}) (hvC : v.val ∉ C) : M.evalMap_overrideC hY hC s c ℓ v = (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v.val, hY v.property⟩)) (fun w => parentMapOverride M s c ℓ (M.observedIndex ⟨v.val, hY v.property⟩).isLt (fun m _ hm_card => evalObservedAuxOverride M hC s c ℓ m hm_card) w) := by rw [evalMap_overrideC_eq] set j : Fin M.observed.card := M.observedIndex ⟨v.val, hY v.property⟩ with hj_def rw [evalObservedAuxOverride_eq] have hAtJ : M.observedAt ⟨j.val, j.isLt⟩ = M.observedAt j := rfl have hcSelf : (M.observedAt ⟨j.val, j.isLt⟩).val ∉ C := by rw [hAtJ] rw [show M.observedAt j = ⟨v.val, hY v.property⟩ from observedAt_observedIndex_subtype M (hY v.property)] exact hvC rw [dif_neg hcSelf] -
evalObservedAux_cast_collapse_at_observedAtlemma — For an observed node, transporting its recursively evaluated value through the round-trip topological-index lookup leaves that value unchanged.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :ℓ :j :Fin M.observed.cardhvObs :(M.observedAt j).val ∈ M.observedconclusion((M.observedAt_observedIndex ⟨(M.observedAt j).val, hvObs⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨(M.observedAt j).val, hvObs⟩).val (M.observedIndex ⟨(M.observedAt j).val, hvObs⟩).isLt)= evalObservedAux M s ℓ j.val j.isLtProof (Lean source)
lemma evalObservedAux_cast_collapse_at_observedAt (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) (j : Fin M.observed.card) (hvObs : (M.observedAt j).val ∈ M.observed) : ((M.observedAt_observedIndex ⟨(M.observedAt j).val, hvObs⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨(M.observedAt j).val, hvObs⟩).val (M.observedIndex ⟨(M.observedAt j).val, hvObs⟩).isLt) = evalObservedAux M s ℓ j.val j.isLt := by -- Step 1: the Subtype ⟨(observedAt j).val, hvObs⟩ equals observedAt j (Subtype.ext). have hsubEq : (⟨(M.observedAt j).val, hvObs⟩ : {v // v ∈ M.observed}) = M.observedAt j := Subtype.ext rfl -- Step 2: the index of observedAt j is j (observedIndex_observedAt). have hjEq : M.observedIndex ⟨(M.observedAt j).val, hvObs⟩ = j := by rw [hsubEq]; exact M.observedIndex_observedAt _ -- Step 3: factor through a free Fin `k` and Subtype `w`. This is the -- `evalObservedAux_cast_eq_structFunAt` trick applied here. suffices h : ∀ (k : Fin M.observed.card) (hkj : k = j) (hcast : (M.observedAt k).val = (M.observedAt j).val), (hcast ▸ evalObservedAux M s ℓ k.val k.isLt : swigΩ Ω (M.observedAt j).val) = evalObservedAux M s ℓ j.val j.isLt by -- Plug in k := observedIndex ⟨(observedAt j).val, hvObs⟩, hkj := hjEq. -- The cast proof becomes (observedAt (observedIndex ⟨...⟩)).val = (observedAt j).val, -- but we have it as (observedAt (observedIndex ⟨...⟩)).val = ⟨...⟩.val = (observedAt j).val. have hcast' : (M.observedAt (M.observedIndex ⟨(M.observedAt j).val, hvObs⟩)).val = (M.observedAt j).val := M.observedAt_observedIndex ⟨(M.observedAt j).val, hvObs⟩ exact h _ hjEq hcast' intro k hkj hcast subst k have hpr_rfl : hcast = rfl := Subsingleton.elim _ _ rw [hpr_rfl] -
evalObservedAuxOverride_eq_evalObservedAux_at_selflemma — When an observed-node override uses the model's own recursively evaluated values, the overridden recursive evaluator agrees with the original evaluator at every topological position.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhC :C ⊆ M.observeds :ℓ :n :ℕhn :n < M.observed.cardconclusionevalObservedAuxOverride M hC s (fun v' : {v // v ∈ C} => (M.observedAt_observedIndex ⟨v'.val, hC v'.property⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨v'.val, hC v'.property⟩).val (M.observedIndex ⟨v'.val, hC v'.property⟩).isLt) ℓ n hn= evalObservedAux M s ℓ n hnProof (Lean source)
lemma evalObservedAuxOverride_eq_evalObservedAux_at_self (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (ℓ : LatentValues M) : ∀ (n : ℕ) (hn : n < M.observed.card), evalObservedAuxOverride M hC s (fun v' : {v // v ∈ C} => (M.observedAt_observedIndex ⟨v'.val, hC v'.property⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨v'.val, hC v'.property⟩).val (M.observedIndex ⟨v'.val, hC v'.property⟩).isLt) ℓ n hn = evalObservedAux M s ℓ n hn := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn rw [evalObservedAuxOverride_eq] by_cases hcSelf : (M.observedAt ⟨n, hn⟩).val ∈ C · rw [dif_pos hcSelf] -- Goal: c-value at v_sub = evalObservedAux M s ℓ n hn. -- Beta-reduce the c-lambda first. change ((M.observedAt_observedIndex ⟨(M.observedAt ⟨n, hn⟩).val, hC hcSelf⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨(M.observedAt ⟨n, hn⟩).val, hC hcSelf⟩).val (M.observedIndex ⟨(M.observedAt ⟨n, hn⟩).val, hC hcSelf⟩).isLt) = evalObservedAux M s ℓ n hn -- Apply the cast-collapse helper at index ⟨n, hn⟩. exact evalObservedAux_cast_collapse_at_observedAt M s ℓ ⟨n, hn⟩ (hC hcSelf) · rw [dif_neg hcSelf] rw [evalObservedAux_eq] congr 1 funext w have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property by_cases huo : w.val ∈ M.unobserved · rw [parentMapOverride_unobserved M hC s _ _ _ _ _ huo, parentMap_unobserved _ _ _ _ _ _ huo] · by_cases hfix : w.val ∈ M.fixed · rw [parentMapOverride_fixed M hC s _ _ _ _ _ hfix, parentMap_fixed _ _ _ _ _ _ hfix] · have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs by_cases hcW : w.val ∈ C · rw [parentMapOverride_C M hC s _ _ _ _ _ hcW] -- Goal: c ⟨w.val, hcW⟩ = parentMap s ℓ hn _ w -- The c-lambda body at w.val matches parentMap_observed's body (def. eq). rw [parentMap_observed _ _ _ _ _ _ hobs] · rw [parentMapOverride_observed M hC s _ _ _ _ _ hobs hcW] rw [parentMap_observed _ _ _ _ _ _ hobs] congr 1 exact ih _ hj _ -
evalObservedAuxOverride_measurablelemma — At every position in an SCM's topological order, its observed-variable evaluator with specified observed values overridden is jointly measurable in fixed, override, and latent inputs.hypothesesconclusionMeasurable (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 n hn)Proof (Lean source)
@[fun_prop] lemma evalObservedAuxOverride_measurable (M : SCM N Ω) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) : ∀ (n : ℕ) (hn : n < M.observed.card), Measurable (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 n hn) := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn have hrw : (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 n hn) = (fun p => if hcSelf : (M.observedAt ⟨n, hn⟩).val ∈ C then p.1.2 ⟨(M.observedAt ⟨n, hn⟩).val, hcSelf⟩ else M.structFun (M.observedAt ⟨n, hn⟩) (fun w => parentMapOverride M p.1.1 p.1.2 p.2 hn (fun m _ hm_card => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 m hm_card) w)) := by funext p exact evalObservedAuxOverride_eq M hC p.1.1 p.1.2 p.2 n hn rw [hrw] by_cases hcSelf : (M.observedAt ⟨n, hn⟩).val ∈ C · simp only [dif_pos hcSelf] exact (measurable_pi_apply _).comp (measurable_snd.comp measurable_fst) · simp only [dif_neg hcSelf] refine (M.structFun_measurable _).comp ?_ refine measurable_pi_lambda _ (fun w => ?_) by_cases huo : w.val ∈ M.unobserved · have hfun : (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => parentMapOverride M p.1.1 p.1.2 p.2 hn (fun m _ hm_card => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 m hm_card) w) = (fun p => p.2 ⟨w.val, huo⟩) := by funext p exact parentMapOverride_unobserved M hC p.1.1 p.1.2 p.2 hn _ w huo rw [hfun] exact (measurable_pi_apply _).comp measurable_snd · by_cases hfix : w.val ∈ M.fixed · have hfun : (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => parentMapOverride M p.1.1 p.1.2 p.2 hn (fun m _ hm_card => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 m hm_card) w) = (fun p => p.1.1 ⟨w.val, hfix⟩) := by funext p exact parentMapOverride_fixed M hC p.1.1 p.1.2 p.2 hn _ w hfix rw [hfun] exact (measurable_pi_apply _).comp (measurable_fst.comp measurable_fst) · have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by have hcls := (M.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hcls with hfo | huo' · rcases Finset.mem_union.mp hfo with hf | ho · exact absurd hf hfix · exact ho · exact absurd huo' huo by_cases hcW : w.val ∈ C · have hfun : (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => parentMapOverride M p.1.1 p.1.2 p.2 hn (fun m _ hm_card => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 m hm_card) w) = (fun p => p.1.2 ⟨w.val, hcW⟩) := by funext p exact parentMapOverride_C M hC p.1.1 p.1.2 p.2 hn _ w hcW rw [hfun] exact (measurable_pi_apply _).comp (measurable_snd.comp measurable_fst) · have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs have hfun : (fun p : (FixedValues M × ValuesOn C (swigΩ Ω)) × LatentValues M => parentMapOverride M p.1.1 p.1.2 p.2 hn (fun m _ hm_card => evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 m hm_card) w) = (fun p => (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 (M.observedIndex ⟨w.val, hobs⟩).val (M.observedIndex ⟨w.val, hobs⟩).isLt) := by funext p exact parentMapOverride_observed M hC p.1.1 p.1.2 p.2 hn _ w hobs hcW rw [hfun] exact measurable_family_cast _ (ih _ hj _) -
measurable_evalMap_overrideCtheorem — The overridden evaluation map is jointly measurable in fixed values, override values, and the latent realization.hypothesesconclusionMeasurable (fun p : (M.FixedValues × ValuesOn C (swigΩ Ω)) × M.LatentValues => M.evalMap_overrideC hY hC p.1.1 p.1.2 p.2)Proof (Lean source)
@[fun_prop] theorem measurable_evalMap_overrideC (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) : Measurable (fun p : (M.FixedValues × ValuesOn C (swigΩ Ω)) × M.LatentValues => M.evalMap_overrideC hY hC p.1.1 p.1.2 p.2) := by refine measurable_pi_iff.mpr (fun v => ?_) have hfun : (fun p : (M.FixedValues × ValuesOn C (swigΩ Ω)) × M.LatentValues => M.evalMap_overrideC hY hC p.1.1 p.1.2 p.2 v) = (fun p => (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ evalObservedAuxOverride M hC p.1.1 p.1.2 p.2 (M.observedIndex ⟨v.val, hY v.property⟩).val (M.observedIndex ⟨v.val, hY v.property⟩).isLt) := by funext p exact evalMap_overrideC_eq M hY hC p.1.1 p.1.2 p.2 v rw [hfun] exact measurable_family_cast _ (evalObservedAuxOverride_measurable M hC _ _)
InterventionMono 5 core · 8 supporting This file defines the one-shot version of a multi-target intervention on a structural causal model. ★ fixMono_observed★ fixMono_fixed★ fixMono_latentDist
Monolithic Multi-Target Intervention
This file defines the one-shot version of a multi-target intervention on a structural causal model. It reroutes all affected outgoing edges in a single graph transformation, which gives later comparison lemmas direct access to the unchanged structural functions at unaffected vertices.
The graph layer is the monolithic SWIG split; latent distributions are inherited unchanged, and structural functions use one parent reindexing map rather than iterated single-target interventions.
Main definitions and results
* SCM.fixMonoParentMap reindexes split-graph parent tuples back to the parent
tuple expected by the original structural function.
* SCM.fixMono builds the monolithic multi-target intervention SCM, inheriting
latent laws and reusing structural functions through fixMonoParentMap.
* SCM.fixMono_observed, SCM.fixMono_unobserved, SCM.fixMono_fixed, and
SCM.fixMono_latentDist expose the preserved or enlarged primitive fields.
* SCM.fixMono_parents_eq_of_no_fixed_parent gives parent-set coincidence at
vertices whose post-intervention parents contain no targeted fixed copy.
For a finite node population with node-value spaces, a SWIG graph, a finite set of intervention targets whose random copies are observed and whose fixed copies are not already fixed, a node, and an assignment of values to that node's parents after the simultaneous split, the monolithic parent reindexing map returns the corresponding assignment on the node's parents before the split. It reads a targeted random parent from its new fixed-copy coordinate and otherwise preserves the parent coordinate; these are respectively the random-parent clause and the fixed-parent clause.
Definition (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, and a finite set of intervention targets whose random copies are observed and whose fixed copies are not already fixed, the monolithic intervened structural causal model simultaneously splits every target, first forming the split graph and then assigning each split edge the corresponding original edge type. It retains the original latent laws and structural mechanisms after reindexing their parent-value inputs.
Definition (Lean source)
Observed-node invariance of the monolithic intervention. For a SWIG graph G and an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed, the monolithic intervention graph obtained by fixing X has the same observed node set as G.
Formal statement
Proof (Lean source)
Fixed-node set of the monolithic intervention. For a SWIG graph G and an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed, the monolithic intervention graph's fixed node set equals G's fixed node set together with the fixed copies of the targeted nodes in X.
Formal statement
Proof (Lean source)
Latent-distribution invariance of the monolithic intervention. For a structural causal model M and an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed, and any latent-root node u of the monolithically intervened model, the intervened model's latent distribution at u equals M's original latent distribution at u.
Formal statement
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
fixMonoParentMap_apply_fixedlemma — At a fixed-coordinate parent, the monolithic parent reindexer reads the same fixed coordinate from the split graph.hypothesesN :sharedType u_1N → Type u_2G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode Nξ :∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.vald :NhwVal :SWIGNode.fixed d ∈ G.dag.parents vconclusionfixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.fixed d, hwVal⟩ : {w // w ∈ G.dag.parents v})= ξ ⟨SWIGNode.fixed d, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.fixed d)).2 (inl ⟨hwVal, fun _ _ heq => by cases heq⟩)⟩Proof (Lean source)
lemma fixMonoParentMap_apply_fixed (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) (ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val) (d : N) (hwVal : SWIGNode.fixed d ∈ G.dag.parents v) : fixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.fixed d, hwVal⟩ : {w // w ∈ G.dag.parents v}) = ξ ⟨SWIGNode.fixed d, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.fixed d)).2 (inl ⟨hwVal, fun _ _ heq => by cases heq⟩)⟩ := rfl -
fixMonoParentMap_apply_random_notMemlemma — At an untreated random-coordinate parent, the monolithic parent reindexer reads the same random coordinate from the split graph.hypothesesN :sharedType u_1N → Type u_2G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode Nξ :∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.valu :Nhu :u ∉ XhwVal :SWIGNode.random u ∈ G.dag.parents vconclusionfixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.random u, hwVal⟩ : {w // w ∈ G.dag.parents v})= ξ ⟨SWIGNode.random u, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.random u)).2 (inl ⟨hwVal, fun _ hD heq => hu (SWIGNode.random.inj heq ▸ hD)⟩)⟩Proof (Lean source)
lemma fixMonoParentMap_apply_random_notMem (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) (ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val) (u : N) (hu : u ∉ X) (hwVal : SWIGNode.random u ∈ G.dag.parents v) : fixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.random u, hwVal⟩ : {w // w ∈ G.dag.parents v}) = ξ ⟨SWIGNode.random u, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.random u)).2 (inl ⟨hwVal, fun _ hD heq => hu (SWIGNode.random.inj heq ▸ hD)⟩)⟩ := by unfold fixMonoParentMap simp only [dif_neg hu] -
fixMonoParentMap_apply_randomlemma — At a treated random-coordinate parent, the monolithic parent reindexer reads the corresponding fixed coordinate from the split graph.hypothesesN :sharedType u_1N → Type u_2G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode ND :NhD :D ∈ Xξ :∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.valhD_parent :SWIGNode.random D ∈ G.dag.parents vconclusionfixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.random D, hD_parent⟩ : {w // w ∈ G.dag.parents v})Proof (Lean source)
lemma fixMonoParentMap_apply_random (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) (D : N) (hD : D ∈ X) (ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val) (hD_parent : SWIGNode.random D ∈ G.dag.parents v) : fixMonoParentMap (Ω := Ω) G X hObs hFix v ξ (⟨SWIGNode.random D, hD_parent⟩ : {w // w ∈ G.dag.parents v}) = ξ ⟨SWIGNode.fixed D, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.fixed D)).2 (inr ⟨D, hD, rfl, hD_parent⟩)⟩ := by unfold fixMonoParentMap simp only [dif_pos hD] -
measurable_fixMonoParentMaplemma — The parent values used by a monolithic intervention depend measurably on the original parent values, so this reindexing can be used safely when constructing intervened structural equations and probability kernels.hypothesesN :sharedType u_1N → Type u_2G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedv :SWIGNode NconclusionMeasurable (fixMonoParentMap (Ω := Ω) G X hObs hFix v)Proof (Lean source)
@[fun_prop] lemma measurable_fixMonoParentMap (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) : Measurable (fixMonoParentMap (Ω := Ω) G X hObs hFix v) := by classical refine measurable_pi_iff.mpr ?_ rintro ⟨wVal, hwVal⟩ match wVal, hwVal with | SWIGNode.random u, hwVal => by_cases hu : u ∈ X · have h_eq : (fun ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val => fixMonoParentMap G X hObs hFix v ξ (⟨SWIGNode.random u, hwVal⟩ : {w // w ∈ G.dag.parents v})) = (fun ξ => ξ ⟨SWIGNode.fixed u, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.fixed u)).2 (inr ⟨u, hu, rfl, hwVal⟩)⟩) := by funext ξ exact fixMonoParentMap_apply_random (Ω := Ω) G X hObs hFix v u hu ξ hwVal rw [h_eq] exact measurable_pi_apply _ · have h_eq : (fun ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val => fixMonoParentMap G X hObs hFix v ξ (⟨SWIGNode.random u, hwVal⟩ : {w // w ∈ G.dag.parents v})) = (fun ξ => ξ ⟨SWIGNode.random u, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.random u)).2 (inl ⟨hwVal, fun D hD heq => hu (SWIGNode.random.inj heq ▸ hD)⟩)⟩) := by funext ξ exact fixMonoParentMap_apply_random_notMem (Ω := Ω) G X hObs hFix v ξ u hu hwVal rw [h_eq] exact measurable_pi_apply _ | SWIGNode.fixed d, hwVal => have h_eq : (fun ξ : ∀ w' : {w' // w' ∈ (G.splitMono X hObs hFix).dag.parents v}, swigΩ Ω w'.val => fixMonoParentMap G X hObs hFix v ξ (⟨SWIGNode.fixed d, hwVal⟩ : {w // w ∈ G.dag.parents v})) = (fun ξ => ξ ⟨SWIGNode.fixed d, (SWIGGraph.splitMono_parents_char G X hObs hFix v (SWIGNode.fixed d)).2 (inl ⟨hwVal, fun _ _ heq => by cases heq⟩)⟩) := by funext ξ exact fixMonoParentMap_apply_fixed (Ω := Ω) G X hObs hFix v ξ d hwVal rw [h_eq] exact measurable_pi_apply _ -
fixMono_unobservedlemma — The monolithic intervention preserves the unobserved node set.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).unobserved = G.unobservedProof (Lean source)
@[simp] lemma fixMono_unobserved (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).unobserved = G.unobserved := rfl -
fixMono_fixed_subsetlemma — The original fixed node set is contained in the fixed node set after the monolithic intervention.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusionG.fixed ⊆ (G.splitMono X hObs hFix).fixedProof (Lean source)
lemma fixMono_fixed_subset (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : G.fixed ⊆ (G.splitMono X hObs hFix).fixed := by intro x hx rw [fixMono_fixed] exact mem_union_left _ hx -
fixMono_image_fixed_subsetlemma — The fixed copies of the intervention targets are contained in the fixed node set after the monolithic intervention.hypothesesN :sharedType u_1G :X :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ G.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ G.fixedconclusionX.image SWIGNode.fixed ⊆ (G.splitMono X hObs hFix).fixedProof (Lean source)
lemma fixMono_image_fixed_subset (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : X.image SWIGNode.fixed ⊆ (G.splitMono X hObs hFix).fixed := by intro x hx rw [fixMono_fixed] exact mem_union_right _ hx -
fixMono_parents_eq_of_no_fixed_parentlemma — If no fixed copy of a target is a parent of a vertex after intervention, that vertex has the same parents as before.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.fixedv :SWIGNode NhNoFP :∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixMono X hObs hFix).dag.parents vconclusion(M.fixMono X hObs hFix).dag.parents v = M.dag.parents vProof (Lean source)
lemma fixMono_parents_eq_of_no_fixed_parent (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) {v : SWIGNode N} (hNoFP : ∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixMono X hObs hFix).dag.parents v) : (M.fixMono X hObs hFix).dag.parents v = M.dag.parents v := by -- `(M.fixMono X).dag = (M.toSWIGGraph.splitMono X …).dag` by definition. exact SWIGGraph.splitMono_parents_eq_of_no_fixed_parent M.toSWIGGraph X hObs hFix v hNoFP
CounterfactualLemmas 2 core · 3 supporting This file proves pathwise identities relating evaluation of a structural causal model before and after interventions. ★ evalMap_fixSet_factual_eq★ evalMap_fixSet_union_eq
Counterfactual Identities for Structural Causal Models
This file proves pathwise identities relating evaluation of a structural causal
model before and after interventions. The one-step lemmas
fixMono_structFun_apply, fixSet_structFun_apply, and
evalMap_fixSet_observed_apply expose how intervened parent values enter the
original structural equations. The main theorems evalMap_fixSet_factual_eq and
evalMap_fixSet_union_eq provide SCM-level factual consistency and composition
with an intermediate-value hypothesis, which are used by the potential-outcome
bridge.
prop:scm-cf-consistency (Basic Concepts.tex L475–480). Fix a structural causal model M, an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed, a base fixed-value assignment s, a latent assignment ℓ, and an intervened fixed-value assignment sx for the model obtained by fixing X. If sx agrees with s on the model's original fixed coordinates and for every targeted node the base evaluation at its random form already equals sx's value at its fixed form — the factual consistency condition, then for every observed node v, evaluating the intervened model with sx and ℓ at v agrees with evaluating the base model with s and ℓ at v.
Formal statement
Proof (Lean source)
Composition of a combined intervention with a single-stage intervention. Fix a structural causal model M, a latent assignment ℓ, and two intervention target sets X₁, X₂ such that every node of X₁ is currently a random observed node with no fixed copy already fixed, and likewise every node of X₁ ∪ X₂, with an X₁-only intervened fixed-value assignment sx₁ and a combined-intervention fixed-value assignment sxU for X₁ ∪ X₂. If sxU agrees with sx₁ on the original fixed coordinates and on the X₁ intervention coordinates and the X₁-intervened model's value at each X₂ node already equals sxU's assignment there — the intermediate condition, then for every observed node v, evaluating the combined-intervention model with sxU and ℓ at v agrees with evaluating the X₁-only intervened model with sx₁ and ℓ at v.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
fixMono_structFun_applylemma — After an intervention on a set of observed variables, each observed variable is still computed by the original structural equation, with intervened parents replaced by their assigned intervention values.hypothesesN :sharedType uNN → Type uΩM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedv :{v // v ∈ (M.fixMono X hObs hFix).observed}ξ :∀ w : {w // w ∈ (M.fixMono X hObs hFix).dag.parents v.val}, swigΩ Ω w.valconclusion(M.fixMono X hObs hFix).structFun v ξ= M.structFun ⟨v.val, v.property⟩ (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val ξ)Proof (Lean source)
@[simp] lemma fixMono_structFun_apply (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (v : {v // v ∈ (M.fixMono X hObs hFix).observed}) (ξ : ∀ w : {w // w ∈ (M.fixMono X hObs hFix).dag.parents v.val}, swigΩ Ω w.val) : (M.fixMono X hObs hFix).structFun v ξ = M.structFun ⟨v.val, v.property⟩ (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val ξ) := by rfl -
fixSet_structFun_applylemma — After an intervention on a set of observed variables, each observed variable is still computed by the original structural equation, with intervened parents replaced by their assigned intervention values.hypothesesN :sharedType uNN → Type uΩM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedv :{v // v ∈ (M.fixSet X hObs hFix).observed}ξ :∀ w : {w // w ∈ (M.fixSet X hObs hFix).dag.parents v.val}, swigΩ Ω w.valconclusion(M.fixSet X hObs hFix).structFun v ξ= M.structFun ⟨v.val, v.property⟩ (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val ξ)Proof (Lean source)
@[simp] lemma fixSet_structFun_apply (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (v : {v // v ∈ (M.fixSet X hObs hFix).observed}) (ξ : ∀ w : {w // w ∈ (M.fixSet X hObs hFix).dag.parents v.val}, swigΩ Ω w.val) : (M.fixSet X hObs hFix).structFun v ξ = M.structFun ⟨v.val, v.property⟩ (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val ξ) := by rfl -
evalMap_fixSet_observed_applylemma — For one recursive evaluation step after an intervention, the value of an observed variable is the original structural equation evaluated at the parent values where intervened parents are pinned to their assigned intervention values.hypothesesN :sharedType uNN → Type uΩM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedsx :FixedValues (M.fixSet X hObs hFix)ℓ :v :{v // v ∈ M.observed}conclusion(M.fixSet X hObs hFix).evalMap sx ℓ ⟨v.val, mem_union_left _ v.property⟩= M.structFun v (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val (fun w : {w // w ∈ (M.fixSet X hObs hFix).dag.parents v.val} => if huo : w.val ∈ (M.fixSet X hObs hFix).unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ (M.fixSet X hObs hFix).fixed then sx ⟨w.val, hfix⟩ else have hedge : (M.fixSet X hObs hFix).dag.edge w.val v.val := (M.fixSet X hObs hFix).dag.mem_parents.mp w.property have hobs : w.val ∈ (M.fixSet X hObs hFix).observed := by rcases Finset.mem_union.mp ((M.fixSet X hObs hFix).dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo (M.fixSet X hObs hFix).evalMap sx ℓ ⟨w.val, mem_union_left _ hobs⟩))Proof (Lean source)
lemma evalMap_fixSet_observed_apply (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (sx : FixedValues (M.fixSet X hObs hFix)) (ℓ : LatentValues M) (v : {v // v ∈ M.observed}) : (M.fixSet X hObs hFix).evalMap sx ℓ ⟨v.val, mem_union_left _ v.property⟩ = M.structFun v (fixMonoParentMap M.toSWIGGraph X hObs hFix v.val (fun w : {w // w ∈ (M.fixSet X hObs hFix).dag.parents v.val} => if huo : w.val ∈ (M.fixSet X hObs hFix).unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ (M.fixSet X hObs hFix).fixed then sx ⟨w.val, hfix⟩ else have hedge : (M.fixSet X hObs hFix).dag.edge w.val v.val := (M.fixSet X hObs hFix).dag.mem_parents.mp w.property have hobs : w.val ∈ (M.fixSet X hObs hFix).observed := by rcases Finset.mem_union.mp ((M.fixSet X hObs hFix).dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo (M.fixSet X hObs hFix).evalMap sx ℓ ⟨w.val, mem_union_left _ hobs⟩)) := by rw [evalMap_observed_unfold (M.fixSet X hObs hFix) sx ℓ ⟨v.val, v.property⟩] rw [fixSet_structFun_apply] rfl
CutsetLatent 3 core · 7 supporting This file isolates the block of latent roots that drive a target set Y without being mediated by an overridden block C. ★ exists_evalMap_overrideC_factors_cutset
The latent cutset C_W for the continuous-backdoor witness kernel
This file isolates the block of latent roots that drive a target set Y
without being mediated by an overridden block C. A latent node belongs to
the cutset when it reaches some node of Y along a directed path whose interior
nodes all avoid C. The keystone result is a structural factorization: the
override evaluation evalMap_overrideC with override block C depends on the
latent assignment only through its values on the cutset, so two latent vectors
that agree on the cutset produce the same override evaluation on Y.
Main definitions
* DAG.isAncestorAvoiding — there is a directed path from u to v whose
strictly interior nodes all avoid a forbidden set C.
* SCM.cutsetLatent — the latent roots reaching Y along a C-avoiding path
(the block C_W).
Main results
* SCM.evalMap_overrideC_agree_cutset — the structural cutset factorization:
agreement of two latent vectors on the cutset forces the override evaluations
on Y to coincide.
* SCM.exists_evalMap_overrideC_factors_cutset — packages the agreement lemma
as a measurable factorization through the cutset projection.
For a finite vertex set whose members can be compared for equality and a directed acyclic graph on it, a set of forbidden vertices, and two vertices, avoiding ancestry is the relation generated by a directed edge from the first vertex to the second and by extending an avoiding path with an edge from an intermediate vertex outside the forbidden set to its endpoint. Thus, it holds exactly when there is a directed path from the first vertex to the second whose strictly interior vertices avoid the forbidden set.
Definition (Lean source)
For a structural causal model, a target set of graph nodes, and an override block of graph nodes, the latent cutset is the set of unobserved nodes that either are themselves targets or have a directed path to some target whose strictly interior nodes avoid the override block.
Definition (Lean source)
Cutset factorization of an override evaluation. Fix a structural causal model M, a target node set Y and an override node set C with Y contained in the observed nodes and C contained in the observed nodes, a fixed-value assignment s, and an override assignment c on C. Then there is a measurable map from assignments on the latent cutset of Y relative to C to assignments on Y such that, for every latent assignment, the overridden evaluation at Y equals this map applied to the latent assignment's projection onto the cutset.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
toIsAncestortheorem — Every avoiding ancestry relation is also ordinary directed ancestry.hypothesesconclusionG.isAncestor u v -
constheorem — An avoiding path can be extended backward by one edge when the new interior node avoids the forbidden set.hypothesesV :sharedType u_1C :Finset Vu w v :Vhe :G.edge u whw :w ∉ Ch :G.isAncestorAvoiding C w vconclusionG.isAncestorAvoiding C u vProof (Lean source)
-
exists_paththeorem — Avoiding ancestry can be materialized as a concrete directed path with all strictly interior nodes avoiding the forbidden set.hypothesesconclusion∃ q : List V,q.length ≥ 2q.head? = some uq.getLast? = some vconclusion 1i :ℕhi :i + 1 < q.lengthG.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)conclusion 2i :ℕhi :i + 2 < q.lengthq.get ⟨i + 1, by omega⟩ ∉ CProof (Lean source)
theorem isAncestorAvoiding.exists_path {C : Finset V} {u v : V} (h : G.isAncestorAvoiding C u v) : ∃ q : List V, q.length ≥ 2 ∧ q.head? = some u ∧ q.getLast? = some v ∧ (∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)) ∧ (∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ C) := by induction h with | edge he => rename_i u v refine ⟨[u, v], by simp, rfl, rfl, ?_, ?_⟩ · intro i hi have : i = 0 := by simp at hi; omega subst this; exact he · intro i hi; simp at hi | trans hav hwC he ih => rename_i u w v obtain ⟨q, hlen, hhead, hlast, hedge, hint⟩ := ih have hqne : q ≠ [] := by intro hq; rw [hq] at hlen; simp at hlen have hlen_q : (q ++ [v]).length = q.length + 1 := by rw [length_append, List.length_singleton] refine ⟨q ++ [v], ?_, ?_, ?_, ?_, ?_⟩ · rw [hlen_q]; omega · rw [List.head?_append_of_ne_nil _ hqne]; exact hhead · rw [getLast?_append]; simp · -- Directed edges: the new last edge `w → v` joins at the old last node `w`. intro i hi rw [hlen_q] at hi by_cases hlast_i : i + 1 = q.length · -- Seam edge: q[i] = q.getLast = w, and q ++ [v] at i+1 = v. have hi_lt : i < q.length := by omega have hwq : q.get ⟨i, hi_lt⟩ = w := by have hgl := getLast?_eq_some_getLast hqne rw [hlast] at hgl have hw_eq : q.getLast hqne = w := Option.some_inj.mp hgl.symm have hidx : (⟨i, hi_lt⟩ : Fin q.length) = ⟨q.length - 1, by omega⟩ := by simp only [Fin.mk.injEq]; omega rw [hidx, List.get_eq_getElem, ← hw_eq, List.getLast_eq_getElem] have hgi : (q ++ [v]).get ⟨i, by omega⟩ = q.get ⟨i, hi_lt⟩ := by rw [List.get_eq_getElem, List.get_eq_getElem, List.getElem_append_left (h := hi_lt)] have hgi1 : (q ++ [v]).get ⟨i + 1, by omega⟩ = v := by rw [List.get_eq_getElem, List.getElem_append_right (by simp; omega)] simp [hlast_i] rw [hgi, hgi1, hwq]; exact he · -- Edge fully inside `q`. have hi_lt : i + 1 < q.length := by omega have hi_lt0 : i < q.length := by omega have hgi : (q ++ [v]).get ⟨i, by omega⟩ = q.get ⟨i, hi_lt0⟩ := by rw [List.get_eq_getElem, List.get_eq_getElem, List.getElem_append_left (h := hi_lt0)] have hgi1 : (q ++ [v]).get ⟨i + 1, by omega⟩ = q.get ⟨i + 1, hi_lt⟩ := by rw [List.get_eq_getElem, List.get_eq_getElem, List.getElem_append_left (h := hi_lt)] rw [hgi, hgi1]; exact hedge i hi_lt · -- Interior avoidance: interior nodes of `q ++ [v]` are either interior of `q`, -- or the seam node `w` (the old last of `q`), which avoids `C` by `hwC`. intro i hi rw [hlen_q] at hi by_cases hlast_i : i + 1 = q.length - 1 · -- The seam node q[i+1] = q.getLast = w. have hi1_lt : i + 1 < q.length := by omega have hwq : q.get ⟨i + 1, hi1_lt⟩ = w := by have hgl := getLast?_eq_some_getLast hqne rw [hlast] at hgl have hw_eq : q.getLast hqne = w := Option.some_inj.mp hgl.symm have hidx : (⟨i + 1, hi1_lt⟩ : Fin q.length) = ⟨q.length - 1, by omega⟩ := by simp only [Fin.mk.injEq]; omega rw [hidx, List.get_eq_getElem, ← hw_eq, List.getLast_eq_getElem] have hgi1 : (q ++ [v]).get ⟨i + 1, by omega⟩ = q.get ⟨i + 1, hi1_lt⟩ := by rw [List.get_eq_getElem, List.get_eq_getElem, List.getElem_append_left (h := hi1_lt)] rw [hgi1, hwq]; exact hwC · -- Interior node of `q`: i + 2 < q.length. have hi2_lt : i + 2 < q.length := by omega have hi1_lt : i + 1 < q.length := by omega have hgi1 : (q ++ [v]).get ⟨i + 1, by omega⟩ = q.get ⟨i + 1, hi1_lt⟩ := by rw [List.get_eq_getElem, List.get_eq_getElem, List.getElem_append_left (h := hi1_lt)] rw [hgi1]; exact hint i hi2_lt -
mem_cutsetLatenttheorem — Membership in the latent cutset means being unobserved and reaching the target set along an avoiding path.hypothesesconclusionu ∈ M.cutsetLatent Y C ↔ u ∈ M.unobserved ∧∃ y ∈ Y, u = y ∨ M.dag.isAncestorAvoiding C u yProof (Lean source)
theorem mem_cutsetLatent (M : SCM N Ω) {Y C : Finset (SWIGNode N)} {u : SWIGNode N} : u ∈ M.cutsetLatent Y C ↔ u ∈ M.unobserved ∧ ∃ y ∈ Y, u = y ∨ M.dag.isAncestorAvoiding C u y := by letI : DecidablePred (fun u : SWIGNode N => ∃ y ∈ Y, u = y ∨ M.dag.isAncestorAvoiding C u y) := Classical.decPred _ change u ∈ M.unobserved.filter _ ↔ _ exact mem_filter -
cutsetLatent_subsettheorem — The latent cutset is contained in the model's unobserved node set.hypothesesconclusionM.cutsetLatent Y C ⊆ M.unobservedProof (Lean source)
theorem cutsetLatent_subset (M : SCM N Ω) (Y C : Finset (SWIGNode N)) : M.cutsetLatent Y C ⊆ M.unobserved := by intro u hu exact (M.mem_cutsetLatent.mp hu).1 -
evalObservedAuxOverride_agree_cutsetlemma — If two latent assignments agree at every unobserved node that is a target or reaches a target along a directed path whose interior avoids the override block, their recursive override evaluations agree at every observed node that is a target or reaches one along such a path.hypothesesN :sharedType u_2N → Type u_3M :SCM N ΩhC :C ⊆ M.observeds :ℓ₁ ℓ₂ :hAgree :∀ (u : SWIGNode N) (hu : u ∈ M.unobserved)if(∃ t ∈ T, u = t ∨ M.dag.isAncestorAvoiding C u t)thenℓ₁ ⟨u, hu⟩ = ℓ₂ ⟨u, hu⟩n :ℕhn :n < M.observed.card_ :∃ t ∈ T,(M.observedAt ⟨n, hn⟩).val = t ∨ M.dag.isAncestorAvoiding C (M.observedAt ⟨n, hn⟩).val tconclusionevalObservedAuxOverride M hC s c ℓ₁ n hn = evalObservedAuxOverride M hC s c ℓ₂ n hnProof (Lean source)
lemma evalObservedAuxOverride_agree_cutset (M : SCM N Ω) (T : Finset (SWIGNode N)) {C : Finset (SWIGNode N)} (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ₁ ℓ₂ : LatentValues M) (hAgree : ∀ (u : SWIGNode N) (hu : u ∈ M.unobserved), (∃ t ∈ T, u = t ∨ M.dag.isAncestorAvoiding C u t) → ℓ₁ ⟨u, hu⟩ = ℓ₂ ⟨u, hu⟩) : ∀ (n : ℕ) (hn : n < M.observed.card) (_ : ∃ t ∈ T, (M.observedAt ⟨n, hn⟩).val = t ∨ M.dag.isAncestorAvoiding C (M.observedAt ⟨n, hn⟩).val t), evalObservedAuxOverride M hC s c ℓ₁ n hn = evalObservedAuxOverride M hC s c ℓ₂ n hn := by intro n induction n using Nat.strongRecOn with | _ n ih => intro hn hReach rw [evalObservedAuxOverride_eq M hC s c ℓ₁ n hn, evalObservedAuxOverride_eq M hC s c ℓ₂ n hn] by_cases hSelf : (M.observedAt ⟨n, hn⟩).val ∈ C · rw [dif_pos hSelf, dif_pos hSelf] · rw [dif_neg hSelf, dif_neg hSelf] congr 1 funext w have hedge : M.dag.edge w.val (M.observedAt ⟨n, hn⟩).val := M.dag.mem_parents.mp w.property -- Extend the avoiding witness from `observedAt n` through `w`. have hReachW : ∃ t ∈ T, w.val = t ∨ M.dag.isAncestorAvoiding C w.val t := by rcases hReach with ⟨t, ht, hOr⟩ refine ⟨t, ht, ?_⟩ rcases hOr with hEq | hAv · exact inr (hEq ▸ DAG.isAncestorAvoiding.edge hedge) · exact inr (DAG.isAncestorAvoiding.cons M.dag hedge hSelf hAv) by_cases huo : w.val ∈ M.unobserved · rw [parentMapOverride_unobserved M hC s c ℓ₁ hn _ w huo, parentMapOverride_unobserved M hC s c ℓ₂ hn _ w huo] exact hAgree w.val huo hReachW · by_cases hfix : w.val ∈ M.fixed · rw [parentMapOverride_fixed M hC s c ℓ₁ hn _ w hfix, parentMapOverride_fixed M hC s c ℓ₂ hn _ w hfix] · have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1' | h2' · rcases Finset.mem_union.mp h1' with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2' huo by_cases hcW : w.val ∈ C · rw [parentMapOverride_C M hC s c ℓ₁ hn _ w hcW, parentMapOverride_C M hC s c ℓ₂ hn _ w hcW] · rw [parentMapOverride_observed M hC s c ℓ₁ hn _ w hobs hcW, parentMapOverride_observed M hC s c ℓ₂ hn _ w hobs hcW] have hj : (M.observedIndex ⟨w.val, hobs⟩).val < n := M.observed_parent_index_lt hn hedge hobs congr 1 apply ih _ hj rcases hReachW with ⟨t, ht, hwt⟩ refine ⟨t, ht, ?_⟩ have h_at : (M.observedAt ⟨(M.observedIndex ⟨w.val, hobs⟩).val, (M.observedIndex ⟨w.val, hobs⟩).isLt⟩).val = w.val := M.observedAt_observedIndex ⟨w.val, hobs⟩ rw [h_at] exact hwt -
evalMap_overrideC_agree_cutsettheorem — The overridden evaluation on the target set depends on latent values only through the latent cutset.hypothesesN :sharedType u_2N → Type u_3M :SCM N ΩhY :Y ⊆ M.observedhC :C ⊆ M.observeds :ℓ₁ ℓ₂ :hAgree :valuesProjection (M.cutsetLatent_subset Y C) ℓ₁= valuesProjection (M.cutsetLatent_subset Y C) ℓ₂conclusionM.evalMap_overrideC hY hC s c ℓ₁ = M.evalMap_overrideC hY hC s c ℓ₂Proof (Lean source)
theorem evalMap_overrideC_agree_cutset (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) (ℓ₁ ℓ₂ : LatentValues M) (hAgree : valuesProjection (M.cutsetLatent_subset Y C) ℓ₁ = valuesProjection (M.cutsetLatent_subset Y C) ℓ₂) : M.evalMap_overrideC hY hC s c ℓ₁ = M.evalMap_overrideC hY hC s c ℓ₂ := by -- Turn the cutset-projection agreement into pointwise latent agreement on the -- avoiding-reachable latents. have hAgree' : ∀ (u : SWIGNode N) (hu : u ∈ M.unobserved), (∃ y ∈ Y, u = y ∨ M.dag.isAncestorAvoiding C u y) → ℓ₁ ⟨u, hu⟩ = ℓ₂ ⟨u, hu⟩ := by intro u hu hReach have huMem : u ∈ M.cutsetLatent Y C := M.mem_cutsetLatent.mpr ⟨hu, hReach⟩ have := congrFun hAgree ⟨u, huMem⟩ simpa [valuesProjection] using this funext v rw [evalMap_overrideC_eq M hY hC s c ℓ₁ v, evalMap_overrideC_eq M hY hC s c ℓ₂ v] congr 1 apply evalObservedAuxOverride_agree_cutset M Y hC s c ℓ₁ ℓ₂ hAgree' refine ⟨v.val, v.property, inl ?_⟩ exact M.observedAt_observedIndex ⟨v.val, hY v.property⟩
EquivKernel 2 core · 4 supporting This file proves that structurally equivalent causal models have matching evaluation maps, latent product measures, joint kernels, and observational kernels. ★ evalMap_eq_of_equiv★ heq_obsKernel
Kernel Transport Across Equivalent Models
This file proves that structurally equivalent causal models have matching evaluation maps, latent product measures, joint kernels, and observational kernels. These transport results allow later do-calculus arguments to compare models whose topological orderings or proof witnesses differ but whose causal content is the same.
Main results
* SCM.evalMap_eq_of_equiv proves pointwise equality of evaluation maps under
SCM.Equiv, assuming matching fixed and latent inputs.
* SCM.Equiv.heq_latentProduct, SCM.Equiv.heq_jointKernel, and
SCM.Equiv.heq_obsKernel transport the induced measures and kernels across
equivalent structural causal models.
* SCM.Equiv.heq_obsCondKernel transports observational conditional kernels
when the conditioning and target coordinate sets are shared.
Cross-SCM pointwise equality of evalMap under SCM.Equiv. For two structural causal models M₁, M₂ that are structurally equivalent — the same graph up to topological reordering, matching edge types and have heterogeneously equal structural functions, fixed-value assignments s₁, s₂ and latent assignments ℓ₁, ℓ₂ on the two models, and a shared node w that is a random-variable node of M₁ and a random-variable node of M₂: if s₁ and s₂ agree coordinatewise on every fixed node shared by both models and ℓ₁ and ℓ₂ agree coordinatewise on every unobserved node shared by both models, then the two models' evaluation maps agree at w: M₁'s evaluation with (s₁, ℓ₁) equals M₂'s evaluation with (s₂, ℓ₂).
Formal statement
Proof (Lean source)
HEq transport for obsKernel. For two structural causal models M₁, M₂ that are structurally equivalent, have heterogeneously equal structural functions, and have heterogeneously equal latent-root distributions, then their observational kernels are heterogeneously equal.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
structFun_apply_eq_of_equivtheorem — Equivalent structural graphs with matching structural functions produce the same output at an observed node whenever corresponding parent values agree.hypotheseshGraph :SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraphhSF :HEq M₁.structFun M₂.structFunv :SWIGNode Nhv_obs₁ :v ∈ M₁.observedhv_obs₂ :v ∈ M₂.observedξ₁ :(w : {w // w ∈ M₁.dag.parents v}) → swigΩ Ω w.valξ₂ :(w : {w // w ∈ M₂.dag.parents v}) → swigΩ Ω w.valhξ :∀ (p : SWIGNode N) (hp₁ : p ∈ M₁.dag.parents v) (hp₂ : p ∈ M₂.dag.parents v),ξ₁ ⟨p, hp₁⟩ = ξ₂ ⟨p, hp₂⟩conclusionM₁.structFun ⟨v, hv_obs₁⟩ ξ₁ = M₂.structFun ⟨v, hv_obs₂⟩ ξ₂Proof (Lean source)
theorem structFun_apply_eq_of_equiv {M₁ M₂ : SCM N Ω} (hGraph : SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraph) (hSF : HEq M₁.structFun M₂.structFun) (v : SWIGNode N) (hv_obs₁ : v ∈ M₁.observed) (hv_obs₂ : v ∈ M₂.observed) {ξ₁ : (w : {w // w ∈ M₁.dag.parents v}) → swigΩ Ω w.val} {ξ₂ : (w : {w // w ∈ M₂.dag.parents v}) → swigΩ Ω w.val} (hξ : ∀ (p : SWIGNode N) (hp₁ : p ∈ M₁.dag.parents v) (hp₂ : p ∈ M₂.dag.parents v), ξ₁ ⟨p, hp₁⟩ = ξ₂ ⟨p, hp₂⟩) : M₁.structFun ⟨v, hv_obs₁⟩ ξ₁ = M₂.structFun ⟨v, hv_obs₂⟩ ξ₂ := by have hObsEq : M₁.observed = M₂.observed := hGraph.2.2.1 have pEq : M₁.dag.parents v = M₂.dag.parents v := SWIGGraph.Equivalent.parents_eq hGraph.1 v -- Target: both sides live in `swigΩ Ω v`. Lift to HEq, then back to Eq. apply eq_of_heq -- Step 1: HEq of the `structFun` applications at `⟨v, ·⟩`. -- M₁.structFun ⟨v, hv_obs₁⟩ : (inputs₁) → swigΩ Ω v -- M₂.structFun ⟨v, hv_obs₂⟩ : (inputs₂) → swigΩ Ω v -- where inputs_i = (w : {w // w ∈ M_i.dag.parents v}) → swigΩ Ω w.val. -- `hSF` gives HEq of the full structFuns; apply it at v-level. have hvHeq : (⟨v, hv_obs₁⟩ : {v // v ∈ M₁.observed}) ≍ (⟨v, hv_obs₂⟩ : {v // v ∈ M₂.observed}) := by apply (Subtype.heq_iff_coe_eq (by intro x; rw [hObsEq])).mpr rfl have hApp1 : HEq (M₁.structFun ⟨v, hv_obs₁⟩) (M₂.structFun ⟨v, hv_obs₂⟩) := by apply dcongr_heq hvHeq · -- β₁ t₁ = β₂ t₂ when t₁ ≍ t₂ (same .val). intro t₁ t₂ ht have hval : t₁.val = t₂.val := by have := (Subtype.heq_iff_coe_eq (by intro x; rw [hObsEq])).mp ht exact this -- Output β is `((w : ...parents t.val) → ...) → swigΩ Ω t.val`, depends on t.val. rw [hval] -- Remaining type difference is in parents via `M₁.dag.parents` vs `M₂.dag.parents`. rw [SWIGGraph.Equivalent.parents_eq hGraph.1 t₂.val] · intro _ _; exact hSF -- Step 2: HEq of the parent tuples. have hξHeq : HEq ξ₁ ξ₂ := by apply Function.hfunext (by rw [pEq]) rintro ⟨p₁val, p₁prop⟩ ⟨p₂val, p₂prop⟩ hp have hval : p₁val = p₂val := by have := (Subtype.heq_iff_coe_eq (by intro x; rw [pEq])).mp hp exact this subst hval apply heq_of_eq exact hξ p₁val p₁prop p₂prop -- Step 3: combine hApp1 and hξHeq via `congr_heq` (common codomain `swigΩ Ω v`). exact heq_of_eq (congr_heq hApp1 hξHeq) -
heq_latentProducttheorem — HEq transport for latentProduct.hypotheseshUnobs :M₁.unobserved = M₂.unobservedhLD :HEq M₁.latentDist M₂.latentDistconclusionHEq M₁.latentProduct M₂.latentProductProof (Lean source)
theorem Equiv.heq_latentProduct {M₁ M₂ : SCM N Ω} (hUnobs : M₁.unobserved = M₂.unobserved) (hLD : HEq M₁.latentDist M₂.latentDist) : HEq M₁.latentProduct M₂.latentProduct := by obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ subst hUnobs -- After subst, lD₁, lD₂ : (u : {u // u ∈ unobserved₁}) → Measure (swigΩ Ω u.val) -- have the same type. have hLD_eq : lD₁ = lD₂ := eq_of_heq hLD subst hLD_eq -- Both sides are `Measure.pi (fun u => lD₁ u)`, the `pL₁`/`pL₂` measurability -- witnesses are `Subsingleton`. rfl -
heq_jointKerneltheorem — HEq transport for jointKernel.hypotheseshGraph :SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraphhSF :HEq M₁.structFun M₂.structFunhLD :HEq M₁.latentDist M₂.latentDistconclusionHEq M₁.jointKernel M₂.jointKernelProof (Lean source)
theorem Equiv.heq_jointKernel {M₁ M₂ : SCM N Ω} (hGraph : SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraph) (hSF : HEq M₁.structFun M₂.structFun) (hLD : HEq M₁.latentDist M₂.latentDist) : HEq M₁.jointKernel M₂.jointKernel := by -- Extract the latent-product HEq first, while `h` still has its -- original (non-destructured) type. Chaining into `eq_of_heq` later -- would force the two `latentProduct` types to unify, prematurely -- identifying the M₁, M₂ metas of `heq_latentProduct`. have h_lp : HEq M₁.latentProduct M₂.latentProduct := Equiv.heq_latentProduct hGraph.2.2.2 hLD have h_evalMap_eq := evalMap_eq_of_equiv hGraph hSF obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ rcases hGraph with ⟨_hEdge, rfl, rfl, rfl⟩ have hLD_eq : lD₁ = lD₂ := eq_of_heq hLD subst hLD_eq -- After subst: FixedValues, RandomValues, latentProduct all have matching types. apply heq_of_eq have hlp := eq_of_heq h_lp -- Work at the compProd definition to avoid rw-matching issues on `jointKernel`. unfold SCM.jointKernel -- Goal: (const _ lp₁ ⊗ₖ det₁).map snd = (const _ lp₂ ⊗ₖ det₂).map snd congr 1 -- Goal: const _ lp₁ ⊗ₖ det₁ = const _ lp₂ ⊗ₖ det₂ rw [hlp] -- Goal: const _ lp₂ ⊗ₖ det₁ = const _ lp₂ ⊗ₖ det₂ congr 1 -- Goal: det₁ = det₂ (Kernel.deterministic (uncurry evalMap_i) _) apply ProbabilityTheory.Kernel.ext rintro ⟨s, ℓ⟩ simp only [ProbabilityTheory.Kernel.deterministic_apply] congr 1 apply funext rintro ⟨w, hw⟩ exact h_evalMap_eq s ℓ s ℓ (fun _ _ => rfl) (fun _ _ => rfl) hw hw -
heq_obsCondKerneltheorem — HEq transport for obsCondKernel.hypotheseshGraph :SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraphhSF :HEq M₁.structFun M₂.structFunhLD :HEq M₁.latentDist M₂.latentDisthY₁ :Y ⊆ M₁.observedhCC₁ :CC ⊆ M₁.observedconclusionhY₂ :by intro v hv rw [← hGraph.2.2.1] exact hY₁ hv (: Y ⊆ M₂.observed)hCC₂ :by intro v hv rw [← hGraph.2.2.1] exact hCC₁ hv (: CC ⊆ M₂.observed)HEq (M₁.obsCondKernel Y CC hY₁ hCC₁) (M₂.obsCondKernel Y CC hY₂ hCC₂)Proof (Lean source)
theorem Equiv.heq_obsCondKernel {M₁ M₂ : SCM N Ω} (hGraph : SWIGGraph.Equivalent M₁.toSWIGGraph M₂.toSWIGGraph) (hSF : HEq M₁.structFun M₂.structFun) (hLD : HEq M₁.latentDist M₂.latentDist) (Y CC : Finset (SWIGNode N)) (hY₁ : Y ⊆ M₁.observed) (hCC₁ : CC ⊆ M₁.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated (FixedValues M₁) (ValuesOn CC (swigΩ Ω))] [CountableOrCountablyGenerated (FixedValues M₂) (ValuesOn CC (swigΩ Ω))] : let hY₂ : Y ⊆ M₂.observed := by intro v hv rw [← hGraph.2.2.1] exact hY₁ hv let hCC₂ : CC ⊆ M₂.observed := by intro v hv rw [← hGraph.2.2.1] exact hCC₁ hv HEq (M₁.obsCondKernel Y CC hY₁ hCC₁) (M₂.obsCondKernel Y CC hY₂ hCC₂) := by dsimp apply heq_obsCondKernel_aux hGraph hSF hLD Y CC hY₁
EvalFactorization 4 core · 4 supporting This file proves that values produced by the evaluation map factor through the appropriate parent or ancestor coordinates. ★ evalMap_factors_through_parents★ evalMap_factors_through_ancestors
Evaluation Map Factorization
This file proves that values produced by the evaluation map factor through the appropriate parent or ancestor coordinates. These factorization results provide the measurable-function inputs needed for local and global Markov arguments in structural causal models.
Main definitions and results
* SCM.evalMap_factors_through_parents expresses an observed node value as a
measurable function of the evaluated random parent coordinates.
* SCM.latentAncestorsOfNode and SCM.fixedAncestorsOfNode collect the latent
and fixed ancestor coordinates relevant to a single observed node.
* SCM.evalMap_factors_through_ancestors upgrades ancestral agreement into a
measurable factorization through the fixed-ancestor and latent-ancestor
projections.
Parent factorization of evalMap at observed nodes. Fix a structural causal model M, a fixed-value assignment s, and a node v with v an observed node. Then there is a measurable function g of the assignment restricted to v's random parent coordinates such that, for every latent assignment ℓ, the evaluated value at v equals g applied to that restriction of the joint evaluation.
Formal statement
Proof (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, and a node, the set of latent ancestors of that node consists exactly of the model's unobserved nodes that are either the node itself or ancestors of it in the directed graph. It is formed by filtering the unobserved nodes by this condition.
Definition (Lean source)
For a finite node population with measurable node-value spaces, a structural causal model, and a node, the set of fixed ancestors of that node consists exactly of the model's fixed nodes that are either the node itself or ancestors of it in the directed graph. It is formed by filtering the fixed nodes by this condition.
Definition (Lean source)
Ancestor factorization (existence form). Fix a structural causal model M and a node v with v an observed node. Then there is a measurable function g of the fixed-ancestor projection and the latent-ancestor projection of v such that, for every fixed-value assignment s and latent assignment ℓ, the evaluated value at v equals g applied to those two projections of s and ℓ.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
mem_latentAncestorsOfNodelemma — Membership in the latent-ancestor set means being unobserved and equal to or ancestral to the node.hypothesesconclusionu ∈ M.latentAncestorsOfNode v ↔ u ∈ M.unobserved ∧ (u = v ∨ M.dag.isAncestor u v)Proof (Lean source)
lemma mem_latentAncestorsOfNode (M : SCM N Ω) {v u : SWIGNode N} : u ∈ M.latentAncestorsOfNode v ↔ u ∈ M.unobserved ∧ (u = v ∨ M.dag.isAncestor u v) := by letI : DecidablePred (fun u : SWIGNode N => u = v ∨ M.dag.isAncestor u v) := Classical.decPred _ change u ∈ M.unobserved.filter (fun u => u = v ∨ M.dag.isAncestor u v) ↔ _ exact mem_filter -
mem_fixedAncestorsOfNodelemma — Membership in the fixed-ancestor set means being fixed and equal to or ancestral to the node.hypothesesconclusiond ∈ M.fixedAncestorsOfNode v ↔ d ∈ M.fixed ∧ (d = v ∨ M.dag.isAncestor d v)Proof (Lean source)
lemma mem_fixedAncestorsOfNode (M : SCM N Ω) {v d : SWIGNode N} : d ∈ M.fixedAncestorsOfNode v ↔ d ∈ M.fixed ∧ (d = v ∨ M.dag.isAncestor d v) := by letI : DecidablePred (fun d : SWIGNode N => d = v ∨ M.dag.isAncestor d v) := Classical.decPred _ change d ∈ M.fixed.filter (fun d => d = v ∨ M.dag.isAncestor d v) ↔ _ exact mem_filter -
fixedAncestorsOfNode_subsetlemma — The fixed-ancestor set is contained in the fixed node set.hypothesesconclusionM.fixedAncestorsOfNode v ⊆ M.fixedProof (Lean source)
lemma fixedAncestorsOfNode_subset (M : SCM N Ω) (v : SWIGNode N) : M.fixedAncestorsOfNode v ⊆ M.fixed := by intro d hd exact ((M.mem_fixedAncestorsOfNode).mp hd).1 -
latentAncestorsOfNode_subsetlemma — The latent-ancestor set is contained in the unobserved node set.hypothesesconclusionM.latentAncestorsOfNode v ⊆ M.unobservedProof (Lean source)
lemma latentAncestorsOfNode_subset (M : SCM N Ω) (v : SWIGNode N) : M.latentAncestorsOfNode v ⊆ M.unobserved := by intro u hu exact ((M.mem_latentAncestorsOfNode).mp hu).1
EvalLatent 1 core · 0 supporting This file proves that, for a latent root and a set of non-descendant random coordinates, the corresponding evaluation projection does not depend on the chosen latent coordinate. ★ evalMap_factors_excluding_latent
Latent-Restricted Evaluation Factorization
This file proves that, for a latent root and a set of non-descendant random coordinates, the corresponding evaluation projection does not depend on the chosen latent coordinate. The result is used to establish independence claims for the global Markov property of structural causal models.
The main theorem, SCM.evalMap_factors_excluding_latent, states that if
T ⊆ M.randomVars contains no descendants of a latent root a, then the
projection of M.evalMap s to T factors through all latent coordinates except
the coordinate at a.
Latent-restricted factorization away from a chosen latent root. Fix a structural causal model M, a fixed-value assignment s, and a latent root node a. For a set T of random-variable nodes such that no node of T is a descendant of a, and none equals a, then the projection of the evaluation evalMap s to T factors through a measurable function of the latent coordinates other than a's — i.e. it does not depend on the latent value at a.
Formal statement
Proof (Lean source)
Induced 4 core · 4 supporting This file defines ancestral closure for structural causal models and states an induced submodel construction on an ancestrally closed set of nodes. ★ induce_evalMap_compat★ induce_marginal_compat
Induced Structural Causal Models
This file defines ancestral closure for structural causal models and states an induced submodel construction on an ancestrally closed set of nodes. The construction supports marginal-compatibility results that relate a submodel to the original structural causal model.
Main definitions and results
* SCM.isAncestrallyClosedSCM is the observed-parent and fixed-counterpart
closure condition needed to inherit structural functions.
* SCM.induce builds the induced sub-SCM on an ancestrally closed node set.
* SCM.measure_pi_map_valuesProjection and SCM.induce_latentProduct_eq_map
identify the latent product of the induced model as a projected product
measure.
* SCM.induce_evalMap_compat compares evaluation in the induced model with
evaluation in the original model.
* SCM.induce_marginal_compat proves the observational-kernel marginal
compatibility theorem for induced submodels.
For a finite node population with measurable node-value spaces, a structural causal model, and a set of graph nodes, the SCM ancestral-closure condition holds exactly when every observed parent of every retained node is retained and the random counterpart of every fixed parent of every retained node is retained.
For a finite node population with measurable node-value spaces, a structural causal model, a set of graph nodes, and the condition that this set is ancestrally closed in the SCM sense, the induced structural causal submodel retains the selected observed and fixed nodes and precisely the original latent roots feeding retained observed nodes. It is defined from the induced SWIG graph, inheriting the relevant value spaces, structural functions, and latent distributions.
Definition (Lean source)
Evaluation-map bridge for the induced sub-SCM. Fix a structural causal model M and a node set R that is ancestrally closed in the SCM sense. Then at every random node v retained by the induced model M.induce R hR, the induced evaluation map at the restriction of sTilde to R and the projected latent assignment computes the same value as the original evaluation map at sTilde.
Formal statement
Proof (Lean source)
Marginal compatibility of the induced sub-SCM (prop:scm-induced-marginal). Fix a structural causal model M, an ancestrally closed node set R, and a fixed-value assignment sTilde on M. Then the observational kernel of the induced sub-SCM at the restriction of sTilde to R equals the pushforward of M's observational kernel at sTilde onto the induced observed coordinates R ∩ M.observed.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
induce_parents_eq_of_ancClosedlemma — An ancestrally closed retained observed set keeps every parent needed to evaluate each retained observed node, so its induced graph has exactly the same parent set at those nodes.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhR :M.isAncestrallyClosedSCM Rv :SWIGNode Nhv :v ∈ (M.toSWIGGraph.induce R).observedconclusion(M.toSWIGGraph.induce R).dag.parents v = M.dag.parents vProof (Lean source)
lemma induce_parents_eq_of_ancClosed (M : SCM N Ω) (R : Finset (SWIGNode N)) (hR : M.isAncestrallyClosedSCM R) {v : SWIGNode N} (hv : v ∈ (M.toSWIGGraph.induce R).observed) : (M.toSWIGGraph.induce R).dag.parents v = M.dag.parents v := by classical have hvInter : v ∈ R ∩ M.observed := hv have hvR : v ∈ R := (Finset.mem_inter.mp hvInter).1 have hvMObs : v ∈ M.observed := (Finset.mem_inter.mp hvInter).2 -- `v` lives in the induced active set via the `newObserved` summand. have hvActive : v ∈ (M.toSWIGGraph.fixed.filter (fun s => iotaMap s ∈ R ∩ M.observed)) ∪ (R ∩ M.observed) ∪ (M.toSWIGGraph.unobserved.filter (fun u => ∃ w ∈ R ∩ M.observed, M.toSWIGGraph.dag.edge u w)) := by refine mem_union_left _ ?_ exact Finset.mem_union_right _ hvInter apply Finset.Subset.antisymm · exact M.toSWIGGraph.inducedDag_parents_subset _ v · intro u huM have huEdge : M.dag.edge u v := M.dag.mem_parents.mp huM have huClass : u ∈ M.fixed ∪ M.observed ∪ M.unobserved := (M.dag_edges_classified u v huEdge).1 have huActive : u ∈ (M.toSWIGGraph.fixed.filter (fun s => iotaMap s ∈ R ∩ M.observed)) ∪ (R ∩ M.observed) ∪ (M.toSWIGGraph.unobserved.filter (fun u => ∃ w ∈ R ∩ M.observed, M.toSWIGGraph.dag.edge u w)) := by rcases Finset.mem_union.mp huClass with hu | hu · rcases Finset.mem_union.mp hu with huFix | huObs · -- `u ∈ M.fixed`: use pairing closure (clause b). have hIotaR : iotaMap u ∈ R := hR.2 v hvR u huM huFix have hIotaObs : iotaMap u ∈ M.observed := M.fixed_image_in_observed u huFix have hIotaNewObs : iotaMap u ∈ R ∩ M.observed := Finset.mem_inter.mpr ⟨hIotaR, hIotaObs⟩ have huNewFixed : u ∈ M.toSWIGGraph.fixed.filter (fun s => iotaMap s ∈ R ∩ M.observed) := Finset.mem_filter.mpr ⟨huFix, hIotaNewObs⟩ exact mem_union_left _ (mem_union_left _ huNewFixed) · -- `u ∈ M.observed`: use observed-ancestor closure (clause a). have huR : u ∈ R := hR.1 v hvR u huM huObs have huNewObs : u ∈ R ∩ M.observed := Finset.mem_inter.mpr ⟨huR, huObs⟩ exact mem_union_left _ (Finset.mem_union_right _ huNewObs) · -- `u ∈ M.unobserved`: a latent parent of retained `v` survives the latent filter. exact Finset.mem_union_right _ (Finset.mem_filter.mpr ⟨hu, v, hvInter, huEdge⟩) refine (M.toSWIGGraph.induce R).dag.mem_parents.mpr ?_ exact ⟨huEdge, huActive, hvActive⟩ -
induce_unobserved_subsetlemma — The latent roots of an induced sub-SCM are original latent roots.hypothesesconclusion(M.induce R hR).unobserved ⊆ M.unobservedProof (Lean source)
lemma induce_unobserved_subset (M : SCM N Ω) (R : Finset (SWIGNode N)) (hR : M.isAncestrallyClosedSCM R) : (M.induce R hR).unobserved ⊆ M.unobserved := by intro u hu simpa [SCM.induce, SWIGGraph.induce] using (Finset.mem_filter.mp hu).1 -
measure_pi_map_valuesProjectionlemma — Product measures marginalize under coordinate restriction.hypotheseshJI :J ⊆ Iμ :∀ i, IsProbabilityMeasure (μ i)conclusion= pi (fun j : {j // j ∈ J} => μ ⟨j.val, hJI j.property⟩)Proof (Lean source)
lemma measure_pi_map_valuesProjection {I J : Finset (SWIGNode N)} (hJI : J ⊆ I) (μ : (i : {i // i ∈ I}) → Measure (swigΩ Ω i.val)) [∀ i, IsProbabilityMeasure (μ i)] : (pi μ).map (valuesProjection (Ω := swigΩ Ω) hJI) = pi (fun j : {j // j ∈ J} => μ ⟨j.val, hJI j.property⟩) := by classical symm refine MeasureTheory.Measure.pi_eq (fun s hs => ?_) rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection hJI) (.univ_pi hs)] let t : (i : {i // i ∈ I}) → Set (swigΩ Ω i.val) := fun i => if h : i.val ∈ J then s ⟨i.val, h⟩ else Set.univ have hpre : valuesProjection (Ω := swigΩ Ω) hJI ⁻¹' pi Set.univ s = pi Set.univ t := by ext x constructor · intro hx a _haI by_cases haJ : a.val ∈ J · have hxj := hx ⟨a.val, haJ⟩ (Set.mem_univ _) simpa [t, valuesProjection, haJ] using hxj · simp [t, haJ] · intro hx a _haJ have hxi := hx ⟨a.val, hJI a.property⟩ (Set.mem_univ _) simpa [t, valuesProjection, a.property] using hxi rw [hpre] rw [MeasureTheory.Measure.pi_pi] let g : SWIGNode N → ℝ≥0∞ := fun a => if h : a ∈ J then μ ⟨a, hJI h⟩ (s ⟨a, h⟩) else 1 have hleft : (∏ i, μ i (t i)) = ∏ a ∈ I, g a := by calc (∏ i : {i // i ∈ I}, μ i (t i)) = ∏ i : {i // i ∈ I}, g i.val := by refine Fintype.prod_congr _ _ ?_ intro i by_cases hiJ : i.val ∈ J · simp [g, t, hiJ] · simp [g, t, hiJ] _ = ∏ a ∈ I, g a := Finset.prod_coe_sort (s := I) (f := g) have hright : (∏ j : {j // j ∈ J}, μ ⟨j.val, hJI j.property⟩ (s j)) = ∏ a ∈ J, g a := by calc (∏ j : {j // j ∈ J}, μ ⟨j.val, hJI j.property⟩ (s j)) = ∏ j : {j // j ∈ J}, g j.val := by refine Fintype.prod_congr _ _ ?_ intro j simp [g, j.property] _ = ∏ a ∈ J, g a := Finset.prod_coe_sort (s := J) (f := g) rw [hleft, hright] exact (Finset.prod_subset_one_on_sdiff hJI (fun a ha => by have haJ : a ∉ J := (Finset.mem_sdiff.mp ha).2 simp [g, haJ]) (fun a ha => by simp [g, ha])).symm -
induce_latentProduct_eq_maplemma — The latent product of an induced sub-SCM is the marginal of the original latent product.hypothesesconclusion(M.induce R hR).latentProduct= M.latentProduct.map (valuesProjection (induce_unobserved_subset M R hR))Proof (Lean source)
lemma induce_latentProduct_eq_map (M : SCM N Ω) (R : Finset (SWIGNode N)) (hR : M.isAncestrallyClosedSCM R) : (M.induce R hR).latentProduct = M.latentProduct.map (valuesProjection (induce_unobserved_subset M R hR)) := by classical haveI hprob : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent rw [SCM.latentProduct, SCM.latentProduct] rw [measure_pi_map_valuesProjection (hJI := induce_unobserved_subset M R hR) (μ := fun u : {u // u ∈ M.unobserved} => M.latentDist u)] simp only [SCM.induce] rfl
InterventionAncestry 1 core · 1 supporting This file relates ancestry in the graph after a set intervention to ancestry in the original structural causal model. ★ fixSet_isAncestor_fixed_forward
Intervention Ancestry
This file relates ancestry in the graph after a set intervention to ancestry in the original structural causal model. It supplies the graph bridge used to turn a non-descendant condition in a back-door criterion into the non-ancestry hypothesis needed for Rule 3 of do-calculus.
The main theorem, SCM.fixSet_isAncestor_fixed_forward, lifts a directed ancestry
path starting at an intervened fixed copy in (M.fixSet X).dag to an ancestry
path starting at the corresponding random node in the base graph. The auxiliary
DAG.not_isAncestor_of_root' records that a root has no proper ancestors.
Forward direction: .fixed D-ancestry in fixSet X lifts to .random D-ancestry in the base graph. Fix a structural causal model M and an intervention target set X such that every targeted node is currently a random observed node and none of its fixed copies is already fixed. For a targeted node D and a node v, if the fixed copy of D is a proper ancestor of v in the post-intervention graph obtained by fixing X, then the random copy of D is a proper ancestor of v in the original base graph.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
fixSet_edge_ifflemma — An edge in a causal model after intervention is exactly the corresponding edge produced by splitting the intervened variables in the original graph.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhX_obs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhX_fixed :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedu v :SWIGNode Nconclusion(M.fixSet X hX_obs hX_fixed).dag.edge u v↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge X u vProof (Lean source)
lemma fixSet_edge_iff (M : SCM N Ω) (X : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (u v : SWIGNode N) : (M.fixSet X hX_obs hX_fixed).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge X u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG]